[Agda] libraries for Bin

[Anton Trunov]

Hi Sergei,

What part of the Coq Standard library have you looked into?

This representation seems to be admitting only unique representations:
https://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#N

Best regards,
Anton Trunov

> On 3 Jul 2018, at 22: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