[HN Gopher] De Bruijn Numerals
___________________________________________________________________
De Bruijn Numerals
Author : marvinborner
Score : 59 points
Date : 2025-11-16 15:22 UTC (7 hours ago)
(HTM) web link (text.marvinborner.de)
(TXT) w3m dump (text.marvinborner.de)
| tromp wrote:
| > Christopher Wadsworth analyzed different properties of numeral
| systems and the requirements they have to fulfill to be useful
| for arithmetic.
|
| > 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 Church2Num c = c
| Nsucc N0
|
| while converting to Church numerals requires functions Nzero? and
| Npred so that Num2Church n = Nzero? n C0 (Csucc
| (Num2Church (Npred n)))
|
| 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
| = lxly.y x
|
| So N0 = id, Nsucc = lnlx.n (T x), Npred = lnlx.n x id, and Nzero?
| = lnltlf. 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)
| marvinborner wrote:
| 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
| emptybits wrote:
| 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.)
| taeric wrote:
| 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.)
| Joker_vD wrote:
| 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)
|
| Addition requires explicit recursion, however (since numbers
| aren't folds), so I guess you'll have to either use Y combinator
| or closure-convert manually: add' = add'. m. n.
| m n (r. Succ (add' add' r n)) add = add' add'
|
| In any case, arithmetic operations can't be made fully constant-
| time for obvious reasons so whether your prefer this to Church
| numerals is a matter of taste. However, for lists/tuples the
| ability to execute head/tail/cons in constant time is much more
| important in practice than being able to do append in constant
| time.
| marvinborner wrote:
| > 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
| jagthebeetle wrote:
| 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.
___________________________________________________________________
(page generated 2025-11-16 23:00 UTC)