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 记法写下——后面我们会形式化它）。

函数抽象 \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

一个接受两个布尔值做参数，并返回第一个参数的函数，接着它被应用于两个布尔值参数 fls 和 tru。

在 Coq 中，应用是左结合的——也即，这个表达式被解析为 ((\x:Bool. \y:Bool. x) fls) tru。
\f:Bool→Bool. f (f tru)

一个高阶函数其接受一个函数 f（从布尔值到布尔值）作为参数，并应用 f 于参数 tru；其结果又被应用于 f。
(\f:Bool→Bool. f (f tru)) (\x:Bool. fls)

同一个高阶函数，被应用于返回 fls 的常函数。

正如最后几个例子中展示的那样，STLC是一个支持'高阶（higher-order）' 函数的语言：我们可以写出接受其他函数作为参数，或返回其他函数作为结果的函数。

但是 STLC 并没提供任何原生语法来定义'有名函数（named functions）'—— 所有的函数都是“匿名的（anonymous）”。我们会在 MoreStlc 一章中看到添加有名函数是十分简单的——确实，基本的命名和绑定机制其实是同一回事。

STLC 的'类型（types）'包括 Bool，其用于把 tru 和 fls 这些常量和其他产生布尔值的复杂计算归为一类；还有'函数类型（arrow types）'，用于把函数归为一类。

T ::= Bool
| T → T

比如说：

\x:Bool. fls 有类型 Bool→Bool
\x:Bool. x 有类型 Bool→Bool
(\x:Bool. x) tru 有类型 Bool
\x:Bool. \y:Bool. x 有类型 Bool→Bool→Bool （即 Bool → (Bool→Bool））
(\x:Bool. \y:Bool. x) fls 有类型 Bool→Bool
(\x:Bool. \y:Bool. x) fls tru 有类型 Bool

语法

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

Module STLC.

类型

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

项

请注意一个形如 \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:Bool→Bool. x

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

idBBBB = \x:(Bool→Bool) → (Bool→Bool). 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 的值时，我们有几个情形需要考虑。

首先，对于布尔值而言是显然的：true 和 false 是仅有的值。一个 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 中的 x 为 s”。

这里有一些例子：

[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 中的 x 为 tru '不'会产生 \x:Bool. tru！因为 \x:Bool. x 中的 x 是被这个抽象所'绑定的（bound）'：它是一个新的、局部的名字，只是恰巧写做了跟某个全局名字一样的 x。

这是非形式化的定义……
       [x:=s]x = s
       [x:=s]y = y if x ≠ y
       [x:=s](\x:T₁₁. t₁₂) = \x:T₁₁. t₁₂
       [x:=s](\y:T₁₁. t₁₂) = \y:T₁₁. [x:=s]t₁₂ if x ≠ y
       [x:=s](t₁ t₂) = ([x:=s]t₁) ([x:=s]t₂)
       [x:=s]tru = tru
       [x:=s]fls = fls
       [x:=s](test t₁ then t₂ else t₃) =
              test [x:=s]t₁ then [x:=s]t₂ else [x:=s]t₃

……以及形式化的：

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 t₁ ⇒
      abs x' T (if eqb_string x x' then t₁ else ([x :=s ] t₁))
  | app t₁ t₂ ⇒
      app ([x :=s ] t₁) ([x :=s ] t₂)
  | tru ⇒
      tru
  | fls ⇒
      fls
  | test t₁ t₂ t₃ ⇒
      test ([x :=s ] t₁) ([x :=s ] t₂) ([x :=s ] t₃)
  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 中的自由引用 r 被 t 所引入的绑定所“捕获”。

为什么这是件坏事呢？因为它违反了“绑定变量的名字不应当改变语义”这个原则。打个比方，如果把 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) v₂ --> [x:=v₂]t₁₂

传统上这也被称作'beta-归约（beta-reduction）'

value v₂	(ST_AppAbs)

(\x:T.t12) v₂ --> [x:=v₂]t₁₂

t₁ --> t₁'	(ST_App1)

t₁ t₂ --> t₁' t₂

value v₁
t₂ --> t₂'	(ST_App2)

v₁ t₂ --> v₁ t₂'

……还有对条件语句的规则：

	(ST_TestTru)

(test tru then t₁ else t₂) --> t₁

	(ST_TestFls)

(test fls then t₁ else t₂) --> t₂

t₁ --> t₁'	(ST_Test)

(test t₁ then t₂ else t₃) --> (test t₁' then t₂ else t₃)

形式化的：

Reserved Notation "t₁ '-->' t₂" (at level 40).

Inductive step : tm → tm → Prop :=
  | ST_AppAbs : ∀ x T t₁₂ v₂,
         value v₂ →
         (app (abs x T t₁₂) v₂ ) --> [x :=v₂ ]t₁₂
  | ST_App1 : ∀ t₁ t₁' t₂,
         t₁ --> t₁' →
         app t₁ t₂ --> app t₁' t₂
  | ST_App2 : ∀ v₁ t₂ t₂',
         value v₁ →
         t₂ --> t₂' →
         app v₁ t₂ --> app v₁ t₂'
  | ST_TestTru : ∀ t₁ t₂,
      (test tru t₁ t₂ ) --> t₁
  | ST_TestFls : ∀ t₁ t₂,
      (test fls t₁ t₂ ) --> t₂
  | ST_Test : ∀ t₁ t₁' t₂ t₃,
      t₁ --> t₁' →
      (test t₁ t₂ t₃ ) --> (test t₁' t₂ t₃ )

where "t₁ '-->' t₂" := (step t₁ t₂).

Hint Constructors step.

Notation multistep := (multi step).
Notation "t₁ '-->*' t₂" := (multistep t₁ t₂) (at level 40).

例子

例子：
(\x:Bool→Bool. 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:Bool→Bool. x) ((\x:Bool→Bool. 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:Bool→Bool. 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:Bool → Bool. 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" 的类型是什么？

'答'：这取决于 x 和 y 的类型是什么！

也就是说，为了给一个项指派类型，我们需要知道关于其中自由变量的类型的假设。

这把我们引向了一个三元'类型断言（type judgement）'，非形式化地写做 Gamma ⊢ t \in T，其中 Gamma 是一个“类型上下文（typing context）”——一个变量到他们的类型的映射。

使用通常偏映射的记号，我们用 (X ⊢> T₁₁, Gamma) 来表示“更新偏函数 Gamma 使其也将 x 映射到 T”。

Definition context := partial_map ty.

类型关系

Gamma x = T	(T_Var)

Gamma ⊢ x ∈ T

(x ⊢> T₁₁ ; Gamma) ⊢ t₁₂ ∈ T₁₂	(T_Abs)

Gamma ⊢ \x:T₁₁.t12 ∈ T₁₁->T₁₂

Gamma ⊢ t₁ ∈ T₁₁->T₁₂
Gamma ⊢ t₂ ∈ T₁₁	(T_App)

Gamma ⊢ t₁ t₂ ∈ T₁₂

	(T_Tru)

Gamma ⊢ tru ∈ Bool

	(T_Fls)

Gamma ⊢ fls ∈ Bool

Gamma ⊢ t₁ ∈ Bool Gamma ⊢ t₂ ∈ T Gamma ⊢ t₃ ∈ T	(T_Test)

Gamma ⊢ test t₁ then t₂ else t₃ ∈ 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 T₁₁ T₁₂ t₁₂,
      (x ⊢> T₁₁ ; Gamma ) ⊢ t₁₂ \in T₁₂ →
      Gamma ⊢ abs x T₁₁ t₁₂ \in Arrow T₁₁ T₁₂
  | T_App : ∀ T₁₁ T₁₂ Gamma t₁ t₂,
      Gamma ⊢ t₁ \in Arrow T₁₁ T₁₂ →
      Gamma ⊢ t₂ \in T₁₁ →
      Gamma ⊢ app t₁ t₂ \in T₁₂
  | T_Tru : ∀ Gamma,
       Gamma ⊢ tru \in Bool
  | T_Fls : ∀ Gamma,
       Gamma ⊢ fls \in Bool
  | T_Test : ∀ t₁ t₂ t₃ T Gamma,
       Gamma ⊢ t₁ \in Bool →
       Gamma ⊢ t₂ \in T →
       Gamma ⊢ t₃ \in T →
       Gamma ⊢ test t₁ t₂ t₃ \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:A→A. y (y x)
\in A → (A→A) → 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)

请在不使用 auto，eauto，eapply（或者 ...）的情况下证明同一个命题：

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:Bool→B. \y:Bool→Bool. \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 H₄; subst; clear H₄.
  inversion H₅; subst; clear H₅ H₄.
  inversion H₂; subst; clear H₂.
  discriminate H₁.
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) *)