「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

t ::= tru | fls | test t then t else t | zro | scc t | prd t | iszro t

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.

Hint Constructors bvalue nvalue.
Hint Unfold value.
Hint Unfold update.

S.O.S

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

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

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

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

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

| T_Test : ∀t1 t2 t3 T,     (** <--- explicit ∀ T **)
       ⊢ t1 ∈ Bool →
       ⊢ t2 ∈ T →
       ⊢ t3 ∈ T →
       ⊢ test t1 t2 t3 ∈ T

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

类型关系是一个保守的（或静态的）近似

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 (可进性)

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 (维型性)

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

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.

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:

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

The proof is weird tho.