Lambda Calculus - Evaluating Custom Rewrite Rules to Increment

26 views Asked by At

I am working with this set of rewrite rules for lambda calculus:

Rewrite Rules

While evaluating "INC 0", I performed these steps: INC 0

Subsequently, I evaluated "INC 1" as such:

INC 1

Are these evaluations accurate? If not, what am I doing incorrectly?

1

There are 1 answers

0
eylion On

the last step is not correct. It seems like you confused the precedences. (\x.x) is not applied to the first \x. .. abstraction, but part of its body.

you can use an online lambda beta-reducer like https://lamboolda.com/lambda to check your results: enter image description here