[\fx -> f(f(fx))]
[\f -> [\x -> f(f(fx))]]
[\f -> S[\x -> f][\x -> f(fx)]]
[\f -> S(Kf)(S[\x -> f][\x -> fx])]
[\f -> S(Kf)(S(Kf)f)]
S[\f -> S(Kf)][\f -> S(Kf)f]
S(S[\f -> S][\f -> Kf])(S[\f -> S(Kf)][\f -> f]))
S(S(KS)K)(S(S[\f -> S][\f -> Kf])I)
S(S(KS)K)(S(S(KS)K)I)

[\nmfx -> nf(mfx)]
[\n -> [\m -> [\f -> [\x -> nf(mfx)]]]]
[\n -> [\m -> [\f -> S[\x -> nf][\x -> mfx]]]]
[\n -> [\m -> [\f -> S(K(nf))(mf)]]]
[\n -> [\m -> S[\f -> S(K(nf))][\f -> mf]]]
[\n -> [\m -> S(S[\f -> S][\f -> K(nf)])m]]
[\n -> [\m -> S(S(KS)(S[\f -> K][\f -> nf]))m]]
[\n -> [\m -> S(S(KS)(S(KK)n))m]]
[\n -> S(S(KS)(S(KK)n))]
S[\n -> S][\n -> S(KS)(S(KK)n)]
S(KS)(S[\n -> S(KS)][\n -> S(KK)n])
S(KS)(S(K(S(KS)))(S(KK)))




S(KS)(S(K(S(KS)))(S(KK))) (S(S(KS)K)(S(S(KS)K)I) (S(S(KS)K)(S(S(KS)K)I)

{This is how we say "2 + 2" in the SKI combinator calculus...}

Post a reply to this message