Untyped \lambda-calculus

The untyped \lambda-calculus is a formal system introduced by Alonzo Church in the 1930s.

Please expand.

Syntax

  M \Coloneqq x \mid \lambda x. M \mid MM

Standard theory

Please expand: head normal forms, etc.

Lazy theory

Please expand.

See also the lazy lambda calculus.

Models

Please expand.

Relationship to set theory

There have been attempts at connecting the untyped \lambda-calculus to set theory. Perhaps the most straightforward approach to doing so consists in interpreting the fundamental predicate of set theory

x \in y

by

y(x) \text{ is true}

In this context, "is true" could mean a number of different things.

See untyped \lambda-calculus and set theory.

References

Please expand.