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.1 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,FREEMAIL_FROM,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 27581 invoked from network); 5 Mar 2021 03:02:36 -0000 Received: from mail-qt1-x83f.google.com (2607:f8b0:4864:20::83f) by inbox.vuxu.org with ESMTPUTF8; 5 Mar 2021 03:02:36 -0000 Received: by mail-qt1-x83f.google.com with SMTP id t5sf466791qti.5 for ; Thu, 04 Mar 2021 19:02:36 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1614913353; cv=pass; d=google.com; s=arc-20160816; b=Pnwa3Pe3Q3CttASv/LFvH48zlDpTkWuW6c33nd9VpxSx3FyR17kENg87xKQRXLskQl ScGK3YNriphhTytacC6aEPUf+vJVCMUGdqt6Qpm2h3oVu69JbM38ChP/r2SoPGJh1q87 JPYxb3YDqe1ZQBoHhz1cOnWc7i7/iYE1GT+Vr3yaI0xMlGmSaUjtolTkyMCJZP3QaP36 NSPqjPYsGZguBZTaia0x4IwxsF4/GfNmU0hkRDwCYTHmPHr60ile5761hjWMPQNfIKqb 3h6tPH2m8S0563OtunPDjSBYJVzfi/CEUiHHeQ16s+TdInO3k5xwmuOWHM3MJdjTcFND BxmA== 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:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:sender:dkim-signature :dkim-signature; bh=i9uXuOahhRRz5f9tKu4uGuSG1wIwg39ykiYVWZJB4tE=; b=Eq8n9DQnsQtcNmBj+pSzE5BuZ3nA6ferGCuQOlN2gdE8cY1gww6+EZZi+H0hWKx0rU +KkhNTKZjDJI4hnyDRZ5AN7Fd8MnB7fODzJASom7QDhT/CChuPYf/FRcsjr7/KEeF04b yqJmi01968qFznHarpDt9hJDc9mjXGnLjC80BlOM2CDT89y/TVVok0PTkCshpJbS+JDC WKQW1zxkYJJ9pSWJRivGaR3qguT1BuLn0y3sjG5gdhLZqIGWCbl1UzmkI6FKtII8lgyS nASKcfYKkBm4uWqu0EaYkkMdKWIdWy5IgPvpzfvDs29/Y+RzuLw6Ncd9LUdQ73o746iw Y0kw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b="j1Q/kW6G"; spf=pass (google.com: domain of jasongross9@gmail.com designates 2607:f8b0:4864:20::d2b as permitted sender) smtp.mailfrom=jasongross9@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com 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:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=i9uXuOahhRRz5f9tKu4uGuSG1wIwg39ykiYVWZJB4tE=; b=HOOuUsB5NDydnB3UKr9RSJPQb9FyG+7WM55cEv1+bVBzgALneO90qzruZIKOyifE6g XfohBbSmuSHlRiaLr1/lXB5/AkQ0XseTEyg6okfhNyJQrdJouRAfGi8Ujz36jRQ8B2NM Yj7WXUpWTzX9BM1uN7ZXeMAMoubxU/W8l/aGAqiH/xoF/mr5AdK8JZbXyQnfptHoFBzU 5V0wvSDvHoUCx7pexUAvUcf0+LooYZlA6z1sWVMPSk1MRgB28tfvub3CKEU8bF5K2wBf vROep9ogF4pcxsSx9mMpKSj179mUdafmeOHHzWNAxzkGwKq8m6QG5MlSlujMh0CJFhXY mcXQ== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc:x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=i9uXuOahhRRz5f9tKu4uGuSG1wIwg39ykiYVWZJB4tE=; b=oHnuS2ACUqCMTkwb97wKIEfn2t9IgZJbwCXuiiIy9ozr0DsNT1rf3Zf4FbKQyEXv8c UI9VFaLXO55AzC4vA2PbcdQkol7QjaeuHRO4P5oC5KGz0yR+fn2+bAgSigswyDelDIe0 o0IyKu7UcfJIEDUs5a5euTxSgt20aB3JkW4FHWFbjbwD5jxgwLRquKHCvCjLHtO0z2k1 kT81UHoJHMBHaGbu3I3SCjLAt39fJyLYO6uLaaqGSbBTs2ObPnbw0zC+pKAZ0swhYbmU a5PdDNiKzUDeLJ9Qv4SqUZKys5iVvLww42QR3/p0EwMP0W+KALs5iIc15SR1UiWTPLCq Y33g== 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: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=i9uXuOahhRRz5f9tKu4uGuSG1wIwg39ykiYVWZJB4tE=; b=qEn6+Linib9Ct9IjoOnJXK18UW1z0T8r7UW6KuQqF4h3pmwG3HlK81wDoFdwtVhayT 4qzOkLINm12dBRhCtPjgR5i4wnHeu3dR0A7Qx3bi/JO8E2xa+RSjQkIeyYNnw6GL3Klz u8iiZmQPhLYmkbZYR0N3K2HwZCfCWtE80eLHXS2Sy//D7iQZVCAjwRgOrOl//GcojvR0 ah/UBlq5B+cu/CKjiqQhwy4B3m5brs9l20Nu2Y0KzzsRQB+pKmh31GJMYcMcVxzAyAGZ ke75UuFMAWEe5CHatx1bhZpjDYQyYdxf4D6DwPldFAEUC8rxaO4ajFb2S/S2ccen8y5J 4UUw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM533J39b/r6+wAeUrbf3AtYf7NIDD+uIvWdHjfhb/R8j3kPF3h8ru /oRS9gJ4dZBTqRZPdWQJzzU= X-Google-Smtp-Source: ABdhPJzVaK8OOz0bWI5JT+5UoRJ5dxjqvcQXIOtGFRdxZuVcen6rLeSZl1QvLYZAMs0zFPiM86DBFA== X-Received: by 2002:a37:a085:: with SMTP id j127mr6987322qke.206.1614913352900; Thu, 04 Mar 2021 19:02:32 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:ac8:6b03:: with SMTP id w3ls499564qts.11.gmail; Thu, 04 Mar 2021 19:02:32 -0800 (PST) X-Received: by 2002:ac8:5912:: with SMTP id 18mr7362731qty.18.1614913352310; Thu, 04 Mar 2021 19:02:32 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1614913352; cv=none; d=google.com; s=arc-20160816; b=KNWSLM1JxRITTD145BTu6jIM19t8sSXm8EOofy46MfHK6IuAyX7Dz2khlNmNSPFJFl GhmkhRsuVhzhvcVL6zZkozyyv+DVDIQkXXb1jHWPhBfRzL0vBwIkQFJzDcwkEea8sEDB LVW7aFTbxk92BhNqPRikv1Xd9xGAEl/N2DWQz8gHxs0H3pV4ut3777pcqtqlcAD818YQ Y4DJSNdiAWeVHJYeBB9govj2WK1Wz73pUFb3I57XDY+L2JPsUB8gttuDspDPMQqZsuRQ Jw/rPNflrxW0i9L/1+ZNeF5nVejnN5SBJyPbc1R/2UuBpewI9yVD5nFKEaLnzKE8RfSr FUyg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:dkim-signature; bh=Uj4vcLMSSiDcuK/1zFkGIzdtKIVwqNbp3Nvm5Wnrf04=; b=MRWWZOEs5bd+70qLJl1p7CjaqsXal/e5q5HED5emtkybc2jfg8lhInsF8eqwhWP2r4 mEEVn3MV/eyWGYyypLMSmQj4qbTGGNekBoPQDIPuuwPoE5kq6QMJx6mVEevbbUOqHr6c 0TIyZc8r8vOgIECdPs1/KjERDM6m3antz/oHPXycQuKZf2g0otYKo1+ugxJGh2NbcqQw uGd0Vo7Ya2HtZ76PU0oOsZ4YEXrgdvWh0ymPFvyvfQEv+a5DNyfpF2yQ0Np6hntYZLgs M+Iu0waaBVt4QRxp4wnN6Z4pTdolQJ1/9NygY5Gv4BFHL67J033wIFXn1sMP1GjlG0VP 7wRQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b="j1Q/kW6G"; spf=pass (google.com: domain of jasongross9@gmail.com designates 2607:f8b0:4864:20::d2b as permitted sender) smtp.mailfrom=jasongross9@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-io1-xd2b.google.com (mail-io1-xd2b.google.com. [2607:f8b0:4864:20::d2b]) by gmr-mx.google.com with ESMTPS id b56si81175qtc.5.2021.03.04.19.02.32 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Thu, 04 Mar 2021 19:02:32 -0800 (PST) Received-SPF: pass (google.com: domain of jasongross9@gmail.com designates 2607:f8b0:4864:20::d2b as permitted sender) client-ip=2607:f8b0:4864:20::d2b; Received: by mail-io1-xd2b.google.com with SMTP id i8so459311iog.7 for ; Thu, 04 Mar 2021 19:02:32 -0800 (PST) X-Received: by 2002:a02:a506:: with SMTP id e6mr7475272jam.56.1614913351802; Thu, 04 Mar 2021 19:02:31 -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: Jason Gross Date: Thu, 4 Mar 2021 22:02:18 -0500 Message-ID: Subject: Re: [HoTT] two's complement integers To: Michael Shulman Cc: Nicolai Kraus , "HomotopyTypeTheory@googlegroups.com" Content-Type: multipart/alternative; boundary="000000000000ad614205bcc1509a" X-Original-Sender: JasonGross9@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b="j1Q/kW6G"; spf=pass (google.com: domain of jasongross9@gmail.com designates 2607:f8b0:4864:20::d2b as permitted sender) smtp.mailfrom=jasongross9@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com 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: , --000000000000ad614205bcc1509a Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Note that the Coq standard library Z is a binary representation of integers and Z.testbit gives access to the infinite twos-compliment representation. 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 before returning it. Is there something you're after by having the representation 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 > wrote: > > 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 in= 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 add= a > 1 in front of the list in order to get a positive integer. What's the > advantage 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 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/msgid/HomotopyTypeTheory/CAOvivQwtAMVnOG7D_A_= s1EMAum4fv_x945MLB%2B01Y_pMdEKC2w%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/CAKObCaqiyUcB%2BFrbvPmR-eS5ZMsb2CTVCtVbAYZeMUcOzCpmbA%40= mail.gmail.com. --000000000000ad614205bcc1509a Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Note that the Coq standard library Z is a binary rep= resentation of integers and Z.testbit gives access to the infinite twos-com= pliment representation.=C2=A0 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 before returning it.=C2=A0 Is there something you'= re after by having the representation not encode sign bits separately?
<= br>
On Thu,= Mar 4, 2021, 21:27 Michael Shulman <shulman@sandiego.edu> wrote:
On Thu, Mar 4, 2021 at 3:16 PM Nicolai Kraus <nicolai.kraus@g= mail.com> wrote:
> 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.= =C2=A0 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 = in 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 yo= u add a 1 in front of the list in order to get a positive integer. What'= ;s the advantage 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)?=C2=A0 I<= br> 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 Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyTypeTheory+unsubscribe@googl= egroups.com.
To view this discussion on the web visit = https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOvivQwtAMVnOG7D_A_s1= EMAum4fv_x945MLB%2B01Y_pMdEKC2w%40mail.gmail.com.

--
You received this message because you are subscribed to the Google Groups &= quot;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://g= roups.google.com/d/msgid/HomotopyTypeTheory/CAKObCaqiyUcB%2BFrbvPmR-eS5ZMsb= 2CTVCtVbAYZeMUcOzCpmbA%40mail.gmail.com.
--000000000000ad614205bcc1509a--