Hermes Agent
6e2914b06e
Converted with pandoc 3.7 (markdown → org), all 17 files: - README, references, 15 tutorial units - Internal file links updated from .md to .org - Source code blocks (#+begin_src lean) preserved - Tables, math notation, links intact For the Emacs workflow.
96 lines
3.3 KiB
Org Mode
96 lines
3.3 KiB
Org Mode
* Unit 15 --- Soundness and Completeness of Algorithm W
|
||
:PROPERTIES:
|
||
:CUSTOM_ID: unit-15-soundness-and-completeness-of-algorithm-w
|
||
:END:
|
||
*Tutorial 2: PL Semantics in Lean* · [[../README.org][← Back to README]]
|
||
|
||
** Goals
|
||
:PROPERTIES:
|
||
:CUSTOM_ID: goals
|
||
:END:
|
||
- Prove that Algorithm W is *sound*: every inferred type is derivable in the declarative system
|
||
- Prove that Algorithm W is *complete*: every derivable type can be inferred (up to generalization)
|
||
- Understand the relationship between inference and declarative rules
|
||
|
||
** Sources
|
||
:PROPERTIES:
|
||
:CUSTOM_ID: sources
|
||
:END:
|
||
- [[https://www.jeffvaughan.net/docs/hmproof.pdf][Vaughan 2008, §4]]
|
||
- [[https://github.com/sdemos/type-inference][sdemos/type-inference]] =Soundness.lean=, =Completeness.lean=
|
||
|
||
** The Theorems
|
||
:PROPERTIES:
|
||
:CUSTOM_ID: the-theorems
|
||
:END:
|
||
*Soundness*: If =infer(Γ, e) = (S, τ)=, then =Γ ⊢ e : τ= declaratively.
|
||
|
||
*Completeness*: If =Γ ⊢ e : τ= declaratively, then there exists =S, τ'= such that
|
||
=infer(Γ, e) = (S, τ')= and =τ= is a substitution instance of =τ'= (i.e., W finds the /most general/ type).
|
||
|
||
** Exercises
|
||
:PROPERTIES:
|
||
:CUSTOM_ID: exercises
|
||
:END:
|
||
#+begin_src lean
|
||
open HMTyping
|
||
open MonoType
|
||
|
||
-- 15.1 — Soundness of Algorithm W
|
||
theorem soundness_W (Γ : HMEnv) (e : HMExpr) (S : Subst) (τ : MonoType) (counter : Nat)
|
||
(h : inferW Γ e counter = some (S, τ, _)) :
|
||
HMTyping (applySubstEnv S Γ) e {vars := [], body := τ} :=
|
||
by
|
||
induction e generalizing Γ S τ counter with
|
||
| var i =>
|
||
-- Case: variable lookup. Need to relate instantiated type scheme to declarative Var rule.
|
||
sorry
|
||
| lam body ih =>
|
||
-- Case: lambda. Use the IH and the Abs rule.
|
||
sorry
|
||
| app f a ihf iha =>
|
||
-- Case: application. The unification produces a substitution that makes types match.
|
||
-- Need substitution composition lemmas.
|
||
sorry
|
||
| lett e₁ e₂ ih₁ ih₂ =>
|
||
-- Case: let. Generalization produces a type scheme; the body gets the polymorphic type.
|
||
sorry
|
||
|
||
-- 15.2 — Completeness of Algorithm W
|
||
theorem completeness_W (Γ : HMEnv) (e : HMExpr) (σ : TypeScheme)
|
||
(h : HMTyping Γ e σ) :
|
||
∃ (S : Subst) (τ : MonoType) (counter : Nat),
|
||
inferW Γ e 0 = some (S, τ, counter) ∧
|
||
∃ (S' : Subst), applySubst S' τ = σ.body :=
|
||
by
|
||
induction h with
|
||
| var Γ i hlook =>
|
||
sorry
|
||
| abs Γ e τ₁ τ₂ hbody ih =>
|
||
sorry
|
||
| app Γ e₁ e₂ σ τ₁ τ₂ σ' h₁ h₂ h_eq ih₁ ih₂ =>
|
||
sorry
|
||
| lett Γ e₁ e₂ σ σ' τ h₁ h₂ ih₁ ih₂ =>
|
||
sorry
|
||
| gen Γ e σ αs hbody hfresh ih =>
|
||
sorry
|
||
| inst Γ e σ τ subst hbody hinst ih =>
|
||
sorry
|
||
|
||
-- 15.3 — Principal Types Corollary
|
||
-- Every well-typed expression has a *principal type* — one that all others are instances of.
|
||
theorem principal_types (Γ : HMEnv) (e : HMExpr) (σ : TypeScheme)
|
||
(h : HMTyping Γ e σ) :
|
||
∃ (τ_principal : MonoType),
|
||
-- W finds the principal type
|
||
(∃ S c, inferW Γ e 0 = some (S, τ_principal, c)) ∧
|
||
-- σ's body is an instance of the principal type
|
||
(∃ S', applySubst S' τ_principal = σ.body) :=
|
||
by
|
||
exact completeness_W Γ e σ h
|
||
#+end_src
|
||
|
||
--------------
|
||
|
||
← [[file:14-algorithm-w.org][Previous: Unit 14]] · [[file:.][← Tutorial 2 Index]] · [[../README.org][← Back to README]]
|