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 \).
Articles by others on the same topic
In the simply typed lambda calculus, types are generated from base types by the arrow constructor . A context assigns types to variables. Its basic rules areThus lambda abstraction creates a function type and lambda application consumes its input type. For example, has type , and has type .
The untyped self-application would require one finite type to satisfy , which is impossible in this type grammar. This excludes the familiar looping term ; more generally the Strong normalization theorem for simply typed lambda calculus says that every reduction sequence from a well-typed term terminates. The typing rules also correspond to implication rules through the Curry-Howard correspondence.