catseye/Lanthorn

An alternative rewrite via tuples and a fixed-point combinator

xavierpinho opened this issue · 1 comments

xavierpinho commented

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:

cpressey commented

Yes. 👍 Thank you for that!