commit 7c971a7989d6f96ca42bf2b09ae11ae03a26f69d Author: Jonathan Chan Date: Thu Mar 20 10:42:00 2025 -0400 Initial commit (up to Homework 7) diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..d163863 --- /dev/null +++ b/.gitignore @@ -0,0 +1 @@ +build/ \ No newline at end of file diff --git a/Homework 1.md b/Homework 1.md new file mode 100644 index 0000000..bf74b40 --- /dev/null +++ b/Homework 1.md @@ -0,0 +1,31 @@ +Here's my formal definition of substitution. Since I wasn't in class last week, I'm not sure what notational conventions are being used, so I'll define my grammar first. + +```ebnf +n, m :: Nat +a, b, c :: Term ::= n | λ b | b a +r :: Nat -> Nat +``` + +I'm using simultaneous renamings r mapping from indices to indices. Lifting a renaming means weakening by 1, so the new mapping refers to the previous entry in the old mapping, and increments what it maps to, defined below. + +```haskell +lift :: (Nat → Nat) → Nat → Nat +lift r n = if n == 0 then 0 else (r (n - 1)) + 1 +``` + +Applying a renaming requires lifting it when going under a binder. + +```haskell +rename :: (Nat → Nat) → Term → Term +rename r n = r n +rename r (b a) = (rename r b) (rename r a) +rename r (λ b) = λ (rename (lift r) b) +``` + +I denote substitution as `b{c/n}`, replacing the index `n` by `c` inside of `b`. Renaming by incrementing `1` is used when going under a binder so that the `c`'s zeroth indices don't get captured. + +```haskell +n{c/m} = if n == m then c else n +(b a){c/m} = b{c/m} a{c/m} +(λ b){c/m} = let c' = rename (+ 1) c in λ (b{c'/m}) +``` \ No newline at end of file diff --git a/Homework 2.md b/Homework 2.md new file mode 100644 index 0000000..bebd33a --- /dev/null +++ b/Homework 2.md @@ -0,0 +1,67 @@ +**N.B.** The definition of multistep reduction I use is composed of a reflexive case (`t →* t`) and a transitive case (`t₁ → t₂ →* t₃`). I need the following two lemmas throughout. + +**Lemma** (transitivity): If `t₁ →* t₂ →* t₃` then `t₁ →* t₃`. +**Proof**: By induction on `t₁ →* t₂`. The reflexive case is trivial and the transitive case uses the induction hypothesis to combine the two multistep reductions. + +**Lemma** (congruence): Multistep reduction is congruent in head positions, i.e. if `t₁ →* t₁'` then `if t₁ then t₂ else t₃ →* if t₁' then t₂ else t₃`, and similarly for `succ`, `pred`, and `iszero`. +**Proof**: If the reduction is reflexive, then the proof is trivial. Otherwise, the reduction is of the form `t₁ → t₁' →* t₁''`. By `E-If` (likewise `E-Succ`, `E-Pred`, `E-Iszero`), we have `if t₁ then t₂ else t₃ → if t₁' then t₂ else t₃`. By the induction hypothesis, we have `if t₁' then t₂ else t₃ →* if t₁'' then t₂ else t₃` (likewise for`succ`, `pred`, `iszero`). We have our goal by combining the two by transitivity. + +---- + +**Exercise 3.5.16**: The two treatments of run-time errors agree if the following hold: +1. If `t` evaluates to a stuck state (using the rules without `E-*-Wrong`), then it evaluates to `wrong` (using the rules with `E-*-Wrong`). More precisely, if `t →* t' ↛` and `t ≠ v`, then `t →* wrong`. +2. If `t` evaluates to `wrong` and does not contain `wrong` as a subterm, then `t` evaluates to a stuck state. This is the converse of the first statement, except we exclude cases where `t` was wrong to begin with. + +**Lemma 0**: If `t ↛` (using the rules without `E-*-Wrong`) and `t ≠ v` then `t → wrong` (using the rules with `E-*-Wrong`). +**Proof**: By induction on the shape of `t`. The cases where `t` is `true`, `false`, `0`, or `succ nv` are impossible. +* Case `t = if t₁ then t₂ else t₃`: The term does not step by `E-IfTrue`, `E-IfFalse`, nor `E-If`, so `t₁` is not `true` nor `false`, and does not step. If `t₁` is a value, then it is either a numeric value `nv`; otherwise, if it is not a value, then by the induction hypothesis, it steps to `wrong`. In both cases, `t₁` is a `badbool`, so the whole expression steps to `wrong` by `E-If-Wrong`. +* Case `t = succ t₁` where `t₁ ≠ nv`: The term does not step by `E-Succ`, so `t₁` does not step. If `t₁` is a value, then it must be `true` or `false`; otherwise, if it is not a value, then by the induction hypothesis, it steps to `wrong`. In both cases, `t₁` is a `badnat`, so the whole expression steps to `wrong` by `E-Succ-Wrong`. +* Case `t = pred t₁`: The term does not step by `E-PredZero`, `E-PredSucc`, nor `E-Pred`, so `t₁ ≠ nv` and does not step. Then the argument for the previous case follows, using instead `E-Pred-Wrong`. +* Case `t = iszero t₁`: The argument for the previous case follows, noting that the term does not step by `E-IszeroZero`, `E-IszeroSucc`, nor `E-Iszero`, and using `E-Iszero-Wrong` to step. + +**Lemma 1**: If `t → t'` (using the rules with `E-*-Wrong`) and `t'` contains a `wrong` subterm, then either `t` contains a `wrong` subterm, or `t ↛` (using the rules without `E-*-Wrong`) and `t ≠ v`. +**Proof**: By induction on `t → t'`. +* Cases `E-If-True`, `E-If-False`: The reduction is `if true then t₁ else t₂ → t₁` or `if false then t₁ else t₂ → t₂`. If the RHS contains a `wrong` subterm, then evidently the LHS does as well. +* Cases `E-If`, `E-Pred`, `E-Iszero`: The three cases are similar; I use `E-Iszero` as representative. The reduction is `iszero t₁ → iszero t₂`, where `t₁ → t₂`, and `t₂` must contain a `wrong` subterm. By the induction hypothesis, either `t₁` contains a `wrong` subterm, in which case so does `iszero t₁`, or `t₁ ↛` and `t₁ ≠ v`. In this latter case, we have `iszero t₁ ↛`, since none of `E-Iszero-Zero`, `E-Iszero-Succ`, and `E-Iszero` apply, and `iszero t₁` is obviously not a value. +* Case `E-Succ`: The reduction is `succ t₁ → succ t₂`, where `t₁ → t₂`, and `t₂` must contain a `wrong` subterm. By the induction hypothesis, either `t₁` contains a wrong subterm, in which case so does `succ t₁`, or `t₁ ↛` and `t₁ ≠ v`. In this latter case, we have `succ t₁ ↛` since `E-Succ` does not apply, and we know that `succ t₁` is not a value since `t₁` is not a value. + +**Lemma 2**: If `t →* wrong` (using the rules with `E-*-Wrong`), then either `t` contains a `wrong` subterm, or `t →* t' ↛` (using the rules without `E-*-Wrong`) and `t' ≠ v`. +**Proof**: By induction on `t →* wrong`. The reflexive case `wrong →* wrong` is trivial. In the transitive case `t → t' →* wrong`, by the induction hypothesis, either `t'` contains a `wrong` subterm, or `t' →* t'' ↛` and `t'' ≠ v`. In the former case, we use Lemma 1 on the reduction `t → t'`. In the latter case, we have `t → t' →* t'' ↛` and `t'' ≠ v` as required. + +**Proof of 3.5.16** (Condition 1): Suppose `t →* t' ↛` and `t' ≠ v`. Then `t' → wrong` by Lemma 0, and `t →* wrong` by transitivity. +**Proof of 3.5.16** (Condition 2): Suppose `t →* wrong` and `t` does not contain a `wrong` subterm. Then by Lemma 2, it must be that `t →* t' ↛` and `t' ≠ v`. + +---- + +**Exercise 3.5.17**: `t →* v` iff `t ⇓ v`. + +**Lemma 3**: If `t₁ → t₂` and `t₂ ⇓ v`, then `t₁ ⇓ v`. +**Proof**: By induction on `t₁ → t₂`. +* Case `E-IfTrue`: The reduction is `if true then t₄ else t₅ → t₂`, with `t₂ ⇓ v`. By `B-Value`, `true ⇓ true`. Then by `B-IfTrue`, we construct `if true then t₄ else t₅ ⇓ v`. +* Case `E-IfFalse`: Similar as above, but using `B-IfFalse`. +* Case `E-If`: The reduction is `if t₃ then t₄ else t₅ → if t₃' then t₄ else t₅`, where `t₃ → t₃'`, with `if t₃' then t₄ else t₅ ⇓ v`. By inversion on the latter, the only possible cases are `B-IfTrue` and `B-IfFalse`. + * Subcase `B-IfTrue`: We have `t₃' ⇓ true` and `t₄ ⇓ v`. By the induction hypothesis, we have `t₃ ⇓ true`. Then by `B-IfTrue`, we construct `if t₃ then t₄ else t₄ ⇓ true`. + * Subcase `B-IfFalse`: Similar as above, but the induction hypothesis gives `t₃ ⇓ false`, and we use `B-IfFalse` instead. +* Case `E-Succ`: The reduction is `succ t₁ → succ t₂`, where `t₁ → t₂`, with `succ t₂ ⇓ v`. By inversion on the latter, the only possible case is `B-Succ`, with `t₂ ⇓ v`. By the induction hypothesis, we have `t₁ ⇓ v`. Then by `B-Succ`, we construct `succ t₁ ⇓ v`. +* Case `E-PredZero`: The reduction is `pred 0 → 0`, with `0 ⇓ v`. By inversion on the latter, the only possible case is `B-Value`, with `v = 0`. The goal `pred 0 ⇓ 0` holds directly by `B-PredZero`. +* Case `E-PredSucc`: The reduction is `pred (succ nv) → nv`, with `nv ⇓ v`. By inversion on the latter, the only possible case is `B-Value`, with `v = nv`. The goal `pred (succ nv) ⇓ nv` holds directly by `B-PredSucc`, whose premise `succ nv ⇓ succ nv` holds by `B-succ`, whose premise `nv ⇓ nv` holds by `B-Value`. +* Case `E-Pred`: The reduction is `pred t₁ → pred t₂`, where `t₁ → t₂`, with `pred t₂ ⇓ v`. By inversion on the latter, the only possible cases are `B-PredZero` and `B-PredSucc`. + * Subcase `B-PredZero`: We have `pred t₂ ⇓ 0`, where `t₂ ⇓ 0`. By the induction hypothesis, we have `t₁ ⇓ 0`. Then by `B-PredZero`, we construct `pred t₁ ⇓ 0`. + * Subcase `B-PredSucc`: We have `pred t₂ ⇓ nv`, where `t₂ ⇓ succ nv`. By the induction hypothesis, we have `t₁ ⇓ succ nv`. Then by `B-PredSucc`, we construct `pred t₁ ⇓ nv`. +* Case `E-IszeroZero`: The reduction is `iszero 0 → true`, with `true ⇓ v`. By inversion on the latter, the only possible case is `B-Value`, with `v = true`. The goal `iszero 0 ⇓ true` holds directly by `B-IszeroZero`, whose premise `0 ⇓ 0` holds by `B-Value`. +* Case `E-IszeroSucc`: The reduction is `iszero (succ nv) → false`, with `false ⇓ v`. By inversion on the latter, the only possible case is `B-Value`, with `v = false`. The goal `iszero (succ nv) ⇓ false` holds directly by `B-IszeroSucc`, whose premise `succ nv ⇓ succ nv` holds by `B-Succ`, whose premise `nv ⇓ nv` holds by `B-Value`. +* Case `E-Iszero`: The reduction is `iszero t₁ → iszero t₂`, where `t₁ → t₂`, with `iszero t₂ ⇓ v`. By inversion on the latter, the only possible cases are `B-IszeroZero` and `B-IszeroSucc`. + * Subcase `B-IszeroZero`: We have `iszero t₂ ⇓ true`, where `t₂ ⇓ 0`. By the induction hypothesis, we have `t₁ ⇓ 0`. Then by `B-IszeroZero`, we construct `iszero t₁ ⇓ true`. + * Subcase `B-IszeroSucc`: We have `iszero t₂ ⇓ false`, where `t₂ ⇓ succ nv`. By the induction hypothesis, we have `t₁ ⇓ succ nv`. Then by `B-IszeroSucc`, we construct `iszero t₁ ⇓ false`. + +**Proof of 3.5.17** (LtR direction): By induction on `t →* v`. In the reflexive case, we have `v → v`, and `v ⇓ v` holds by `B-Value`. In the transitive case, we have `t₁ → t₂ →* v`. By the induction hypothesis, we have `t₂ ⇓ v`. Then by Lemma 3, we have `t₁ ⇓ v`. + +**Proof of 3.5.17** (RtL direction): By induction on `t ⇓ v`. I freely use the transitivity and congruence lemmata to combine multistep reductions. +* Case `B-Value`: By reflexivity. +* Case `B-IfTrue`: The evaluation is `if t₁ then t₂ else t₃ ⇓ v`, where `t₁ ⇓ true` and `t₂ ⇓ v`. By the induction hypothesis, we have `t₁ →* true` and `t₂ →* v`. Then we have `if t₁ then t₂ else →* if true then t₂ else t₃ →* t₂ →* v`, the middle step by `E-IfTrue`. +* Case `B-IfFalse`: Similar as above, but using `E-IfFalse`. +* Case `B-Succ`: The evaluation is `succ t ⇓ succ v`, where `t ⇓ v`. By the induction hypothesis, we have `t →* v`. Then we have `succ t →* succ v` by congruence. +* Case `B-PredZero`: The evaluation is `pred t ⇓ 0`, where `t ⇓ 0`. By the induction hypothesis, we have `t →* 0`. Then we have `pred t →* pred 0 →* 0`, the last step by `E-PredZero`. +* Case `B-PredSucc`: The evaluation is `pred t ⇓ nv`, where `t ⇓ succ nv`. By the induction hypothesis, we have `t →* succ nv`. Then we have `pred t →* pred (succ nv) →* nv`, the last step by `E-PredSucc`. +* Case `B-IszeroZero`: The evaluation is `iszero t ⇓ true`, where `t ⇓ 0`. By the induction hypothesis, we have `t →* 0`. Then we have `iszero t →* iszero 0 →* true`, the last step by `E-IszeroZero`. +* Case `B-IszeroSucc`: The evaluation is `iszero t ⇓ false`, where `t ⇓ succ nv`. By the induction hypothesis, we have `t →* succ nv`. Then we have `iszero t →* iszero (succ nv) →* false`, the last step by `E-IszeroSucc`. \ No newline at end of file diff --git a/Homework 3.md b/Homework 3.md new file mode 100644 index 0000000..b666ece --- /dev/null +++ b/Homework 3.md @@ -0,0 +1,40 @@ +**Definition** (negative formulation of hereditary termination): +* 🆕 HT{T₁ × T₂}(M) ≝ HT{T₁}(M.1) ∧ HT{T₂}(M.2) +* 🆕 HT{T₁ → T₂}(M) ≝ ∀M₁, HT{T₁}(M₁) ⊃ HT{T₂}(M M₁) +* HT{1}(M) ≝ M →* ⟨⟩ +* HT{Ans}(M) ≝ M →* yes ∨ M →* no + +**Lemma** (head expansion): If M' → M and HT{A}(M) then HT{A}(M'). + +**Theorem** (fundamental): If Γ ⊢ M : A then Γ ≫ M ∈ A. +**Proof**: By induction on the typing derivation. Assume γ and HT{Γ}(γ); the goal is to show HT{A}(γ̂(M)). +* Case Lam: The premise is Γ, x : A₁ ⊢ M₂ : A₂, with conclusion Γ ⊢ λx. M₂ : A₁ → A₂. + Assuming M₁ and HT{A₁}(M₁), the goal is to show HT{A₂}((λx. γ̂(M₂)) M₁). + Using the assumptions, we have HT{Γ, x : A₁}(γ, x ↦ M₁), + which we apply to the induction hypothesis on the premise to get HT{A₂}(γ̂(M₂)[x ↦ M₁]). + By head expansion on (λx. γ̂(M₂)) M₁ → γ̂(M₂)[x ↦ M₁], we obtain our goal. +* Case App: The premises are Γ ⊢ M : A₁ → A₂ and Γ ⊢ M₁ : A₁, with conclusion is Γ ⊢ M M₁ : A₂; the goal is to show HT{A₂}(γ̂(M) γ̂(M₁)). + By the induction hypothesis on the first premise specialized to γ̂(M₁), + we have that HT{T₁}(γ̂(M₁)) implies HT{T₂}(γ̂(M) γ̂(M₁)), our goal. + It suffices to show the antecedent, which holds by the induction hypothesis on the second premise. +* Case Pair: The premises are Γ ⊢ M₁ : A₁ and Γ ⊢ M₂ : A₂, with conclusion Γ ⊢ ⟨M₁, M₂⟩ : A₁ × A₂. + The goal is to show HT{A₁}(⟨γ̂(M₁), γ̂(M₂)⟩.1) and HT{A₂}(⟨γ̂(M₁), γ̂(M₂)⟩.2). + By the induction hypotheses on the two premises, we have HT{A₁}(γ̂(M₁)) and HT{A₂}(γ̂(M₂)). + By head expansion on ⟨γ̂(M₁), γ̂(M₂)⟩.i → γ̂(Mᵢ), we have our goal. +* Case Left/Right: The premise is Γ ⊢ M : A₁ × A₂, and the conclusion is Γ ⊢ M.i : Aᵢ. + The goal is to show HT{Aᵢ}(γ̂(M).i). + By the induction hypothesis on the premise, we have HT{Aᵢ}(γ̂(M).i) as needed. +* Cases Var, Yes, No, Unit: Unchanged. + +---- + +**Lemma**: If M₁ and M₂[x ↦ M₁] are strongly normalizing, then M₂ is strongly normalizing. +**Proof**: By induction on M₂. In the variable case for x, we use strong normalization of M₂. + +**Claim**: The largest saturated set is SN itself. Obviously there is no larger set, since all saturated sets are subsets of SN. To check saturation: +* If N... ∈ SN then x N... ∈ SN: By congruence of application, the only possible reduction paths are through reduction of N..., which are strongly normalizing. +* If M₁, N... ∈ SN and M₂[x ↦ M₁] N... ∈ SN then (λx. M₂) M₁ N... ∈ SN: The possible reduction paths are by congruence through M₁, M₂, or N..., or by β-reduction of the head redex. + * β-reduction: (λx. M₂) M₁ N... → M₂[x ↦ M₁] N..., which was assumed to be strongly normalizing. + * Congruence (M₁ and N...): They were assumed to be strongly normalizing. + * Congruence (M₂): By assumption, M₂[x ↦ M₁] N... is strongly normalizing, so M₂[x ↦ M₁] must be strongly normalizing.† Then by the above lemma, M₂ is strongly normalizing. + † I'm fairly certain this is true, but I'm now doubting that it's simple to prove rigorously... \ No newline at end of file diff --git a/Homework 4.md b/Homework 4.md new file mode 100644 index 0000000..e5eb1a9 --- /dev/null +++ b/Homework 4.md @@ -0,0 +1,136 @@ +**Exercise 13.3.1**: I don't think you could model automatic garbage collection using single step semantics, given that it has no information about the outer evaluation context and whether a label will be used or not. We could write single step evaluation with an explicit context like this: + +``` +E ⩴ _ | t E | E v | !E | E := t | v := E | ref E + +t | μ → t' | μ' +--------------------- +E[t] | μ → E[t'] | μ' +``` + +and analyse for labels in `E`, but I think it would be cleaner to instead have an explicit freeing operator and error value: + +``` +t ⩴ ... | free t | error + +┌───────────────┐ +│ t | μ → t | μ │ +└───────────────┘ + +t | μ → t' | μ' +------------------------- +free t | μ → free t' | μ' + +-------------------------------- +free l | μ → unit | μ[l ↦ error] + +----------------------- +error t | μ → error | μ + +----------------------- +v error | μ → error | μ + +------------------------- +ref error | μ → error | μ + +---------------------- +!error | μ → error | μ + +-------------------------- +error := t | μ → error | μ + +-------------------------- +v := error | μ → error | μ + +┌───────────────┐ +│ Γ | Σ ⊢ t : T │ +└───────────────┘ + +Γ | Σ ⊢ t : Ref T +--------------------- +Γ | Σ ⊢ free t : Unit + +----------------- +Γ | Σ ⊢ error : T +``` + +`free`ing updates the store with an `error` value , so the store still never shrinks. `error`s propagate upward, so if it's encountered anywhere inside a computation, the entire computation `error`s. The preservation theorem remains the same, but the progress theorem now says that either a well typed term evaluates to a value or it evaluates to `error` (if you don't consider `error` to be a value). + +Unfortunately, the type system isn't strong enough to rule out usage after free (i.e. if a term is well typed then it never errors), and I'm not sure whether it would be possible to design a type system that does. Originally, I was thinking you could remove locations from the store typing, but then it's unclear which location should be removed when typing `free`, and even more unclear how to fix the preservation theorem. + +_Theorem_ (preservation): If `Γ | Σ ⊢ μ`, `Γ | Σ ⊢ t : T`, `t | μ → t' | μ'`, then there exists `Σ'` such that `Γ | Σ' ⊢ μ'`, `Γ | Σ' ⊢ t' : T`, and `Σ ??? Σ'`. + +We would want to allow, for instance, `t₁ := free (ref t₂)` where `t₁ ≠ t₂`, but not `t₁ := free t₁`, nor `(free t₁; t₁) := t₂`. All of these would shrink the store typing in some way, but it doesn't seem like there would be a way to combine the store typings from the two premises of typing assignment in a way that rules out the last two but not the first. + +---- + +**Exercise 13.5.8**: First, suppose we had a sequencing operation `t₁; t₂`, which could be primitive, or just sugar for `(λ_. t₂) t₁` in our CBV language. Assuming the typing rules for the booleans and natural numbers from Chapter 8, as well as a `mult`iplication function, here is a factorial function: + +``` +(λn: Nat. + (λf: Ref (Nat → Nat). + λg: Ref (Nat → Nat). + f := λx: Nat. + if (iszero x) + then (succ 0) + else (mult x (!g (pred x))); + g := !f; + !g n) + (ref (λx: Nat. x)) + (ref (λx: Nat. x))) +``` + +Given some concrete `n`, after evaluating the two initial references, this steps to the following: + +``` +lf ↦ λx: Nat. x +lg ↦ λx: Nat. x + +lf := λx: Nat. + if (iszero x) + then (succ 0) + else (mult x (!lg (pred x))); +lg := !lf; +!lg n +``` + +After one step, we update `lf`: + +``` +lf ↦ λx: Nat. + if (iszero x) + then (succ 0) + else (mult x (!lg (pred x))) +lg ↦ λx: Nat. x + +lg := !lf; +!lg n +``` + +After another step, we update `lg`: + +``` +lf ↦ λx: Nat. + if (iszero x) + then (succ 0) + else (mult x (!lg (pred x))) +lg ↦ λx: Nat. + if (iszero x) + then (succ 0) + else (mult x (!lg (pred x))) + +!lg n +``` + +Then finally yield the factorial function we expect (dropping `lf` now that we no longer need it): + +``` +lg ↦ λx: Nat. + if (iszero x) + then (succ 0) + else (mult x (!lg (pred x))) + +if (iszero n) +then (succ 0) +else (mult n (!lg (pred n))) +``` \ No newline at end of file diff --git a/Homework 5.md b/Homework 5.md new file mode 100644 index 0000000..127848a --- /dev/null +++ b/Homework 5.md @@ -0,0 +1,52 @@ +This lemma wasn't part of the exercises assigned but it's needed for the exercises and not proven in the book so I thought I'd sketch it out quickly. + +**Lemma 15.3.2** (Inversion of the subtype relation): +1. If `S <: T₁ → T₂`, then `S = S₁ → S₂` such that `T₁ <: S₁` and `S₂ <: T₂`. +2. If `S <: {lᵢ : Tᵢ}`, then `S = {kⱼ : Sⱼ}` such that `{lᵢ} ⊆ {kⱼ}` and `Sⱼ <: Tᵢ` when `lᵢ = kⱼ`. +**Proof**: +1. By induction on the subtyping derivation. The applicable cases are `S-Refl` (holds directly), `S-Trans` (holds by induction hypothesis twice), and `S-Arrow` (holds directly). +2. By induction on the subtyping derivation. The applicable cases are `S-Refl` (holds directly), `S-Trans` (holds by induction hypothesis twice, using `S-Trans` and transitivity of subsets of labels), `S-RcdWidth` (holds directly using `S-Refl` and `{l₁..lₙ} ⊆ {l₁..lₙ₊ₖ})`, `S-RcdDepth` (holds directly), and `S-RcdPerm` (holds by induction hypothesis). + +Here are the assigned exercises. + +**Lemma 15.3.6** (Canonical forms): +1. If `v` is a closed value of type `T₁ → T₂`, then `v` has the form `λx: S₁. t₂`. +2. If `v` is a closed value of type `{lᵢ : Tᵢ}`, then `v` has the form `{kⱼ = vⱼ}`, where `{lᵢ} ⊆ {kⱼ}`. +**Proof**: +1. By induction on the typing derivation of `Γ ⊢ v : T₁ → T₂`. The only applicable cases are `T-Abs` and `T-Sub`; the first case holds directly. In the second case, we have `Γ ⊢ v : S` and `S <: T₁ → T₂`. By inversion on subtyping (Lemma 15.3.2), `S = S₁ → S₂`. Then `v` has the form of a function by the induction hypothesis. +2. By induction on the typing derivation of `Γ ⊢ v : {lᵢ : Tᵢ}`. We proceed similarly to the above, where the applicable cases are `T-Rcd` and `T-Sub`, the first case holds directly, and the second case holds using inversion (Lemma 15.3.2) and the induction hypothesis. +The top-level lemmas hold by instantiating `Γ = ∅`. + +**Exercise 16.1.3**: If we add `Bool`, we also need to add the subtyping rule `Bool <: Bool` so that the judgement remains reflexive. + +**Theorem 16.2.5**: If `Γ ⊢ t : T`, then `Γ ⊢> t : S` and `⊢> S <: T`. +**Proof**: By induction on the typing derivation. +* Case `T-Var`: Holds by `TA-Var`. +* Case `T-Abs`: The premise is `Γ, x: T₁ ⊢ t₂ : T₂`, concluding with `Γ ⊢ λx: T₁. t₂ : T₁ → T₂`. By the induction hypothesis, we have `Γ, x: T₁ ⊢> t₂ : S₂` and `⊢> S₂ <: T₂`. By `TA-Abs`, we have `Γ ⊢> λx: T₁. t₂ : T₁ → S₂`, and by reflexivity and `SA-Arrow` we have `⊢> T₁ → S₂ <: T₁ → T₂`. +* Case `T-App`: The premises are `Γ ⊢ t₁ : T₁₁ → T₁₂` and `Γ ⊢ t₂ : T₁₁`, concluding with `Γ ⊢ t₁ t₂ : T₁₂`. By the induction hypothesis, we have `Γ ⊢> t₁ : S₁`, `⊢> S₁ <: T₁₁ → T₁₂` for the first premise and `Γ ⊢> t₂ : S₂`, `⊢> S₂ <: T₁₁` for the second. By inversion on subtyping, `S₁ = S₁₁ → S₁₂` , `⊢> T₁₁ <: S₁₁`, and `⊢> S₁₂ <: T₁₂`. By transitivity, `⊢> S₂ <: T₁₁ <: S₁₁`. Then we can use `TA-App` to build `Γ ⊢> t₁ t₂ : S₁₂`, with `⊢> S₁₂ <: T₁₂` as needed. +* Case `T-Rcd`: The premises are `Γ ⊢ tᵢ : Tᵢ`, concluding with `Γ ⊢ {lᵢ = tᵢ} : {lᵢ : Tᵢ}`. By the induction hypothesis, we have `Γ ⊢> tᵢ : Sᵢ` and `⊢> Sᵢ <: Tᵢ`. By `TA-Rcd`, we have `Γ ⊢> {lᵢ = tᵢ} : {lᵢ : Sᵢ}`, and by `SA-Rcd`, we have `⊢> {lᵢ : Sᵢ} <: {lᵢ : Tᵢ}`. +* Case `T-Proj`: The premise is `Γ ⊢ t : {lᵢ : Tᵢ}`, concluding with `Γ ⊢ t.lⱼ : Tⱼ`. By the induction hypothesis, we have `Γ ⊢> t : S` and `⊢> S <: {lᵢ : Tᵢ}`. By inversion on subtyping, `S = {kᵢ : Sᵢ}`, where `{lᵢ} ⊆ {kᵢ}` and `⊢> Sᵢ <: Tⱼ` when `lⱼ = kᵢ`. Letting `lⱼ = kᵢ`, we can use `TA-Proj` to build `Γ ⊢> t.lⱼ : Sᵢ`, with `⊢> Sᵢ <: Tⱼ`. +* Case `T-Sub`: The premises are `Γ ⊢ t : S` and `S <: T`, concluding with `Γ ⊢ t : T`. By the induction hypothesis, we have `Γ ⊢> t : U` and `⊢> U <: S`. By completeness (Proposition 16.1.5), we get `⊢> S <: T`. Then by transitivity, we get `⊢> U <: S <: T` as needed. + +**Exercise 16.2.6**: I think the system without `S-Arrow` would still have the minimal typing property. The proof would proceed exactly as in Theorem 16.2.5. Completeness (`S <: T` implies `⊢> S <: T`) still holds, since the induction would just be missing one case. + +**Lemma** (existence of a subtype): For every `S`, `T`, either there exists some `N` such that `N <: S` or `N <: T`, or no such `N` is possible. +**Proof**: By induction on the structure of `S` and `T`. If one of the types is `Top`, then the other type is a subtype of both by reflexivity and `S-Top`. If the types have different shapes (i.e. one is a function type, the other a record type), supposing we have a subtype `N`, by inversion on the subtyping derivations, `N` would have to be both a function type and a record type, which is a contradiction, so no such `N` exists. That leaves the cases where both types are function types or record types. +* Case `S₁ → S₂`, `T₁ → T₂`. By the induction hypothesis, either `S₂` and `T₂` have a subtype `N₂`, or no such subtype exists. If it exists, then `Top → N₂` is a subtype, since `S₁ <: Top`, `T₁ <: Top`, `N₂ <: S₂`, and `N₂ <: T₂`, and we construct `Top → N₂ <: S₁ → S₂` and `Top → N₂ <: T₁ → T₂` by `S-Arrow`. If it does not exist, then supposing we had a subtype `N₁ → N₂` of both `S₁ → S₂` and `T₁ → T₂`, by inversion, we have `N₂ <: S₂` and `N₂ <: T₂`, which is a contradiction, so there must be no such subtype. +* Case `{kᵢ : Sᵢ}`, `{lⱼ : Tⱼ}`. By the induction hypothesis, each pair `Sᵢ`, `Tᵢ` either have a subtype `Nᵢⱼ`, or no such subtype exists. Let `{klᵢⱼ} = {kᵢ} ∪ {lⱼ}`. + * If all `Sᵢ` and `Tⱼ` for which `kᵢ = lⱼ` have a subtype, then we claim the subtype is `{klᵢⱼ : Uᵢⱼ}` such that `Uᵢⱼ = Nᵢⱼ` if `klᵢⱼ = kᵢ = lⱼ`, `Uᵢⱼ = Sᵢ` if `klᵢⱼ = kᵢ` only, or `Uᵢⱼ = Tⱼ` if `klᵢⱼ = lⱼ` only. We can construct `{klᵢⱼ : Uᵢⱼ} <: {kᵢ : Sᵢ}` by `S-Rcd` since `{kᵢ} ⊆ {klᵢⱼ}`, and `kᵢ = kₗᵢⱼ` implies `Sᵢ <: Uᵢⱼ`, where `Uᵢⱼ = Sᵢ` or `Uᵢⱼ = Nᵢⱼ`. Similarly, we can construct `{klᵢⱼ : Uᵢⱼ} <: {lⱼ : Tⱼ}` by `S-Rcd`. + * If there exists some `klᵢⱼ` such that `klᵢⱼ = kᵢ = lⱼ` but `Sᵢ` and `Tⱼ` have no subtype, then we claim there is no subtype. Supposing there were a subtype `N`, by inversion we must have that `N = {nₘ : Nₘ}` where `kᵢ = nₘ` implies `Nₘ <: Sᵢ` and `lⱼ = nₘ` implies `Nₘ <: Tⱼ`. In the case where `nₘ = klᵢⱼ`, this gives us a subtype of `Sᵢ` and `Tⱼ`, which is a contradiction. + +**Proposition 16.3.2**: +1. For every `S`, `T`, there exists some `J = S ∨ T`. +2. For every `S`, `T`, `N` such that `N <: S` and `N <: T`, there exists some `M = S ∧ T`. +**Proof**: +By induction on the structure of `S` and `T`, proving both simultaneously, although I will write them separately, even though I use the induction hypotheses jointly. +1. Goal `S ∨ T`. If one of the types is `Top`, then the join is `Top`. If the types have different shapes, then the join must be `Top`, since a function type cannot be the supertype of a record type and vice versa by inversion. That leaves the cases where both types are function types or record types. + * Case `S₁ → S₂`, `T₁ → T₂`. By the induction hypothesis, we know that`J₂ = S₂ ∨ T₂` exists. There are two possible subcases to consider, using the above lemma (existence of a subtype). + * If `S₁` and `T₁` have a subtype, then by the induction hypothesis, we know that `M₁ = S₁ ∧ T₁` exists. We claim that `M₁ → J₂` is the join; we know it is a supertype by `S-Arrow`. It remains to show that it is minimal, i.e. for every `U` such that `S₁ → S₂ <: U` and `T₁ → T₂ <: U`, we have `M₁ → J₂ <: U`. If `U` is `Top`, then we are done. Otherwise, it must be that `U = U₁ → U₂`, and by inversion, `U₁ <: S₁`, `U₁ <: T₁`, `S₂ <: U₂`, and `T₂ <: U₂`. It suffices to show that `U₁ <: M₁` and `J₂ <: U₂`. The former holds by maximality of the meet `M₁ = S₁ ∨ T₁`, while the latter holds by minimality of the join `J₂ = S₂ ∨ T₂`. + * If `S₁` and `T₁` do not have a subtype, then we claim that `Top` is the join. We must show it to be minimal: for every `U` such that `S₁ → S₂ <: U` and `T₁ → T₂ <: U`, we have `Top <: U`. If `U` is `Top`, then we are done. Otherwise, it must be that `U = U₁ → U₂`, and by inversion, `U₁ <: S₁`, `U₁ <: T₁`, `S₂ <: U₂`, and `T₂ <: U₂`. However, this makes `U₁` a subtype of `S₁` and `T₁`, which is a contradiction. + * Case `{kᵢ : Sᵢ}`, `{lⱼ : Tⱼ}`. By the induction hypothesis, we know that every `Sᵢ`, `Tⱼ` have a join. Let `{klᵢⱼ | klᵢⱼ = kᵢ = lⱼ}` be the common labels, i.e. `{kᵢ} ∩ {lⱼ}`, and let `Jᵢⱼ = Sᵢ ∨ Tⱼ`. We claim that `{klᵢⱼ : Jᵢⱼ}` is the join; we know it is a supertype by `S-Rcd`. It remains to show that it is minimal, i.e. for every `U` such that `{kᵢ : Sᵢ} <: U` and `{lⱼ : Tⱼ} <: U`, we have `{klᵢⱼ : Jᵢⱼ} <: U`. If `U` is `Top`, then we are done. Otherwise, it must be that `U = {uₙ : Uₙ}`, and by inversion, `{uₙ} ⊆ {kᵢ}`, `{uₙ} ⊆ {lⱼ}`, `kᵢ = uₙ` implies `Sᵢ <: Uₙ`, and `lⱼ = uₙ` implies `Tⱼ <: Uₙ`. Then we know `{uₙ} ⊆ {kᵢ} ∩ {lⱼ} = {klᵢⱼ}`, and if `kᵢⱼ = uₙ`, then `Sᵢ <: Uₙ` and `Tᵢ <: Uₙ`. By minimality of the join `Jᵢⱼ`, we have `Jᵢⱼ <: Uₙ`. Then we can use `S-Rcd` to build `{klᵢⱼ : Jᵢⱼ} <: U`. +2. Goal `S ∧ T`. If one of the types is `Top`, then the meet is the other type. If the types have different shapes, then `N` being a subtype of both is a contradiction by inversion. That leaves the cases where both types are function types or record types. + * Case `S₁ → S₂`, `T₁ → T₂`. By inversion, `N = N₁ → N₂` where `S₁ <: N₁`, `T₁ <: N₁`, `N₂ <: S₂`, `N₂ <: T₂`. By the induction hypothesis, we know that `M₂ = S₂ ∨ T₂` and `J₁ = S₁ ∧ T₁` exist. We claim that `J₁ → M₂` is the meet; we know it is a subtype by `S-Arrow`. It remains to show that it is maximal, i.e. for every `U` such that `U <: S₁ → S₂` and `U <: T₁ → T₂`, we have `U <: J₁ → M₂`. By inversion, `U = U₁ → U₂` such that `S₁ <: U₁`, `T₁ <: U₁`, `U₂ <: S₂`, and `U₂ <: T₂`. It suffices to show that `J₁ <: U₁` and `U₂ <: M₂`. The former holds by minimality of the join `J₁ = S₁ ∧ T₁`, while the latter holds by maximality of the meet `M₂ = S₂ ∨ T₂`. + * Case `{kᵢ : Sᵢ}`, `{lⱼ : Tⱼ}`. By inversion, `N = {nₘ : Nₘ}` where `{nₘ} ⊆ {kᵢ}`, `{nₘ} ⊆ {lⱼ}`, `kᵢ = nₘ` implies `Nₘ <: Sᵢ`, and `lⱼ = nₘ` implies `Nₘ <: Tⱼ`. By the induction hypothesis, we know that every `Sᵢ`, `Tⱼ` have a meet. Let `{klᵢⱼ} = {kᵢ} ∪ {lⱼ}` be the union of all labels, and for every `klᵢⱼ`, let `Mᵢⱼ = Sᵢ ∧ Tᵢ` if `klᵢⱼ ∈ {kᵢ} ∩ {lⱼ}`, `Mᵢⱼ = Sᵢ` if `klᵢⱼ ∈ {kᵢ}` only, and `Mᵢⱼ = Tᵢ` if `klᵢⱼ ∈ {lⱼ}` only. We claim that `{klᵢⱼ : Mᵢⱼ}` is the meet; we know it is a subtype by `S-Rcd`. It remains to show that it is maximal, ie. for every `U` such that `U <: {kᵢ : Sᵢ}` and `U <: {lⱼ : Tⱼ}`, we have `U <: {Mᵢⱼ : Jᵢⱼ}`. By inversion, `U = {uₙ : Uₙ}` where `{kᵢ} ⊆ {uₙ}`, `{lⱼ} ⊆ {uₙ}`, `kᵢ = uₙ` implies `Uₙ <: Sᵢ`, and `lⱼ = uₙ` implies `Uₙ <: Tⱼ`. Then we know `{kᵢⱼ} = {kᵢ} ∪ {lⱼ} ⊆ {uₙ}`. Supposing `kᵢⱼ = uₙ`, either `uₙ = kᵢ = lⱼ`, in which case `Uₙ <: Sᵢ ∧ Tⱼ` by maximality of the meet, or `uₙ = kᵢ` only, in which case `Uₙ <: Sᵢ`, or `uₙ = lⱼ` only, in which case `Uₙ <: Tⱼ`, so together we have `Uₙ <: Mᵢⱼ`. Then we can use `S-Rcd` to build `U <: {klᵢⱼ : Mᵢⱼ}`. \ No newline at end of file diff --git a/Homework 6.md b/Homework 6.md new file mode 100644 index 0000000..81a8958 --- /dev/null +++ b/Homework 6.md @@ -0,0 +1,333 @@ +I have an issue with the notion of saturated sets as defined in class: +it seems to be tailored specifically to the exact system it's for, +and it's unclear how it should be extended to fit an extended system +with additional eliminators and reduction rules. + +In the POPLMark reloaded[^1] paper, +they provide an inductive definition of strongly normalizing terms +and a notion of reducibility candidates/saturated sets based on this definition, +and I think it's much clearer how the proof of normalization can be extended. + +To demonstrate, I'm going to consider System F extended with booleans, +and try to prove normalization directly using their inductive definition. +First, here are the complete typing rules including booleans and the conditional. + +``` +┌───────────┐ +│ Γ ⊢ M : σ │ +└───────────┘ + +x : σ ∈ Γ Γ, x : σ ⊢ M : τ Γ ⊢ M : σ → τ Γ ⊢ N : σ +--------- Var ----------------- Abs -------------------------- App +Γ ⊢ x : σ Γ ⊢ λx. M : σ → τ Γ ⊢ M N : τ + +Γ ⊢ M : σ α ∉ FV(Γ) Γ ⊢ M : ∀α. σ α ∉ FV(τ) +---------------------- TAbs -------------------------- TApp +Γ ⊢ M : ∀α. σ Γ ⊢ M : σ{α ↦ τ} + +--------------- True ---------------- False +Γ ⊢ true : Bool Γ ⊢ false : Bool + +Γ ⊢ b : Bool Γ ⊢ M : A Γ ⊢ N : A +-------------------------------------- If +Γ ⊢ if b then M else N : A +``` + +## Strongly normalizing terms + +Strongly normalizing terms are defined mutually with +strongly normalizing neutral terms and strong head reduction. +For short, I interchangeably refer to strongly normalizing terms as "normal terms", +and strongly normalizing neutral terms as "neutral terms", +since there is no separate notion of normal and neutral terms that precludes reduction. + +The underlying principles are: +1. Neutral terms are variables and eliminators neutral in the head position + and normal in all other arguments; +2. Normal terms are neutral terms and constructors with normal components, + backward closed under head reduction; +3. Head reduction consists of β-reduction on normal arguments, + and congruence rules for eliminators in the head position. +Reduction is defined mutually with normality to ensure backward closure of normal terms, +since otherwise looping terms may disappear after reduction, +e.g. the function application argument if it is unused, or the other branch of a conditional. +Using these principles, the definition in POPLMark reloaded can be extended to booleans. +(In contrast to the paper, I'll stick to untyped judgements, which is an orthogonal feature.) + +``` +┌─────────┐ +│ M ∈ SNe │ +└─────────┘ + M ∈ SNe N ∈ SN +------- SNe-Var ----------------- SNe-App +x ∈ SNe M N ∈ SNe + +M ∈ SNe N₁, N₂ ∈ SN +-------------------------- SNe-If +if M then N₁ else N₂ ∈ SNe + +┌────────┐ +│ M ∈ SN │ +└────────┘ + +M ∈ SNe M ⇝ N N ∈ SN +------- SN-SNe --------------- SN-Red +M ∈ SN M ∈ SN + +M ∈ SN +---------- SN-Abs ---------------- SN-True,False +λx. M ∈ SN true, false ∈ SN + +┌───────┐ +│ M ⇝ N │ +└───────┘ + +N ∈ SN M ⇝ M' +-------------------- Red-β ---------- Red-App +(λx. M) N ⇝ M{x ↦ N} M N ⇝ M' N + +N₂ ∈ SN +---------------------------- Red-True +if true then N₁ else N₂ ⇝ N₁ + +N₁ ∈ SN +----------------------------- Red-False +if false then N₁ else N₂ ⇝ N₂ + +M ⇝ M' +------------------------------------------- Red-If +if M then N₁ else N₂ ⇝ if M then N₁ else N₂ +``` + +I assume the following property because I don't want to prove it but I'm sure it's true. + +**Proposition** (antisubstitution): +1. If N ∈ SN and M{x ↦ N} ∈ SN then M ∈ SN. +2. If N ∈ SN and M{x ↦ N} ∈ SNe then M ∈ SN. +3. If M{x ↦ N} ⇝ M' and M' ∈ SN then M ∈ SN. + +Because these are inductive definitions, we will need some lemmas +for properties that formerly held by definition, namely inversion and congruence. + +**Lemma** (Inv-App): If (M N) ∈ SN then M ∈ SN. +**Proof**: By induction on SN. +There are two possible cases: +* Case SN-SNe. We have (M N) ∈ SNe, and we wish to show M ∈ SN. + By inversion on neutrals, the only possible case is SNe-App, + where M ∈ SNe. Then M ∈ SN by SN-SNe. +* Case SN-Red. We have (M N) ⇝ N' ∈ SN, and we wish to show M ∈ SN. + By inversion on the reduction, there are two possible cases. + * Case Red-β. We have M = (λx. M'), N ∈ SN, and N' = M'{x ↦ N}. + By antisubstitution, M' ∈ SN, so (λx. M') ∈ SN. + * Case Red-App. We have M N ⇝ M' N = N' ∈ SN and M ⇝ M'. + By the induction hypothesis, M' ∈ SN. By SN-Red, M ∈ SN. + +**Lemma** (Reds-If): If M ⇝* M' then (if M then N₁ else N₂) ⇝* (if M' then N₁ else N₂). +**Proof**: By induction on the reflexive, transitive closure of reduction, +using Red-If and the induction hypothesis in the transitive case. + +**Lemma** (Reds-App): If M ⇝* M' then M N ⇝* M' N. +**Proof**: By induction on the reflexive, transitive closure of reduction, +using Red-App and the induction hypothesis in the transitive case. + +## Reducibility candidates + +Their definition of reducibility candidates (CR) then captures the same properties SAT did, +namely backward closure under head reduction, +and that SATs/CRs are squeezed between neutrals and normals. + +**Definition**: A set R is a reducibility candidate (R ∈ CR) when the following hold: +1. R ⊆ SN; +2. If M ⇝ M' and M' ∈ R then M ∈ R; and +3. SNe ⊆ R. +I refer to these as CR1, CR2, and CR3. + +We can prove the same lemmas for CR as we did for SAT, +with an additional backward closure under the reflexive, transitive closure of reduction. + +**Lemma 0** (CR2*): Let R ∈ CR. If M ⇝* M' and M' ∈ R then M ∈ R. +**Proof**: By induction on the reflexive, transitive closure of reduction, +using CR2 and the induction hypothesis in the transitive case. + +**Lemma 1**: SN ∈ CR. +**Proof**: CR1 holds trivially, CR2 holds by SN-Red, and CR3 holds by SN-SNe. + +**Lemma 2**: If A, B ∈ CR, then A ⇒ B ∈ CR, where (M ∈ A ⇒ B) ⇔ for all N ∈ A, M N ∈ B. +**Proof**: Let A, B ∈ CR. +1. Suppose M ∈ A ⇒ B. We need to show that M ∈ SN. + Picking any variable x, we know x ∈ A since SNe ⊆ A ∈ CR by CR3. + Then by definition, M x ∈ B ∈ CR, so by M x ∈ SN by CR1. + Then by Inv-App, M ∈ SN. +2. Suppose M ⇝ M' ∈ A ⇒ B. We need to show that M ∈ A ⇒ B, + i.e. supposing N ∈ A, M N ∈ B. By supposition, we know M' N ∈ B. + By Red-App, we know M N ⇝ M' N, and by CR2, we have M N ∈ B. +3. Suppose M ∈ SNe. We need to show that M ∈ A ⇒ B, + i.e. supposing N ∈ A, M N ∈ B. + By CR1, we know N ∈ A ⊆ SN, so by SNe-App, we have M N ∈ SNe. + Then by CR2, we have M N ∈ SNe ⊆ B. + +**Lemma 3**: Let Aᵢ be some family of sets of terms indexed by i ∈ I (potentially infinite). +If Aᵢ ∈ CR, then ∩ᵢ Aᵢ ∈ CR. +**Proof**: Suppose Aᵢ ∈ CR. +1. Let M ∈ ∩ᵢ Aᵢ. We need to show that M ∈ SN. + By definition, M ∈ Aᵢ for some Aᵢ, and by CR1, we have M ∈ Aᵢ ⊆ SN. +2. Suppose M ⇝ M' ∈ ∩ᵢ Aᵢ. We need to show that M ∈ ∩ᵢ Aᵢ. + By definition, M' ∈ Aᵢ for every Aᵢ. + By CR2, we have M ∈ Aᵢ for every Aᵢ, so M ∈ ∩ᵢ Aᵢ. +3. Suppose M ∈ SNe. We need to show that M ∈ ∩ᵢ Aᵢ. + By CR3, we have M ∈ Aᵢ for every Aᵢ, so M ∈ ∩ᵢ Aᵢ. + +## Type interpretations + +With the addition of booleans, we need an interpretation of the type of booleans. +The positive formulation states that elements of the interpretation +reduce to normal constructor forms or is neutral; +the negative formulation states that elements of the interpretation +behave "as expected" when eliminated. +For booleans, the latter looks like this: + +**_not_ the Definition** (semantic booleans): M ∈ ⟦Bool⟧ξ ⇔ for all σ and N₁, N₂ ∈ ⟦σ⟧ξ, +(if M then N₁ else N₂) ∈ ⟦σ⟧ξ. + +However, Joe Cutler says this doesn't work (don't tell him I said he said this), +and I can't be bothered to check, so I'll stick with the positive formulation. +We also need to show that it, too, is a reducibility candidate. + +**Definition** (semantic booleans): M ∈ ⟦Bool⟧ξ ⇔ M ∈ SNe or M ⇝* true or M ⇝* false. + +**Lemma 4**: ⟦Bool⟧ξ ∈ CR. +**Proof**: +1. We need to show that if M ∈ ⟦Bool⟧ξ, then M ∈ SN. + By definition of ⟦Bool⟧ξ, there are three cases. + If M ∈ SNe, then M ∈ SN by SN-SNe. + If M ⇝* true or M ⇝* false, then induct on the reflexive, transitive closure. + In the reflexive case, we use SN-True and SN-False. + In the transitive case, we use SN-Red followed by the induction hypothesis. +2. We need to show that if M ⇝ M' ∈ ⟦Bool⟧ξ, then M ∈ ⟦Bool⟧ξ. + By definition of ⟦Bool⟧ξ, there are three cases. + If M' ∈ SNe, then by SN-SNe and SN-Red, we have M ∈ SNe, so M ∈ ⟦Bool⟧ξ + If M' ⇝* true or M ⇝* false, by transitivity, M ⇝ M' ⇝* true or false. +3. We need to show that if M ∈ SNe, then M ∈ ⟦Bool⟧ξ, which holds by definition. + +With these four lemmas, the interpretation of types is a reducibility candidate. + +**Definition** (type interpretation): Let ξ be a function from type variables to CRs. +We define ⟦·⟧ξ recursively on types: +* ⟦α⟧ξ ≔ ξ(α) +* ⟦σ → τ⟧ξ ≔ ⟦σ⟧ξ ⇒ ⟦τ⟧ξ +* ⟦∀α. σ⟧ξ ≔ ∩ₓ ⟦σ⟧(ξ, α ↦ x) where X ∈ CR +* ⟦Bool⟧ξ ≔ semantic booleans as above + +**Lemma 5**: ⟦σ⟧ξ ∈ CR. +**Proof**: By induction on types, using Lemmas 2, 3, 4 +for functions, polymorphism, and booleans, respectively. + +## Soundness and normalization + +The definitions of semantic typing remain unchanged, reproduced below, +using ρ for substitution maps from term variables to terms, +ξ for substitution maps from type variables to sets, +and M{ρ} for applying the substitutions of ρ in M. + +**Definitions**: +* ⟦M⟧ρ ⇔ M{ρ} +* ρ, ξ ⊧ Γ ⇔ ∀x : σ ∈ Γ, ρ(x) ∈ ⟦σ⟧ξ +* Γ ⊧ M : σ ⇔ ∀ρ, ξ ⊧ Γ, ⟦M⟧ρ ∈ ⟦σ⟧ξ + +We can now prove the fundamental soundness theorem. +All of the old cases hold as usual; +I'll cover just the old polymorphism cases along with the new boolean cases. + +**Theorem** (soundness): If Γ ⊢ M : σ then Γ ⊧ M : σ. +**Proof**: By induction on the typing derivation. +* Case TAbs: We have premises Γ ⊢ M : σ and α ∉ FV(Γ), + and we need to show Γ ⊧ M : ∀α. σ, + i.e. for every ρ, ξ ⊧ Γ, we have ⟦M⟧ρ ∈ ⟦∀α. σ⟧ξ = ∩ₓ ⟦σ⟧{ξ, α ↦ X}. + By the induction hypothesis, for every ρ', ξ' ⊧ Γ, we have ⟦M⟧ρ ∈ ⟦σ⟧ξ. + Consequently, for every X ∈ CR, we have ρ, {ξ, α ↦ X} ⊧ Γ implies ⟦M⟧ρ ∈ ⟦σ⟧ξ. + Since α ∉ FV(Γ), given ρ, ξ ⊧ Γ, we can harmlessly extend to ρ, {ξ, α ↦ X} ⊧ Γ. + Then for every X ∈ CR, ⟦M⟧ρ ∈ ⟦σ⟧{ξ, α ↦ X}, i.e. ⟦M⟧ρ ∈ ∩ₓ ⟦σ⟧{ξ, α ↦ X}. +* Case TApp: We have premises Γ ⊢ M : ∀α. σ and α ∉ FV{τ}, + and we need to show Γ ⊧ M : σ{α ↦ τ}, + i.e. for every ρ, ξ ⊧ Γ, we have ⟦M⟧ρ ∈ ⟦σ{α ↦ τ}⟧ξ = ⟦σ⟧{ξ, α ↦ ⟦τ⟧ξ}. + By the induction hypothesis, we have ⟦M⟧ρ ∈ ⟦∀α. σ⟧ξ = ∩ₓ ⟦σ⟧{ξ, α ↦ X}. + By Lemma 5, ⟦τ⟧ξ ∈ CR, so we can instantiate X with ⟦τ⟧ξ. +* Case True: We need to show Γ ⊧ true : Bool, + i.e. for every ρ, ξ ⊧ Γ, we have ⟦true⟧ρ ∈ ⟦Bool⟧ξ. + This holds trivially by true ⇝* true. +* Case False: As above. +* Case If: We have premises Γ ⊢ M : Bool, Γ ⊢ N₁ : σ, Γ ⊢ N₂ : σ, + and we need to show Γ ⊧ if M then N₁ else N₂, + i.e. for every ρ, ξ ⊧ Γ, we have (if ⟦M⟧ρ then ⟦N₁⟧ρ else ⟦N₂⟧ρ) ∈ ⟦σ⟧ξ. + By the induction hypotheses, we have ⟦M⟧ρ ∈ ⟦Bool⟧ξ and ⟦Nᵢ⟧ρ ∈ ⟦σ⟧ξ. + By Lemma 5, we have ⟦M⟧ρ, ⟦Nᵢ⟧ρ ∈ CR, and by CR1, we have ⟦M⟧ρ, ⟦Nᵢ⟧ρ ∈ SN. + By definition of ⟦Bool⟧ξ, there are three cases to consider. + * ⟦M⟧ρ ∈ SNe: By SNe-If, we know that (if ⟦M⟧ρ then ⟦N₁⟧ρ else ⟦N₂⟧ρ) ∈ SNe. + Then by CR3, we have (if ⟦M⟧ρ then ⟦N₁⟧ρ else ⟦N₂⟧ρ) ∈ ⟦σ⟧ξ. + * ⟦M⟧ρ ⇝* true or false: By Reds-If, Red-True/-False, and transitivity, we have + (if ⟦M⟧ρ then ⟦N₁⟧ρ else ⟦N₂⟧ρ) ⇝* ⟦N₁⟧ρ or ⟦N₂⟧ρ ∈ ⟦σ⟧ξ. + Then by CR2*, (if ⟦M⟧ρ then ⟦N₁⟧ρ else ⟦N₂⟧ρ) ∈ ⟦σ⟧ξ. + +Strong normalization holds as a corollary like before. + +**Corollary** (strong normalization): If Γ ⊢ M : σ then M ∈ SN. +**Proof**: By soundness, unfolding the definition of semantic typing, we have +∀ρ, ξ, (∀x : τ ∈ Γ, ρ(x) ∈ ⟦τ⟧ξ) ⇒ M{ρ} ∈ ⟦σ⟧ξ. +Pick ρ(x) ↦ x and ξ(α) ↦ SAT. We need to show that ∀x : τ ∈ Γ, x ∈ ⟦τ⟧ξ. +By CR3, ⟦τ⟧ξ ⊆ SNe, so by SN-Var, x ∈ ⟦τ⟧ξ. +Then we have M ∈ ⟦σ⟧ξ ∈ CR, and by CR1, M ∈ SN. + +## Normalization and infinite reductions + +However, this proof of strong normalization is still stated using the inductive definition, +not the original statement of strong normalization, +which states that there are no infinite reduction sequences, +where the usual notion of reduction is single-step congruent β-reduction. +We can show that the former implies the latter, +assuming the corresponding antisubstitution property for the latter, +as well as various inversion properties. + +**Proposition** (antisubstitution): If N and M{x ↦ N} have no infinite reduction sequences, +then M has no infinite reduction sequences. + +**Proposition** (inversion): If M has no infinite reduction sequences, +then neither do its syntactic components. +For example, if (M N) has no infinite reduction sequences, then neither do M nor N. + +**Lemma** (soundness of SN): +1. If M ∈ SN then M has no infinite reduction sequences. +2. If M ∈ SNe then M has no infinite reduction sequences. +3. If M ⇝ M' and M' has no infinite reduction sequences, + then M has no infinite reduction sequences. +**Proof**: By mutual induction. +The first and second parts are fairly direct by the induction hypotheses. +We look at the third part in detail. +* Case SN-Red: We have M ⇝ N and N ∈ SN. + By the first induction hypothesis, N has no infinite reduction sequences. + Then by the third induction hypothesis, M has no infinite reduction sequeces. +* Case Red-β: We have ((λx. M) N) ⇝ M{x ↦ N} and N ∈ SN, + where M{x ↦ N} has no infinite reduction sequences. + By the first induction hypothesis, N has no infinite reduction sequences. + By antisubstitution, M has no infinite reduction sequences, + so neither does ((λx. M) N) +* Case Red-App: We have (M N) ⇝ (M' N) and M ⇝ M", + where (M' N) has no infinite reduction sequences. + By inversion, M', N have no infinite reduction sequences. + By the third induction hypothesis, M has no infinite reduction sequences. + Then (M N) has no infinite reduction sequence. +* Case Red-True: We have (if true then N₁ else N₂) ⇝ N₁ and N₂ ∈ SN, + where N₁ has no infinite reduction sequences. + By the first induction hypothesis, N₂ has no infinite reduction sequences. + Then (if true then N₁ else N₂) has no infinite reduction sequences. +* Case Red-False: As above. +* Case Red-If: We have (if M then N₁ else N₂) ⇝ (if M' then N₁ else N₂) and M ⇝ M', + where (if M' then N₁ else N₂) has no infinite reduction sequences. + By inversion, M', N₁, and N₂ have no infinite reduction sequences. + By the third induction hypothesis, M has no infinite reduction sequences. + Then (if M then N₁ else N₂) has no infinite reduction sequences. + +**Corollary** (no infinite reductions): If Γ ⊢ M : σ, then M has no infinite reduction sequences. + +--- + +[^1]: Andreas Abel, Guillaume Allais, Aliya Hameer, Brigitte Pientka, Alberto Momigliano, Steven Schäfer, and Kathrin Stark. (2019). POPLMark reloaded: Mechanizing proofs by logical relations. Journal of Functional Programming, 29(e19). DOI:[10.1017/S0956796819000170](https://doi.org/10.1017/S0956796819000170 ) \ No newline at end of file diff --git a/Homework 7.md b/Homework 7.md new file mode 100644 index 0000000..5b37de1 --- /dev/null +++ b/Homework 7.md @@ -0,0 +1,82 @@ +**Exercise 22.3.9**: For clarity, the original constraint typing rules from class are reproduced below. + +``` +┌──────────────────┐ +│ Γ ⊢ t : T | V; C │ +└──────────────────┘ + +x : T ∈ Γ +---------------- CT-Var +Γ ⊢ x : T | ∅, ∅ + +Γ, x : T₁ ⊢ t₂ : T₂ | V; C +-------------------------------- CT-Abs +Γ ⊢ λx : T₁. t₂ : T₁ → T₂ | V; C + +Γ ⊢ t₁ : T₁ | V₁; C₁ +Γ ⊢ t₂ : T₂ | V₂; C₂ +V₁ ∩ V₂ = V₁ ∩ FV(T₂) = V₂ ∩ FV(T₁) = ∅ +X ∉ V₁, V₂, FV(T₁, T₂, C₁, C₂, Γ, t₁, t₂) +------------------------------------------------------ CT-App +Γ ⊢ t₁ t₂ : X | V₁ ∪ V₂ ∪ {X}; C₁ ∪ C₂ ∪ {T₁ = T₂ → X} +``` + +The new constraint typing rules that thread through unused type variables are below. + +``` +┌─────────────────────┐ +│ Γ; F ⊢ t : T | F; C │ +└─────────────────────┘ + +x : T ∈ Γ +------------------- FCT-Var +Γ; F ⊢ x : T | F; ∅ + +Γ, x : T₁; F ⊢ t₂ : T₂ | F'; C +------------------------------------ FCT-Abs +Γ; F ⊢ λx : T₁. t₂ : T₁ → T₂ | F'; C + +Γ; F₁ ⊢ t₁ : T₁ | F₂; C₁ +Γ; F₂ ⊢ t₂ : T₂ | F₃; C₂ +X ∈ F₃ F₄ = F₃ \ {X} +----------------------------------------------------- FCT-App +Γ; F₁ ⊢ t₁ t₂ : X | F₄; C₁ ∪ C₂ ∪ {T₁ = T₂ → X} +``` + +A key property of the new rules is that the output variables +are indeed fresh with respect to the inputs and the other outputs. + +**Lemma**: If Γ; Fᵢ ⊢ t : T | Fₒ; C and Fᵢ ∩ (FV(Γ) ∪ FV(t)) = ∅ then Fₒ ⊆ Fᵢ and Fₒ ∩ (FV(T) ∪ FV(C)) = ∅. +**Proof**: By induction on the derivation of the new typing rules. +* Case FCT-Var (F₀ = Fᵢ = F): F ∩ FV(Γ) = ∅ and x : T ∈ Γ so F ∩ FV(T) = ∅. +* Case FCT-Abs: By supposition, F ∩ FV(T₁) = ∅. + Then by the induction hypothesis, F' ⊆ F and F' ∩ (FV(T₂) ∪ FV(C)) = ∅, + and we also have F ∩ FV(T₁) = ∅ by the supposition and by subset, + so we have F ∩ FV(T₁ → T₂) = ∅ as needed. +* Case FCT-App: By supposition, F₁ ∩ FV(t₁) = F₁ ∩ FV(t₂) = ∅. + By the induction hypothesis on both premises in sequence, + we have F₃ ⊆ F₂ ⊆ F₁ and F₂ ∩ (FV(T₁) ∪ FV(C₁)) = F₃ ∩ (FV(T₂) ∪ FV(C₂)) = ∅. + By definition, F₄ ⊆ F₃, and X ∉ F₄. + Then F₄ ∩ (FV(T₁) ∪ FV(T₂) ∪ FV(C₁) ∪ FV(C₂)) = ∅ by subset, + so F₄ ∩ (FV(C₁ ∪ C₂ ∪ {T₁ = T₂ → X})) - ∅ as well. + +We can then show that the typing judgements imply one another. + +**Lemma** (soundness of FCT wrt CT): Suppose Fᵢ ∩ (FV(Γ) ∪ FV(t)) = ∅. +If Γ; Fᵢ ⊢ t : T | Fₒ : C, then Γ ⊢ t : T | Fᵢ \ Fₒ; C. +**Proof**: By induction on the derivation of the new typing rules. +* Case FCT-App: The premises are Γ; F₁ ⊢ t₁ : T₁ | F₂; C₁ and Γ; F₂ ⊢ t₂ : T₂ | F₃; C₂, + along with X ∈ F₃ and F₄ = F₃ \ {X}. + The goal is to show that Γ ⊢ t : T | F₁ \ F₄; C₁ ∪ C₂ ∪ {T₁ = T₂ → X}. + Applying CT-App, we need the following premises: + 1. Γ ⊢ t₁ : T₁ | V₁; C₁ for some V₁; + 2. Γ ⊢ t₂ : T₂ | V₂; C₂ for some V₂; + 3. V₁ ∩ V₂ = V₁ ∩ FV(T₂) = V₂ ∩ FV(T₁) = ∅; and + 4. X ∉ V₁, V₂, FV(T₁, T₂, C₁, C₂, Γ, t₁, t₂). + By the induction hypothesis, we have the first goal where V₁ = F₁ \ F₂. + By the above lemma, F₂ ⊆ F₁, so its variables are not free in Γ or t₂. + Then we apply the induction hypothesis again to yield the second goal where V₂ = F₂ \ F₃. + By set subtraction, we know that V₁ ∩ V₂ = ∅. + +**Lemma** (completeness of FCT wrt CT): V ∩ (FV(Γ) ∪ FV(t)) = ∅. +If Γ ⊢ t : T | V; C, then Γ; V ⊢ t : T | {}; C. \ No newline at end of file diff --git a/README.md b/README.md new file mode 100644 index 0000000..46551c5 --- /dev/null +++ b/README.md @@ -0,0 +1,15 @@ +# CIS 6700: Type Systems - Spring 2025 + +## Homeworks + +Exercise numbers refer to TAPL. + +| # | Homework | Due | +| - | -------- | --- | +| 1 | Formal definition of substitution on de Bruijn terms | 27 January | +| 2 | 3.5.16, 3.5.17 | 3 February | +| 3 | [Exercise 2](https://www.cs.cmu.edu/~rwh/courses/atpl/pdfs/tait.pdf); largest and smallest saturated sets | 10 February | +| 4 | 13.3.1, 13.5.8 | 19 Feburary | +| 5 | 15.3.6, 16.1.3, 16.2.5, 16.2.6, 16.3.2 | 24 Feburary | +| 6 | Barendregt's or Gallier's normalization proof | 5 March | +| 7 | 22.3.9, 22.3.10, 22.4.6, 22.5.5 | 17 March | \ No newline at end of file diff --git a/TyRecon.idr b/TyRecon.idr new file mode 100644 index 0000000..10a3ef4 --- /dev/null +++ b/TyRecon.idr @@ -0,0 +1,300 @@ +import Data.Fin +import Data.Vect +import Control.Monad.State +import Control.Monad.Reader +import Control.Monad.Either + +%default total + +{-- Basic data definitions: + * types; + * length-indexed contexts and lookup; + * well-scoped terms; + * constraint sets; and + * solutions. +--} + +data Ty : Type where + TyId : String -> Ty + TyArr : Ty -> Ty -> Ty + TyBool : Ty + TyNat : Ty + +FromString Ty where + fromString = TyId + +0 Ctxt : Nat -> Type +Ctxt n = Vect n Ty + +data Tm : Nat -> Type where + Var : forall n. Fin n -> Tm n + Abs : forall n. Ty -> Tm (S n) -> Tm n + App : forall n. Tm n -> Tm n -> Tm n + True : forall n. Tm n + False : forall n. Tm n + If : forall n. Tm n -> Tm n -> Tm n -> Tm n + Zero : forall n. Tm n + Succ : forall n. Tm n -> Tm n + Pred : forall n. Tm n -> Tm n + IsZero : forall n. Tm n -> Tm n + +0 Constrs : Type +Constrs = List (Ty, Ty) + +0 Solution : Type +Solution = (Ty, Constrs) + +{-- Raw, unscoped terms to scoped terms --} + +private infix 1 `Then` +data TmRaw : Type where + ι : String -> TmRaw + λ : String -> Ty -> TmRaw -> TmRaw + (#) : TmRaw -> TmRaw -> TmRaw + T : TmRaw + F : TmRaw + Then : TmRaw -> (TmRaw, TmRaw) -> TmRaw + ZZ : TmRaw + SS : TmRaw -> TmRaw + PP : TmRaw -> TmRaw + IZ : TmRaw -> TmRaw + +FromString TmRaw where + fromString = ι + +Iff : TmRaw -> TmRaw +Iff = id + +private infix 2 `Else` +Else : TmRaw -> TmRaw -> (TmRaw, TmRaw) +Else = (,) + +scoped : forall n. Vect n String -> TmRaw -> Either String (Tm n) +scoped g (ι x) = + case findIndex (== x) g of + Just n => pure $ Var n + Nothing => throwError "The variable \{x} is not in scope" +scoped g (λ x t b) = Abs t <$> scoped (x :: g) b +scoped g (b # a) = App <$> scoped g b <*> scoped g a +scoped g T = pure True +scoped g F = pure False +scoped g (b `Then` (c, d)) = If <$> scoped g b <*> scoped g c <*> scoped g d +scoped g ZZ = pure Zero +scoped g (SS n) = Succ <$> scoped g n +scoped g (PP n) = Pred <$> scoped g n +scoped g (IZ n) = IsZero <$> scoped g n + +{-- Some instances for the above, Interpolation acting as pretty printer --} + +Eq Ty where + TyId x == TyId y = x == y + TyArr tal tbl == TyArr tar tbr = tal == tar && tbl == tbr + TyBool == TyBool = True + TyNat == TyNat = True + _ == _ = False + +isTerminal : forall n. Tm n -> Bool +isTerminal (Var _) = True +isTerminal True = True +isTerminal False = True +isTerminal Zero = True +isTerminal _ = False + +Interpolation Ty where + interpolate (TyId x) = x + interpolate (TyArr ta@(TyArr _ _) tb) = "(\{ta}) -> \{tb}" + interpolate (TyArr ta tb) = "\{ta} → \{tb}" + interpolate TyBool = "Bool" + interpolate TyNat = "Nat" + +Interpolation (Tm n) where + interpolate (Var n) = "v" ++ show n + interpolate (Abs ta b) = "λ_: \{ta}. \{b}" + interpolate (App b a) = + case b of + App _ _ => "\{b}" + _ => if isTerminal b then "\{b}" else "(\{b})" + ++ " " ++ if isTerminal a then "\{a}" else "(\{a})" + interpolate True = "true" + interpolate False = "false" + interpolate (If b c d) = "if \{b} then \{c} else \{d}" + interpolate Zero = "0" + interpolate (Succ n) = + case n of + Succ _ => "\{n} + 1" + Pred _ => "\{n} + 1" + _ => if isTerminal n then "\{n} + 1" else "(\{n}) + 1" + interpolate (Pred n) = + case n of + Succ _ => "\{n} - 1" + Pred _ => "\{n} - 1" + _ => if isTerminal n then "\{n} - 1" else "(\{n}) - 1" + interpolate (IsZero n) = + if isTerminal n then "zero? \{n}" else "zero? (\{n})" + +Interpolation (Ctxt n) where + interpolate [] = "·" + interpolate [t] = "\{t}" + interpolate (t :: ts) = "\{ts}, \{t}" + +Interpolation Constrs where + interpolate [] = "" + interpolate [(ta, tb)] = "\{ta} = \{tb}" + interpolate ((ta, tb) :: cs) = "\{ta} = \{tb}, \{cs}" + +{-- Constraint-based type checking monad with: + * state monad for generating fresh type variables; and + * reader monad for extending type context. +--} + +0 CTM : Nat -> Type -> Type +CTM n = ReaderT (Ctxt n) (State Nat) + +-- Reader.local doesn't work since extending the context changes its type +withTy : forall a, n. Ty -> CTM (S n) a -> CTM n a +withTy t ctm = MkReaderT (\ctxt => runReaderT (t :: ctxt) ctm) + +nextVar : forall n. CTM n Ty +nextVar = do + c <- get + put (S c) + pure $ TyId ("?X_" ++ show c) + +{-- Constraint-based type checking algorithm --} + +ctype : forall n. Tm n -> CTM n Solution +ctype (Var n) = do + ctxt <- ask + pure (index n ctxt, []) +ctype (Abs ta b) = do + (tb, cb) <- withTy ta (ctype b) + pure (TyArr ta tb, cb) +ctype (App b a) = do + (tb, cb) <- ctype b + (ta, ca) <- ctype a + x <- nextVar + pure (x, (tb, TyArr ta x) :: cb ++ ca) +ctype True = pure (TyBool, []) +ctype False = pure (TyBool, []) +ctype (If b c d) = do + (tb, cb) <- ctype b + (tc, cc) <- ctype c + (td, cd) <- ctype d + pure (tc, (tb, TyBool) :: (tc, td) :: cb ++ cc ++ cd) +ctype Zero = pure (TyNat, []) +ctype (Succ n) = do + (tn, cn) <- ctype n + pure (TyNat, (tn, TyNat) :: cn) +ctype (Pred n) = do + (tn, cn) <- ctype n + pure (TyNat, (tn, TyNat) :: cn) +ctype (IsZero n) = do + (tn, cn) <- ctype n + pure (TyBool, (tn, TyNat) :: cn) + +solve : forall n. Ctxt n -> Tm n -> Solution +solve ctxt = runIdentity . evalStateT 0 . runReaderT ctxt . ctype + +{-- Substitutions are mappings from strings to types + and act on terms and types --} + +0 Subst : Type +Subst = String -> Ty + +(:<) : Subst -> (String, Ty) -> Subst +s :< (x, t) = \y => if x == y then t else s y + +subst : Subst -> Ty -> Ty +subst s (TyId x) = s x +subst s (TyArr ta tb) = TyArr (subst s ta) (subst s tb) +subst s t = t + +substTm : forall n. Subst -> Tm n -> Tm n +substTm s (Abs ta b) = Abs (subst s ta) (substTm s b) +substTm s (App b a) = App (substTm s b) (substTm s a) +substTm s (If b c d) = If (substTm s b) (substTm s c) (substTm s d) +substTm s a = a + +{-- Constraint unification algorithm --} + +occurs : Ty -> String -> Bool +occurs (TyId y) x = x == y +occurs (TyArr ta tb) x = occurs ta x || occurs tb x +occurs _ _ = False + +0 UCM : Type -> Type +UCM = StateT Subst $ EitherT String Identity + +covering +unify : Constrs -> UCM () +unify [] = pure () +unify ((ta, tb) :: cs) = do + s <- get + let ta = subst s ta + let tb = subst s tb + if ta == tb then unify cs else + case (ta, tb) of + (TyId x, t) => + if occurs t x + then throwError "The variable \{x} occurs in the right hand side \{t}" + else do + put $ s :< (x, t) + unify cs + (t, TyId x) => + if occurs t x + then throwError "The variable \{x} occurs in the left hand side \{t}" + else do + put $ s :< (x, t) + unify cs + (TyArr tal tbl, TyArr tar tbr) => + unify ((tal, tar) :: (tbl, tbr) :: cs) + _ => throwError "Cannot unify \{ta} with \{tb}" + +covering +unifier : Constrs -> Either String Subst +unifier = runIdentity . runEitherT . execStateT TyId . unify + +{-- Example expressions from 22.5.2, 22.5.5 --} + +-- λx: X. x y +test0 : TmRaw +test0 = λ "x" "X" $ "x" # "y" + +-- λx: X. x +test1 : TmRaw +test1 = λ "x" "X" "x" + +-- λz: Z. λy: Y. z (y true) +test2 : TmRaw +test2 = λ "z" "Z" $ λ "y" "Y" $ "z" # ("y" # T) + +-- λw: W. if true then false else w false +test3 : TmRaw +test3 = λ "w" "W" $ Iff T `Then` F `Else` ("w" # F) + +-- λx: X. λy: Y. λz: Z. (x z) (y z) +test4 : TmRaw +test4 = λ "x" "X" $ λ "y" "Y" $ λ "z" "Z" $ ("x" # "z") # ("y" # "z") + +-- λx: X. x x +test5 : TmRaw +test5 = λ "x" "X" $ "x" # "x" + +covering +printSolveUnify : TmRaw -> IO () +printSolveUnify a = do + let Right a = scoped [] a + | Left e => putStrLn "scope failed: \{e}" + let (ta, cs) = solve [] a + -- [context] ⊢ (term) : (type) | {constraints} + putStrLn "solve: ⊢ (\{a}) : (\{ta}) | {\{cs}}" + let Right s = unifier cs + | Left e => putStrLn "unify failed: \{e}" + -- [context{s}] ⊢ (term{s}) : (type{s}) + putStrLn "unify: ⊢ (\{substTm s a}) : (\{subst s ta})" + +covering +main : IO () +main = do + traverse_ {t = List} printSolveUnify + [test0, test1, test2, test3, test4, test5] \ No newline at end of file diff --git a/tyrecon.ipkg b/tyrecon.ipkg new file mode 100644 index 0000000..826ddee --- /dev/null +++ b/tyrecon.ipkg @@ -0,0 +1,4 @@ +package tyrecon + +modules = TyRecon +depends = contrib \ No newline at end of file