From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.0 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 5686 invoked from network); 5 Mar 2021 04:41:33 -0000 Received: from mail-ej1-x63e.google.com (2a00:1450:4864:20::63e) by inbox.vuxu.org with ESMTPUTF8; 5 Mar 2021 04:41:33 -0000 Received: by mail-ej1-x63e.google.com with SMTP id rl7sf335473ejb.16 for ; Thu, 04 Mar 2021 20:41:33 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1614919286; cv=pass; d=google.com; s=arc-20160816; b=DuMF69rPzCxAOwalwoTV3FgmDhsfr1vLxEPEttL38qPqFBfOxC4NYQu00Z+7X3sTFf DDXMUuie0j8w9v+wpvsezV/f1mVpk1SjvUE5etT84K1bzNuUXUswLv5vP9IfmBVmE3oc VMdHZhWd+YdIQyXIUD2GuTrC91IG8h/Bi1/gLYJrCyQOdbghrVeMpBzQVfjQX7uG7OOH pihyO7DOoEP4HKTDNMOujNmfMgAjzFdXmR0jqOSaOc1fsQIb+igQjJYnoQsIxMjzxEsR xX/TE1JqPNXhtA+PvqWmNd97ARy37UXN4GUe+YnbhMzq34WxIvGwpl6Mt85JT+X7cp6I CwBA== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:content-transfer-encoding:cc:to:subject :message-id:date:from:in-reply-to:references:mime-version:sender :dkim-signature; bh=4ZJBzHgN2RZR9s8fsinORzu4+AU1HVgQmhzU1ZMQc7k=; b=EFRj8y6xxTAxdFbA0OAWhntNGYmlJIoo4sUMhLfPPzhHsF/0mpL6gLBtkGUGej5qh7 mqW/4LRcVLbi3gt5HWFdQ+phV3KBbSrAS033Wd9wzixyzM5BbZrNY/MvTn6y/I8W6FZe OXj3dV+MnPIluPSouBDYjKlf6Es8t+xRoiIiZCFnwm+dbanCH+8HORUtE6s43RxGqS8U VvkwLDRI4B3yN/0HIV5eJP1MqlJVwo7Hb+H1V3NsHO92izHhDbZwfaK8G69NFB0AUS3r Dq0LEZTUOoenzMI2aLRSIZhoc7N+sYpjcFdswzO1P/pylm+gEpXriG2UKvqF1PYmrW7A CZhQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego.edu header.s=google header.b=CPVRakNO; spf=pass (google.com: domain of shulman@sandiego.edu designates 2a00:1450:4864:20::52e as permitted sender) smtp.mailfrom=shulman@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:references:in-reply-to:from:date:message-id :subject:to:cc:content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=4ZJBzHgN2RZR9s8fsinORzu4+AU1HVgQmhzU1ZMQc7k=; b=i0zdGAde6gVB72p3wf12vSzNUwDLxXpj+Ku9KsR71WIPQ/9IdGqMUy5b1B+OrAwt5u 2Oj7+XSC4+iOzyj1R+wheaUwqvamwG9pT7kF16cQD19omiTqev4C3wppXA7EtUqhAna5 TPzMNQQWoZerFjF2bBwBh/ni+HM+k8p1+czPLoW2DiivPFTJsq+NrKrrXDFzOdXSEZqW ADQ20ckuIomEkJIAaPFM4c9OcnRkmwotXjxPClMUDHSDG2g7lpE4tRI5t4i/qN43hjKh W9dA5xZIK/WFS6hpBAIzRJSJPj/IMc6JIjZ2hwsnLR3fu4R3ZXgsKpeamwA8S4+yM8Lm MWaw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:references:in-reply-to:from :date:message-id:subject:to:cc:content-transfer-encoding :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-unsubscribe; bh=4ZJBzHgN2RZR9s8fsinORzu4+AU1HVgQmhzU1ZMQc7k=; b=JBR1Uua4+LxfIQQVQqjK2bwdGRJO7Zoyb6dk8qzkmAnfNrHuMsy/eYL8SzT4Ntn7U8 Nem4hptlehjXwv3aTfXZN96tVKStY2gpkP1etNqTJROBvlIPoIngJr3fK8lPJHBLu4b9 MKpzmgmTUI10f5hZaOUh87l/S/FHvPBsn7EzYPAa1XWKj/LoRfS6Jux5CpkQuXsbKSMi dO49h/FctZYq8TL9LBZ/vHhWRveEduL+3YD2Rs6U/4M9oqw41SNsEplNhSJU8LYvQh6G /Tt/VwIsa51EjVra0lpHYSMS5pf4PbmAXfEAaUCwF1ALDTFJUlqenfxhxiEHAwKVIN5+ pWVw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM533KGRsZ7v1wMPm4/FfLryQK6JO965+rbtqP7bhmNKr9lhBgiS2p bZ0cY9iroY8c8leiEw3U72U= X-Google-Smtp-Source: ABdhPJx9DJloQlIAGTNnRGpXCBKFB3qyBRfel7sQydUSEEL3/d5uuakGarGg8l4EYK7TQrgrh33lQw== X-Received: by 2002:a17:907:78d9:: with SMTP id kv25mr709460ejc.415.1614919286246; Thu, 04 Mar 2021 20:41:26 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:907:2d0f:: with SMTP id gs15ls3895382ejc.8.gmail; Thu, 04 Mar 2021 20:41:25 -0800 (PST) X-Received: by 2002:a17:906:6c93:: with SMTP id s19mr682162ejr.151.1614919285175; Thu, 04 Mar 2021 20:41:25 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1614919285; cv=none; d=google.com; s=arc-20160816; b=CSzi4NFLCD9962QBKcKdyW8yNJWoTVte8HtZZnRH2vFZ7ST25Wk/K3UnCVcyLZTTYG 4Nzgh67O6SfxmoXRD1kEexdcqjZKY7JY82PULezOMx2xysHV65QtGxGG9J/rue2AuirR MgY/ZFTo9uR8BV7R1uNQG7sBkM50ayEV7/k7RvaZSZcaqsD9gy10M9EnxfQHC4HBhEKi wg/XdTrNt/QQgJ1T8oT1Vd2gufGUV3HwH3APB/KdWXITrR2uAq85qpdeVZB34/1xpvNr OoExg8/fRkhcEkM31xzBzjKzco6mZsXjb5fIKlSUcapfKt8h/7u5txkTtqHrmM9xHq2T m5DA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:dkim-signature; bh=c57dSUyN2hMIrlWdtV3bxqRD+lpwBYl25GBIYSPsuX8=; b=bq1yrfrguRHnjYl4fhK8T9Z3QegreoDEPmbL9ejyiBoHFEPo+3XA+gxXKAlVAbYUS5 3G8FAb9h1Awtlmlqbnk1gHox/8wMIYYXWARj92PKZ/19czJEASuI4PyekthjeGZuhrP6 4WRauurendOQjpLEnmpTisYPOcjU7rjBEyh7NWhod6vLm6yAmmrDDSvYZjOjSzTiZQ5i UiQxqDiV+B5CRlrxB+BF6y/EDOikPDL3/9oP9tK1/G/a+OgDb+NDSvUfVkI/3VD9LH3X BSYiJF8JV7FfGcGo/4cP2F+iIG146WaI1Kn/vVZIxah/DeJX2djJiDk9aticllsk4Lb2 6zrQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego.edu header.s=google header.b=CPVRakNO; spf=pass (google.com: domain of shulman@sandiego.edu designates 2a00:1450:4864:20::52e as permitted sender) smtp.mailfrom=shulman@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu Received: from mail-ed1-x52e.google.com (mail-ed1-x52e.google.com. [2a00:1450:4864:20::52e]) by gmr-mx.google.com with ESMTPS id df17si61223edb.3.2021.03.04.20.41.25 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Thu, 04 Mar 2021 20:41:25 -0800 (PST) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2a00:1450:4864:20::52e as permitted sender) client-ip=2a00:1450:4864:20::52e; Received: by mail-ed1-x52e.google.com with SMTP id bd6so797328edb.10 for ; Thu, 04 Mar 2021 20:41:25 -0800 (PST) X-Received: by 2002:a05:6402:350f:: with SMTP id b15mr7539281edd.6.1614919284640; Thu, 04 Mar 2021 20:41:24 -0800 (PST) Received: from mail-ej1-f50.google.com (mail-ej1-f50.google.com. [209.85.218.50]) by smtp.gmail.com with ESMTPSA id sb4sm787846ejb.71.2021.03.04.20.41.23 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Thu, 04 Mar 2021 20:41:23 -0800 (PST) Received: by mail-ej1-f50.google.com with SMTP id lr13so953388ejb.8 for ; Thu, 04 Mar 2021 20:41:23 -0800 (PST) X-Received: by 2002:a17:906:2db2:: with SMTP id g18mr725634eji.73.1614919282956; Thu, 04 Mar 2021 20:41:22 -0800 (PST) MIME-Version: 1.0 References: <9eefbc82-ba49-b101-433d-c3c1e452ecda@googlemail.com> <58a0a515-d8fa-4eb2-9555-d3a41fdee728@gmail.com> In-Reply-To: From: Michael Shulman Date: Thu, 4 Mar 2021 20:41:11 -0800 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] two's complement integers To: Jason Gross Cc: Nicolai Kraus , "HomotopyTypeTheory@googlegroups.com" Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Original-Sender: shulman@sandiego.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@sandiego.edu header.s=google header.b=CPVRakNO; spf=pass (google.com: domain of shulman@sandiego.edu designates 2a00:1450:4864:20::52e as permitted sender) smtp.mailfrom=shulman@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , I don't have a particular application in mind at the moment. It just struck me how 2-adic integers have such simple coinductive definitions of the arithmetic operations, without any case distinctions at all, and I wondered whether there was a definition of plain integers with a similar property. It seems annoying to have to constantly case-split on a sign bit. I guess a lower-inductive representation could take advantage of the fact that the 2-adic representation of an integer other than 0 or -1 has a unique largest digit that differs from all larger digits, i.e. it's either ...0000 (i.e. 0) ...1111 (i.e. -1) ...0001 + arbitrary bit string ...1110 + arbitrary bit string This involves more case splits when defining arithmetic, but it would probably be an easy set to show that the HIT one is equivalent to. On Thu, Mar 4, 2021 at 7:02 PM Jason Gross wrote: > > Note that the Coq standard library Z is a binary representation of intege= rs and Z.testbit gives access to the infinite twos-compliment representatio= n. Of course, it makes use of case-distinctions on sign to define it, but = you go bit-by-bit; if the number is negative, you just invert the bit befor= e returning it. Is there something you're after by having the representati= on not encode sign bits separately? > > On Thu, Mar 4, 2021, 21:27 Michael Shulman wrote: >> >> On Thu, Mar 4, 2021 at 3:16 PM Nicolai Kraus w= rote: >> > I'm not sure what the precise thing is that you're looking for because= , without further specification, any standard definition of Z would qualify= :-) >> >> Yes, that seems to be what Martin suggested too with =E2=84=95 + =E2=84= =95. It seemed >> to me as though the distance between =E2=84=95 + =E2=84=95 and my =E2=84= =A4 is greater than >> the distance between his =F0=9D=94=B9 and =F0=9D=94=B9', but maybe not i= n any important >> way. >> >> > The HIT is neat, but wouldn't it in practice behave pretty similar to = a standard representation via binary lists? E.g. something like Unit + Bool= * List(Bool), where inl(*) is zero, the first Bool is the sign, and you ad= d a 1 in front of the list in order to get a positive integer. What's the a= dvantage of the HIT - maybe one can avoid case distinctions? >> >> Is there a non-HIT binary representation that can be interpreted as >> two's-complement (thereby avoiding case distinctions on sign)? I >> haven't been able to figure out a way to do that with mere lists of >> booleans. >> >> -- >> You received this message because you are subscribed to the Google Group= s "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >> To view this discussion on the web visit https://groups.google.com/d/msg= id/HomotopyTypeTheory/CAOvivQwtAMVnOG7D_A_s1EMAum4fv_x945MLB%2B01Y_pMdEKC2w= %40mail.gmail.com. > > -- > You received this message because you are subscribed to the Google Groups= "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an= email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > To view this discussion on the web visit https://groups.google.com/d/msgi= d/HomotopyTypeTheory/CAKObCaqiyUcB%2BFrbvPmR-eS5ZMsb2CTVCtVbAYZeMUcOzCpmbA%= 40mail.gmail.com. --=20 You received this message because you are subscribed to the Google Groups "= Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/CAOvivQxy2EJNScHu9Y2U%3DGLiHDrDxDq-Kg8Dz9TrFk3ZepiW8Q%40= mail.gmail.com.