The simply typed lambda calculus assigns arrow types to variables, abstractions, and applications according to syntax-directed typing rules.
Every well-typed term in the simply typed lambda calculus has some finite beta-reduction sequence ending in a beta-normal form.
If a lambda term beta-reduces to both and , then and beta-reduce to a common term. Consequently two beta-equivalent beta-normal forms are alpha-equivalent.
An untyped lambda term is a fixed-point combinator when for every term .
Every well-typed simply typed lambda term admits no infinite beta-reduction sequence.
The Church numeral encodes the natural number by iteration.
At type , the Church Booleans are and .
A partial function is lambda-definable when one lambda term maps Church numerals in its domain to the numeral of the output and produces no numeral on inputs outside its domain.

Ancestors (5)

  1. Computability theory
  2. Foundations of mathematics
  3. Area of mathematics
  4. Mathematics
  5. Home

Incoming links (1)

View article source

Discussion (0)

New discussion

There are no discussions about this article yet.

Articles by others on the same topic (1)

Simply typed lambda calculus by Wikipedia Bot 1
View more
Simply Typed Lambda Calculus (STLC) is a formal system in mathematical logic and computer science that serves as a foundation for understanding typing and functional programming languages. It extends the basic lambda calculus by introducing a simple type system to ensure that functions can only be applied to arguments of compatible types. ### Key Features of STLC: 1. **Syntax**: - **Variables**: Represented by symbols like \( x, y, z \).
Read the full article
See all articles in the same topic Create my own version