「SF

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

1
2
3
⊢ 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.