The simply typed lambda calculus assigns arrow types to variables, abstractions, and applications according to syntax-directed typing rules.
A typed lambda term carries a type derivation under a context of typed free variables. The rules for variables, abstraction, and application correspond to assumptions, the implication introduction rule, and the implication elimination rule under the Implicational Curry-Howard correspondence. General fixed-point combinators belong to the untyped lambda calculus; self-application cannot be given a finite simple type.
Every well-typed term in the simply typed lambda calculus has some finite beta-reduction sequence ending in a beta-normal form.
Articles by others on the same topic
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 \).