Discussion:
[Agda] libraries for Bin
Sergei Meshveliani
2018-07-02 09:46:14 UTC
Permalink
Dear all,

This year I announced a library Binary (the current version is 3.2)
that adds certain necessary things to Standard library:
http://www.botik.ru/pub/local/Mechveliani/binNat/

But it looks like the same things were done by Arseniy Alekseyev in
2013:
https://github.com/Rotsor/BinDivMod

(only the code, no `readme', no docs).
I am sorry for not looking into this attentively year ago.

Also I could, may be, save three months of effort.
Anyway this was an exercise, the same proof functionality built in two
different ways.

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.

Regards,

------
Sergei
Martin Escardo
2018-07-03 10:29:36 UTC
Permalink
Post by Sergei Meshveliani
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 : 𝔹 β†’ 𝔹

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
Sergei Meshveliani
2018-07-03 20:06:27 UTC
Permalink
Post by Martin Escardo
Post by Sergei Meshveliani
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
Post by Martin Escardo
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.
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
https://lists.chalmers.se/mailman/listinfo/agda
Anton Trunov
2018-07-03 20:18:01 UTC
Permalink
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
Post by Sergei Meshveliani
Post by Martin Escardo
Post by Sergei Meshveliani
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 : 𝔹 β†’ 𝔹
[..]
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
Post by Martin Escardo
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.
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
https://lists.chalmers.se/mailman/listinfo/agda
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
Sergei Meshveliani
2018-07-04 12:52:04 UTC
Permalink
Post by Anton Trunov
Hi Sergei,
What part of the Coq Standard library have you looked into?
Somewhere there: BinNatDef, ZArith, NArith.

I shall try to repeat the search when I get to appropriate machine.


By the way, can you inform me, please, what is a common way to find
materials on the packages or methods in Coq ?
Typically, there is announced a package Foo in Coq, and it refers to the
code (written, may be, in Gallina, I do not know), and I see this code.
But where is a reference to the method explanation, to comments, to
manual on the package, to papers, to books?
A program package is somehow supposed to have a manual on this package.

I wonder of what I am missing.
May be binary naturals are too simple to provide it with comments, but
there are many other quite involved packages.

For example, when one programs factoring an integer, one is supposed to
add a comment: the theory is described in this paper <reference>, and
the algorithm is taken from <reference>, its evaluation cost is O(foo),
and this estimation is proved in <reference>.

Can you, please, explain: how is this organized in Coq packages?

Regards,

------
Sergei
Post by Anton Trunov
https://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#N
Best regards,
Anton Trunov
Post by Sergei Meshveliani
Post by Martin Escardo
Post by Sergei Meshveliani
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 : 𝔹 β†’ 𝔹
[..]
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
Post by Martin Escardo
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.
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
https://lists.chalmers.se/mailman/listinfo/agda
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
Anton Trunov
2018-07-04 21:36:25 UTC
Permalink
Sure, we can chat about Coq packages, but let’s do that off the Agda mailing list! :)

Best,
Anton
Post by Sergei Meshveliani
Post by Anton Trunov
Hi Sergei,
What part of the Coq Standard library have you looked into?
Somewhere there: BinNatDef, ZArith, NArith.
I shall try to repeat the search when I get to appropriate machine.
By the way, can you inform me, please, what is a common way to find
materials on the packages or methods in Coq ?
Typically, there is announced a package Foo in Coq, and it refers to the
code (written, may be, in Gallina, I do not know), and I see this code.
But where is a reference to the method explanation, to comments, to
manual on the package, to papers, to books?
A program package is somehow supposed to have a manual on this package.
I wonder of what I am missing.
May be binary naturals are too simple to provide it with comments, but
there are many other quite involved packages.
For example, when one programs factoring an integer, one is supposed to
add a comment: the theory is described in this paper <reference>, and
the algorithm is taken from <reference>, its evaluation cost is O(foo),
and this estimation is proved in <reference>.
Can you, please, explain: how is this organized in Coq packages?
Regards,
------
Sergei
Post by Anton Trunov
https://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#N
Best regards,
Anton Trunov
Post by Sergei Meshveliani
Post by Martin Escardo
Post by Sergei Meshveliani
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 : 𝔹 β†’ 𝔹
[..]
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
Post by Martin Escardo
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.
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
https://lists.chalmers.se/mailman/listinfo/agda
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
Sergei Meshveliani
2018-07-05 11:25:07 UTC
Permalink
Post by Anton Trunov
Hi Sergei,
What part of the Coq Standard library have you looked into?
https://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#N
I was looking at
https://coq.inria.fr/distrib/current/stdlib/Coq.NArith.BinNatDef.html

There it is written
Operation x -> 2*x+1

Definition succ_double x :=
match x with
| 0 => 1
| pos p => pos p~1
end.

Operation x -> 2*x

Definition double n :=
match n with
| 0 => 0
| pos p => pos p~0
end.
...

I do not know Coq, nor its language Gallina.
I thought that double and suc_double are constructors for a data type
of Bin(ary natural).
But probably they are not (?).

And where I have seen 0# -- I do not recall, probably I have
`invented' it.

Generally: looking at this www page, and in other Coq pages, I cannot
guess how natural numbers are represented in Coq Standard library in the
binary system.

Can anybody, please, explain shortly ?

------
Sergei
Post by Anton Trunov
Post by Sergei Meshveliani
Post by Martin Escardo
Post by Sergei Meshveliani
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 : 𝔹 β†’ 𝔹
[..]
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
Post by Martin Escardo
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.
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
https://lists.chalmers.se/mailman/listinfo/agda
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
Anton Trunov
2018-07-05 12:51:36 UTC
Permalink
The file you linked uses `N` type from https://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html as
the underlying implementation.
I think that the comments explaining the representation are quite clear but let me retell the story a bit.

Inductive positive : Set :=
| xI : positive -> positive
| xO : positive -> positive
| xH : positive.

defines essentially a list of bits (in reverse order): a_0 a_1 … a_n 1
which can be interpreted as a positive natural number.

To introduce the non-negative numbers the library uses yet another datatype:

Inductive N : Set :=
| N0 : N
| Npos : positive -> N.

This ensures that each natural number has unique representation.
It looks like the Coq devs did it this way to reuse `positive` type for binary integers.

The `succ_double` and `double` definitions you mentioned are functions on N type.

I hope it helps. You can get more insights about Coq asking on
Coq Club mailing list, Reddit (/r/Coq), Stackoverflow (`coq` tag), IRC (freenode, #coq), functionalprogramming.slack.com (#coq), the Telegram Dependent Types group,
or feel free to drop me a personal email (I don’t want to keep spamming the Agda list with Coq).

Best,
Anton
Post by Sergei Meshveliani
Post by Anton Trunov
Hi Sergei,
What part of the Coq Standard library have you looked into?
https://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#N
I was looking at
https://coq.inria.fr/distrib/current/stdlib/Coq.NArith.BinNatDef.html
There it is written
Operation x -> 2*x+1
Definition succ_double x :=
match x with
| 0 => 1
| pos p => pos p~1
end.
Operation x -> 2*x
Definition double n :=
match n with
| 0 => 0
| pos p => pos p~0
end.
...
I do not know Coq, nor its language Gallina.
I thought that double and suc_double are constructors for a data type
of Bin(ary natural).
But probably they are not (?).
And where I have seen 0# -- I do not recall, probably I have
`invented' it.
Generally: looking at this www page, and in other Coq pages, I cannot
guess how natural numbers are represented in Coq Standard library in the
binary system.
Can anybody, please, explain shortly ?
------
Sergei
Post by Anton Trunov
Post by Sergei Meshveliani
Post by Martin Escardo
Post by Sergei Meshveliani
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 : 𝔹 β†’ 𝔹
[..]
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
Post by Martin Escardo
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.
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
https://lists.chalmers.se/mailman/listinfo/agda
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
Arseniy Alekseyev
2018-07-03 20:28:33 UTC
Permalink
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].
Post by Sergei Meshveliani
Post by Martin Escardo
Post by Sergei Meshveliani
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
Post by Martin Escardo
Post by Sergei Meshveliani
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 : 𝔹 ҆’ 𝔹
[..]
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
Post by Martin Escardo
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.
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
https://lists.chalmers.se/mailman/listinfo/agda
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
Sergei Meshveliani
2018-11-09 09:58:22 UTC
Permalink
Post by Martin Escardo
Post by Sergei Meshveliani
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.
(I)
Post by Martin Escardo
Post by Sergei Meshveliani
`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
-- (II)
Post by Martin Escardo
zero : 𝔹
l : 𝔹 β†’ 𝔹
r : 𝔹 β†’ 𝔹
[..]
1) I have improved the representation 0#, double, suc-double
to
0#,
2suc -- (2(n+1)),
suc2* -- (1+2n) (III),

and this has produced the library
https://github.com/mechvel/Binary-4

2) I have come to the representation III due to misunderstanding of a
certain part of the Coq documentation. In fact, Coq represents Bin very
differently.

3) Now, returning to Martin's letter, I see that my III differs from II
only in constructor renaming.

So that I apologize.
And I need to say that

my Binary-4 uses the Bin representation that have been used earlier
by Martin Escardo

(the algorithms implementation is done independently).
Due to not paying enough attention to Martin's letter, I used the
representation III without understanding that it repeats II.

Regards,

------
Sergei

Loading...