「SF-PLF」6 Types

This chapter:

  • typing relation – 定型关系
  • type preservation and progress (i.e. soundness proof) – 类型保留,可进性

Typed Arithmetic Expressions (Toy Typed Language)

The toy lang from SmallStep is too “safe” to demonstrate any runtime (or dynamic) type errors. – 运行时类型错误
So that’s add some operations (common church numeral ones), and bool type.

…same teaching order as TAPL. In PLT, we went directly to STLC.

Syntax

1
t ::= tru | fls | test t then t else t | zro | scc t | prd t | iszro t
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
Inductive tm : Type :=
| tru : tm
| fls : tm
| test : tm → tm → tm → tm
| zro : tm
| scc : tm → tm
| prd : tm → tm
| iszro : tm → tm.

(* object language has its own bool / nat , 这里不使用 Coq (meta-language) 比较 pure 一些? *)
Inductive bvalue : tm → Prop :=
| bv_tru : bvalue tru
| bv_fls : bvalue fls.
Inductive nvalue : tm → Prop :=
| nv_zro : nvalue zro
| nv_scc : ∀t, nvalue t → nvalue (scc t). (** 注意这里 nv_scc 是描述所有 [scc t] 是 nvalue 的一个 constructor / tag **)

(* [value?] predicate *)
Definition value (t : tm) := bvalue t ∨ nvalue t.

Automation

Hint are added to database to help with auto.
More details on auto. eapply. eauto. were mentioned in lf/Auto.

1
2
3
Hint Constructors bvalue nvalue.
Hint Unfold value.
Hint Unfold update.

S.O.S

Small-step operational semantics…
can be made formally in Coq code:

1
2
3
4
5
Reserved Notation "t1 '-->' t2" (at level 40).
Inductive step : tm → tm → Prop :=
| ST_TestTru : ∀t1 t2,
(test tru t1 t2) --> t1
...

“is stuck” vs. “can get stuck” 卡住的项 vs. 将会卡住的项

Noticed that the small-step semantics doesn’t care about if some term would eventually get stuck.

Normal Forms and Values

因为这个语言有 stuck 的情况,所以 value != normal form (terms cannot make progress)
possible_results_of_reduction = value | stuck

1
2
3
Notation step_normal_form := (normal_form step).
Definition stuck (t : tm) : Prop :=
step_normal_form t ∧ ¬value t.

Slide Q&A 1

  1. Yes
  2. No scc zro is a value
  3. No is a value

Typing

1
2
3
Inductive ty : Type :=
| Bool : ty
| Nat : ty.

Noticed that it’s just a non-dependently-typed ADT, but : ty is written explcitly here…they are the same!

Typing Relations

okay the funny thing…
it make sense to use here since : has been used by Coq.
but this notation is actually represented as \in.
We suddenly switch to LaTex mode…

1
Reserved Notation "'|-' t '\in' T" (at level 40).

Noticed the generic T here.
In PLT we sometimes treat them as “magic” meta variable, here we need to make the T explcit (we are in the meta-language).

⊢ t1 ∈ Bool    ⊢ t2 ∈ T    ⊢ t3 ∈ T	
----------------------------------  (T_Test)
  ⊢ test t1 then t2 else t3 ∈ T
1
2
3
4
5
| T_Test : ∀t1 t2 t3 T,     (** <--- explicit ∀ T **)
⊢ t1 ∈ Bool →
⊢ t2 ∈ T →
⊢ t3 ∈ T →
⊢ test t1 t2 t3 ∈ T
1
2
3
4
5
6
7
8
9
Example has_type_1 :
⊢ test fls zro (scc zro) ∈ Nat.
Proof.
apply T_Test. (** <--- we already know [T] from the return type [Nat] **)
- apply T_Fls. (** ⊢ _ ∈ Bool **)
- apply T_Zro. (** ⊢ _ ∈ Nat **)
- apply T_Scc. (** ⊢ _ ∈ Nat **)
+ apply T_Zro.
Qed.

(Since we’ve included all the constructors of the typing relation in the hint database, the auto tactic can actually find this proof automatically.)

typing relation is a conservative (or static) approximation

类型关系是一个保守的(或静态的)近似

1
2
3
4
Example has_type_not :
¬( ⊢ test fls zro tru ∈ Bool ).
Proof.
intros Contra. solve_by_inverts 2. Qed. (** 2-depth inversions **)

Lemma Canonical Forms 典范形式

As PLT.

Progress (可进性)

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

Progress vs Strong Progress?
Progress require the “well-typeness”!

Induction on typing relation.

Slide Q&A

  • partial function yes
  • total function no
    • thinking as our inference rules.
    • we could construct some terms that no inference rules can apply and get stucked.

Type Preservation (维型性)

1
2
3
4
Theorem preservation : ∀t t' T,
⊢ t ∈ T → (** HT **)
t --> t' → (** HE **)
⊢ t' ∈ T. (** HT' **)

按 PLT 的思路 Induction on HT,需要 inversion HE 去枚举所有情况拿到 t’ 之后证明 HT’
按 PFPL 的思路 Inudction on HE, 只需 inversion HT,因为 HT 是按 reduction 相反方向定义的!

  • reduction 方向,AST top-down e.g. (+ 5 5) —–> 10
  • typing 方向,AST bottom-up e.g. |- ..:N |—– |- (+ 5 5):N
1
2
3
4
5
6
7
Proof with eauto.
intros t t' T HT HE.
generalize dependent T.
induction HE; intros T HT;
inversion HT; subst...
apply nvalue_in_nat... (** 除了 ST_PrdScc 全部 inversion 解决... **)
Qed.

The preservation theorem is often called subject reduction, – 主语化简
想象 term 是主语,仅仅 term 在化简,而谓语宾语不变

one might wonder whether the opposity property — subject expansion — also holds. – 主语拓张
No, 我们可以很容易从 (test tru zro fls) 证明出 |- fls \in Nat. – 停机问题 (undecidable)

Type Soundness (Type Safety)

a well-typed term never get stuck.

1
2
3
4
5
6
7
8
9
10
11
12
Definition multistep := (multi step).  (** <--- from SmallStep **)
Notation "t1 '-->*' t2" := (multistep t1 t2) (at level 40).

Corollary soundness : ∀t t' T,
⊢ t ∈ T →
t -->* t' →
~(stuck t').
Proof.
intros t t' T HT P. induction P; intros [R S].
destruct (progress x T HT); auto.
apply IHP. apply (preservation x y T HT H).
unfold stuck. split; auto. Qed.

Induction on -->*, the multi-step derivation. (i.e. the reflexive-transtive closure)

Noticed that in PLT, we explcitly write out what is “non-stuck”.
But here is ~(stuck t')
thus the proof becomes:

1
2
3
4
R : step_normal_form x    (** normal form **)
S : ~ value x (** and not value **)
=======================
False (** prove this is False **)

The proof is weird tho.