91 lines
4.5 KiB
Markdown
91 lines
4.5 KiB
Markdown
**Exercise 26.3.5**:
|
||
```
|
||
SBool ≜ ∀X <: ⊤. ∀T <: X. ∀F <: X. T → F → X
|
||
STrue ≜ ∀X <: ⊤. ∀T <: X. ∀F <: X. T → F → T
|
||
SFalse ≜ ∀X <: ⊤. ∀T <: X. ∀F <: X. T → F → F
|
||
|
||
notft : SFalse → STrue
|
||
notft = λsfalse : SFalse. ΛX <: ⊤. ΛT <: X. ΛF <: X. λt : T. λf : F. t
|
||
|
||
nottf : STrue → SFalse
|
||
nottf = λstrue : STrue. ΛX <: ⊤. ΛT <: X. ΛF <: X. λt : T. λf : F. f
|
||
```
|
||
**Exercise 26.4.11**:
|
||
1. If Γ ⊢ S₁ → S₂ <: T, then T = ⊤ or T = T₁ → T₂ with Γ ⊢ T₁ <: S₁ and Γ ⊢ S₂ <: T₂.
|
||
2. If Γ ⊢ ∀X <: U. S₂ <: T, then T = ⊤ or T = ∀X <: U. T₂ with Γ, X <: U ⊢ S₂ <: T₂.
|
||
3. If Γ ⊢ X <: T, then T = ⊤ or T = X or Γ ⊢ S <: T with X <: S ∈ Γ.
|
||
4. If Γ ⊢ ⊤ <: T, then T = ⊤.
|
||
|
||
**Proof**:
|
||
4. By induction on the subtyping derivation. The cases not listed are impossible.
|
||
* S-Refl: T = ⊤.
|
||
* S-Trans: The premises are Γ ⊢ ⊤ <: U and Γ ⊢ U <: T.
|
||
By the induction hypothesis, U = ⊤ and T = ⊤.
|
||
* S-Top: Trivial.
|
||
1. By induction on the subtyping derivation. The cases not listed are impossible.
|
||
* S-Refl: T = S₁ → S₂ with Γ ⊢ S₁ <: S₁ and Γ ⊢ S₂ <: S₂ by S-Refl.
|
||
* S-Trans: The premises are Γ ⊢ S₁ → S₂ <: U and Γ ⊢ U <: T.
|
||
By the induction hypothesis on the first premise, either U = ⊤, so T = ⊤ by (4),
|
||
or U = U₁ → U₂ with Γ ⊢ U₁ <: S₁ and Γ ⊢ S₂ <: U₂.
|
||
By the induction hypothesis on the second premise, either T = ⊤,
|
||
or T = T₁ → T₂ with Γ ⊢ T₁ <: U₁ and Γ ⊢ U₂ <: T₂.
|
||
Then by S-Trans, Γ ⊢ T₁ <: S₁ and Γ ⊢ S₂ <: T₂.
|
||
* S-Arrow: Trivially the second case by the premises.
|
||
2. By induction on the subtyping derivation. The cases not listed are impossible.
|
||
* S-Refl: T = ∀X <: U. S₂ with Γ, X <: U ⊢ S₂ <: S₂ by S-Refl.
|
||
* S-Trans: The premises are Γ ∀X <: U. S₂ <: V and Γ ⊢ V <: T.
|
||
By the induction hypothesis on the first premise, either V = ⊤, so T = ⊤ by (4),
|
||
or V = ∀X <: U. V₂ with Γ, X <: U ⊢ S₂ <: V₂.
|
||
By the induction hypothesis on the second premise, either T = ⊤,
|
||
or T = ∀X <: U. T₂ with Γ, X <: U ⊢ V₂ <: T₂.
|
||
Then by S-Trans, Γ, X <: U ⊢ S₂ <: T₂.
|
||
* S-All: Trivially the second case by the premise.
|
||
3. By induction on the subtyping derivation. The cases not listed are impossible.
|
||
* S-Refl: Trivially the second case.
|
||
* S-Trans: The premises are Γ ⊢ X <: U and Γ ⊢ U <: T.
|
||
By the induction hypothesis on the first premise, there are three possibilities:
|
||
- U = ⊤, so T = ⊤ by (4).
|
||
- U = X. By the induction hypothesis on the second premise,
|
||
either T = ⊤ by (4), or T = X, or Γ ⊢ S <: T with X <: S ∈ Γ, as desired.
|
||
- Γ ⊢ S <: U with X <: S ∈ Γ. Then by S-Trans, Γ ⊢ S <: T.
|
||
* S-Var: Trivially the last case with Γ ⊢ T <: T by S-Refl.
|
||
|
||
**Exercise 28.2.3**:
|
||
2. If Γ ⊢ t : T, then Γ ⊢> t : M with Γ ⊢ M <: T.
|
||
|
||
**Proof**:
|
||
1. Case T-TApp: The premises are Γ ⊢ t₁ : ∀X <: T₁₁. T₁₂ and Γ ⊢ T₂ <: T₁₁.
|
||
We wish to show that Γ ⊢> t₁ [T₂] : M₂ for some M₂ with Γ ⊢ M₂ <: T₁₂[X ↦ T₂].
|
||
By the induction hypothesis, we have Γ ⊢> t₁ : M₁ with Γ ⊢ M₁ <: ∀X <: T₁₁. T₁₂.
|
||
Let M₁ ⇑ N₁, knowing that N₁ is not a variable.
|
||
By the exposure lemma, we have Γ ⊢ N₁ <: ∀X <: T₁₁. T₁₂.
|
||
By inversion, N₁ = ∀X <: S₁₁. S₁₂ with Γ ⊢ T₁₁ <: S₁₁ and Γ, X <: S₁₁ ⊢ S₁₂ <: T₁₂.
|
||
By S-Trans, Γ ⊢ T₂ <: S₁₁.
|
||
By TA-TApp, we have Γ ⊢> t₁ [T₂] : S₁₂[X ↦ T₂].
|
||
Finally, we have Γ ⊢ S₁₂[X ↦ T₂] <: T₁₂[X ↦ T₂] by preservation of subtyping under substitution.
|
||
|
||
**Exercise 28.7.1**:
|
||
It seems to me that you would also need to compute a *maximal X-free subtype*,
|
||
which I'll call Q{X,Γ}(T), defined mutually with R{X,Γ}(T)
|
||
both by recursion on the type.
|
||
|
||
```
|
||
R{X,Γ} : Type → Type
|
||
Q{X,Γ} : Option Type → Type
|
||
|
||
R{X,Γ}(Y) ≜ if X == Y then ⊤ else Y
|
||
R{X,Γ}(S → T) ≜
|
||
case Q{X,Γ}(S) of
|
||
some S' ⇒ S' → R{X,Γ}(T)
|
||
none ⇒ ⊤
|
||
R{X,Γ}(∀Y <: U. T) ≜ ∀Y <: U. R{X,Γ}(T)
|
||
R{X,Γ}(∃Y <: S. T) ≜ ∃Y <: R{X,Γ}(S). R{X,Γ}(T)
|
||
|
||
Q{X,Γ}(Y) ≜ if X == Y then none else some Y
|
||
Q{X,Γ}(S → T) ≜
|
||
case Q{X,Γ}(T) of
|
||
some T' ⇒ R{X,Γ}(S) → T'
|
||
none ⇒ none
|
||
Q{X,Γ}(∀Y <: U. T) ≜ ∀Y <: U. Q{X,Γ}(T)
|
||
Q{X,Γ}(∃Y <: S. T) ≜ ∃Y <: Q{X,Γ}(S). Q{X,Γ}(T)
|
||
``` |