The untyped -calculus is a formal system introduced by Alonzo Church in the 1930s.
Please expand.
Please expand: head normal forms, etc.
Please expand.
See also the lazy lambda calculus.
Please expand.
There have been attempts at connecting the untyped -calculus to set theory. Perhaps the most straightforward approach to doing so consists in interpreting the fundamental predicate of set theory
by
In this context, "is true" could mean a number of different things.
See untyped -calculus and set theory.
Please expand.