Untyped Lambda Calculus

There are two basic notions in the Lambda calculus:

• Abstractions: The idea is that we define a function by specifying which variable we want to be able to substitute. A very simple example is the identity function, which takes a term as parameter and maps it to itself: λx . x
• Applications: This allows us to actually evaluate a function. We derive a new term by substituting the variable in the abstraction with the argument term: (λ x . x x) (y z) → (y z) (y z)

The Lambda Shell allows you to use either λ or \ as lambda symbol for abstractions.

You are allowed to abbreviate multiple abstractions as one: \x . \y . x y = \x y . x y.

In batch mode (when processing .lsh files) you are required to end every statement with a semicolon (;). This is not necessary in interactive mode.

Assignments

In order to keep this readable the Lambda Shell allows you to name terms and reuse them. To assign a name to a term the := tag is used:

one := \f . \x . f x
true := \x . \y . y

These terms are referred to with their name until they get resolved explicitly or during reduction (see macros).