平时使用 Windows 时总结的一些实用的小技巧。

为基于 xulrunner 为内嵌 Gecko 程序启用 Profile

• auto - proof search
• Ltac - automated forward reasoning (hypothesis matching machinery)
• eauto, eapply - deferred instantiation of existentials

Ltac macro

1
2
3
4

Ltac inv H := inversion H; subst; clear H.

(** later in the proof... **)
inv H5.

The auto Tactic

auto can free us by searching for a sequence of applications that will prove the goal:

1
2
3
4
5
6

intros P Q R H1 H2 H3.
apply H2. apply H1. assumption.


(** can be replaced by... **)
auto.

auto solves goals that are solvable by any combination of

• intros
• apply (of hypotheses from the local context, by default)

使用 auto 一定是“安全”的，它不会失败，也不会改变当前证明的状态： auto 要么完全解决它，要么什么也不做。

Proof search could, in principle, take an arbitrarily long time,
so there are limits to how far auto will search by default. (i.e. 5)

1
2
3
4
5
6
7
8
9
10
11
12
13
14

Example auto_example_3 : ∀(P Q R S T U: Prop),
  (P → Q) →
  (Q → R) →
  (R → S) →
  (S → T) →
  (T → U) →
  P →
  U.
Proof.
  (* 当 auto 无法解决此目标时，它就什么也不做 *)
  auto.
  (* 可选的参数用来控制它的搜索深度（默认为 5）, 6 就刚好能解决了！ *)
  auto 6.
Qed.

Hint Database 提示数据库

auto auto considers a hint database of other lemmas and constructors.
common lemmas about equality and logical operators are installed by default.

just for the purposes of one application of auto
我们可以为某次 auto 的调用扩展提示数据库，auto using ...

1
2
3
4
5
6
7
8

Example auto_example_6 : ∀n m p : nat,
  (n ≤ p → (n ≤ m ∧ m ≤ n)) →
  n ≤ p →
  n = m.
Proof.
  intros.
  auto using le_antisym.
Qed.

Global Hint Database 添加到全局提示数据库

1
2
3
4
5

Hint Resolve T.          

Hint Constructors c.

Hint Unfold d.

Proof with auto.

Under Proof with t, t1... == t1; t.

Searching For Hypotheses

对于很常见的一种矛盾情形：

1
2

H1: beval st b = false
H2: beval st b = true

contradiction 并不能解决，必须 rewrite H1 in H2; inversion H2.

1. 宏：

1
2
3
4

Ltac rwinv H1 H2 := rewrite H1 in H2; inv H2.

(** later in the proof... **)
rwinv H H2.

2. match goal 调用宏

1
2
3
4
5
6
7
8
9
10
11
12
13
14

Ltac find_rwinv :=
  match goal with
    H1: ?E = true,
    H2: ?E = false
    ⊢ _ ⇒ rwinv H1 H2
  end.
  
(** later in the proof... **)
induction E1; intros st2 E2; inv E2; try find_rwinv; auto. (** 直接解决所有矛盾 case **)
- (* E_Seq *)
  rewrite (IHE1_1 st'0 H1) in *. auto.
- (* E_WhileTrue *)
  + (* b 求值为 true *)
    rewrite (IHE1_1 st'0 H3) in *. auto. Qed.

可以看到最后只剩这种改写形式…我们也把他们自动化了：

1
2
3
4
5
6

Ltac find_eqn :=
  match goal with
    H1: ∀x, ?P x → ?L = ?R,
    H2: ?P ?X
    ⊢ _ ⇒ rewrite (H1 X H2) in *
  end.

配合上 repeat…我们可以 keep doing useful rewrites until only trivial ones are left.
最终效果：

1
2
3
4
5
6
7
8
9
10
11

Theorem ceval_deterministic''''': ∀c st st1 st2,
    st =[ c ]⇒ st1 →
    st =[ c ]⇒ st2 →
    st1 = st2.
Proof.
  intros c st st1 st2 E1 E2.
  generalize dependent st2;
  induction E1; intros st2 E2; inv E2; 
    try find_rwinv;
    repeat find_eqn; auto.
Qed.

即使我们给 IMP 加上一个 CRepeat（其实就是 DO c WHILE b)，
会发现颠倒一下自动化的顺序就能 work 了

1
2
3

induction E1; intros st2 E2; inv E2; 
  repeat find_eqn; 
  try find_rwinv; auto.

当然，这种「超级自动化」(hyper-automation) 并不总是现实，也不好调试…

The eapply and eauto variants

推迟量词的实例化

比如对于

1
2
3
4
5
6
7
8
9
10
11
12
13
14

Example ceval_example1:
  empty_st =[
    X ::= 2;;
    TEST X ≤ 1
      THEN Y ::= 3
      ELSE Z ::= 4
    FI
  ]⇒ (Z !-> 4 ; X !-> 2).
Proof.
  (* 我们补充了中间状态 st'... *)
  apply E_Seq with (X !-> 2).
  - apply E_Ass. reflexivity.
  - apply E_IfFalse. reflexivity. apply E_Ass. reflexivity.
Qed.

没有 with 就会 Error: Unable to find an instance for the variable st'

但其实 st' 的取值在后面的步骤是很明显（很好 infer/unify）的，所以 eapply works.

issues on coqc module linking

Some module (e.g.Map) not found
either maunally make map.vo or proof general can solve that.

Behavioral Equivalence 行为等价

How to define the correctness of program transformation, e.g. optimize_0plus ?

• in the setting w/o var (imp w/o var and state) : yield a program the evals to same number as original.
• in the setting w/ var (full imp w/ assignment) : we need to consider the role of var and state.

Definitions

Two aexps or bexps are behaviorally equivalent if they evaluate to the same result in every state.

1
2
3
4

Definition aequiv (a1 a2 : aexp) : Prop :=
  ∀(st : state), aeval st a1 = aeval st a2.
Definition bequiv (b1 b2 : bexp) : Prop :=
  ∀(st : state), beval st b1 = beval st b2.

For commands, We can’t simply say … if they evaluate to the same ending state
some commands don’t terminate in any final state at all!

So to define, they either or…

1. both diverge 都发散
2. both terminate in the same final state 都在同一个状态停机

A compact way is

“if the first one terminates in a particular state then so does the second, and vice versa.”

1
2
3

Definition cequiv (c1 c2 : com) : Prop :=
  ∀(st st' : state),
    (st =[ c1 ]⇒ st') ↔ (st =[ c2 ]⇒ st'). 

Example 1 - Simple (but demonstrated)

1
2
3
4
5
6
7
8
9
10
11
12
13

Theorem skip_left : forall c,
  cequiv (SKIP;; c) c.
Proof.
  intros c st st'. split; intros H.
  - (* -> *)         
    inversion H; subst.  (* inverse E_Seq   *)
    inversion H2. subst. (* inverse E_Skip  *)
    assumption.
  - (* <- *)             (* reversely *)
    apply E_Seq with st. (* apply E_Seq *)
    apply E_Skip.        (* apply E_Skip *)
    assumption.
Qed.

Noticed that the inversion is like use the inverse function of constructors.

Example 2 - WHILE true non-terminating

one interesting theorem is that we can prove WHILE <things ⇓ true> is not terminating.
and is equivalent to any other non-terminating program, e.g. WHILE BTrue DO SKIP END: (因为我们的「等价」只要求同「发散」即可)

1
2
3
4
5

Theorem WHILE_true : ∀b c,
  bequiv b true →
  cequiv
    (WHILE b DO c END)
    (WHILE true DO SKIP END).

Example 3 - Loop Unrolling

any number of copies of the body can be “unrolled” without changing meaning

1
2
3
4

Theorem loop_unrolling : ∀b c,
  cequiv
    (WHILE b DO c END)         
    (TEST b THEN (c ;; WHILE b DO c END) ELSE SKIP FI).    (** 展开一层 **)

Example 4 - Use of extenionality 外延性

x !-> m x ; x is same map with m by extenionality!

1
2

Theorem identity_assignment : ∀x,
  cequiv (x ::= x) SKIP.

Properties of Behavioral Equivalence 行为等价的性质

等价关系 (Equivalence)

自反性（reflexive）、对称性（symmetric）和传递性 （transitive）

同余关系（Congruence）

That is, the equivalence of two subprograms implies the equivalence of the larger programs in which they are embedded
如果两个子程序等价，那么当二者所在的更大的程序中_只有二者不同_时， 这两个更大的程序也等价

          aequiv a1 a1'
  -----------------------------
  cequiv (x ::= a1) (x ::= a1')

          cequiv c1 c1'
          cequiv c2 c2'
     --------------------------
     cequiv (c1;;c2) (c1';;c2')

这个术语应该是来自抽象代数 : 能在运算下保持的等价关系
…in the sense that algebraic operations done with equivalent elements will yield equivalent elements.
Congruence relation

1
2
3
4

Theorem CAss_congruence : ∀x a1 a1',     (** cequiv 是集合 commands 上的等价关系 **)
  aequiv a1 a1' →
  cequiv (CAss x a1) (CAss x a1').       (** 在 `CAss` 这个 operation 下保持等价 => 同余 **)
  cequiv (x ::= a1) (x ::= a1').         (** 或，在 `::=` 这个 command 下保持等价 => 同余 **)

在 commands 上等价但不同余的关系?

I guess…”both terminating” relation?
which is equivalence relation on commands, but the equivalence would not be maintained after, say C_WHILE operation.

Example - Using Congruence

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28

Example congruence_example:
  cequiv
    (* 程序 1： *)
    (X ::= 0;;
     TEST X = 0
     THEN
       Y ::= 0
     ELSE
       Y ::= 42
     FI)
    (* 程序 2： *)
    (X ::= 0;;
     TEST X = 0
     THEN
       Y ::= X - X (* <--- 这里不同 *)
     ELSE
       Y ::= 42
     FI).
Proof.
  apply CSeq_congruence.
  - apply refl_cequiv.
  - apply CIf_congruence.
    + apply refl_bequiv.
    + apply CAss_congruence.     (** <--- 化简到只需要证明 aequiv 0 (X - X) **) 
      unfold aequiv. simpl.
      * symmetry. apply minus_diag.
    + apply refl_cequiv.
Qed.

Program Transformations 程序变换

A program transformation is sound if it preserves the behavior of the original program.
如果一个程序变换保留了其原始行为，那么它就是_可靠_的

我们可以定义在不同集合 aexp, bexp, com 上的 sound 关系：
(有趣的是，Inductive 定义的非 Prop 的 Type, 确实就是 Set, 这是一种 PL 和数学的 Correspondence)

• 当我们的 datatype 是 constructor 时 => 不交并
• 当我们的 datatype 有 recursive 时 => 集合的递归定义

1
2
3
4
5
6

Definition atrans_sound (atrans : aexp → aexp) : Prop :=
  ∀(a : aexp), aequiv a (atrans a).
Definition btrans_sound (btrans : bexp → bexp) : Prop :=
  ∀(b : bexp), bequiv b (btrans b).
Definition ctrans_sound (ctrans : com → com) : Prop :=
  ∀(c : com), cequiv c (ctrans c).

Constant Folding 常量折叠

An expression is constant when it contains no variable references.
不引用变量的表达式为_常量_

Constant folding is an optimization that finds constant expressions and replaces them by their values.
常量折叠是一种找到常量表达式并把它们替换为其值的优化方法。

Soundness of Constant Folding

aexp

1
2
3
4
5
6
7
8
9
10
11
12

Theorem fold_constants_aexp_sound :
  atrans_sound fold_constants_aexp.
Proof.
  unfold atrans_sound. intros a. unfold aequiv. intros st.
  
(** 这个时候的状态：**)

  a : aexp
  st : state
  ============================
  aeval st a = aeval st (fold_constants_aexp a)
  

bexp

证明 btrans_sound fold_constants_bexp. 要难一些，因为其中还用到了 fold_constants_aexp, 所以我们需要一些技巧

1
2
3
4
5
6
7
8
9
10
11
12

(** 如果不记住而是直接 destruct 的话，这部分信息就丢失了 **)
    remember (fold_constants_aexp a1) as a1' eqn:Heqa1'.
    remember (fold_constants_aexp a2) as a2' eqn:Heqa2'.

(** 保留了这部分信息的目的是，使用 aexp 的可靠性定理来建立 aexp 与 值 的关系 **)
    replace (aeval st a1) with (aeval st a1') by
       (subst a1'; rewrite <- fold_constants_aexp_sound; reflexivity).
    replace (aeval st a2) with (aeval st a2') by
       (subst a2'; rewrite <- fold_constants_aexp_sound; reflexivity).

(** 最后才分类讨论 **)
    destruct a1'; destruct a2'; try reflexivity.

cmd

主要技巧在于配合使用 Congruence 与 IH 解决大部分 case，然后分类讨论 fold_constants_bexp 用 sound 做替换解决剩余 case.

Soundness of (0 + n)

类似，但是接下来我们就可以证明先 fold_constants 再 optimize_0plus 也是 sound 的.
这里我更 general 得证明了 ctrans 关系的传递性：

1
2
3
4

Theorem trans_ctrans_sound : forall tr1 tr2,
  ctrans_sound tr1 -> 
  ctrans_sound tr2 -> 
  ctrans_sound (fun c => tr2 (tr1 c)).

Proving Inequivalence 证明程序不等价

在这个例子中，subst_aexp 是 sound 得，被称为 Constant Propagation (常量传播)

1
2
3
4

(**    [X := 42 + 53](Y + X)  =>  Y + (42 + 53)    **)
Example subst_aexp_ex :
  subst_aexp X (42 + 53) (Y + X)%imp = (Y + (42 + 53))%imp.
Proof. reflexivity. Qed.

所以我们断言这么做是 always sound 得：

1
2
3

Definition subst_equiv_property := ∀x1 x2 a1 a2,
  cequiv (x1 ::= a1;; x2 ::= a2)
         (x1 ::= a1;; x2 ::= subst_aexp x1 a1 a2).

然而如果 a1 不是常量，副作用很容易让这个转换 unsound
那么怎么证明 ¬subst_equiv_property (即该性质不成立)? 举一个反例就好

Informal proof

• provide a witness

Formal

• give counterexamples via remember, then show ⊥.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46

(** 给出一组反例，使用性质证明他们 cequiv **)

  remember (X ::= X + 1;;
            Y ::= X)%imp     as c1.
  remember (X ::= X + 1;;
            Y ::= X + 1)%imp as c2.
  assert (cequiv c1 c2) by (subst; apply Contra).
  
(* => *)  Heqc1 : c1 = (X ::= X + 1;; Y ::= X)%imp
          Heqc2 : c2 = (X ::= X + 1;; Y ::= X + 1)%imp
          H : cequiv c1 c2
          ============================
          False
    
    
(** 给出他们将 eval 出不同的 heap **)

  remember (Y !-> 1 ; X !-> 1) as st1.
  remember (Y !-> 2 ; X !-> 1) as st2.
  assert (H1 : empty_st =[ c1 ]=> st1);
  assert (H2 : empty_st =[ c2 ]=> st2);

  apply H in H1. (** 使用 H : cequiv c1 c2 , 我们得到 **)
  
(* => *)  H1 : empty_st =[ c2 ]=> st1
          H2 : empty_st =[ c2 ]=> st2
          ============================
          False


(** 利用 ceval 的 deterministic **)

  assert (Hcontra : st1 = st2)
    by (apply (ceval_deterministic c2 empty_st); assumption).
    
(* => *)  Hcontra : st1 = st2
          ============================
          False

    
(** st1, st2 are map, which are actually function! 
    这时我们可以反用 functional extenionality，直接 apply Y 然后 discrinminate **)

  assert (Hcontra' : st1 Y = st2 Y)
    by (rewrite Hcontra; reflexivity).
  subst. inversion Hcontra'.  Qed.

Extended Exercise: Nondeterministic Imp

HAVOC roughly corresponds to an uninitialized variable in a low-level language like C.
After the HAVOC, the variable holds a fixed but arbitrary number.

我们增加一个 HAVOC X 语句（大灾难），会为 X 随机赋一个值…类似于「未初始化变量」

1
2
3
4
5
6
7
8
9
10
11
12

Inductive com : Type :=
  ...
  | CHavoc : string → com. (* <--- 新增 *)

Notation "'HAVOC' l" :=
  (CHavoc l) (at level 60) : imp_scope.
  

Inductive ceval : com -> state -> state -> Prop :=
  ...
  | E_Havoc : forall st (n : nat) x,
      st =[ HAVOC x ]=> (x !-> n)        (** can eval to arbitraty heap **)

Small-Step

deterministic

also the def of partial function?

solve_by_inverts

in LTac. (used to generate proof)
LTac doesn’t have termination check. (might not be able to find…)

match is back-tracking point.

number passing in = depth of the iteration/recursion

ST_Plus2 need value v1. not redundant with ST_Plus1
we might have things not value but cannot take step as well.

Strong Progress

Normal form

= no relation related to (so cannot step to)

vs Value…

destruct (apply t).
can we do that?

Slide Q&A.

value_not_sae_as normal_form

e.g (1+2) + 7
e.g. 3 + 7

One-step

• plus
• left + 0
• right + 0

Inf-step -> Inf terms

go from 3 to 3+0

Stuck

No StepR

0 term can step into

Multi-Step Reduction ->*

1
2
3
4
5
6

Inductive multi {X : Type} (R : relation X) : relation X :=
  | multi_refl : ∀(x : X), multi R x x
  | multi_step : ∀(x y z : X),
                    R x y →
                    multi R y z →
                    multi R x z.

can be either defined as a “head + tail” style (or “tail + head” style), or “refl + trans” style (as in Rel.v).

the trans relation are underteministic in terms of the transtive relation using. (you can throw infinitely many trans constructors in)

having multiple form so we can jump back and forth to pick one easier for proof.

PLT PM lang

multiple smallstep relation can be markded deepner state.qjw
er state.

IMP

astep no need for `value``

for If, in PLT we have 2 rules for T/F.
here we can compute…

Par w/o Concurrency is deterministic
(not vice versa)

suddenly / ->* / tuple

Recall Big-step Pros & Cons

Big-step

一步到位 : eval to its final value (plus final store)

Pros - natural (so called natural semantics), “all in one big step”

Cons - not catch the essence of how program behave

大步语义只是一个 程序 ↦ 结果 这样的 pair 集合，而「如何一步步处理」才是程序「执行」的本质

not just input state get mapped to output state.
but also intermediate state (which could be observed by concurrent code!)

Cons - not technically expressive enough to express exception / crash / non-termination

比如说，大步语义无法区分「不停机」与「卡住」
two quite different reasons of “fail to map a given state to any ending state”

1. 不停机 nontermination - we want to allow this (infinite loop is the price paid for usability)
2. 卡住 getting stuck / undefiend behaviour 未定义行为 - we want to prevent (wrong)

• WHILE_true_nonterm 仅仅表达了「程序不能再 take step」，无法与「卡住」区分
• WHILE_true 更是直接让任何「无限循环」的程序都「等价」了…而忽略了中间状态和 effect (作用)

we need a way of presenting semantics that distinguish nontermination from erroneous “stuck states”

Small-step

更精细化 : a finer-grained way of defining and reasoning about program behaviors.
原子步骤 : “atomic steps” of computation are performed.

A Toy Language

Only Constant and Plus

1
2
3

Inductive tm : Type :=
  | C : nat → tm (* Constant *)
  | P : tm → tm → tm. (* Plus *)

Big-Step

==> is really ⇓

            ---------        (E_Const)
            C n ==> n

            t1 ==> n1
            t2 ==> n2
        -------------------  (E_Plus)
        P t1 t2 ==> n1 + n2

Small-Step

single reduction step
find leftmost redex

  -------------------------------   (ST_PlusConstConst)
  P (C n1) (C n2) --> C (n1 + n2)

          t1 --> t1'
      --------------------          (ST_Plus1)
      P t1 t2 --> P t1' t2

          t2 --> t2'
  ----------------------------      (ST_Plus2)
  P (C n1) t2 --> P (C n1) t2'

Relations

Check notes of rel and tactics for more details about bi-relation.

Deterministic 确定性

a.k.a Partial Function.
in terms of its right uniqueness under mathematical context, not its emphasise on partial under programming context)

1
2

Definition deterministic {X : Type} (R : relation X) :=
  ∀x y1 y2 : X, R x y1 → R x y2 → y1 = y2.

deterministic step can be proved by induction on derivation x --> y1

• use generalize dependent y2!
• in informal proof, we usually just take ∀ y2 by default.

Ltac solve_by_inverts n

1
2
3
4
5
6
7

Ltac solve_by_inverts n :=
  match goal with | H : ?T ⊢ _ ⇒
  match type of T with Prop ⇒
    solve [
      inversion H;
      match n with S (S (?n')) ⇒ subst; solve_by_inverts (S n') end ]
  end end.

Values 值

Abstract Machine 抽象机!

think of the --> relation as defining an abstract machine:

• term = state of machine 项 = 机器状态
• step = atomic unit of computation (think as assembly opcode / CPU instructrion)
• halting state = no more computation. 停机状态

execute a term t:

• starting state = t
• repeatedly use -->
• when halt, read out the final state as result of execution

Intutively, we call such (final state) terms values.
Okay so the point is…this language is simple enough (no stuck state).
and in this lang, value can only be Const:

在这个语言中，我们「规定」只有 Const 是「值」:

1
2

Inductive value : tm → Prop :=
  | v_const : ∀n, value (C n).

and we can write ST_Plus2 more elegant:
well…in this lang, not really, since only one form of value to write out.
in cases we have multiple form of value, by doing this we don’t have to write out any cases.

         value v1
        t2 --> t2'
    --------------------  (ST_Plus2)
    P v1 t2 --> P v1 t2'

Strong Progress and Normal Forms 强可进性和正规式

strong progress: every term either is a value or can “make progress”

1
2

Theorem strong_progress : ∀t,
  value t ∨ (∃t', t --> t').

terms that cannot make progress.
for an arbitrary relation R over an arbitrary set X

normal form: term that cannot make progress (take a step)
其实我个人比较喜欢理解为「常态」或「无能量稳定态」

1
2

Definition normal_form {X : Type} (R : relation X) (t : X) : Prop :=
  ¬∃t', R t t'.

theorem: in this language, normal forms and values are actually the same thing.

1
2
3

Lemma value_is_nf : v, value v → normal_form step v.
Lemma nf_is_value : ∀t, normal_form step t → value t.
Corollary nf_same_as_value : ∀t, normal_form step t ↔ value t.

Value != Normal Form (not always)

value is a syntactic concept : it is defined by looking at the form of a term
normal form is a semantic one : it is defined by looking at how the term steps.

E.g. we can defined term that can take a step as “value”:
添加一个不是 normal form 的 value

1
2
3

Inductive value : tm → Prop :=
  | v_const : ∀n, value (C n)
  | v_funny : ∀t1 n2, value (P t1 (C n2)). (* <--- it can actually progress! *)

或者更改 step 让 value 不是 normal form…

1
2
3

Inductive step : tm -> tm -> Prop :=
  | ST_Funny : forall n,   
      C n --> P (C n) (C 0)                (* <--- or a weird  *)

Multi-Step Reduction -->* 多步规约

relation multi R: multi-step closure of R
same as clos_refl_trans_1n in Rel chapter.

1
2
3
4
5
6

Inductive multi {X : Type} (R : relation X) : relation X :=
  | multi_refl : ∀(x : X), multi R x x
  | multi_step : ∀(x y z : X),
                    R x y →
                    multi R y z →
                    multi R x z.

以上是一种方便的定义，而以下则给了我们两个 helper 定理：

1
2
3
4
5
6
7
8

Theorem multi_R : ∀(X : Type) (R : relation X) (x y : X),
    R x y → 
    multi R x y.

Theorem multi_trans : ∀(X : Type) (R : relation X) (x y z : X),
    multi R x y →
    multi R y z →
    multi R x z.

Normal Forms Again

1
2
3
4
5
6

Definition step_normal_form := normal_form step.  (** 这个是一个「性质」 Property : _ -> Prop , 从 polymorphic 的 [normal_form] 以 [step] 实例化而来 **) 
Definition normal_form_of (t t' : tm) :=          (** 是两个项之间的（i.e. 定义在 [tm] 集合上的) 二元关系, 即 t' 是 t 的正规式 **)
  (t -->* t' ∧ step_normal_form t').
  
Theorem normal_forms_unique:                      (** single-step reduction is deterministic 可以推出 normal form is unique for a given term **)
  deterministic normal_form_of.

Normalizing 总是可正规化得 – “Evaluating to completion”

something stronger is true for this language (though not for all languages)
reduction of any term t will eventually reach a normal form (我们知道 STLC 也有这个特性)

1
2
3

Definition normalizing {X : Type} (R : relation X) :=
  ∀t, ∃t',
    (multi R) t t' ∧ normal_form R t'.

To prove this, we need lemma showing some congruence of -->*:
同余关系，不过这次是定义在 -->* 这个关系上，again，同余指的是「关系对于结构上的操作保持」

1
2
3
4
5
6
7
8

Lemma multistep_congr_1 : ∀t1 t1' t2,
     t1 -->* t1' → 
     P t1 t2 -->* P t1' t2.

Lemma multistep_congr_2 : ∀t1 t2 t2',
     value t1 →
     t2 -->* t2' →
     P t1 t2 -->* P t1 t2'.

Then we can prove…

1
2

Theorem step_normalizing :
  normalizing step.

Equivalence of Big-Step and Small-Step

1
2
3
4
5

Theorem eval__multistep : ∀t n,
  t ==> n → t -->* C n.

Theorem multistep__eval : ∀t t',
  normal_form_of t t' → ∃n, t' = C n ∧ t ==> n.    (* might be better to say value here? *)

Additional: Combined Language

What if we combined the lang Arith and lang Boolean?
Would step_deterministic and strong_progress still holds?

Intuition:

• step_deterministic should still hold
• but strong_progress would definitely not!!
  • now we mixed two types so we will have stuck terms e.g. test 5 or tru + 4.
  • we will need type check and then we would be able to prove progress (which require well-typeness)

1
2
3
4
5
6
7
8
9
10
11

Theorem strong_progress :
  (forall t, value t \/ (exists t', t --> t')) \/
  ~ (forall t, value t \/ (exists t', t --> t')).
Proof.
  right. intros Hcontra.
  remember (P tru fls) as stuck.   (** 类似 disprove equiv = 举一个反例就好 **)
  specialize (Hcontra stuck).
  destruct Hcontra as [Hcvalue | Hcprogress]; subst.
  - inversion Hcvalue; inversion H.
  - destruct Hcprogress. inversion H. inversion H3. inversion H4.
Qed.

Small-Step IMP

又到了老朋友 IMP……还好没练习……简单看一下

首先对于定义小步语义，我们需要定义 value 和 --> (step)

aexp, bexp

1
2

Inductive aval : aexp → Prop :=
  | av_num : ∀n, aval (ANum n).

bexp 不需要 value 因为在这个语言里 BTrue 和 BFalse 的 step 总是 disjointed 得，所以并没有任何复用 value predicate 的时候

-->a, -->b

这里，我们先为 aexp, bexp 定义了它们各自的小步语义，

但是，其实 from PLT we know, 我们其实也可以直接复用 aexp, bexp 的大步语义！

1. 大步语义要短得多
2. aexp, bexp 其实并不会出

• 「不停机」: 没有 jump 等控制流结构
• 「异常」/「卡住」: 我们在 meta-language 的 AST 里就区分了 aexp 和 bexp，相当于主动约束了类型，所以不会出现 5 || 3 这样 type error 的 AST

cmd, -->

我们把 SKIP 当作一个「命令值（command value）」 i.e. 一个已经到达 normal form 的命令。

• 赋值命令归约到 SKIP （和一个新的 state）。
• 顺序命令等待其左侧子命令归约到 SKIP，然后丢弃它，并继续对右侧子命令归约。

对 WHILE 命令的归约是把 WHILE 命令变换为条件语句，其后紧跟同一个 WHILE 命令。

这些都与 PLT 是一致的

Concurrent IMP

为了展示 小步语义 的能力，let’s enrich IMP with concurrency.

• unpredictable scheduling (subcommands may be interleaved)
• share same memory

It’s slightly confusing here to use Par (meaning in parallel)
I mean, concurrency could be in parallel but it doesn’t have to…

1
2
3
4
5
6
7
8
9
10
11
12
13

Inductive com : Type :=
  | CPar : com → com → com. (* <--- NEW *)

Inductive cstep : (com * state) → (com * state) → Prop :=
  (* New part: *)
  | CS_Par1 : ∀st c1 c1' c2 st',
      c1 / st --> c1' / st' →
      (PAR c1 WITH c2 END) / st --> (PAR c1' WITH c2 END) / st'
  | CS_Par2 : ∀st c1 c2 c2' st',
      c2 / st --> c2' / st' →
      (PAR c1 WITH c2 END) / st --> (PAR c1 WITH c2' END) / st'
  | CS_ParDone : ∀st,
      (PAR SKIP WITH SKIP END) / st --> SKIP / st

A Small-Step Stack Machine 小步栈机

啊哈！IMP 章节 Stack Machine，我们之前仅仅定义了 Fixpoint s_execute 和 Fixpoint s_compile，这里给出其小步语义

对于本身就与「小步语义」在精神上更统一的「抽象机」，我怀疑其语义都应该是足够「小」的（即大小步将是一致的？)

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17

Definition stack := list nat.
Definition prog  := list sinstr.

Inductive stack_step : state -> prog * stack -> prog * stack -> Prop :=
  | SS_Push : forall st stk n p',
    stack_step st (SPush n :: p', stk)      (p', n :: stk)
  | SS_Load : forall st stk i p',
    stack_step st (SLoad i :: p', stk)      (p', st i :: stk)
  | SS_Plus : forall st stk n m p',
    stack_step st (SPlus :: p', n::m::stk)  (p', (m+n)::stk)
  | SS_Minus : forall st stk n m p',
    stack_step st (SMinus :: p', n::m::stk) (p', (m-n)::stk)
  | SS_Mult : forall st stk n m p',
    stack_step st (SMult :: p', n::m::stk)  (p', (m*n)::stk).
    
(** closure of stack_step **)
Definition stack_multistep st := multi (stack_step st).

Compiler Correctness

「编译器的正确性」= the notion of semantics preservation (in terms of observable behaviours)
S = e
C = s_compile e
B(S) = aeval st e
B(C) = functional s_execute
| relational stack_multistep

之前我们证明过 functional/computational Fixpoint 的性质

1
2
3
4
5
6
7
8

Theorem s_compile_correct : forall (st : state) (e : aexp),
  s_execute st [] (s_compile e) = [ aeval st e ].

(** 重要的是这个更一般的「描述了 prog 如何与 stack 交互」的定理 **)
Theorem s_execute_theorem : forall (st : state) (e : aexp) (stack : list nat) (prog : list sinstr),
    s_execute st                  stack  (s_compile e ++ prog) 
  = s_execute st ((aeval st e) :: stack)                 prog.

现在则是证明 relational Inductive 的性质，同样我们需要一个更一般的定理（然后原命题作为推论）

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17

Theorem stack_step_theorem : forall (st : state) (e : aexp) (stack : list nat) (prog : list sinstr),
  stack_multistep st
                  ((s_compile e ++ prog),                 stack) 
                  (                prog , (aeval st e) :: stack).      (** 这里 prog 和 stack 的交互本质上和上面是一样的 **)
Proof.
  unfold stack_multistep.
  induction e; intros; simpl in *;        (** 证明 induction on aexp，然后利用 transivitiy、constructor 与 IH 即可，非常快 **)
    try (apply multi_R; constructor);
    try (
        repeat (rewrite <- app_assoc);
        eapply multi_trans; try apply IHe1;
        eapply multi_trans; try apply IHe2;
        eapply multi_R; constructor
      ).
      
Definition compiler_is_correct_statement : Prop := forall (st : state) (e : aexp),
  stack_multistep st (s_compile e, []) ([], [aeval st e]).

Aside: A normalize Tactic

Even with eapply and auto…manual normalization is tedious:

1
2
3
4
5
6
7
8

Example step_example1' :
  (P (C 3) (P (C 3) (C 4)))
  -->* (C 10).
Proof.
  eapply multi_step. auto. simpl.
  eapply multi_step. auto. simpl.
  apply multi_refl.
Qed.

We could write custom Tactic Notation…(i.e. tactic macros)

1
2
3
4
5
6
7

Tactic Notation "print_goal" :=
  match goal with ⊢ ?x ⇒ idtac x end.
  
Tactic Notation "normalize" :=
  repeat (print_goal; eapply multi_step ;
            [ (eauto 10; fail) | (instantiate; simpl)]);
  apply multi_refl.

instantiate seems here for intros ∃?

1
2
3
4
5
6

Example step_example1''' : exists e',
  (P (C 3) (P (C 3) (C 4)))
  -->* e'.
Proof.
  eapply ex_intro. normalize.
Qed.

But what surprise me is that we can eapply ex_intro, which leave the ∃ as a hole ?ex (unification variable).

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.

this chapter:

• (change to new syntax…)
• function abstraction
• variable binding – 变量绑定
• substitution – 替换

Overview

“Base Types”, only Bool for now. – 基类型
…again, exactly following TAPL.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16

t ::= 
    | x                         variable
    | \x:T1.t2                  abstraction       -- haskell-ish lambda
    | t1 t2                     application
    | tru                       constant true
    | fls                       constant false
    | test t1 then t2 else t3   conditional

T ::= 
    | Bool
    | T → T                     arrow type

-- example
\x:Bool. \y:Bool. x
(\x:Bool. \y:Bool. x) fls tru
\f:Bool→Bool. f (f tru)

Some known λ-idioms:

two-arg functions are higher-order one-arg fun, i.e. curried
no named functions yet, all “anonymous” – 匿名函数

Slide QA 1

1. 2
2. Bool, fls

Syntax

Formalize syntax.
things are, as usual, in the Type level, so we can “check” them w/ dependent type.

1
2
3
4
5
6
7
8
9
10
11

Inductive ty : Type :=
  | Bool : ty
  | Arrow : ty → ty → ty.

Inductive tm : Type :=
  | var : string → tm
  | app : tm → tm → tm
  | abs : string → ty → tm → tm
  | tru : tm
  | fls : tm
  | test : tm → tm → tm → tm.

Noted that, \x:T.t (formally, abs x T t), the argument type is explicitly annotated (not inferred.)

另外，这里介绍了一个小 trick: 用 Notation (更接近 宏 ) 而非 Defintion 使得我们可以使用 auto…

1
2

(** idB = \x:Bool. x **)
Notation idB := (abs x Bool (var x)).

Operational Semantics

Values 值

• tru and fls are values
• what about function?
  1. \x:T. t is value iff t value. – Coq
  2. \x:T. t is always value – most FP lang, either CBV or CBN

Coq 这么做挺奇怪的，不过对 Coq 来说:

terms can be considered equiv up to the computation VM (在其项化简可以做到的范围内都算相等)
this rich the notion of Coq’s value (所以 Coq 的值的概念是比一般要大的)

Three ways to construct value (unary relation = predicate)

1
2
3
4

Inductive value : tm → Prop :=
  | v_abs : ∀x T t, value (abs x T t)
  | v_tru : value tru
  | v_fls : value fls.

STLC Programs 「程序」的概念也是要定义的

• closed = term not refer any undefined var = complete program
• open term = term with free variable

Having made the choice not to reduce under abstractions, we don’t need to worry about whether variables are values, since we’ll always be reducing programs “from the outside in,” and that means the step relation will always be working with closed terms.

if we could reduce under abstraction and variables are values… What’s the implication here? 始终不懂…

Substitution (IMPORTANT!) 替换

[x:=s]t and pronounced “substitute s for x in t.”

(\x:Bool. test x then tru else x) fls   ==>    test fls then tru else fls

Important capture example:

[x:=tru] (\x:Bool. x)  ==>  \x:Bool. x     -- x is bound, we need α-conversion here
                       !=>  \x:Bool. tru

Informal definition…

[x:=s]x               = s
[x:=s]y               = y                     if x ≠ y
[x:=s](\x:T11. t12)   = \x:T11. t12
[x:=s](\y:T11. t12)   = \y:T11. [x:=s]t12     if x ≠ y
[x:=s](t1 t2)         = ([x:=s]t1) ([x:=s]t2)
...

and formally:

1
2
3
4
5
6
7

Reserved Notation "'[' x ':=' s ']' t" (at level 20).
Fixpoint subst (x : string) (s : tm) (t : tm) : tm :=
  match t with
  | var x' ⇒ if eqb_string x x' then s else t    (* <-- computational eqb_string *)
  | abs x' T t1 ⇒ abs x' T (if eqb_string x x' then t1 else ([x:=s] t1))
  | app t1 t2 ⇒ app ([x:=s] t1) ([x:=s] t2)
  ...

Computable Fixpoint means meta-function! (in metalanguage, Coq here)

如果我们考虑用于替换掉某个变量的项 s 其本身也含有自由变量， 那么定义替换将会变得困难一点。

Is if x ≠ y for function abstraction one sufficient? – 在 PLT 中我们采取了更严格的定义

Only safe if we only consider s is closed term.

Prof.Mtf:

here…it’s not really “defining on closed terms”. Technically, you can still write open terms.
if we want, we could define the real closed_term…more works to prove things tho.

Prof.Mtf:

In some more rigorous setting…we might define well_typed_term
and the definition itself is the proof of Preservation!

Slide QA 2

1. (3)

Reduction （beta-reduction） beta-归约

Should be familar

                value v2
      ----------------------------                   (ST_AppAbs)   until value, i.e. function  (β-reduction)
      (\x:T.t12) v2 --> [x:=v2]t12

                t1 --> t1'
            ----------------                           (ST_App1)   reduce lhs, Function side
            t1 t2 --> t1' t2

                value v1
                t2 --> t2'
            ----------------                           (ST_App2)   reduce rhs, Arg side 
            v1 t2 --> v1 t2'

Formally,
(I was expecting they invents some new syntax for this one…so we only have AST)

1
2
3
4
5
6
7
8
9
10
11
12
13

Reserved Notation "t1 '-->' t2" (at level 40).
Inductive step : tm → tm → Prop :=
  | ST_AppAbs : ∀x T t12 v2,
         value v2 →
         (app (abs x T t12) v2) --> [x:=v2]t12
  | ST_App1 : ∀t1 t1' t2,
         t1 --> t1' →
         app t1 t2 --> app t1' t2
  | ST_App2 : ∀v1 t2 t2',
         value v1 →
         t2 --> t2' →
         app v1 t2 --> app v1 t2'
...

Slide QA 3

1. (1) idBB idB -> idB
2. (1) idBB (idBB idB) -> idB
3. if () ill-typed idBB (notB tru) -> idBB fls ....
   • we don’t type check in step
4. (3) idB fls
5. NOT…ill-typed one & open term

Typing

Typing Contexts 类型上下文

we need something like environment but for Types.

three-place typing judgment, informally written – 三元类型断言

Gamma ⊢ t ∈ T

“under the assumptions in Gamma, the term t has the type T.”

1
2

Definition context := partial_map ty.
(X ⊢> T11, Gamma) 

Why partial_map here?
IMP can use total_map because it gave default value for undefined var.

Typing Relations

                          Gamma x = T
                        ----------------                            (T_Var)   look up
                        Gamma |- x \in T

               (x |-> T11 ; Gamma) |- t12 \in T12
               ----------------------------------                   (T_Abs)   type check against context w/ arg
                Gamma |- \x:T11.t12 \in T11->T12

                    Gamma |- t1 \in T11->T12
                      Gamma |- t2 \in T11
                     ----------------------                         (T_App)
                     Gamma |- t1 t2 \in T12

1
2
3
4

Example typing_example_1 :
  empty ⊢ abs x Bool (var x) ∈ Arrow Bool Bool.
Proof.
  apply T_Abs. apply T_Var. reflexivity. Qed.

example_2

• eapply
• A ?? looks like need need another environment to look up A…

Typable / Deciable

decidable type system = decide term if typable or not.
done by type checker…

can we prove…?
∀ Γ e, ∃ τ, (Γ ⊢ e : τ) ∨ ¬(Γ ⊢ e : τ) – a type inference algorithm!

Provability in Coq witness decidabile operations.

show term is “not typeable”

Keep inversion till the contradiction.

基本的定理依赖关系 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_map 的 neq 和 permute
这里，我们直接进一步地证明 「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

make the STLC into a PL!

Simple Extensions to STLC

其实这一部分我好像没有任何必要做笔记……

Numbers

See StlcProp.v exercise stlc_arith.

Let Bindings

• In PLT slide, we treat let x = t1 in e as a derived form of (λx . e) t1.
• In PLT langF, we treat let x:T = t1 in e as a derived form of (λx:T . e) t1. (both require explicit type annotation)

SF here, same as TaPL, treat it less derived by _compute the type T1 from t1.

• but TaPL treat it by desugar to λ later on, here we directly “execute” it via substituion.

我想这里有一个原因是， λ 必须要可以独立被 typed，但是这时候我们还没有 t1，无法计算出 T1。而 let 的形式中包括了 t1，所以可以直接计算:

1
2
3

t ::=                Terms
    | ...
    | let x=t in t      let-binding

Reduction:

                             t1 --> t1'
                 ----------------------------------               (ST_Let1)
                 let x=t1 in t2 --> let x=t1' in t2

                    ----------------------------              (ST_LetValue)  <-- substitute as λ
                    let x=v1 in t2 --> [x:=v1]t2

Typing:

         Gamma |- t1 \in T1      x|->T1; Gamma |- t2 \in T2
         --------------------------------------------------        (T_Let)
                    Gamma |- let x=t1 in t2 \in T2

Pairs (Product Type)

1
2
3
4
5
6
7
8
9
10
11
12
13

t ::=                Terms
    | ...
    | (t,t)             pair
    | t.fst             first projection
    | t.snd             second projection

v ::=                Values
    | ...
    | (v,v)             pair value

T ::=                Types
    | ...
    | T * T             product type

Reduction:

                          t1 --> t1'
                     --------------------                        (ST_Pair1)
                     (t1,t2) --> (t1',t2)

                          t2 --> t2'
                     --------------------                        (ST_Pair2)
                     (v1,t2) --> (v1,t2')

                          t1 --> t1'
                      ------------------                          (ST_Fst1)
                      t1.fst --> t1'.fst

                      ------------------                       (ST_FstPair)
                      (v1,v2).fst --> v1

                          t1 --> t1'
                      ------------------                          (ST_Snd1)
                      t1.snd --> t1'.snd

                      ------------------                       (ST_SndPair)
                      (v1,v2).snd --> v2


Typing:

           Gamma |- t1 \in T1     Gamma |- t2 \in T2
           -----------------------------------------               (T_Pair)
                   Gamma |- (t1,t2) \in T1*T2

                    Gamma |- t \in T1*T2
                    ---------------------                          (T_Fst)
                    Gamma |- t.fst \in T1

                    Gamma |- t \in T1*T2
                    ---------------------                          (T_Snd)
                    Gamma |- t.snd \in T2

Unit (Singleton Type) 单元类型

unit is the only value/normal form of type Unit, but not the only term (also any terms that would reduce to unit)

1
2
3
4
5
6
7
8
9
10
11

t ::=                Terms
    | ...
    | unit              unit              -- often written `()` as well

v ::=                Values
    | ...
    | unit              unit value

T ::=                Types
    | ...
    | Unit              unit type         -- Haskell even write this `()`

No reduction rule!

Typing:

                     ----------------------                        (T_Unit)
                     Gamma |- unit \in Unit

wouldn’t every computation living in such a type be trivial?
难道不是每个计算都不会在这样的类型中_居留_吗？

Where Unit really comes in handy is in richer languages with side effects
在更丰富的语言中，使用 Unit 类型来处理副作用（side effect） 会很方便

Sum Type (Disjointed Union)

deal with values that can take two distinct forms – binary sum type
两个截然不同的 … “二元和”类型

We create elements of these types by tagging elements of the component types
我们在创建这些类型的值时，会为值_标记_上其”成分”类型

标签 inl, inr 可以看做为函数，即 Data Constructor

inl : Nat  -> Nat + Bool
inr : Bool -> Nat + Bool

that “inject” (注入) elements of Nat or Bool into the left and right components of the sum type Nat+Bool

不过这里并没有把他们作为 function 来形式化，而是把 inl inr 作为关键字，把 inl t inr t 作为 primitive syntactic form…

• In PLT slide, we use L (e) and say the T2 would be “guessed” to produce T1 + T2, as TaPL option 1
• In PLT langF, we use L [T1 +T2] (e) i.e. provide a explicit type annotation for the sum type, as TaPL option 3 (ascription)

SF here, use something in the middle:

• you provide only T2 to L(t1) and T1 would be computed from t1 to form the T1 + T2.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16

t ::=                Terms
    | ...
    | inl T t           tagging (left)
    | inr T t           tagging (right)
    | case t of         case
        inl x => t
      | inr x => t

v ::=                Values
    | ...
    | inl T v           tagged value (left)
    | inr T v           tagged value (right)

T ::=                Types
    | ...
    | T + T             sum type

Reduction:

                           t1 --> t1'
                    ------------------------                       (ST_Inl)
                    inl T2 t1 --> inl T2 t1'

                           t2 --> t2'
                    ------------------------                       (ST_Inr)
                    inr T1 t2 --> inr T1 t2'

                           t0 --> t0'
           -------------------------------------------            (ST_Case)
            case t0 of inl x1 => t1 | inr x2 => t2 -->
           case t0' of inl x1 => t1 | inr x2 => t2

        -----------------------------------------------        (ST_CaseInl)
        case (inl T2 v1) of inl x1 => t1 | inr x2 => t2
                       -->  [x1:=v1]t1

        -----------------------------------------------        (ST_CaseInr)
        case (inr T1 v2) of inl x1 => t1 | inr x2 => t2
                       -->  [x2:=v1]t2

Typing:

                      Gamma |- t1 \in T1
               ------------------------------                       (T_Inl)
               Gamma |- inl T2 t1 \in T1 + T2

                      Gamma |- t2 \in T2
               -------------------------------                      (T_Inr)
                Gamma |- inr T1 t2 \in T1 + T2

                    Gamma |- t \in T1+T2
                 x1|->T1; Gamma |- t1 \in T
                 x2|->T2; Gamma |- t2 \in T
     ----------------------------------------------------          (T_Case)
     Gamma |- case t of inl x1 => t1 | inr x2 => t2 \in T

Lists

The typing features we have seen can be classified into

• 基本类型 base types like Bool, and
• 类型构造子 type constructors like → and * that build new types from old ones.

In principle, we could encode lists using pairs, sums and recursive types. (and type operator to give the type a name in SystemFω)

但是 recursive type 太 non-trivial 了……于是我们直接处理为一个特殊的类型吧

• in PLT slide, again, we omit the type and simply write nil : List T

  • 有趣的是, Prof.Mtf 并不满意这个，因为会有 hd nil 这样 stuck 的可能，所以额外给了一个用 unlist (unempty list) 的 def

• in PLT langF, we did use pairs + sums + recursive types:

  • langF nil : all('a . rec('b . unit + ('a * 'b)))
  • StlcE nil : ∀α . µβ . unit + (α ∗ β)

• in TaPL ch11, we manually provide T to all term (data constructor)

  • but actually, only nil need it! (others can be inferred by argument)

and that’s we did for SF here!

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15

t ::=                Terms
    | ...
    | nil T                          -- nil need explicit type annotation
    | cons t t
    | lcase t of nil  => t           -- a special case for list
               | x::x => t

v ::=                Values
    | ...
    | nil T             nil value
    | cons v v          cons value

T ::=                Types
    | ...
    | List T            list of Ts

Reduction:

                            t1 --> t1'
                   --------------------------                    (ST_Cons1)
                   cons t1 t2 --> cons t1' t2

                            t2 --> t2'
                   --------------------------                    (ST_Cons2)
                   cons v1 t2 --> cons v1 t2'

                          t1 --> t1'
            -------------------------------------------         (ST_Lcase1)
             (lcase t1 of nil => t2 | xh::xt => t3) -->
            (lcase t1' of nil => t2 | xh::xt => t3)

           -----------------------------------------          (ST_LcaseNil)
           (lcase nil T of nil => t2 | xh::xt => t3)
                            --> t2

        ------------------------------------------------     (ST_LcaseCons)
        (lcase (cons vh vt) of nil => t2 | xh::xt => t3)
                      --> [xh:=vh,xt:=vt]t3                  -- multiple substi


Typing:

                    -------------------------                       (T_Nil)
                    Gamma |- nil T \in List T

         Gamma |- t1 \in T      Gamma |- t2 \in List T
         ---------------------------------------------             (T_Cons)
                Gamma |- cons t1 t2 \in List T

                    Gamma |- t1 \in List T1
                    Gamma |- t2 \in T
            (h|->T1; t|->List T1; Gamma) |- t3 \in T
      ---------------------------------------------------         (T_Lcase)
      Gamma |- (lcase t1 of nil => t2 | h::t => t3) \in T

General Recursion (Fixpoint)

通用的递归，而非 primitive recursion (PFPL)

1

fact = \x:Nat . if x=0 then 1 else x * (fact (pred x)))

这个在 Stlc 中不被允许，因为我们在定义 fact 的过程中发现了一个 free 的 fact，要么未定义，要么不是自己。
所以我们需要 Fixpoint

1
2

fact = fix (\fact:Nat->Nat. 
       \x:Nat . if x=0 then 1 else x * (fact (pred x)))

1
2
3

t ::=                Terms
    | ...
    | fix t             fixed-point operator

Reduction:

                            t1 --> t1'
                        ------------------                        (ST_Fix1)
                        fix t1 --> fix t1'

           --------------------------------------------         (ST_FixAbs)
           fix (\xf:T1.t2) --> [xf:=fix (\xf:T1.t2)] t2         -- fix f = f (fix f)

Typing:

                       Gamma |- t1 \in T1->T1
                       ----------------------                       (T_Fix)
                       Gamma |- fix t1 \in T1

Records

这里的定义非常 informal:

1
2
3
4
5
6
7
8
9
10
11
12

t ::=                          Terms
    | ...
    | {i1=t1, ..., in=tn}         record
    | t.i                         projection

v ::=                          Values
    | ...
    | {i1=v1, ..., in=vn}         record value

T ::=                          Types
    | ...
    | {i1:T1, ..., in:Tn}         record type

Reduction:

                          ti --> ti'
             ------------------------------------                  (ST_Rcd)
                 {i1=v1, ..., im=vm, in=ti , ...}
             --> {i1=v1, ..., im=vm, in=ti', ...}

                          t1 --> t1'
                        --------------                           (ST_Proj1)
                        t1.i --> t1'.i

                  -------------------------                    (ST_ProjRcd)
                  {..., i=vi, ...}.i --> vi

Typing:

        Gamma |- t1 \in T1     ...     Gamma |- tn \in Tn
      ----------------------------------------------------          (T_Rcd)
      Gamma |- {i1=t1, ..., in=tn} \in {i1:T1, ..., in:Tn}

                Gamma |- t \in {..., i:Ti, ...}
                -------------------------------                    (T_Proj)
                      Gamma |- t.i \in Ti

其他

提了一嘴

• Variant
• Recursive type μ

加起来就可以

give us enough mechanism to build arbitrary inductive data types like lists and trees from scratch

Basically

ADT = Unit + Product + Sum (Variant) + Function (Expo)

但是 Coq 的 Inductive 还需要进一步的 Pi (Dependent Product), Sigma (Dependent Sum).

Exercise: Formalizing the Extensions

STLCE definitions

基本上就是把上面的 rule 用 AST 写进来

STLCE examples

a bit of Coq hackery to automate searching for typing derivation

基本上就是自动化的 pattern matching + tactics

1
2
3
4
5
6
7

Hint Extern 2 (has_type _ (app _ _) _) =>
  eapply T_App; auto.

Hint Extern 2 (has_type _ (tlcase _ _ _ _ _) _) =>
  eapply T_Lcase; auto.

Hint Extern 2 (_ = _) => compute; reflexivity.

效果非常酷：typecheck 只需要 eauto，reduction 只需要 normalize.

Concepts

The Subsumption Rule

The Subtype Relation

Slide QA1

Record Subtyping…

row type

index? record impl as list

width/depth/permulation

• multiple step rules

Java

1. class - no index (thinking about offset)

having both width/permulation subtyping make impl slow

• OOP - hmm
• ML has no permulation - for perf reason (static structure) as C

ML has depth?

• a little bit by equality

OCaml objection has all three

Slide QA2

Looking at Contravariant!

1. (2) {i1:S,i2:T}→U <: {i1:S,i2:T,i3:V}→U

2. (4) {i1:T,i2:V,i3:V} <: {i1:S,i2:U} * {i3:V} is interesting:

the interesting thing is, why don’t we make some subtyping rules for that as well?

• there are definitely code can do that
• their runtime semantics are different tho they carry same information
• coercion can used for that

3 and 4. (5) …

A <: Top => Top -> A <: A -> A – contravariant

if we only care (A*T), can use T:Top

but to type the whole thing : A

Top -> A?
but noticed that we said \z:A.z

can we pass A -> A into Top -> A?
more specific more general

smallest -> most specific -> A -> A
largest -> most specific -> Top -> A

5.
“The type Bool has no proper subtypes.” (I.e., the only type smaller than Bool is Bool itself.)
Ture unless we have Bottom

hmm seems like Bottom in subtyping is different with Empty/Void, which is closer to logical Bottom ⊥ since Bottom here is subtyping of everything..
OH they are the same: (nice)

https://en.wikipedia.org/wiki/Bottom_type

6. True

Inversion Lemmas for Subtyping

inversion doesn’t lose information, induction does.

auto rememeber?? — dependent induction
hetergeous equaltiy

In soundness proof

• subtyping only affects Canonical Forms + T_Sub case in induction

Lemma: If Gamma ⊢ \x:S1.t2 ∈ T, then there is a type S2 such that x⊢>S1; Gamma ⊢ t2 ∈ S2 and S1 → S2 <: T.

why T not arrow? Top…

if including Bottom…many proof becomes hard, canonical form need to say…might be Bottom?

no, no value has type Bottom (Void)…