De Bruijn Numerals(text.marvinborner.de)
text.marvinborner.de
De Bruijn Numerals
https://text.marvinborner.de/2023-08-22-22.html
10 コメント
Thanks, added it to bruijn's standard library [0]. Looks like it has some very interesting properties!
[0]: https://bruijn.marvinborner.de/std/Number_Tuple.bruijn.html
[0]: https://bruijn.marvinborner.de/std/Number_Tuple.bruijn.html
Looking at https://text.marvinborner.de/2023-04-06-01.html helped me understand the syntax a bit (though I'm just a non-theoretical programmer).
I was confused about what <4> = \lambda ^ 5 4 meant, since it already seemed to have a "4" in it.
The trick is that the 4 seems to be similar to a positional argument index, but numbered inside out.
IOW, in this encoding, <4> is a function that can be called 5 times (the exponent on the lambda) and upon the fifth call will resolve to whatever was passed in 1st (which because of the inside-out ordering is labeled "4").
(For a simpler example, 0 is a function that can be called once and returns its argument.)
So succ is 3-ary; it says, give me a function (index 2, outermost call); next, give me its first argument (index 1, second-outermost call); when you call that (index 0, dropped, innermost call), I'll apply the function to the argument.
But note that if index 2 is a numeral <N>, the outermost call returns a function that will "remember" the next thing passed in and return it after 1 (succ's innermost call) + N + 1 (<N>'s contract) calls.
I was confused about what <4> = \lambda ^ 5 4 meant, since it already seemed to have a "4" in it.
The trick is that the 4 seems to be similar to a positional argument index, but numbered inside out.
IOW, in this encoding, <4> is a function that can be called 5 times (the exponent on the lambda) and upon the fifth call will resolve to whatever was passed in 1st (which because of the inside-out ordering is labeled "4").
(For a simpler example, 0 is a function that can be called once and returns its argument.)
So succ is 3-ary; it says, give me a function (index 2, outermost call); next, give me its first argument (index 1, second-outermost call); when you call that (index 0, dropped, innermost call), I'll apply the function to the argument.
But note that if index 2 is a numeral <N>, the outermost call returns a function that will "remember" the next thing passed in and return it after 1 (succ's innermost call) + N + 1 (<N>'s contract) calls.
Just use Scott-Mogensen encoding, seriously.
Zero = z. s. z
Succ = n. z. s. s n
isZero = n. n True (_. False)
pred = n. n Zero (r. r)
add' = add'. m. n. m n (r. Succ (add' add' r n))
add = add' add'
> Scott-Mogensen encoding
just Scott encoding, Scott-Mogensen refers to a meta encoding of LC in LC. Scott's encoding is fine but requires fixpoint recursion for many operations as you said.
Interestingly though, Mogensen's ternary encoding [1] does not require fixpoint recursion and is the most efficient (wrt being compact) encoding in LC known right now.
> Just use [..], seriously
do you have any further arguments for Scott's encoding? There are many number encodings with constant time predecessor, and with any number requiring O(n) space and `add` being this complex, it becomes quite hard to like
[1]: https://dl.acm.org/doi/10.5555/646802.705958
just Scott encoding, Scott-Mogensen refers to a meta encoding of LC in LC. Scott's encoding is fine but requires fixpoint recursion for many operations as you said.
Interestingly though, Mogensen's ternary encoding [1] does not require fixpoint recursion and is the most efficient (wrt being compact) encoding in LC known right now.
> Just use [..], seriously
do you have any further arguments for Scott's encoding? There are many number encodings with constant time predecessor, and with any number requiring O(n) space and `add` being this complex, it becomes quite hard to like
[1]: https://dl.acm.org/doi/10.5555/646802.705958
First, if we're talking about practicality, and not just theoretical considerations, then the numbers should not be stored as Peano integers a.k.a. base 1 in the first place. Use lists of 8-tuples of bools or native machine integers or whatever, otherwise, you will suffer from O(n) complexities somewhere in your arithmetic, that's just how base 1 works. Fretting over which particular basic operation has to house this linear-over-logarithmic overhead is IMO unproductive: use better data structures instead of counting sticks.
Second, if we're talking about other data structures, especially recursive ones, e.g. lists, then having easily available (and performant) structural recursion is just more useful than having right folds out of the box: those can be recreated easily, but going in the other direction is much more convoluted.
Second, if we're talking about other data structures, especially recursive ones, e.g. lists, then having easily available (and performant) structural recursion is just more useful than having right folds out of the box: those can be recreated easily, but going in the other direction is much more convoluted.
> then the numbers should not be stored as Peano integers a.k.a. base 1 in the first place
That's my point though. The linked n-ary encoding by Mogensen, for example, does not suffer from such complexities. Depending on the reducer's implementation, (supported) operations on my presented de Bruijn numerals are also sublinear. I doubt 8-tuples of Church booleans would be efficient though - except when letting machine instructions leak into LC.
Though I agree that the focus of functional data structures should lie on embedded folds. Compared to nested Church pairs, folded Church tuples (\cons nil.cons a (cons b nil)) or Church n-tuples (\s.s a b c) should be preferred in many cases.
That's my point though. The linked n-ary encoding by Mogensen, for example, does not suffer from such complexities. Depending on the reducer's implementation, (supported) operations on my presented de Bruijn numerals are also sublinear. I doubt 8-tuples of Church booleans would be efficient though - except when letting machine instructions leak into LC.
Though I agree that the focus of functional data structures should lie on embedded folds. Compared to nested Church pairs, folded Church tuples (\cons nil.cons a (cons b nil)) or Church n-tuples (\s.s a b c) should be preferred in many cases.
If you’re “into” de Bruijn numerals or Project Euler then you might be familiar with this little treat:
https://projecteuler.net/problem=941
Otherwise, have a go and don’t spoil it! (I have failed thus far.)
https://projecteuler.net/problem=941
Otherwise, have a go and don’t spoil it! (I have failed thus far.)
If it helps, you can find a treatment of this in Knuth's vol 4, I believe. Will have to see if I can actually solve it later.
Amusingly, this same basic problem was given to me by Google as an interview question. I was baffled, as I could name the problem, and knew of a reference book that covered it; but I wasn't able to just "on the fly" solve it. Felt like I was living a strawman of pointlessly difficult interview questions. (To be fully fair, I'm not sure I bombed this part. Been far too long for me to remember the other parts.)
Amusingly, this same basic problem was given to me by Google as an interview question. I was baffled, as I could name the problem, and knew of a reference book that covered it; but I wasn't able to just "on the fly" solve it. Felt like I was living a strawman of pointlessly difficult interview questions. (To be fully fair, I'm not sure I bombed this part. Been far too long for me to remember the other parts.)
Seems like an abstract/symbolic variation related to tetration[0]
[0] : tetration : https://en.wikipedia.org/wiki/Tetration
[0] : tetration : https://en.wikipedia.org/wiki/Tetration
> Specifically, he calls a numeral system adequate if it allows for a successor (succ) function, predecessor (pred) function, and a zero? function yielding a true (false) encoding when a number is zero (or not).
A numeral system is adequate iff it can be converted to and from Church numerals. Converting from Church numerals requires functions N0 and Nsucc so that
while converting to Church numerals requires functions Nzero? and Npred so that
with an implicit use of the fixpoint combinator.
An interesting adequate numeral system is what i call the tuple numerals [1], which are simply iterates of the 1-tuple function T = λxλy.y x
So N0 = id, Nsucc = λnλx.n (T x), Npred = λnλx.n x id, and Nzero? = λnλtλf. n (K t) (K f).
These tuple numerals are useful in proving lower bounds on a functional busy beaver [2].
[1] https://github.com/tromp/AIT/blob/master/numerals/tuple_nume...
[2] https://oeis.org/A333479 (see bms.lam link)