「SF-PLF」8 StlcProp

基本的定理依赖关系 top-down:

Type Safety

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

Canonical Forms

对于我们只有 bool 一个 base type 的 STLC,只需要 boolλ:

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'.

类似 Types 章节的 progress 和 PLT 中的 proof.

  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

在 PLT/TAPL 中,我们将 “free variables of an term” 定义为一个集合 FV(t). (集合是一种 computational 的概念)

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

在这里,我们则将 “appears_free in” 定义为 var x 与 term t 上的二元关系: (读作 judgement 即可)

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

首先我们需要一个「free var 都是 well-typed 」的 lemma

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'.

由此我们可以推论 所有在 empty context 下 well typed 的 term 都是 closed 得:

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.

可以被看做一种交换律 (“commutation property”)
即先 type check 再 substitution 和 先 substition 再 type check 是等价的

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).
(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

这里的 Uniqueness 与 Right-unique / deterministic / functional 其实都是相同的内涵

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

Additional Exercises

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.

更多拓展见下一章 MoreStlc.v