Beta reduction of S combinator in pure lambda calculus

Question

S is defined as S x y z = x z (y z)

This suggest that (y z) should be evaluated just after x z and the the results of x z is applied to the results of (y z).

I'm implementing call by value in lambda calculus, I would need to support parenthesis when evaluating this expression right? Does this affect the results? I thought that the order would not matter, so why the parenthesis in (y z)?

Regards

Answer 1

Parentheses matter. Honestly, if you are unclear about how $\lambda$-calculus works, it is going to be rather hard to implement it.

Here is an explicit counter-example: $$(K S)(K S) = S$$ but $$K S K S = ((K S) K) S = S S \neq S.$$

I would recommend learning about parsers, abstract syntax trees, and other bits and pieces that make up an implementation of a programming language.

An example of the implementation of the $\lambda$-calculus is available as lambda at PL Zoo. See repl-in-browser for an implementation that runs in the browser (an instance of which is available here).

• geckos: Hi Andre, thanks for the answer. In fact I do support parentheses. My problem was more at understanding that $x z y z \not\equiv_\beta x z (y z)$ I'll try to get a proof of that to my self
• Andrej Bauer: Application is defined to be left-associative, i.e., $A B C = (A B) C$. Thus you are asking whether $x z y z = ((x z) y) z$ is equal to $(x z)(y z)$. The answer is "obviously not" because application is not associative. If that is what you are asking?
• Andrej Bauer: I added an explicit counter-example.
• geckos: Woooow, that PLZoo is a Gold mine, thank you so much to sharing!!! I will take a look, I have a lambda calc implemented here github.com/dhilst/funcyou/blob/master/lambdac.py. It uses the fn x => x syntax for lambda. I will use your implementation as review resource, thank you!!
• geckos: yeah, I confused the evaluation semantics with associativity. If I have $PQ$ evaluating P or Q first would not really change the reduction result right? But if I have $PQR$ then this is $(PQ)R$ which is different from $P(QR)$