My notes on Lambda Calculus.
The syntax of the lambda-calculus comprises just three sorts of terms.
- A variable
x
by itself is a term; - The abstraction of a variable
x
from a termt1
, writtenλx.t1
, is a term; - And the application of a term
t1
to another termt2
, writtent1 t2
, is a term.
These ways of forming terms are summarized in the following grammar.