[Agda] libraries for Bin

[Arseniy Alekseyev]

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].

On Tue, 3 Jul 2018 at 21:06, Sergei Meshveliani <mechvel at botik.ru> wrote:

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