You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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:
Hi! First off, kudos for a very clear, educational demonstration!
If it's appropriate, I feel like sharing another rewrite of
letrec
intolet
, 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.
Grouping the two equations into one. Assume
<,>
is the pairing construct, such thatp1<a,b> = a
andp2<a,b> = b
.Rewriting
letrec
aslet
together withY
(a fixed-point combinator.)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:Rewriting
let
as an application.Beta-conversion (on pairs.)
Beta-conversion (twice).
Y
Beta-conversion (on pairs.)
p2
Beta-conversion
ifzero and arithmetic
Y
And so on, you get where this is going.
References:
The text was updated successfully, but these errors were encountered: