[Agda] libraries for Bin

[Sergei Meshveliani]

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