<div dir="ltr">I just realized another way to understand this encoding: a natural number [n] is encoded by a 1-terminated string of bits of [n + 1].</div><br><div class="gmail_quote"><div dir="ltr">On Tue, 3 Jul 2018 at 21:06, Sergei Meshveliani <<a href="mailto:mechvel@botik.ru">mechvel@botik.ru</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">On Tue, 2018-07-03 at 11:29 +0100, Martin Escardo wrote:<br>
> <br>
> On 02/07/18 10:46, <a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a> wrote:<br>
> > Also I look now into Coq Standard library, the part for binary natural.<br>
> > Generally, Coq shows the code, and it is difficult to find any reference<br>
> > to the related papers, docs. May be, this particular subject is too<br>
> > simple for a paper, but one page `readme' is desirable.<br>
> > <br>
> > Looking at the code, I have an impression that the Bin data is defined<br>
> > there with the constructors<br>
> > <br>
> >                              0#, double, suc-double.<br>
> > <br>
> > `double' constructs any even number, suc-double any odd number.<br>
> > I suspect that this way binary arithmetic is expressed simpler.<br>
> > Only zero is not uniquely represented. But this can be fixed by<br>
> > introducing four constructors instead.<br>
> <br>
> I have a very simple binary naturals library with *unique* <br>
> representations, and which allows linear addition.<br>
> <br>
> <br>
> <a href="http://www.cs.bham.ac.uk/~mhe/agda-new/BinaryNaturals.html" rel="noreferrer" target="_blank">http://www.cs.bham.ac.uk/~mhe/agda-new/BinaryNaturals.html</a><br>
> <br>
> data 𝔹 : Set where<br>
>   zero : 𝔹<br>
>   l    : 𝔹 → 𝔹<br>
>   r    : 𝔹 → 𝔹<br>
> [..]<br>
<br>
<br>
For me, it is easier to understand what is written at the referred page:<br>
<br>
  The isomorphic copy is formally constructed from 0 iterating the<br>
  functions L(n)=2n+1 and R(n)=2n+2.<br>
<br>
So: instead of       0#, double, suc-double     of Coq  <br>
(not unique for 0)<br>
there are suggested  0#, 2n+1, 2n+2<br>
<br>
-- zero, arbitrary odd, arbitrary non-zero even. <br>
This represents Bin uniquely.<br>
<br>
Looks nicer!<br>
Thank you.<br>
<br>
------<br>
Sergei<br>
<br>
<br>
<br>
<br>
> The interpretation function is<br>
> <br>
> unary : 𝔹 → ℕ<br>
> unary zero = zero<br>
> unary(l m) = L(unary m)<br>
> unary(r m) = R(unary m)<br>
> <br>
> where<br>
> <br>
> double : ℕ → ℕ<br>
> double zero    = zero<br>
> double(succ n) = succ(succ(double n))<br>
> <br>
> L : ℕ → ℕ<br>
> L n = succ(double n)<br>
> <br>
> R : ℕ → ℕ<br>
> R n = succ(L n)<br>
> <br>
> This interpretation function is an equivalence in the sense of HoTT/UF. <br>
> Its inverse is easy to define:<br>
> <br>
> Succ : 𝔹 → 𝔹<br>
> Succ zero  = l zero<br>
> Succ(l m)  = r m<br>
> Succ(r m)  = l(Succ m)<br>
> <br>
> binary : ℕ → 𝔹<br>
> binary zero    = zero<br>
> binary(succ n) = Succ(binary n)<br>
> <br>
> I am sure people must have considered this isomorphic representation of <br>
> the natural numbers, though, because it is very simple and natural.<br>
> <br>
> Martin<br>
> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>