Typing judgment M is of type t in contextI T上M:T Typing context(a set of typing assumptions) T=·|,x:t Include types of all the free variables in M(each free variable x is of type t) 。Empty context·is for closed terms Under l,M is a well-typed term of type t
Typing judgment • Typing context (a set of typing assumptions) • Include types of all the free variables in M (each free variable 𝑥 is of type τ) • Empty context ∙ is for closed terms • Under , M is a well-typed term of type Γ ⊢ M ∶ τ Γ ∷= ∙ | Γ, 𝑥: τ M is of type in context
Typing rules 一 (var) D,X:T上X: T上M:O→t T上N:o (app) T上MN:t T,x:O上M:t -(abs) T上(Ox:0.M):0→
Typing rules Γ, 𝑥 ∶ τ ⊢ 𝑥 ∶ τ Γ ⊢ 𝑀 ∶ 𝜎 → 𝜏 Γ ⊢ 𝑁 ∶ 𝜎 Γ ⊢ 𝑀 𝑁 ∶ τ Γ, 𝑥 ∶ 𝜎 ⊢ 𝑀 ∶ 𝜏 Γ ⊢ λ𝑥: 𝜎. 𝑀 ∶ 𝜎 → τ (var) (app) (abs)
Typing derivation (var) ,x:T上X:T examples r上M:o→t THN:o THMN:t (app) T,x:o上M:T-(abs) T上(x:o.M):o→t (var) X:T上X:T (abs) ·上x:.x):T→T
Typing derivation examples ⋅ ⊢ λ𝑥: τ. 𝑥 ∶ τ → τ 𝑥: τ ⊢ 𝑥: τ (var) (abs) Γ, 𝑥 ∶ τ ⊢ 𝑥 ∶ τ (var) Γ ⊢ 𝑀 ∶ 𝜎 → 𝜏 Γ ⊢ 𝑁 ∶ 𝜎 Γ ⊢ 𝑀 𝑁 ∶ τ (app) Γ, 𝑥 ∶ 𝜎 ⊢ 𝑀 ∶ 𝜏 Γ ⊢ λ𝑥: 𝜎. 𝑀 ∶ 𝜎 → τ (abs)
Typing derivation (var) T,x:THx:T examples rkM:g→T THN: T上MN:T _(app) T,x:o卜M：t一(abs) Tk(x:o.M):o→T (var) x:T,y:0卜x:t (abs) x:t上(y:o.x):0→t (abs) ·上x:t.y:0.x):T→0→T
Typing derivation examples ⋅ ⊢ λ𝑥: τ. λ𝑦: σ. 𝑥 ∶ τ → σ → τ 𝑥: τ ⊢ λ𝑦: σ. 𝑥 ∶ σ → τ (var) (abs) 𝑥: τ, 𝑦: σ ⊢ 𝑥 ∶ 𝜏 (abs) Γ, 𝑥 ∶ τ ⊢ 𝑥 ∶ τ (var) Γ ⊢ 𝑀 ∶ 𝜎 → 𝜏 Γ ⊢ 𝑁 ∶ 𝜎 Γ ⊢ 𝑀 𝑁 ∶ τ (app) Γ, 𝑥 ∶ 𝜎 ⊢ 𝑀 ∶ 𝜏 Γ ⊢ λ𝑥: 𝜎. 𝑀 ∶ 𝜎 → τ (abs)
Typing derivation (var) ,x:T上x:T examples r上M:oT THN:G THMN:t (app) I,x:M:t (abs) T上(x:o.M):o→T (var) (var) x:T→T,y:T卜X:T→T x:T→t,y:TFy:T (app) x:T→t,y:T上xy:t (abs) x:T→T上(Oy:t.xy):T→T (abs) ·上(x:T→t.λy:T.xy):(t→)→T→t
Typing derivation examples Γ, 𝑥 ∶ τ ⊢ 𝑥 ∶ τ (var) Γ ⊢ 𝑀 ∶ 𝜎 → 𝜏 Γ ⊢ 𝑁 ∶ 𝜎 Γ ⊢ 𝑀 𝑁 ∶ τ (app) Γ, 𝑥 ∶ 𝜎 ⊢ 𝑀 ∶ 𝜏 Γ ⊢ λ𝑥: 𝜎. 𝑀 ∶ 𝜎 → τ (abs) ⋅ ⊢ λ𝑥: τ → τ. λ𝑦: τ. 𝑥 𝑦 ∶ (τ → τ) → τ → τ 𝑥: τ → τ ⊢ λ𝑦: τ. 𝑥 𝑦 ∶ τ → τ (var) (abs) (abs) 𝑥: τ → τ, 𝑦: τ ⊢ 𝑥 𝑦 ∶ τ (app) 𝑥: τ → τ, 𝑦: τ ⊢ 𝑥: τ → τ 𝑥: τ → τ, 𝑦: τ ⊢ 𝑦: τ (var)