Stlc简单类型 Lambda-演算

简单类型 lambda-演算(simply typed lambda-calculus,STLC) 作为一种小型演算系统体现了'函数抽象(functional abstraction)'这个重要概念, 函数抽象也以很多种形式(函数,过程,方法等)出现在真实世界的程序语言中。
在形式化这个演算系统(语法,小步语义和定型规则)及其主要性质(可进性和保型性)时, 我们采用与上一章相同的流程。新的技术挑战来自于'变量绑定(variable binding)''替换(substitution)'。我们将会费一些功夫来处理他们。

Set Warnings "-notation-overridden,-parsing".
From Coq Require Import Strings.String.
From PLF Require Import Maps.
From PLF Require Import Smallstep.

简介

STLC 构建于一些'基础类型(base types)'的集合之上: 布尔值,数字,字符串等。具体选择哪些基础类型并不重要——语言的构造和它的理论性质 不会受到影响——因此简单起见,让我们暂时只使用 Bool。在本章的最后,我们会看到 如何添加更多的基础类型,后面的章节我们还会用一些实用的构造,例如序对、记录、子类型 和可变状态来扩展纯 STLC。
我们以布尔值常量和条件语句开始,并添加三个构造:
  • 变量
  • 函数抽象
  • 应用
这给了我们如下的抽象语法构造(先以非形式化的 BNF 记法写下——后面我们 会形式化它)。

       t ::= x variable
           | \x:T.t abstraction
           | t t application
           | tru constant true
           | fls constant false
           | test t then t else t conditional
函数抽象 \x:T.t 中的 \ 符号一般写作希腊字母“lambda”(本演算系统由此得名)。 变量 x 叫做函数的'参数(parameter)';项 t'函数体(body)'。 记号 :T 指明了函数可以被应用的参数类型。
一些例子:
  • \x:Bool. x
    布尔值的恒等函数。
  • (\x:Bool. x) tru
    被应用于 tru 的布尔值恒等函数。
  • \x:Bool. test x then fls else tru
    布尔值的“否定”函数。
  • \x:Bool. tru
    总是接受(布尔值)参数并返回 tru 的常量函数。
  • \x:Bool. \y:Bool. x
    接受两个布尔值做参数,并返回第一个参数的函数。(在 Coq 中,二元函数 其实就是一个一元函数,只是其函数体也是一元函数。)
  • (\x:Bool. \y:Bool. x) fls tru
    一个接受两个布尔值做参数,并返回第一个参数的函数,接着它被应用于两个布尔值参数 flstru
    在 Coq 中,应用是左结合的——也即,这个表达式被解析为 ((\x:Bool. \y:Bool. x) fls) tru
  • \f:BoolBool. f (f tru)
    一个高阶函数其接受一个函数 f(从布尔值到布尔值)作为参数,并应用 f 于参数 tru;其结果又被应用于 f
  • (\f:BoolBool. f (f tru)) (\x:Bool. fls)
    同一个高阶函数,被应用于返回 fls 的常函数。
正如最后几个例子中展示的那样,STLC是一个支持'高阶(higher-order)' 函数的语言:我们可以写出接受其他函数作为参数,或返回其他函数作为结果的函数。
但是 STLC 并没提供任何原生语法来定义'有名函数(named functions)'—— 所有的函数都是“匿名的(anonymous)”。我们会在 MoreStlc 一章中看到添加有名 函数是十分简单的——确实,基本的命名和绑定机制其实是同一回事。
STLC 的'类型(types)'包括 Bool,其用于把 trufls 这些常量 和其他产生布尔值的复杂计算归为一类;还有'函数类型(arrow types)',用于把函 数归为一类。

      T ::= Bool
          | TT
比如说:
  • \x:Bool. fls 有类型 BoolBool
  • \x:Bool. x 有类型 BoolBool
  • (\x:Bool. x) tru 有类型 Bool
  • \x:Bool. \y:Bool. x 有类型 BoolBoolBool (即 Bool (BoolBool
  • (\x:Bool. \y:Bool. x) fls 有类型 BoolBool
  • (\x:Bool. \y:Bool. x) fls tru 有类型 Bool

语法

我们接下来形式化 STLC 的语法。

Module STLC.

类型


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.
请注意一个形如 \x:T.t 的抽象(形式化地讲是 abs x T t)包含其参数 T 的类型注释,相反在 Coq(以及其他函数式语言,比如 ML,Haskell等)中, 会使用类型推导来填补这些类型注释。我们在此不考虑类型推导。
一些例子……

Open Scope string_scope.

Definition x := "x".
Definition y := "y".
Definition z := "z".

Hint Unfold x.
Hint Unfold y.
Hint Unfold z.
idB = \x:Bool. x

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

Notation idBB :=
  (abs x (Arrow Bool Bool) (var x)).
idBBBB = \x:(BoolBool) (BoolBool). x

Notation idBBBB :=
  (abs x (Arrow (Arrow Bool Bool)
                      (Arrow Bool Bool))
    (var x)).
k = \x:Bool. \y:Bool. x

Notation k := (abs x Bool (abs y Bool (var x))).
notB = \x:Bool. test x then fls else tru

Notation notB := (abs x Bool (test (var x) fls tru)).
(我们使用 Notation 而非 Definition 使 atuo 更有效。)

操作语义

为了定义 STLC 项的小步语义,我们以值的集合的定义开始。接着,我们定义两个 重要的概念,'自由变量(free variables)''替换(substitution)', 他们在函数应用的归约规则中会被用到。最后,我们给出小步归约关系。

在定义 STLC 的值时,我们有几个情形需要考虑。
首先,对于布尔值而言是显然的:truefalse 是仅有的值。 一个 test 表达式不是值。
其次,一个应用也不会是值:它表示一个函数正在某个参数上被调用,显然还可以继续归约。
第三,对于抽象,我们有几个选择:
  • 我们可以说仅当 t 是值时 \x:T. t 是值——也即,仅当函数体已经被归约 (在不知道被应用的参数是什么的情况下尽可能地归约)。
  • 或者,我们可以说不论 t 是不是值,\x:T. t 都是一个值——换句话说, 归约止于抽象。
在 Coq 中表达式通常是以第一种方式求值的——比如说,
         Compute (fun x:bool ⇒ 3 + 4)
会得到
          fun x:bool ⇒ 7
多数现实世界中的程序语言选择了第二种方式——函数体的归约仅发生在函数实际被应用 于某个参数时。在这里我们也选择第二种方式。

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

Hint Constructors value.
最后,我们必须考虑什么构成了一个'完整(complete)'的程序。
直观地讲,一个“完整的程序”不能包含未定义的变量。我们很快会看到如何定义 STLC 项中的'自由(free)'变量。一个完整的程序是'闭合的(closed)'——也就是说, 它不含有自由变量。
(相反,含有自由变量的项一般被叫做'开放项(open term)'。)
由于我们决定不对抽象内的表达式进行归约,因此也不必担心变量是否是值这个问题。 因为我们总是“从外向内”地归约程序,这意味着 step 关系仅会处理闭合项。

替换

现在我们来到了 STLC 的核心:用一个项替换另一个项中的变量。这个操作在下面用于 定义函数应用的操作语义,其中我们会需要用一个参数项替换函数体中出现的形式参数。 比如说,我们会归约
       (\x:Bool. test x then tru else x) fls

       test fls then tru else fls
这步归约将函数体中出现的参数 x 替换为 fls
一般来说,我们可以用给定的项 s 替换的某另一个项 t 中出现个变量 x。 在非形式化的讨论中,这通常被写做 [x:=s]t ,并读做“替换 t 中的 xs”。
这里有一些例子:
  • [x:=tru] (test x then x else fls) 产生 test tru then tru else fls
  • [x:=tru] x 产生 tru
  • [x:=tru] (test x then x else y) 产生 test tru then tru else y
  • [x:=tru] y 产生 y
  • [x:=tru] fls yields fls (vacuous substitution)
  • [x:=tru] (\y:Bool. test y then x else fls) 产生 \y:Bool. test y then tru else fls
  • [x:=tru] (\y:Bool. x) 产生 \y:Bool. tru
  • [x:=tru] (\y:Bool. y) 产生 \y:Bool. y
  • [x:=tru] (\x:Bool. x) 产生 \x:Bool. x
最后一个例子非常重要:替换 \x:Bool. x 中的 xtru '不'会产生 \x:Bool. tru!因为 \x:Bool. x 中的 x 是被这个抽象所'绑定的(bound)': 它是一个新的、局部的名字,只是恰巧写做了跟某个全局名字一样的 x
这是非形式化的定义……
       [x:=s]x = s
       [x:=s]y = y if xy
       [x:=s](\x:T11. t12) = \x:T11. t12
       [x:=s](\y:T11. t12) = \y:T11. [x:=s]t12 if xy
       [x:=s](t1 t2) = ([x:=s]t1) ([x:=s]t2)
       [x:=s]tru = tru
       [x:=s]fls = fls
       [x:=s](test t1 then t2 else t3) =
              test [x:=s]t1 then [x:=s]t2 else [x:=s]t3
……以及形式化的:

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
  | 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)
  | tru
      tru
  | fls
      fls
  | test t1 t2 t3
      test ([x:=s] t1) ([x:=s] t2) ([x:=s] t3)
  end

where "'[' x ':=' s ']' t" := (subst x s t).
'技术注解':如果我们考虑用于替换掉某个变量的项 s 其本身也含有自由变量, 那么定义替换将会变得困难一点。由于我们仅对定义在'闭合'项(也即像 \x:Bool. x 这种绑定了内部全部变量的项)上的 step 关系有兴趣,我们可以规避这个额外的复杂性, 但是当形式化构造更丰富的语言时,我们必须考虑这一点。
比如说,使用上面的替换定义将 t = \r:Bool. z(其中 r 为绑定变量)中的 z 替换为'开放's = \x:Bool. r(其中 r 是引用了某个全局资源的自由变量), 我们会得到 \r:Bool. \x:Bool. r。这时,s 中的自由引用 rt 所引入 的绑定所“捕获”。
为什么这是件坏事呢?因为它违反了“绑定变量的名字不应当改变语义”这个原则。打个比方, 如果把 t 的绑定变量重命名,比如说,t' = \w:Bool. z,那么 [z:=s]t' 会产生 \w:Bool. \x:Bool. r,其行为和 [z:=s]t = \r:Bool. \x:Bool. r 并不相同。这意味着,重命名绑定变量改变了 t 在替换时的行为。
对于这个问题,更详细的讨论可参考 [Aydemir 2008]

练习:3 星, standard (substi_correct)

上面我们使用了 Coq 的 Fixpoint 功能将替换定义为一个'函数'。 假设,现在我们想要将替换定义为一个归纳的'关系' substi。作为开始,我们给出了 Inductive 定义的头部和其中一个构造子;你的任务是完成剩下的构造子,并证明 你的定义同替换函数的定义相一致。

Inductive substi (s : tm) (x : string) : tm tm Prop :=
  | s_var1 :
      substi s x (var x) s
  (* 请在此处解答 *)
.

Hint Constructors substi.

Theorem substi_correct : s x t t',
  [x:=s]t = t' substi s x t t'.
Proof.
  (* 请在此处解答 *) Admitted.

归约

STLC 的小步语义与之前学过的小步语义遵循了同样的模式。直观地说, 对于函数应用我们首先归约其左手边的项(也即函数)直到其成为一个抽象; 接着归约其右手边的项(也即参数)直到其成为一个值;最后我们用参数替换函数 体内的绑定变量。最后一条规则可以非形式化地写做
      (\x:T.t12) v2 --> [x:=v2]t12
传统上这也被称作'beta-归约(beta-reduction)'
value v2 (ST_AppAbs)  

(\x:T.t12) v2 --> [x:=v2]t12
t1 --> t1' (ST_App1)  

t1 t2 --> t1' t2
value v1
t2 --> t2' (ST_App2)  

v1 t2 --> v1 t2'
……还有对条件语句的规则:
   (ST_TestTru)  

(test tru then t1 else t2) --> t1
   (ST_TestFls)  

(test fls then t1 else t2) --> t2
t1 --> t1' (ST_Test)  

(test t1 then t2 else t3) --> (test t1' then t2 else t3)
形式化的:

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'
  | ST_TestTru : t1 t2,
      (test tru t1 t2) --> t1
  | ST_TestFls : t1 t2,
      (test fls t1 t2) --> t2
  | ST_Test : t1 t1' t2 t3,
      t1 --> t1'
      (test t1 t2 t3) --> (test t1' t2 t3)

where "t1 '-->' t2" := (step t1 t2).

Hint Constructors step.

Notation multistep := (multi step).
Notation "t1 '-->*' t2" := (multistep t1 t2) (at level 40).

例子

例子:
      (\x:BoolBool. x) (\x:Bool. x) -->* \x:Bool. x

      idBB idB -->* idB

Lemma step_example1 :
  (app idBB idB) -->* idB.
Proof.
  eapply multi_step.
    apply ST_AppAbs.
    apply v_abs.
  simpl.
  apply multi_refl. Qed.
例子:
      (\x:BoolBool. x) ((\x:BoolBool. x) (\x:Bool. x))
            -->* \x:Bool. x

      (idBB (idBB idB)) -->* idB.

Lemma step_example2 :
  (app idBB (app idBB idB)) -->* idB.
Proof.
  eapply multi_step.
    apply ST_App2. auto.
    apply ST_AppAbs. auto.
  eapply multi_step.
    apply ST_AppAbs. simpl. auto.
  simpl. apply multi_refl. Qed.
例子:
      (\x:BoolBool. x)
         (\x:Bool. test x then fls else tru)
         tru
            -->* fls

       (idBB notB) tru -->* fls.

Lemma step_example3 :
  app (app idBB notB) tru -->* fls.
Proof.
  eapply multi_step.
    apply ST_App1. apply ST_AppAbs. auto. simpl.
  eapply multi_step.
    apply ST_AppAbs. auto. simpl.
  eapply multi_step.
    apply ST_TestTru. apply multi_refl. Qed.
例子:
      (\x:BoolBool. x)
         ((\x:Bool. test x then fls else tru) tru)
            -->* fls

      idBB (notB tru) -->* fls.
(请注意,虽然这个项并不会通过类型检查,我们还是可以看看它是如何归约的。)

Lemma step_example4 :
  app idBB (app notB tru) -->* fls.
Proof.
  eapply multi_step.
    apply ST_App2. auto.
    apply ST_AppAbs. auto. simpl.
  eapply multi_step.
    apply ST_App2. auto.
    apply ST_TestTru.
  eapply multi_step.
    apply ST_AppAbs. auto. simpl.
  apply multi_refl. Qed.
我们可以使用 Smallstep 一章中定义的 normalize 策略来简化这些证明。

Lemma step_example1' :
  app idBB idB -->* idB.
Proof. normalize. Qed.

Lemma step_example2' :
  app idBB (app idBB idB) -->* idB.
Proof. normalize. Qed.

Lemma step_example3' :
  app (app idBB notB) tru -->* fls.
Proof. normalize. Qed.

Lemma step_example4' :
  app idBB (app notB tru) -->* fls.
Proof. normalize. Qed.

练习:2 星, standard (step_example5)

请分别使用和不使用 normalize 证明以下命题。

Lemma step_example5 :
       app (app idBBBB idBB) idB
  -->* idB.
Proof.
  (* 请在此处解答 *) Admitted.

Lemma step_example5_with_normalize :
       app (app idBBBB idBB) idB
  -->* idB.
Proof.
  (* 请在此处解答 *) Admitted.

定型

接下来我们考虑 STLC 的类型关系。

上下文

'问':项 "x y" 的类型是什么?
'答':这取决于 xy 的类型是什么!
也就是说,为了给一个项指派类型,我们需要知道关于其中自由变量的类型的假设。
这把我们引向了一个三元'类型断言(type judgement)',非形式化地写做 Gamma t \in T, 其中 Gamma 是一个“类型上下文(typing context)”——一个变量到他们的 类型的映射。
使用通常偏映射的记号,我们用 (X > T11, Gamma) 来表示“更新偏函数 Gamma 使其也将 x 映射到 T”。

Definition context := partial_map ty.

类型关系

Gamma x = T (T_Var)  

Gamma ⊢ x ∈ T
(x > T11 ; Gamma) ⊢ t12 ∈ T12 (T_Abs)  

Gamma ⊢ \x:T11.t12 ∈ T11->T12
Gamma ⊢ t1 ∈ T11->T12
Gamma ⊢ t2 ∈ T11 (T_App)  

Gamma ⊢ t1 t2 ∈ T12
   (T_Tru)  

Gamma ⊢ tru ∈ Bool
   (T_Fls)  

Gamma ⊢ fls ∈ Bool
Gamma ⊢ t1 ∈ Bool    Gamma ⊢ t2 ∈ T    Gamma ⊢ t3 ∈ T (T_Test)  

Gamma ⊢ test t1 then t2 else t3 ∈ T
我们可以把形如 Gamma t \in T 的三元关系读做: “在假设 Gamma 下,项 t 有类型 T。”

Reserved Notation "Gamma '⊢' t '∈' T" (at level 40).

Inductive has_type : context tm ty Prop :=
  | T_Var : Gamma x T,
      Gamma x = Some T
      Gamma var x \in T
  | T_Abs : Gamma x T11 T12 t12,
      (x > T11 ; Gamma) t12 \in T12
      Gamma abs x T11 t12 \in Arrow T11 T12
  | T_App : T11 T12 Gamma t1 t2,
      Gamma t1 \in Arrow T11 T12
      Gamma t2 \in T11
      Gamma app t1 t2 \in T12
  | T_Tru : Gamma,
       Gamma tru \in Bool
  | T_Fls : Gamma,
       Gamma fls \in Bool
  | T_Test : t1 t2 t3 T Gamma,
       Gamma t1 \in Bool
       Gamma t2 \in T
       Gamma t3 \in T
       Gamma test t1 t2 t3 \in T

where "Gamma '⊢' t '∈' T" := (has_type Gamma t T).

Hint Constructors has_type.

例子


Example typing_example_1 :
  empty abs x Bool (var x) \in Arrow Bool Bool.
Proof.
  apply T_Abs. apply T_Var. reflexivity. Qed.
请注意,由于我们在提示数据库中添加了 has_type 构造子,因此 auto 将可以直接解决这个证明。

Example typing_example_1' :
  empty abs x Bool (var x) \in Arrow Bool Bool.
Proof. auto. Qed.
更多例子:
       empty ⊢ \x:A. \y:AA. y (y x)
             \in A → (AA) → A.

Example typing_example_2 :
  empty
    (abs x Bool
       (abs y (Arrow Bool Bool)
          (app (var y) (app (var y) (var x))))) \in
    (Arrow Bool (Arrow (Arrow Bool Bool) Bool)).
Proof with auto using update_eq.
  apply T_Abs.
  apply T_Abs.
  eapply T_App. apply T_Var...
  eapply T_App. apply T_Var...
  apply T_Var...
Qed.

练习:2 星, standard, optional (typing_example_2_full)

请在不使用 autoeautoeapply(或者 ...)的情况下证明同一个命题:

Example typing_example_2_full :
  empty
    (abs x Bool
       (abs y (Arrow Bool Bool)
          (app (var y) (app (var y) (var x))))) \in
    (Arrow Bool (Arrow (Arrow Bool Bool) Bool)).
Proof.
  (* 请在此处解答 *) Admitted.

练习:2 星, standard (typing_example_3)

请形式化地证明以下类型导出式成立:
       empty ⊢ \x:BoolB. \y:BoolBool. \z:Bool.
                   y (x z)
             \in T.

Example typing_example_3 :
   T,
    empty
      (abs x (Arrow Bool Bool)
         (abs y (Arrow Bool Bool)
            (abs z Bool
               (app (var y) (app (var x) (var z)))))) \in
      T.
Proof with auto.
  (* 请在此处解答 *) Admitted.
我们也可以证明某些项'不'可定型。比如说,我们可以形式化地检查对于 \x:Bool. \y:Bool, x y 来说没有类型导出式为其定型——也即,
    ¬ T,
        empty ⊢ \x:Bool. \y:Bool, x y \in T.

Example typing_nonexample_1 :
  ¬ T,
      empty
        (abs x Bool
            (abs y Bool
               (app (var x) (var y)))) \in
        T.
Proof.
  intros Hc. destruct Hc as [T Hc].
  (* The clear tactic is useful here for tidying away bits of
     the context that we're not going to need again. *)

  inversion Hc; subst; clear Hc.
  inversion H4; subst; clear H4.
  inversion H5; subst; clear H5 H4.
  inversion H2; subst; clear H2.
  discriminate H1.
Qed.

练习:3 星, standard, optional (typing_nonexample_3)

另一个例子:
    ¬( S T,
          empty ⊢ \x:S. x x \in T).

Example typing_nonexample_3 :
  ¬ ( S T,
        empty
          (abs x S
             (app (var x) (var x))) \in
          T).
Proof.
  (* 请在此处解答 *) Admitted.

End STLC.

(* 2022-03-14 05:28:22 (UTC+00) *)