-calculus
-calculus (Church 1932, Schoenfinkel 1924,
Barendregt 1984) is a syntactical (as opposed to an
algebraic) system intended as a convenient means for writing
expressions which denote functions.
The "objects" are symbolic strings (i.e., expressions) constructed
according to certain rules of grammar. The "multiplication" or binary
operation among expressions is application. It's operation is
defined in terms of a scheme for rewriting the structure of
expressions. That scheme derives from an analysis of the concept of
"substitution" (i.e., the process of replacing a variable in an
expression by an argument expression). The ingredients of
-calculus are syntactical concepts, such as "variable",
the associated notion of "scope", and "substitution". The rewrite
scheme of -calculus generates an equality relation
between different combinations of expressions, much like the rules of
arithmetic allow to deduce the equality of different symbol sequences,
such as 2+2 and 3+1.
There exists a translation from -expressions to terms
of a combinatory algebra such that all equations which hold in the
-world are exactly those that hold in combinatory
algebra.