Derivation

What's Lambda Calculus?

Learn about it here.

Your first β-reduction

  1. Enter (λx.x) a in the text field in the main section (use the backslash key to write the λ-symbol).
  2. Click the start button.
  3. You can see that all the reducible expressions are highlighted. In this case there is only one reducible expression, click on it.
  4. Congratulations, you just did your first β-reduction!

Your first δ-reduction

  1. In this example, we are going to solve the boolean expression True or False using lambda calculus.
  2. Enter or True False in the text field in the main section.
  3. Click the start button.
  4. 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.
  5. 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.

  1. Enter plus = + in the text field in the sidebar.
  2. Click the + button.
  3. Now we are going to test the just created rule. Enter plus 1 0 in the text field in the main section.
  4. Click start.
  5. Click "Next _ Steps" until the term is fully reduced.
  6. The result should be λf.λx.fx (1 in church encoding).