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 18146 invoked from network); 4 Mar 2021 20:43:44 -0000 Received: from mail-wr1-x438.google.com (2a00:1450:4864:20::438) by inbox.vuxu.org with ESMTPUTF8; 4 Mar 2021 20:43:44 -0000 Received: by mail-wr1-x438.google.com with SMTP id h30sf6644wrh.10 for ; Thu, 04 Mar 2021 12:43:44 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1614890622; cv=pass; d=google.com; s=arc-20160816; b=vJvsFK5abjLu58Z3QU3FjAiw+Rlg+tm1N94BlZomTipfzjKCEwf4K5CLwbKcpPiT9E ZqDasInBmv/RDdnAML4acaDJxUzBcIx8WfFiFsEhRX1juITaqSArBJjmTNNxpwdwPcw6 LGmMiNdpn3UJ2kYbIp18kDZ9p6RY5LwLEms4vdugqfEMWRdHkZOt/Oh3UYL5WA0BTwB9 19Rds7Ej+j+l2oHhKbc1DWKA4L0JWyaLvZCgcgk08mMHMsrxWo/UVzY8QPIzaO96N8is z9QOIs8o2rU3ssYuOyVOaWoyxRtQBFJWo9LNaGoQmBR3Sikc6rxd04LizbKAJP4EHL8r DaUA== 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:to:subject :message-id:date:from:mime-version:sender:dkim-signature; bh=LkZXKwJpjVhNXWn+OG6Ye5hA39whx5hpOQWjBv0jOF8=; b=kwMeor89eSWp0LvUZbNic7M+F8c+Rx8xogQuom3zRxAbX0MX8lPPaR0Fni1pAN2chN pPxy3IOk4sk86X2XBrNVF9AJzicM4CTOvORvoZkTEl5KuPQV+pPWi7nmE6RULdTK0Fs0 cXVE2Ta4heDyvLCvP5HSvSLUqbklBrn6DkxcLWWfaTjgcsXZ/QZkYfNbywzJxwFLWRXc 1s1qJItTUBJI0uy/VkcomduvTL3sthE4puYX6Ljuo9ssd6HVZvtgnbpUfPoyPBMj+io/ xwvkXqBF3Ma79B9cLocn92PmpA7cttxW++4210g6CjPnLvHNkkJ7WfidLRSj2nxEwOA1 Gljg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego.edu header.s=google header.b="YPEqO/oP"; 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:from:date:message-id:subject:to :content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=LkZXKwJpjVhNXWn+OG6Ye5hA39whx5hpOQWjBv0jOF8=; b=AFwIt7aBo6AI/7HEMWJ0ULXVnuU7f+UpOAHh6lueLkN77bluXory9Rn86TQ/sCJCcr 63X7/SNhy5peLaf6n8tcScL+riSF9thVghFpbW7NyPeWEFiTPEZFFx2sBEd4uLgYARIN ue8kICCoOQJITYoS7Rrni+cRtg7/ZsJl/48KGJ+yZw7BuSYYuC+LyjmcnYbbnfDICeD8 Q/CKNFCnKuPeLwhEgXwaVR1lNFpxF/mII3v7aqoXE5w99XCpCutIurozE05/CoPsxwI9 2BYNdyD9huOKr1J6St0hGJtPc/+N1nS4/j/ZMiUUXr0zNgkeWok3W1vXaV5A8138FxRE 3WNg== 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:from:date:message-id:subject :to: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=LkZXKwJpjVhNXWn+OG6Ye5hA39whx5hpOQWjBv0jOF8=; b=J2jmtrppHuWGfZzjsfdRH/kvN4ltuIwQfxbgcsv6embvgN/BhfMyVelEeEchiwXZ1f yLei6B9oGWjdFihLZbjVRgCROw9s1dTQ77DneQ6cinUhpVEurlFv1cDm0TL0PPwx6mDO 4rs9ySuntj92t7cCtmPwPbF4nOQHQHQVpT5onGfym7VYPnxBFHenFrzfE2ev3krcsjkW GrSnqaf+PJrusVVRSIVAA6IiNSYt6WF87VV/aerlNB3skLQaVvihmojC0sgKjBcdpU7W 95G63gZ86YGkHtGUm47wLzodkbuAe+3Z3XVOlly8dOjKztkEmjEqMMtmgFyQmArQdMjE DU/Q== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM5328DJWI5r3/X2nke/AKit5zSB1ttNesS18yUVOVssJLZNgyAybq UHyDkyko2aCeRz9cmH0p9yc= X-Google-Smtp-Source: ABdhPJwaqQuXobJBHOdp6xcfLoGCrQ0JStF5sVV3iw6yXrJtSwG3ls4iT8Hcpl90YT5/iAahfiuDsw== X-Received: by 2002:a05:600c:3587:: with SMTP id p7mr5577390wmq.176.1614890622642; Thu, 04 Mar 2021 12:43:42 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a5d:4ecf:: with SMTP id s15ls4969062wrv.1.gmail; Thu, 04 Mar 2021 12:43:41 -0800 (PST) X-Received: by 2002:adf:e38a:: with SMTP id e10mr5916956wrm.37.1614890621653; Thu, 04 Mar 2021 12:43:41 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1614890621; cv=none; d=google.com; s=arc-20160816; b=w/QBSilqftIqtX+gq7dGs6HBIsI4Ckz8LZ8gLBdyw3hk/IrSjMHNBKQ1uEH0hIPvEh Bt3SDUaL7PHHl07BBP2HnMoNxC8W7ZMnN+/YBoHxh6pGK52vAa7OnYW0lB8UvL/DQGbt lwuD42h1kQlWGiVCtTKxzhzjZ3ZHk6wk31Mil5NJu7QRRCfA9Es0Ib+HTweQHvITDaIj Sy76kQWN+9Z2zoFq+j1DrowWxw9Iivz6ErkNUGDIeXQat9htAYDdCCveq3Hx1qRNKQEl e10pzXFspzmQgghEhVW51dIJaMK3y/1Ug6ekFM1pf9BXgMhDnzjW49G7ES9E3EO1wUlS opnQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:to:subject:message-id:date:from :mime-version:dkim-signature; bh=G63nwxF2w1n+G5483QCWKhrZfSIo0UA3uNgvcLYdpZY=; b=rEuCt8XCi8AnMFBILzLjcD2PM/B0oNmPC24hL8mANuOfZaJud4eRb/oyPomGPmfA2S jjZTGGD+0eWlNmNPx+/QaMeQ2M42sITcrPP4IhjzeFaJGR0IBqW8+FAVZhx21MT8VlaM BsRQq+r7fnto07iEA/gXCZ30JF2mEH3NN/zjjFsZfMeIrAC27jyfkZTtVG0XADL1M75+ xo5+DvFJ3bo7sAmL6q8MzPnIbSRhsHnQ1+ovS34j6WcZ6vShYy3vuanAuOEJfLIWRwwE C/65Ybc0PQicPnaR6QSv7HH2kMjR4rgKKGtcySQtfjd1cMdRljUSdwK5RChf593UksZS TZSQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego.edu header.s=google header.b="YPEqO/oP"; 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 t9si35167wmj.2.2021.03.04.12.43.41 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Thu, 04 Mar 2021 12:43:41 -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 bd6so23498129edb.10 for ; Thu, 04 Mar 2021 12:43:41 -0800 (PST) X-Received: by 2002:aa7:c944:: with SMTP id h4mr6383204edt.233.1614890621206; Thu, 04 Mar 2021 12:43:41 -0800 (PST) Received: from mail-ej1-f42.google.com (mail-ej1-f42.google.com. [209.85.218.42]) by smtp.gmail.com with ESMTPSA id jj15sm202421ejc.99.2021.03.04.12.43.40 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Thu, 04 Mar 2021 12:43:40 -0800 (PST) Received: by mail-ej1-f42.google.com with SMTP id c10so25566294ejx.9 for ; Thu, 04 Mar 2021 12:43:40 -0800 (PST) X-Received: by 2002:a17:906:25c4:: with SMTP id n4mr6357041ejb.359.1614890620250; Thu, 04 Mar 2021 12:43:40 -0800 (PST) MIME-Version: 1.0 From: Michael Shulman Date: Thu, 4 Mar 2021 12:43:28 -0800 X-Gmail-Original-Message-ID: Message-ID: Subject: [HoTT] two's complement integers To: "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="YPEqO/oP"; 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: , Has anyone considered the following HIT definition of the integers? data =E2=84=A4 : Type where zero : =E2=84=A4 -- 0 negOne : =E2=84=A4 -- -1 dbl : =E2=84=A4 =E2=86=92 =E2=84=A4 -- n =E2=86= =A6 2n sucDbl : =E2=84=A4 =E2=86=92 =E2=84=A4 -- n =E2=86= =A6 2n+1 dblZero : dbl zero =E2=89=A1 zero -- 2=C2=B70 =3D 0 sucDblNegOne : sucDbl negOne =E2=89=A1 negOne -- 2=C2=B7(-1)+1 =3D -1 The idea is that it's an arbitrary-precision version of little-endian two's-complement, with sucDbl and dbl representing 1 and 0 respectively, and negOne and zero representing the highest-order sign bit 1 and 0 respectively. Thus for instance sucDbl (dbl (sucDbl (sucDbl zero))) =3D 01101 =3D 13 dbl (sucDbl (dbl (dbl negOne))) =3D 10010 =3D -14 The two path-constructors enable arbitrary expansion of the precision, e.g. 01101 =3D 001101 =3D 0001101 =3D ... 10010 =3D 110010 =3D 1110010 =3D ... This seems like a fairly nice definition: it should already be a set without any truncation, it's binary rather than unary, and the arithmetic operations can be defined in the usual digit-by-digit way without splitting into cases by sign. Mathematically speaking, it represents integers by their images in the 2-adic integers, with zero and negOne representing infinite tails of 0s and 1s respectively. (An arbitrary 2-adic integer, of course, is just a stream of bits.) Best, Mike --=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/CAOvivQw4h46DtKATiwUvm%3DL%3DjEGng2XdYGAhKbi7fhis%2By_TP= w%40mail.gmail.com.