An alternative rewrite via tuples and a fixed-point combinator #1
Description
Hi! First off, kudos for a very clear, educational demonstration!
If it's appropriate, I feel like sharing another rewrite of letrec into let, but this time using tuples (surjective pairing) and a fixed-point combinator. In fact, this is how I first learned how to implement mutual recursion in a functional paradigm. (And also because it brings to my mind the so-called banana-split law, curiously enough.)
Please excuse my syntactical deviations from Lanthorn's syntax in the sequel. I trust the meaning is still unambiguous.
letrec od = \x. ifzero(x, FF, ev(x-1))
ev = \x. ifzero(x, TT, od(x-1))
in ev 6
Grouping the two equations into one. Assume <,> is the pairing construct, such that p1<a,b> = a and p2<a,b> = b .
letrec <od, ev> = <\x. ifzero(x, FF, ev(x-1)), \x. ifzero(x, TT, od(x-1)> in ev 6
Rewriting letrec as let together with Y (a fixed-point combinator.)
let <od, ev> = Y (\<od,ev>. <\x. ifzero(x, FF, ev(x-1)), \x. ifzero(x, TT, od(x-1))>) in ev 6
To keep expressions short, let's introduce a meta-variable, say H, standing for the sub-expression (\<od,ev>. <\x. ifzero(x, FF, ev(x-1)), \x. ifzero(x, TT, od(x-1))>). Hence, the above can be read as:
let <od, ev> = Y H in ev 6
Rewriting let as an application.
(\<od, ev>. ev 6) (Y H)
Beta-conversion (on pairs.)
(\od.\ev. ev 6) (p1 (Y H))
(p2 (Y H))
Beta-conversion (twice).
(p2 (Y H)) 6
Y
(p2 (H (Y H))) 6
Beta-conversion (on pairs.)
(p2 <\x. ifzero(x, FF, p2(Y H)(x-1)), \x. ifzero(x, TT, p1(Y H)(x-1)>) 6
p2
(\x. ifzero(x, TT, p1(Y H)(x-1)) 6
Beta-conversion
ifzero(6, TT, p1(Y H)(6-1))
ifzero and arithmetic
p1 (Y H) 5
Y
p1 (H (Y H)) 5
And so on, you get where this is going.
References:
- The Implementation of Functional Programming Languages (Simon Peyton Jones, 1987). Available at: https://www.microsoft.com/en-us/research/publication/the-implementation-of-functional-programming-languages/
- Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire (Meijer, Fokkinga, Patterson, 1991). Available at: https://maartenfokkinga.github.io/utwente/mmf91m.pdf