2
$\begingroup$

I have played around with evaluation of Lambda terms in Lambda calculus and their counterparts using SKI combinators. While the results are extensionally equal (as they should be), there are striking differences in intensional behavior. I suspect that the notion "SKI combinator calculus is Lambda calculus without the need for abstraction" is quite misleading.

Let me explain with some examples:

While the fixed-point combinator Y := λg.(λx.g (x x)) (λx.g (x x)) does not have a normal form in Lambda calculus and tends to "explode" when reduced, evaluation of its SKI-counterpart stops after some steps. Only when it is supplied with an argument will it explode into an endless recursion. When the B and C combinators are allowed, no reduction of the SKI-counterpart at all is possible (without an argument supplied).

Calculation with Church-numerals in Lambda-calculus always seems to generate the familiar form λf.λx.f (f ... (f x) while in SKI complex trees are generated that reduce to the familiar multiple application of something only after you supply f and x. This is best illustrated by multiplication MULT := λm.λn.λf.m (n f) which translates to the B combinator. B needs 3 arguments so with combinators, the multiplication is carried out only when the result is "used" by supplying it with arguments.

This behavior can be explained with the transformation rules: λx. (E1 E2) translates to S E1' E2' if x occurs free in E1 or E2. While (E1 E2) can be reduceable in Lambda-calculus (if E1 is an abstraction), there is no way E2' can be put into E1' before S got its third argument.

It seems that I get comparable results with both systems when I modify my Lambda-evaluator not to reduce stuff inside abstractions - a kind of "super lazy" evaluation. So could the SKI combinator calculus be characterised as Lambda calculus with "super lazy evaluation"?

There are several different notions of normal forms described in https://en.wikipedia.org/wiki/Beta_normal_form but I can find none that corresponds to the behavior described above (not reducing inside an abstraction that cannot be beta-reduced). I find this odd because this seems to be what the SKI system produces.

Maybe someone can shed more light on the relation between the two systems.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.