Soundness and completeness A sound type system never accepts a program that can go wrong ·No false negatives The language is type-safe A complete type system never rejects a program that can't go wrong ·No false positives However,for any Turing-complete PL,the set of programs that may go wrong is undecidable Type system cannot be sound and complete Choose soundness,try to reduce false positives in practice
Soundness and completeness • A sound type system never accepts a program that can go wrong • No false negatives • The language is type-safe • A complete type system never rejects a program that can’t go wrong • No false positives • However, for any Turing-complete PL, the set of programs that may go wrong is undecidable • Type system cannot be sound and complete • Choose soundness, try to reduce false positives in practice
Soundness-well-typed terms in STLC never go wrong Theorem(Type Safety): If.M:t and M→*M',then .kM':t,and either M'∈Values or 3M'".M'→M'" Defined in language semantics (e.g.A-abstraction,constants) That is,the reduction of a well-typed term either diverges,or terminates in a value of the expected type. Follows from two key lemmas(next page)
Soundness – well-typed terms in STLC never go wrong Theorem (Type Safety): That is, the reduction of a well-typed term either diverges, or terminates in a value of the expected type. Follows from two key lemmas (next page). If ⋅ ⊢ 𝑀: 𝜏 and 𝑀 →∗ 𝑀′ , then Defined in language semantics (e.g. -abstraction, constants) ⋅ ⊢ 𝑀′ : 𝜏, and either 𝑀′ ∈ Values or ∃𝑀′′. 𝑀′ → 𝑀′′
Soundness-well-typed terms in STLC never go wrong Preservation (subject reduction):well-typed terms reduce only to well-typed terms of the same type If·kM:t and M→M',then·kM':t Progress:a well-typed term is either a value or can be reduced If·kM:t,then either M∈Values or]M'.M→M
Soundness – well-typed terms in STLC never go wrong • Preservation (subject reduction): well-typed terms reduce only to well-typed terms of the same type • Progress: a well-typed term is either a value or can be reduced If ⋅ ⊢ 𝑀: 𝜏 and 𝑀 → 𝑀′ , then ⋅ ⊢ 𝑀′ : 𝜏 If ⋅ ⊢ 𝑀: 𝜏, then either 𝑀 ∈ Values or ∃𝑀′ . 𝑀 → 𝑀′
Not complete -the type system may reject terms that do not go wrong ·(x.(x(2y.y)(x3)(2z.z Cannot find o,t such that x:0上（x(2y.y))(x3):t because we have to pick one type for x ·But(x.(x(y.y》(x3)》(2z.z →(2z.z)(y.y)(2z.z3) →(y.yW3→3
Not complete – the type system may reject terms that do not go wrong • (x. (x (y. y)) (x 3)) (z. z) Cannot find , such that because we have to pick one type for x • But 𝑥: σ ⊢ 𝑥 𝜆𝑦. 𝑦 𝑥 3 ∶ τ (x. (x (y. y)) (x 3)) (z. z) → ((z. z) (y. y)) ((z. z) 3) → (y. y) 3 → 3
Well-typed terms in STLC always terminate (strong normalization theorem) Recall (Ax.xx)(7x.x x) →(2x.xx)(2x.xx) →… .(x.xx)(7x.x x)cannot be assigned a type Expect o to be in the form of o->, which is impossible! x:0上x:? x:0上x:o x:0上XX:?
Well-typed terms in STLC always terminate (strong normalization theorem) • Recall • (x. x x) (x. x x) cannot be assigned a type (x. x x) (x. x x) → (x. x x) (x. x x) → … 𝑥: σ ⊢ 𝑥 𝑥 ∶ ? 𝑥: σ ⊢ 𝑥: ? 𝑥: σ ⊢ 𝑥: σ Expect to be in the form of → , which is impossible!