What's Lambda Calculus?
Learn about it here.
Your first β-reduction
- Enter
(λx.x) a
in the text field in the main section (use the backslash key to write the λ-symbol). - Click the start button.
- You can see that all the reducible expressions are highlighted. In this case there is only one reducible expression, click on it.
- Congratulations, you just did your first β-reduction!
Your first δ-reduction
- In this example, we are going to solve the boolean expression
True or False
using lambda calculus. - Enter
or True False
in the text field in the main section. - Click the start button.
- Just like in the previous example, the reducible expressions get highlighted. The underlines indicate that the expressions will be reduced using δ-reduction. This time we are not clicking on the highlighted expression but instead use the "Next _ Steps" button, click it.
- The term should now be reduced to its normal for and you should see that the result is
λx.λy.x
which is "true" expressed in lambda calculus.
How to write your own rewrite rule
Take a look at the predefined rewrite rule list in the left sidebar. You will find that there is a rule called +, but what if we want to write "plus" instead?
We are going to create our own rewrite rule for that in two different ways, but let us start with the simpler version.
- Enter
plus = +
in the text field in the sidebar. - Click the + button.
- Now we are going to test the just created rule. Enter
plus 1 0
in the text field in the main section. - Click start.
- Click "Next _ Steps" until the term is fully reduced.
- The result should be
λf.λx.fx
(1 in church encoding).