michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

halfway through updating LambdaProp to PCF

Browse source
This commit is contained in:
wadler 2018-05-21 13:48:33 -03:00
parent cab70cb41e
commit ebc9832f29
2 changed files with 149 additions and 260 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

35
src/Lambda.lagda
View file

@ -262,15 +262,15 @@ The predicate `Value M` holds if term `M` is a value.
\begin{code}
data Value : Term → Set where
value-ƛ : ∀ {x N}
V-ƛ : ∀ {x N}
---------------
→ Value (ƛ x ⇒ N)
value-zero :
V-zero :
-----------
Value `zero
value-suc : ∀ {V}
V-suc : ∀ {V}
→ Value V
--------------
→ Value (`suc V)
@ -472,42 +472,42 @@ infix 4 _⟹_
data _⟹_ : Term → Term → Set where
ξ·₁ : ∀ {L L′ M}
ξ-·₁ : ∀ {L L′ M}
→ L ⟹ L′
-----------------
→ L · M ⟹ L′ · M
ξ·₂ : ∀ {V M M′}
ξ-·₂ : ∀ {V M M′}
→ Value V
→ M ⟹ M′
-----------------
→ V · M ⟹ V · M′
βλ· : ∀ {x N V}
β-ƛ· : ∀ {x N V}
→ Value V
------------------------------
→ (ƛ x ⇒ N) · V ⟹ N [ x := V ]
ξsuc : ∀ {M M′}
ξ-suc : ∀ {M M′}
→ M ⟹ M′
------------------
→ `suc M ⟹ `suc M′
ξcase : ∀ {x L L′ M N}
ξ-case : ∀ {x L L′ M N}
→ L ⟹ L′
-----------------------------------------------------------------
→ `case L [zero⇒ M |suc x ⇒ N ] ⟹ `case L′ [zero⇒ M |suc x ⇒ N ]
βcase-zero : ∀ {x M N}
β-case-zero : ∀ {x M N}
----------------------------------------
→ `case `zero [zero⇒ M |suc x ⇒ N ] ⟹ M
βcase-suc : ∀ {x V M N}
β-case-suc : ∀ {x V M N}
→ Value V
---------------------------------------------------
→ `case `suc V [zero⇒ M |suc x ⇒ N ] ⟹ N [ x := V ]
βμ : ∀ {x M}
β-μ : ∀ {x M}
------------------------------
→ μ x ⇒ M ⟹ M [ x := μ x ⇒ M ]
\end{code}
@ -714,16 +714,16 @@ the rules for typing are written as follows.
-------------- ⇒-E
Γ ⊢ L · M ⦂ B
------------- `ℕ-I₁
------------- ℕ-I₁
Γ ⊢ true ⦂ `ℕ
-------------- `ℕ-I₂
-------------- ℕ-I₂
Γ ⊢ false ⦂ `ℕ
Γ ⊢ L : `ℕ
Γ ⊢ M ⦂ A
Γ ⊢ N ⦂ A
-------------------------- `ℕ-E
-------------------------- ℕ-E
Γ ⊢ if L then M else N ⦂ A
As we will show later, the rules are deterministic, in that
@ -791,12 +791,17 @@ data _⊢_⦂_ : Context → Term → Type → Set where
---------------
→ Γ ⊢ `suc M ⦂ `ℕ
`ℕ-E : ∀ {Γ L M x N A}
ℕ-E : ∀ {Γ L M x N A}
→ Γ ⊢ L ⦂ `ℕ
→ Γ ⊢ M ⦂ A
→ Γ , x ⦂ `ℕ ⊢ N ⦂ A
--------------------------------------
→ Γ ⊢ `case L [zero⇒ M |suc x ⇒ N ] ⦂ A
Fix : ∀ {Γ x M A}
→ Γ , x ⦂ A ⊢ M ⦂ A
------------------
→ Γ ⊢ μ x ⇒ M ⦂ A
\end{code}
### Example type derivations

374
src/LambdaProp.lagda
View file

@ -21,7 +21,7 @@ open import Data.Product
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Function using (_∘_)
open import StlcNew
open import Lambda
\end{code}
@ -33,18 +33,43 @@ belonging to each type. For function types the canonical forms are lambda-abstr
while for boolean types they are values `true` and `false`.
\begin{code}
data canonical_for_ : Term → Type → Set where
canonical-λ : ∀ {x A N B} → canonical (ƛ x ⇒ N) for (A ⇒ B)
canonical-true : canonical true for 𝔹
canonical-false : canonical false for 𝔹
infix 4 Canonical_⦂_
canonical-forms : ∀ {L A} → ∅ ⊢ L ⦂ A → Value L → canonical L for A
canonical-forms (Ax ()) ()
canonical-forms (⇒-I ⊢N) value-λ = canonical-λ
canonical-forms (⇒-E ⊢L ⊢M) ()
canonical-forms 𝔹-I₁ value-true = canonical-true
canonical-forms 𝔹-I₂ value-false = canonical-false
canonical-forms (𝔹-E ⊢L ⊢M ⊢N) ()
data Canonical_⦂_ : Term → Type → Set where
C-ƛ : ∀ {x A N B}
-----------------------------
→ Canonical (ƛ x ⇒ N) ⦂ (A ⇒ B)
C-zero :
--------------------
Canonical `zero ⦂ `ℕ
C-suc : ∀ {V}
→ Canonical V ⦂ `ℕ
---------------------
→ Canonical `suc V ⦂ `ℕ
canonical : ∀ {M A}
→ ∅ ⊢ M ⦂ A
→ Value M
---------------
→ Canonical M ⦂ A
canonical (Ax ()) ()
canonical (⇒-I ⊢N) V-ƛ = C-ƛ
canonical (⇒-E ⊢L ⊢M) ()
canonical ℕ-I₁ V-zero = C-zero
canonical (ℕ-I₂ ⊢V) (V-suc VV) = C-suc (canonical ⊢V VV)
canonical (ℕ-E ⊢L ⊢M ⊢N) ()
canonical (Fix ⊢M) ()
value : ∀ {M A}
→ Canonical M ⦂ A
----------------
→ Value M
value C-ƛ = V-ƛ
value C-zero = V-zero
value (C-suc CM) = V-suc (value CM)
\end{code}
## Progress
@ -55,73 +80,39 @@ step or it is a value.
\begin{code}
data Progress (M : Term) : Set where
steps : ∀ {N} → M ⟹ N → Progress M
done : Value M → Progress M
progress : ∀ {M A} → ∅ ⊢ M ⦂ A → Progress M
\end{code}
steps : ∀ {N}
→ M ⟹ N
----------
→ Progress M
We give the proof in English first, then the formal version.
done :
Value M
----------
→ Progress M
_Proof_: By induction on the derivation of `∅ ⊢ M ⦂ A`.
- The last rule of the derivation cannot be `Ax`,
since a variable is never well typed in an empty context.
- If the last rule of the derivation is `⇒-I`, `𝔹-I₁`, or `𝔹-I₂`
then, trivially, the term is a value.
- If the last rule of the derivation is `⇒-E`, then the term has the
form `L · M` for some `L` and `M`, where we know that `L` and `M`
are also well typed in the empty context, giving us two induction
hypotheses. By the first induction hypothesis, either `L`
can take a step or is a value.
- If `L` can take a step, then so can `L · M` by `ξ·₁`.
- If `L` is a value then consider `M`. By the second induction
hypothesis, either `M` can take a step or is a value.
- If `M` can take a step, then so can `L · M` by `ξ·₂`.
- If `M` is a value, then since `L` is a value with a
function type we know from the canonical forms lemma
that it must be a lambda abstraction,
and hence `L · M` can take a step by `βλ·`.
- If the last rule of the derivation is `𝔹-E`, then the term has
the form `if L then M else N` where `L` has type `𝔹`.
By the induction hypothesis, either `L` can take a step or is
a value.
- If `L` can take a step, then so can `if L then M else N` by `ξif`.
- If `L` is a value, then since it has type boolean we know from
the canonical forms lemma that it must be either `true` or
`false`.
- If `L` is `true`, then `if L then M else N` steps by `βif-true`
- If `L` is `false`, then `if L then M else N` steps by `βif-false`
This completes the proof.
\begin{code}
progress : ∀ {M A}
→ ∅ ⊢ M ⦂ A
----------
→ Progress M
progress (Ax ())
progress (⇒-I ⊢N) = done value-λ
progress (⇒-I ⊢N) = done V-ƛ
progress (⇒-E ⊢L ⊢M) with progress ⊢L
... | steps L⟹L′ = steps (ξ·₁ L⟹L′)
... | done valueL with progress ⊢M
... | steps M⟹M′ = steps (ξ·₂ valueL M⟹M′)
... | done valueM with canonical-forms ⊢L valueL
... | canonical-λ = steps (βλ· valueM)
progress 𝔹-I₁ = done value-true
progress 𝔹-I₂ = done value-false
progress (𝔹-E ⊢L ⊢M ⊢N) with progress ⊢L
... | steps L⟹L′ = steps (ξif L⟹L′)
... | done valueL with canonical-forms ⊢L valueL
... | canonical-true = steps βif-true
... | canonical-false = steps βif-false
... | steps L⟹L′ = steps (ξ-·₁ L⟹L′)
... | done VL with progress ⊢M
... | steps M⟹M′ = steps (ξ-·₂ VL M⟹M′)
... | done VM with canonical ⊢L VL
... | C-ƛ = steps (β-ƛ· VM)
progress ℕ-I₁ = done V-zero
progress (ℕ-I₂ ⊢M) with progress ⊢M
... | steps M⟹M′ = steps (ξ-suc M⟹M′)
... | done VM = done (V-suc VM)
progress (ℕ-E ⊢L ⊢M ⊢N) with progress ⊢L
... | steps L⟹L′ = steps (ξ-case L⟹L′)
... | done VL with canonical ⊢L VL
... | C-zero = steps β-case-zero
... | C-suc CL = steps (β-case-suc (value CL))
progress (Fix ⊢M) = steps β-μ
\end{code}
This code reads neatly in part because we consider the
@ -142,7 +133,7 @@ postulate
progress′ : ∀ M {A} → ∅ ⊢ M ⦂ A → Progress M
\end{code}
## Preservation
## Prelude to preservation
The other half of the type soundness property is the preservation
of types during reduction. For this, we need to develop
@ -152,157 +143,38 @@ property we are actually interested in to the lowest-level
technical lemmas), the story goes like this:
- The _preservation theorem_ is proved by induction on a typing derivation.
derivation, pretty much as we did in chapter [Types]({{ "Types" | relative_url }})
- The one case that is significantly different is the one for the
`βλ·` rule, whose definition uses the substitution operation. To see that
The definition of `β-ƛ· uses substitution. To see that
this step preserves typing, we need to know that the substitution itself
does. So we prove a ...
- _substitution lemma_, stating that substituting a (closed) term
`V` for a variable `x` in a term `N` preserves the type of `N`.
The proof goes by induction on the form of `N` and requires
looking at all the different cases in the definition of
substitition. The lemma does not require that `V` be a value,
The proof goes by induction on the typing derivation of `N`.
The lemma does not require that `V` be a value,
though in practice we only substitute values. The tricky cases
are the ones for variables and for function abstractions. In both
cases, we discover that we need to take a term `V` that has been
are the ones for variables and those that do binding, namely,
function abstraction, case over a natural, and fixpoints. In each
case, we discover that we need to take a term `V` that has been
shown to be well-typed in some context `Γ` and consider the same
term in a different context `Γ′`. For this we prove a ...
term in a different context `Δ`. For this we prove a ...
- _context invariance_ lemma, showing that typing is preserved
under "inessential changes" to the context---a term `M`
well typed in `Γ` is also well typed in `Γ′`, so long as
all the free variables of `M` appear in both contexts.
And finally, for this, we need a careful definition of ...
- _free variables_ of a term---i.e., those variables
mentioned in a term and not bound in an enclosing
lambda abstraction.
- _renaming lemma_, showing that typing is preserved
under weakening of the context---a term `M`
well typed in `Γ` is also well typed in `Δ`, so long as
every free variable found in `Γ` is also found in `Δ`.
To make Agda happy, we need to formalize the story in the opposite
order.
### Free Occurrences
A variable `x` appears _free_ in a term `M` if `M` contains an
occurrence of `x` that is not bound in an enclosing lambda abstraction.
For example:
- Variable `x` appears free, but `f` does not, in ``ƛ "f" ⇒ # "f" · # "x"``.
- Both `f` and `x` appear free in ``(ƛ "f" ⇒ # "f" · # "x") · # "f"``.
Indeed, `f` appears both bound and free in this term.
- No variables appear free in ``ƛ "f" ⇒ ƛ "x" ⇒ # "f" · # "x"``.
Formally:
\begin{code}
data _∈_ : Id → Term → Set where
free-# : ∀ {x} → x ∈ # x
free-ƛ : ∀ {w x N} → w ≢ x → w ∈ N → w ∈ (ƛ x ⇒ N)
free-·₁ : ∀ {w L M} → w ∈ L → w ∈ (L · M)
free-·₂ : ∀ {w L M} → w ∈ M → w ∈ (L · M)
free-if₁ : ∀ {w L M N} → w ∈ L → w ∈ (if L then M else N)
free-if₂ : ∀ {w L M N} → w ∈ M → w ∈ (if L then M else N)
free-if₃ : ∀ {w L M N} → w ∈ N → w ∈ (if L then M else N)
\end{code}
A term in which no variables appear free is said to be _closed_.
\begin{code}
_∉_ : Id → Term → Set
x ∉ M = ¬ (x ∈ M)
closed : Term → Set
closed M = ∀ {x} → x ∉ M
\end{code}
Here are proofs corresponding to the first two examples above.
\begin{code}
x≢f : "x" ≢ "f"
x≢f ()
ex₃ : "x" ∈ (ƛ "f" ⇒ # "f" · # "x")
ex₃ = free-ƛ x≢f (free-·₂ free-#)
ex₄ : "f" ∉ (ƛ "f" ⇒ # "f" · # "x")
ex₄ (free-ƛ f≢f _) = f≢f refl
\end{code}
#### Exercise: 1 star (free-in)
Prove formally the remaining examples given above.
\begin{code}
postulate
ex₅ : "x" ∈ ((ƛ "f" ⇒ # "f" · # "x") · # "f")
ex₆ : "f" ∈ ((ƛ "f" ⇒ # "f" · # "x") · # "f")
ex₇ : "x" ∉ (ƛ "f" ⇒ ƛ "x" ⇒ # "f" · # "x")
ex₈ : "f" ∉ (ƛ "f" ⇒ ƛ "x" ⇒ # "f" · # "x")
\end{code}
Although `_∈_` may appear to be a low-level technical definition,
understanding it is crucial to understanding the properties of
substitution, which are really the crux of the lambda calculus.
### Substitution
To prove that substitution preserves typing, we first need a technical
lemma connecting free variables and typing contexts. If variable `x`
appears free in term `M`, and if `M` is well typed in context `Γ`,
then `Γ` must assign a type to `x`.
\begin{code}
free-lemma : ∀ {w M A Γ} → w ∈ M → Γ ⊢ M ⦂ A → ∃[ B ](Γ ∋ w ⦂ B)
free-lemma free-# (Ax {Γ} {w} {B} ∋w) = ⟨ B , ∋w ⟩
free-lemma (free-ƛ {w} {x} w≢ ∈N) (⇒-I ⊢N) with w ≟ x
... | yes refl = ⊥-elim (w≢ refl)
... | no _ with free-lemma ∈N ⊢N
... | ⟨ B , Z ⟩ = ⊥-elim (w≢ refl)
... | ⟨ B , S _ ∋w ⟩ = ⟨ B , ∋w ⟩
free-lemma (free-·₁ ∈L) (⇒-E ⊢L ⊢M) = free-lemma ∈L ⊢L
free-lemma (free-·₂ ∈M) (⇒-E ⊢L ⊢M) = free-lemma ∈M ⊢M
free-lemma (free-if₁ ∈L) (𝔹-E ⊢L ⊢M ⊢N) = free-lemma ∈L ⊢L
free-lemma (free-if₂ ∈M) (𝔹-E ⊢L ⊢M ⊢N) = free-lemma ∈M ⊢M
free-lemma (free-if₃ ∈N) (𝔹-E ⊢L ⊢M ⊢N) = free-lemma ∈N ⊢N
\end{code}
<!--
A subtle point: if the first argument of `free-λ` was of type
`x ≢ w` rather than of type `w ≢ x`, then the type of the
term `Γx≡C` would not simplify properly; instead, one would need
to rewrite with the symmetric equivalence.
-->
As a second technical lemma, we need that any term `M` which is well
typed in the empty context is closed (has no free variables).
#### Exercise: 2 stars, optional (∅⊢-closed)
\begin{code}
postulate
∅⊢-closed : ∀ {M A} → ∅ ⊢ M ⦂ A → closed M
\end{code}
<div class="hidden">
\begin{code}
∅-empty : ∀ {x A} → ¬ (∅ ∋ x ⦂ A)
∅-empty ()
∅⊢-closed′ : ∀ {M A} → ∅ ⊢ M ⦂ A → closed M
∅⊢-closed′ ⊢M ∈M with free-lemma ∈M ⊢M
... | ⟨ B , ∋w ⟩ = ∅-empty ∋w
\end{code}
</div>
### Renaming
Sometimes, when we have a proof `Γ ⊢ M ⦂ A`, we will need to
replace `Γ` by a different context `Γ′`. When is it safe
to do this? Intuitively, the only variables we care about
in the context are those that appear free in `M`. So long
as the two contexts agree on those variables, one can be
exchanged for the other.
replace `Γ` by a different context `Δ`. When is it safe
to do this? Intuitively, whenever every variable given a type
by `Γ` is also given a type by `Δ`.
*(((Need to explain ext)))*
\begin{code}
ext : ∀ {Γ Δ}
@ -316,15 +188,16 @@ rename : ∀ {Γ Δ}
→ (∀ {w B} → Γ ∋ w ⦂ B → Δ ∋ w ⦂ B)
----------------------------------
→ (∀ {M A} → Γ ⊢ M ⦂ A → Δ ⊢ M ⦂ A)
rename σ (Ax ∋w) = Ax (σ ∋w)
rename σ (⇒-I ⊢N) = ⇒-I (rename (ext σ) ⊢N)
rename σ (⇒-E ⊢L ⊢M) = ⇒-E (rename σ ⊢L) (rename σ ⊢M)
rename σ 𝔹-I₁ = 𝔹-I₁
rename σ 𝔹-I₂ = 𝔹-I₂
rename σ (𝔹-E ⊢L ⊢M ⊢N) = 𝔹-E (rename σ ⊢L) (rename σ ⊢M) (rename σ ⊢N)
rename σ (Ax ∋w) = Ax (σ ∋w)
rename σ (⇒-I ⊢N) = ⇒-I (rename (ext σ) ⊢N)
rename σ (⇒-E ⊢L ⊢M) = ⇒-E (rename σ ⊢L) (rename σ ⊢M)
rename σ ℕ-I₁ = ℕ-I₁
rename σ (ℕ-I₂ ⊢M) = ℕ-I₂ (rename σ ⊢M)
rename σ (ℕ-E ⊢L ⊢M ⊢N) = ℕ-E (rename σ ⊢L) (rename σ ⊢M) (rename (ext σ) ⊢N)
rename σ (Fix ⊢M) = Fix (rename (ext σ) ⊢M)
\end{code}
We have three important corrolaries. First,
We have three important corollaries. First,
any closed term can be weakened to any context.
\begin{code}
rename-∅ : ∀ {Γ M A}
@ -340,7 +213,7 @@ rename-∅ {Γ} ⊢M = rename σ ⊢M
σ ()
\end{code}
Second, if the last two variable in a context are
Second, if the last two variables in a context are
equal, the term can be renamed to drop the redundant one.
\begin{code}
rename-≡ : ∀ {Γ x M A B C}
@ -377,6 +250,8 @@ rename-≢ {Γ} {x} {y} {M} {A} {B} {C} x≢y ⊢M = rename σ ⊢M
σ (S z≢x (S z≢y ∋z)) = S z≢y (S z≢x ∋z)
\end{code}
## Substitution
Now we come to the conceptual heart of the proof that reduction
preserves types---namely, the observation that _substitution_
@ -419,19 +294,25 @@ subst : ∀ {Γ x N V A B}
-----------------------
→ Γ ⊢ N [ x := V ] ⦂ B
subst {Γ} {y} {# x} (Ax Z) ⊢V with x ≟ y
... | yes refl = rename-∅ ⊢V
... | no x≢y = ⊥-elim (x≢y refl)
subst {Γ} {y} {# x} (Ax (S x≢y ∋x)) ⊢V with x ≟ y
... | yes refl = ⊥-elim (x≢y refl)
... | no _ = Ax ∋x
subst {Γ} {y} {ƛ x ⇒ N} (⇒-I ⊢N) ⊢V with x ≟ y
... | yes refl = ⇒-I (rename-≡ ⊢N)
... | no x≢y = ⇒-I (subst (rename-≢ x≢y ⊢N) ⊢V)
subst (⇒-E ⊢L ⊢M) ⊢V = ⇒-E (subst ⊢L ⊢V) (subst ⊢M ⊢V)
subst 𝔹-I₁ ⊢V = 𝔹-I₁
subst 𝔹-I₂ ⊢V = 𝔹-I₂
subst (𝔹-E ⊢L ⊢M ⊢N) ⊢V = 𝔹-E (subst ⊢L ⊢V) (subst ⊢M ⊢V) (subst ⊢N ⊢V)
subst {x = y} (Ax {x = x} Z) ⊢V with x ≟ y
... | yes refl = rename-∅ ⊢V
... | no x≢y = ⊥-elim (x≢y refl)
subst {x = y} (Ax {x = x} (S x≢y ∋x)) ⊢V with x ≟ y
... | yes refl = ⊥-elim (x≢y refl)
... | no _ = Ax ∋x
subst {x = y} (⇒-I {x = x} ⊢N) ⊢V with x ≟ y
... | yes refl = ⇒-I (rename-≡ ⊢N)
... | no x≢y = ⇒-I (subst (rename-≢ x≢y ⊢N) ⊢V)
subst (⇒-E ⊢L ⊢M) ⊢V = ⇒-E (subst ⊢L ⊢V) (subst ⊢M ⊢V)
subst ℕ-I₁ ⊢V = ℕ-I₁
subst (ℕ-I₂ ⊢M) ⊢V = ℕ-I₂ (subst ⊢M ⊢V)
subst {x = y} (ℕ-E {x = x} ⊢L ⊢M ⊢N) ⊢V with x ≟ y
... | yes refl = ℕ-E (subst ⊢L ⊢V) (subst ⊢M ⊢V) (rename-≡ ⊢N)
... | no x≢y = ℕ-E (subst ⊢L ⊢V) (subst ⊢M ⊢V) (subst (rename-≢ x≢y ⊢N) ⊢V)
subst {x = y} (Fix {x = x} ⊢M) ⊢V with x ≟ y
... | yes refl = Fix (rename-≡ ⊢M)
... | no x≢y = Fix (subst (rename-≢ x≢y ⊢M) ⊢V)
{-
\end{code}
@ -451,12 +332,12 @@ preservation (⇒-E ⊢L ⊢M) (ξ·₁ L⟹L′) with preservation ⊢L L⟹L
preservation (⇒-E ⊢L ⊢M) (ξ·₂ valueL M⟹M′) with preservation ⊢M M⟹M′
... | ⊢M′ = ⇒-E ⊢L ⊢M′
preservation (⇒-E (⇒-I ⊢N) ⊢V) (βλ· valueV) = subst ⊢N ⊢V
preservation 𝔹-I₁ ()
preservation 𝔹-I₂ ()
preservation (𝔹-E ⊢L ⊢M ⊢N) (ξif L⟹L′) with preservation ⊢L L⟹L′
... | ⊢L′ = 𝔹-E ⊢L′ ⊢M ⊢N
preservation (𝔹-E 𝔹-I₁ ⊢M ⊢N) βif-true = ⊢M
preservation (𝔹-E 𝔹-I₂ ⊢M ⊢N) βif-false = ⊢N
preservation `ℕ-I₁ ()
preservation `ℕ-I₂ ()
preservation (`ℕ-E ⊢L ⊢M ⊢N) (ξif L⟹L′) with preservation ⊢L L⟹L′
... | ⊢L′ = `ℕ-E ⊢L′ ⊢M ⊢N
preservation (`ℕ-E `ℕ-I₁ ⊢M ⊢N) βif-true = ⊢M
preservation (`ℕ-E `ℕ-I₂ ⊢M ⊢N) βif-false = ⊢N
\end{code}
@ -600,10 +481,10 @@ false, give a counterexample.
Suppose instead that we add the following new rule to the typing
relation:
Γ ⊢ L ⦂ 𝔹 ⇒ 𝔹 ⇒ 𝔹
Γ ⊢ M ⦂ 𝔹
Γ ⊢ L ⦂ `ℕ ⇒ `ℕ ⇒ `ℕ
Γ ⊢ M ⦂ `ℕ
------------------------------ (T_FunnyApp)
Γ ⊢ L · M ⦂ 𝔹
Γ ⊢ L · M ⦂ `ℕ
Which of the following properties of the STLC remain true in
the presence of this rule? For each one, write either
@ -622,10 +503,10 @@ false, give a counterexample.
Suppose instead that we add the following new rule to the typing
relation:
Γ ⊢ L ⦂ 𝔹
Γ ⊢ M ⦂ 𝔹
Γ ⊢ L ⦂ `ℕ
Γ ⊢ M ⦂ `ℕ
--------------------- (T_FunnyApp')
Γ ⊢ L · M ⦂ 𝔹
Γ ⊢ L · M ⦂ `ℕ
Which of the following properties of the STLC remain true in
the presence of this rule? For each one, write either
@ -646,7 +527,7 @@ Suppose we add the following new rule to the typing relation
of the STLC:
-------------------- (T_FunnyAbs)
∅ ⊢ λ[ x ⦂ 𝔹 ] N ⦂ 𝔹
∅ ⊢ λ[ x ⦂ `ℕ ] N ⦂ `ℕ
Which of the following properties of the STLC remain true in
the presence of this rule? For each one, write either
@ -660,3 +541,6 @@ false, give a counterexample.
- Preservation
\begin{code}
-}
\end{code}