The simply typed lambda calculus adds types to the untyped lambda calculus, ensuring well-formed terms. It introduces basic types, function types, and typing rules for variables, abstraction, and application. This system prevents terms from getting stuck during evaluation.
Well-typed terms in this calculus follow specific construction rules and can be evaluated using beta-reduction. The system guarantees strong normalization, meaning every well-typed term reduces to a normal form in finite steps, proven through logical relations or reducibility methods.
Simply Typed Lambda Calculus
Basic Components and Type System
- The simply typed lambda calculus extends the untyped lambda calculus by introducing a type system to ensure well-formedness of lambda terms
- Basic components of the simply typed lambda calculus:
- Types, usually denoted by T, can be either base types (Int, Bool) or function types (T1 -> T2)
- Variables are annotated with their types (x:T)
- Abstraction takes the form λx:T.M, where x is a variable of type T and M is a lambda term
- Application takes the form (M N), where M is a lambda term of function type T1 -> T2 and N is a lambda term of type T1
- The typing rules of the simply typed lambda calculus ensure that well-typed terms do not get stuck during evaluation
Typing Rules and Evaluation
- Typing judgment takes the form Γ ⊢ M : T, where Γ is a typing context (a set of variable-type pairs), M is a lambda term, and T is the type of M
- Typing rule for variables: if x:T is in the typing context Γ, then Γ ⊢ x : T
- Typing rule for abstraction: if Γ, x:T1 ⊢ M : T2, then Γ ⊢ λx:T1.M : T1 -> T2
- Typing rule for application: if Γ ⊢ M : T1 -> T2 and Γ ⊢ N : T1, then Γ ⊢ (M N) : T2
- Evaluation of well-typed lambda terms uses the beta-reduction rule: (λx:T.M) N → M[x := N], where M[x := N] denotes the substitution of N for x in M
- The simply typed lambda calculus satisfies the subject reduction property: if Γ ⊢ M : T and M → M', then Γ ⊢ M' : T
Well-Typed Lambda Terms
Constructing Well-Typed Terms
- To construct well-typed lambda terms, follow the typing rules of the simply typed lambda calculus
- Example of a well-typed lambda term: λx:Int.λy:Int.(x y) : Int -> (Int -> Int)
- Example of an ill-typed lambda term: λx:Int.(x true), as the argument true does not match the expected type Int
- Ensure that variable types match the types of their arguments in applications and abstractions
Evaluating Reductions
- Apply the beta-reduction rule to evaluate well-typed lambda terms: (λx:T.M) N → M[x := N]
- Example of beta-reduction: (λx:Int.λy:Int.(+ x y)) 3 5 → (λy:Int.(+ 3 y)) 5 → (+ 3 5) → 8
- The subject reduction property ensures that the resulting term after reduction maintains the same type as the original term
- Reduction order does not affect the final result, as the simply typed lambda calculus is confluent
Strong Normalization Property
Logical Relations Method
- The strong normalization property states that every well-typed lambda term in the simply typed lambda calculus terminates, reducing to a normal form in a finite number of steps
- The logical relations method defines a family of relations R_T between lambda terms and values of type T
- Base case: if v is a value of base type, then (v, v) ∈ R_T
- Inductive case: if for all (N, w) ∈ R_T1, (M N, v w) ∈ R_T2, then (M, v) ∈ R_{T1 -> T2}
- If (M, v) ∈ R_T, then M reduces to v in a finite number of steps, proving strong normalization
Reducibility Method
- The reducibility method assigns a reducibility predicate to each type, such that every well-typed lambda term satisfies its corresponding reducibility predicate
- Reducibility predicate for base types: a lambda term of base type is reducible if it is in normal form
- Reducibility predicate for function types: a lambda term of type T1 -> T2 is reducible if, when applied to any reducible lambda term of type T1, it yields a reducible lambda term of type T2
- By proving that every well-typed lambda term satisfies its reducibility predicate, the reducibility method demonstrates strong normalization
- Both the logical relations and reducibility methods can be used to prove strong normalization in the simply typed lambda calculus