1
$\begingroup$

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

Improve this question
$\endgroup$

1 Answer 1

Reset to default
4
$\begingroup$

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).

Improve this answer
$\endgroup$
5
  • $\begingroup$ 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 $\endgroup$
    – geckos
    Nov 29, 2020 at 11:27
  • 2
    $\begingroup$ 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? $\endgroup$
    – Andrej Bauer
    Nov 29, 2020 at 13:29
  • 1
    $\begingroup$ I added an explicit counter-example. $\endgroup$
    – Andrej Bauer
    Nov 29, 2020 at 13:39
  • $\begingroup$ 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!! $\endgroup$
    – geckos
    Nov 29, 2020 at 15:31
  • $\begingroup$ 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)$ $\endgroup$
    – geckos
    Nov 29, 2020 at 15:35

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.