Lambda Calculus/Basic Definitions

From Wikibooks, open books for an open world
< Lambda Calculus
Jump to: navigation, search

Axioms[edit]

The first concept is that of abstraction. It is analogous to defining a function.

λx.M

This defines a function which takes an argument x and returns a term M. Functions in lambda calculus have no name.

The second concept is that of invocation. IT is essentially a function call.

M N

This binds the argument N to the term M

Definitions[edit]

Term 
A term in Lambda calculus is a defined function. A term may contain variables.
Variable 
A variable, may represent any term. A term may contain free variables or bound variables
Bound variables 
A bound variable is a variable which will be bound to some term passed as an argument. Eg, In λx.xy, x is a bound variable.
Free variables 
A free variable is any variable in a term which is not bound to some other term. Eg, In λx.xy, y is a free variable.