# 「SF-PLF」8 StlcProp

## Programming Language Foundations - Properties of STLC

Posted by Hux on March 8, 2019

Type Safety

• Progress
• Canonical Forms (one for each type of value)
• Preservation
• Substituion
• Context Invariance (in PLT, Exchange, and Weakening)

## Canonical Forms

1
2
3
4
5
6
7
8
9
Lemma canonical_forms_bool : ∀t,
empty ⊢ t ∈ Bool →
value t →
(t = tru) ∨ (t = fls).

Lemma canonical_forms_fun : ∀t T1 T2,
empty ⊢ t ∈ (Arrow T1 T2) →
value t →
∃x u, t = abs x T1 u.


## Progress

1
2
3
Theorem progress : ∀t T,
empty ⊢ t ∈ T →
value t ∨ ∃t', t --> t'.


1. induction on typing relation
2. induction on term

• auto 上来就用把 tru, fls, abs 三个 value 的 case 干掉了，
• take step 的 case 则需要 witness 一个 t', 这时候 Canonical Form 就派上用场了

## Preservation

preservation theorem

• induction on typing; prove it type-preserving after reduction/evaluation (what about induction on reduction?)
• ST_AppAbs 比较麻烦，需要做 substitution，所以我们需要证明 substituion 本身是 type-preserving… substitution lemma
• induction on term; prove it type-preserving after a substitution
• 替换会将 bound var 加入 Context，所以我们需要证明 free var 对于新的 Context 仍然是 type-preserving…
• 这里我们需要 the formal definition of free var as well. context invariance
• exchange : 交换顺序显然无影响
• weakening : 如果不是 override 的话，添加新变量显然对于之前的 well-typeness 无影响

### Free Occurrences

1
2
3
FV(x) = {x}
FV(λx.t1) = FV(t1) ∪ FV(t2)
FV(t1 t2) = FV(t1) \ {x}


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
Inductive appears_free_in : string → tm → Prop :=
| afi_var : ∀x,
appears_free_in x (var x)
| afi_app1 : ∀x t1 t2,
appears_free_in x t1 →
appears_free_in x (app t1 t2)
| afi_app2 : ∀x t1 t2,
appears_free_in x t2 →
appears_free_in x (app t1 t2)
| afi_abs : ∀x y T11 t12,
y ≠ x →
appears_free_in x t12 →
appears_free_in x (abs y T11 t12)
(** 省略 test **)
...

Hint Constructors appears_free_in.

(** a term with no free vars. 等价于 ¬(∃x,  appears_free_in x t). **)
Definition closed (t:tm) :=           ∀x, ¬appears_free_in x t.


An open term is one that may contain free variables.
“Open” precisely means “possibly containing free variables.”

the closed terms are a subset of the open ones. closed 是 open 的子集…这样定义吗（

### Free Vars is in Context

1
2
3
4
Lemma free_in_context : ∀x t T Gamma,   (** 名字有一点 misleading，意思是 "free vars is in context" 而不是 "var is free in context"... **)
appears_free_in x t →
Gamma ⊢ t ∈ T →
∃T', Gamma x = Some T'.


1
2
3
Corollary typable_empty__closed : ∀t T,
empty ⊢ t ∈ T →
closed t.


### Context Invariance 上下文的一些「不变式」

PLT 的 Weaking 和 Exchanging 其实就对应了 Gamma 作为 partial_mapneqpermute 这里，我们直接进一步地证明 「term 的 well-typeness 在『free var 的值不变的 context 变化下』是 preserving 得」:

1
2
3
4
Lemma context_invariance : ∀Gamma Gamma' t T,
Gamma ⊢ t ∈ T →
(∀x, appears_free_in x t → Gamma x = Gamma' x) →    (** <-- 这句的意思是：对于 freevar，我们有其值不变。（如果没有括号就变成所有值都不变了……）**)
Gamma' ⊢ t ∈ T.


### Substitution!

1
2
3
4
Lemma substitution_preserves_typing : ∀Gamma x U t v T,
(x ⊢> U ; Gamma) ⊢ t ∈ T →
empty ⊢ v ∈ U →              (** 这里我们其实 assume 被替换进来的项，即「参数」，是 closed 得。这是一个简化的版本 **)
Gamma ⊢ [x:=v]t ∈ T.


Proof by induction on term 不好证，挺麻烦的

### Finally, Preservation

1
2
3
4
Theorem preservation : ∀t t' T,
empty ⊢ t ∈ T →
t --> t' →
empty ⊢ t' ∈ T.


### Not subject expansion

1
2
Theorem not_subject_expansion:
~(forall t t' T, t --> t' /\ empty |- t' \in T -> empty |- t \in T).

1
2
3
4
5
6
(app (abs x (Arrow Bool Bool) tru) tru)  -- 考虑 term

(λx:Bool->Bool . tru) tru   -->   tru    -- 可以 step
empty   |-   Bool    -- step 后 well-typed

empty |-/-  (λx:Bool->Bool . tru) tru    -- 但是原 term 显然 ill-typed


## Type Soundness

1
2
3
4
5
6
7
8
9
(** stuck 即在不是 value 的时候无法 step **)
Definition stuck (t:tm) : Prop :=
(normal_form step) t ∧ ¬value t.

(** well-typed term never get stuck! **)
Corollary soundness : ∀t t' T,
empty ⊢ t ∈ T →
t -->* t' →
~(stuck t').


## Uniqueness of Types

1
2
3
4
Theorem unique_types : ∀Gamma e T T',
Gamma ⊢ e ∈ T →
Gamma ⊢ e ∈ T' →
T = T'.


### STLC with Arithmetic

only Nat…这样就不用管 the interaction between Bool and Nat

1
2
3
4
5
6
7
8
9
10
11
12
13
14
Inductive ty : Type :=
| Arrow : ty → ty → ty
| Nat : ty.            (** <-- the only concrete base type **)

Inductive tm : Type :=
| var : string → tm
| app : tm → tm → tm
| abs : string → ty → tm → tm
| const : nat → tm     (** <-- 居然用 metalang 的 nat 而非 zro **)
| scc : tm → tm
| prd : tm → tm
| mlt : tm → tm → tm
| test0 : tm → tm → tm → tm.