module plfa.part2.Lambda where

λ-演算，最早由逻辑学家 Alonzo Church 在 1932 年发表，是一种只含有三种构造的演算—— 变量（Variable）、抽象（Abstraction）与应用（Application）。 λ-演算刻画了函数抽象（Functional Abstraction）的核心概念。这样的概念 以函数、过程和方法的形式，在基本上每一个编程语言中都有体现。 简单类型的 λ-演算（Simply-Typed Lambda Calculus，简写为 STLC）是 λ-演算的一种变体， 由 Church 在 1940 年发表。 除去之前提到的三种构造，简单类型的 λ-演算还拥有函数类型和任何所需的基本类型。 Church 使用了最简单的没有任何操作的基本类型。 我们在这里使用 Plotkin 的可编程的可计算函数（Programmable Computable Functions，PCF）， 并加入自然数和递归函数及其相关操作。

在本章中，我们将形式化简单类型的 λ-演算，给出它的语法、小步语义和类型规则。 在下一章 Properties 中，我们将 证明它的主要性质，包括可进性与保型性。 后续的章节将研究 λ-演算的不同变体。

请注意，我们在这里使用的方法不是将它形式化的推荐方法。使用 de Bruijn 索引和 固有类型的项（我们会在 DeBruijn 章节中进一步研究）， 可以让我们的形式化更简洁。 不过，我们先从使用带名字的变量和外在类型的项来表示 λ-演算开始。 一方面是因为名字比索引更易于阅读，另一方面是因为这样的表述更加传统。

这一章启发自《软件基础》（Software Foundations）/《程序语言基础》（Programming Language Foundations）中对应的 Stlc 的内容。 我们的不同之处在于使用显式的方法来表示语境（由标识符和类型的序对组成的列表）， 而不是部分映射（从标识符到类型的部分函数）。 这样的做法与后续的 de Bruijn 索引表示方法能更好的对应。 我们使用自然数作为基础类型，而不是布尔值，这样我们可以表示更复杂的例子。 特别的是，我们将可以证明（两次！）二加二得四。

导入

open import Data.Bool.Base using (Bool; true; false; T; not)
open import Data.List.Base using (List; _∷_; [])
open import Data.Nat.Base using (ℕ; zero; suc)
open import Data.Product.Base using (∃-syntax; _×_)
open import Data.String using (String; _≟_)
open import Data.Unit.Base using (tt)
open import Relation.Nullary.Negation using (¬_; contradiction)
open import Relation.Nullary.Decidable using (Dec; yes; no; False; toWitnessFalse; ¬?)
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)

项的语法

项由七种构造组成。首先是 λ-演算中核心的三个构造：

  • 变量 ` x
  • 抽象 ƛ x ⇒ N
  • 应用 L · M

三个与自然数有关的构造：

  • 零 `zero
  • 后继 `suc M
  • 匹配 case L [zero⇒ M |suc x ⇒ N ]

一个与递归有关的构造：

  • 不动点 μ x ⇒ M

抽象也被叫做 λ-抽象，这也是 λ-演算名字的由来。

除了变量和不动点以外，每一个项要么构造了一个给定类型的值 （抽象产生了函数，零和后继产生了自然数）， 要么解构了一个这样的值（应用使用了函数，匹配使用了自然数）。 我们在给项赋予类型的时候将重新探讨这一对应关系。 构造子对应了引入规则，解构子对应了消去规则。

下面是以 Backus-Naur 范式（BNF）给出的语法：

L, M, N  ::=
  ` x  |  ƛ x ⇒ N  |  L · M  |
  `zero  |  `suc M  |  case L [zero⇒ M |suc x ⇒ N ]  |
  μ x ⇒ M

而下面是用 Agda 形式化后的代码：

Id : Set
Id = String

infix  5  ƛ_⇒_
infix  5  μ_⇒_
infixl 7  _·_
infix  8  `suc_
infix  9  `_

data Term : Set where
  `_                      :  Id → Term
  ƛ_⇒_                    :  Id → Term → Term
  _·_                     :  Term → Term → Term
  `zero                   :  Term
  `suc_                   :  Term → Term
  case_[zero⇒_|suc_⇒_]    :  Term → Term → Id → Term → Term
  μ_⇒_                    :  Id → Term → Term

我们用字符串来表示标识符。 我们使用的优先级使得 λ-抽象和不动点结合的最不紧密，其次是应用，再是后继， 结合得最紧密的是变量的构造子。 匹配表达式自带了括号。

项的例子

下面是一些项的例子：自然数二和一个将自然数相加的函数：

two : Term
two = `suc `suc `zero

plus : Term
plus = μ "+" ⇒ ƛ "m" ⇒ ƛ "n" ⇒
         case ` "m"
           [zero⇒ ` "n"
           |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n") ]

加法的递归定义与我们一开始在 Naturals 章节中定义的 _+_ 相似。 在这里，变量「m」被约束了两次，一个在 λ-抽象中，另一次在匹配表达式的后继分支中。 第一次使用的「m」指代前者，第二次使用的指代后者。 任何在后继分支中的「m」必须指代后者，因此我们称之为后者屏蔽（Shadow）了前者。 后面我们会证实二加二得四，也就是说下面的项

plus · two · two

会归约为 `suc `suc `suc `suc `zero。

第二个例子里，我们使用高阶函数来表示自然数。 具体来说，数字 n 由一个接受两个参数的函数来表示，这个函数将第一个参数 应用于第二个参数上 n 次。 这样的表示方法叫做自然数的 Church 表示法。 下面是一些项的例子：Church 表示法的数字二、一个将两个用 Church 表示法表示的数字相加的函数和 一个计算后继的函数：

twoᶜ : Term
twoᶜ =  ƛ "s" ⇒ ƛ "z" ⇒ ` "s" · (` "s" · ` "z")

plusᶜ : Term
plusᶜ =  ƛ "m" ⇒ ƛ "n" ⇒ ƛ "s" ⇒ ƛ "z" ⇒
         ` "m" · ` "s" · (` "n" · ` "s" · ` "z")

sucᶜ : Term
sucᶜ = ƛ "n" ⇒ `suc (` "n")

Church 法表示的二取两个参数 s 和 z，将 s 应用于 z 两次。 加法取两个数 m 和 n，函数 s 和参数 z，使用 m 将 s 应用于 使用 n 应用于 s 和 z 的结果。因此 s 对于 z 被应用了 m 加 n 次。 为了方便起见，我们定义一个计算后继的函数。 为了将一个 Church 数转化为对应的自然数，我们将它应用到 sucᶜ 函数和自然数零上。 同样，我们之后会证明二加二得四，也就是说，下面的项

plusᶜ · twoᶜ · twoᶜ · sucᶜ · `zero

会归约为 `suc `suc `suc `suc `zero。

练习 mul （推荐）

写出一个项来定义两个自然数的乘法。你可以使用之前定义的 plus。

-- 请将代码写在此处

练习 mulᶜ （习题）

写出一个项来定义两个用 Church 法表示的自然数的乘法。 你可以使用之前定义的 plusᶜ。 （当然也可以不用，用或不用都有很好的表示方法）

-- 请将代码写在此处

练习 primed （延伸）

用 ` "x" 而不是 x 来表示变量可能并不是每个人都喜欢。 我们可以加入下面的定义，来帮助我们表示项的例子：

var? : (t : Term) → Bool
var? (` _)  =  true
var? _      =  false

ƛ′_⇒_ : (t : Term) → {_ : T (var? t)} → Term → Term
ƛ′_⇒_ (` x) N = ƛ x ⇒ N

case′_[zero⇒_|suc_⇒_] : Term → Term → (t : Term) → {_ : T (var? t)} → Term → Term
case′ L [zero⇒ M |suc (` x) ⇒ N ]  =  case L [zero⇒ M |suc x ⇒ N ]

μ′_⇒_ : (t : Term) → {_ : T (var? t)} → Term → Term
μ′ (` x) ⇒ N  =  μ x ⇒ N

回顾 T 是一个将计算映射到证明的函数，如同在 Decidable 章节中的定义。 我们只在项参数是变量时使用带一撇的函数，用隐式证明来保证这一点。 例如，如果我们试着定义一个绑定非变量的抽象：

_ : Term
_ = ƛ′ two ⇒ two

Agda 会抱怨它无法为隐式参数找到一个底类型的值。 注意此处隐式参数的类型在 t 不是变量时会归约至 ⊥。

现在我们可以用下面的形式重新写出 plus 的定义：

plus′ : Term
plus′ = μ′ + ⇒ ƛ′ m ⇒ ƛ′ n ⇒
          case′ m
            [zero⇒ n
            |suc m ⇒ `suc (+ · m · n) ]
  where
  +  =  ` "+"
  m  =  ` "m"
  n  =  ` "n"

用这样的形式写出乘法的定义。

形式化与非正式

在形式化语义的非正式表述中，我们使用变量名来消除歧义，用 x 而不是 ` x 来表示一个变量项。Agda 要求我们对两者进行区分。

相似地来说，非正式的表达通常在对象语言（Object Language）（我们正在描述的语言） 和元语言（Meta-Language）（我们用来描述对象语言的语言） 中使用相同的记法来表示函数类型、λ-抽象和函数应用，相信读者可以通过语境区分两种语言。 而 Agda 并不能做到这样，因此我们在对象语言中使用 ƛ x ⇒ N 和 L · M ， 与我们使用的元语言 Agda 中的 λ x → N 和 L M 相对。

约束变量与自由变量

在抽象 ƛ x ⇒ N 中，我们把 x 叫做约束变量，N 叫做抽象体。 λ-演算一个重要的特性是将相同的约束变量同时重命名不会改变一个项的意义。 因此下面的五个项

  • ƛ "s" ⇒ ƛ "z" ⇒ ` "s" · (` "s" · ` "z")
  • ƛ "f" ⇒ ƛ "x" ⇒ ` "f" · (` "f" · ` "x")
  • ƛ "sam" ⇒ ƛ "zelda" ⇒ ` "sam" · (` "sam" · ` "zelda")
  • ƛ "z" ⇒ ƛ "s" ⇒ ` "z" · (` "z" · ` "s")
  • ƛ "😇" ⇒ ƛ "😈" ⇒ ` "😇" · (` "😇" · ` "😈" )

都可以认为是等价的。使用 Haskell Curry 引入的约定，这样的规则 用希腊字母 α （alpha） 来表示，因此这样的等价关系也叫做 α-重命名。

当我们从一个项中观察它的子项时，被约束的变量可能会变成自由变量。 考虑下面的项：

  • ƛ "s" ⇒ ƛ "z" ⇒ ` "s" · (` "s" · ` "z") s 和 z 都是约束变量。

  • ƛ "z" ⇒ ` "s" · (` "s" · ` "z") z 是约束变量，s 是自由变量。

  • ` "s" · (` "s" · ` "z") s 和 z 都是自由变量。

我们将没有自由变量的项叫做闭项，否则它是一个开项。 上面的三个项中，第一个是闭项，剩下两个是开项。我们在讨论归约时，会注重闭项。

一个变量在不同地方出现时，可以同时是约束变量和自由变量。在下面的项中：

(ƛ "x" ⇒ ` "x") · ` "x"

内部的 x 是约束变量，外部的是自由变量。使用 α-重命名，上面的项等同于

(ƛ "y" ⇒ ` "y") · ` "x"

此处 y 是约束变量，x 是自由变量。Barendregt 约定，一个常见的约定，使用 α-重命名 来保证约束变量与自由变量完全不同。这样可以避免因为约束变量和自由变量名称相同而造成的混乱。

匹配和递归同样引入了约束变量，我们也可以使用 α-重命名。下面的项

μ "+" ⇒ ƛ "m" ⇒ ƛ "n" ⇒
  case ` "m"
    [zero⇒ ` "n"
    |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n") ]

注意这个项包括了两个 m 的不同绑定，第一次出现在第一行，第二次出现在最后一行。 这个项与下面的项等同

μ "plus" ⇒ ƛ "x" ⇒ ƛ "y" ⇒
  case ` "x"
    [zero⇒ ` "y"
    |suc "x′" ⇒ `suc (` "plus" · ` "x′" · ` "y") ]

其中两次出现的 m 现在用 x 和 x′ 两个不同的名字表示。

值

值（Value）是一个对应着答案的项。 因此，`suc `suc `suc `suc `zero 是一个值， 而 plus · two · two 不是。 根据惯例，我们将所有的抽象当作值；所以 plus本身是一个值。

谓词 Value M 当一个项 M 是一个值时成立：

data Value : Term → Set where

  V-ƛ : ∀ {x N}
      ---------------
    → Value (ƛ x ⇒ N)

  V-zero :
      -----------
      Value `zero

  V-suc : ∀ {V}
    → Value V
      --------------
    → Value (`suc V)

后文中我们用 V 和 W 来表示值。

正式与非正式

在形式化语义的非正式表达中，我们用元变量 V 来表示一个值。 在 Agda 中，我们必须使用 Value 谓词来显式地表达。

其他方法

另一种定义不注重封闭的项，将变量视作值。 ƛ x ⇒ N 只有在 N 是一个值的时候，才是一个值。 这是 Agda 范式化项的方法，我们在 Untyped 章节中考虑这种方法。

替换

λ-演算的核心操作是将一个项中的变量用另一个项来替换。 替换在定义函数应用的操作语义中起到了重要的作用。 比如说，我们有

  (ƛ "s" ⇒ ƛ "z" ⇒ ` "s" · (` "s" · ` "z")) · sucᶜ · `zero
—→
  (ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")) · `zero
—→
  sucᶜ · (sucᶜ · `zero)

其中，我们在抽象体中用 sucᶜ 替换 ` "s"，用 `zero 替换 ` "z"。

我们将替换写作 N [ x := V ]，意为用 V 来替换项 N 中出现的所有自由变量 x。 简短地说，就是用 V 来替换 N 中的 x，或者是把 N 中的 x 换成 V。 替换只在 V 是一个封闭项时有效。它不一定是一个值，我们在这里使用 V 是因为 常常我们使用值进行替换。

下面是一些例子：

  • (ƛ "z" ⇒ ` "s" · (` "s" · ` "z")) [ "s" := sucᶜ ] 得 ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")。
  • (sucᶜ · (sucᶜ · ` "z")) [ "z" := `zero ] 得 sucᶜ · (sucᶜ · `zero)。
  • (ƛ "x" ⇒ ` "y") [ "y" := `zero ] 得 ƛ "x" ⇒ `zero。
  • (ƛ "x" ⇒ ` "x") [ "x" := `zero ] 得 ƛ "x" ⇒ ` "x"。
  • (ƛ "y" ⇒ ` "y") [ "x" := `zero ] 得 ƛ "y" ⇒ ` "y"。

在倒数第二个例子中，用 `zero 在 ƛ "x" ⇒ ` "x" 出现的 x 得到的不是 ƛ "x" ⇒ `zero， 因为 x 是抽象中的约束变量。 约束变量的名称是无关的， ƛ "x" ⇒ ` "x" 和 ƛ "y" ⇒ ` "y" 都是恒等函数。 可以认为 x 在抽象体内和抽象体外是不同的变量，而它们恰好拥有一样的名字。

我们将要给出替换的定义在用来替换变量的项是封闭时有效。 这是因为用不封闭的项可能需要对于约束变量进行重命名。例如：

  • (ƛ "x" ⇒ ` "x" · ` "y") [ "y" := ` "x" · `zero] 不应该得到
    (ƛ "x" ⇒ ` "x" · (` "x" · `zero)).

不同如上，我们应该将约束变量进行重命名，来防止捕获：

  • (ƛ "x" ⇒ ` "x" · ` "y") [ "y" := ` "x" · `zero ] 应该得到
    ƛ "x′" ⇒ ` "x′" · (` "x" · `zero).

这里的 x′ 是一个新的、不同于 x 的变量。 带有重命名的替换的形式化定义更加复杂。在这里，我们将替换限制在封闭的项之内， 可以避免重命名的问题，但对于我们要做的后续的内容来说也是足够的。

下面是对于封闭项替换的 Agda 定义：

infix 9 _[_:=_]

_[_:=_] : Term → Id → Term → Term
(` x) [ y := V ] with x ≟ y
... | yes _         = V
... | no  _         = ` x
(ƛ x ⇒ N) [ y := V ] with x ≟ y
... | yes _         = ƛ x ⇒ N
... | no  _         = ƛ x ⇒ N [ y := V ]
(L · M) [ y := V ]  = L [ y := V ] · M [ y := V ]
(`zero) [ y := V ]  = `zero
(`suc M) [ y := V ] = `suc M [ y := V ]
(case L [zero⇒ M |suc x ⇒ N ]) [ y := V ] with x ≟ y
... | yes _         = case L [ y := V ] [zero⇒ M [ y := V ] |suc x ⇒ N ]
... | no  _         = case L [ y := V ] [zero⇒ M [ y := V ] |suc x ⇒ N [ y := V ] ]
(μ x ⇒ N) [ y := V ] with x ≟ y
... | yes _         = μ x ⇒ N
... | no  _         = μ x ⇒ N [ y := V ]

下面我们来看一看前三个情况：

  • 对于变量，我们将需要替换的变量 y 与项中的变量 x 进行比较。 如果它们相同，我们返回 V，否则返回 x 不变。
  • 对于抽象，我们将需要替换的变量 y 与抽象中的约束变量 x 进行比较。 如果它们相同，我们返回抽象不变，否则对于抽象体内部进行替换。
  • 对于应用，我们递归地替换函数和其参数。

匹配表达式和递归也有约束变量，我们使用与抽象相似的方法处理它们。 除此之外的情况，我们递归地对于子项进行替换。

例子

下面是上述替换正确性的证明：

_ : (ƛ "z" ⇒ ` "s" · (` "s" · ` "z")) [ "s" := sucᶜ ]
      ≡ ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")
_ = refl

_ : (sucᶜ · (sucᶜ · ` "z")) [ "z" := `zero ] ≡ sucᶜ · (sucᶜ · `zero)
_ = refl

_ : (ƛ "x" ⇒ ` "y") [ "y" := `zero ] ≡ ƛ "x" ⇒ `zero
_ = refl

_ : (ƛ "x" ⇒ ` "x") [ "x" := `zero ] ≡ ƛ "x" ⇒ ` "x"
_ = refl

_ : (ƛ "y" ⇒ ` "y") [ "x" := `zero ] ≡ ƛ "y" ⇒ ` "y"
_ = refl

小测验

下面替换的结果是？

(ƛ "y" ⇒ ` "x" · (ƛ "x" ⇒ ` "x")) [ "x" := `zero ]
  1. (ƛ "y" ⇒ ` "x" · (ƛ "x" ⇒ ` "x"))
  2. (ƛ "y" ⇒ ` "x" · (ƛ "x" ⇒ `zero))
  3. (ƛ "y" ⇒ `zero · (ƛ "x" ⇒ ` "x"))
  4. (ƛ "y" ⇒ `zero · (ƛ "x" ⇒ `zero))

练习 _[_:=_]′ （延伸）

上面的替换定义中有三条语句（ƛ、 case 和 μ） 使用了 with 语句来处理约束变量。 将上述语句的共同部分提取成一个函数，然后用共同递归重写替换的定义。

-- 请将代码写在此处

归约

我们接下来给出 λ-演算的传值归约规则。 归约一个应用时，我们首先归约左手边，直到它变成一个值（必须是抽象）； 接下来我们归约右手边，直到它变成一个值； 最后我们使用替换，把变量替换成参数。

在非正式的操作语言表达中，我们可以如下写出应用的归约规则：

L —→ L′
--------------- ξ-·₁
L · M —→ L′ · M

M —→ M′
--------------- ξ-·₂
V · M —→ V · M′

----------------------------- β-ƛ
(ƛ x ⇒ N) · V —→ N [ x := V ]

稍后给出的 Agda 版本的规则与上述相似，但是我们需要将全称量化显式地表示出来，也需要 使用谓词来表示一个是值的项。

规则可以分为两类。 兼容性规则让我们归约一个项的一部分。我们用希腊字母 ξ （xi）开头的规则表示。 当一个项归约到足够的时候，它将会包括一个构造子和一个解构子，在这里是 ƛ 和 ·， 我们可以直接归约。这样的规则我们用希腊字母 β （beta）表示，也被称为 β-规则。

一些额外的术语：可以匹配归约规则左手边的项被称之为可归约项（Redex）。 在可归约项 (ƛ x ⇒ N) · V 中，我们把 x 叫做函数的形式参数（形参，Formal Parameter）， 把 V 叫做函数应用的实际参数（实参，Actual Parameter）。 β-归约将形参用实参来替换。

如果一个项已经是一个值，它就没有可以归约的规则； 反过来说，如果一个项可以被归约，那么它就不是一个值。 我们在下一章里证明这概括了所有的情况——所以良类型的项要么可以归约要么是一个值。

对于数字来说，零不可以归约，后继可以对它的子项进行归约。 匹配表达式先将它的参数归约至一个数字，然后根据它是零还是后继选择相应的分支。 不动点会把约束变量替换成整个不动点项——这是我们唯一一处用项、而不是值进行的替换。

我们在 Agda 里这样形式化这些规则：

infix 4 _—→_

data _—→_ : Term → Term → Set where

  ξ-·₁ : ∀ {L L′ M}
    → L —→ L′
      -----------------
    → L · M —→ L′ · M

  ξ-·₂ : ∀ {V M M′}
    → Value V
    → M —→ M′
      -----------------
    → V · M —→ V · M′

  β-ƛ : ∀ {x N V}
    → Value V
      ------------------------------
    → (ƛ x ⇒ N) · V —→ N [ x := V ]

  ξ-suc : ∀ {M M′}
    → M —→ M′
      ------------------
    → `suc M —→ `suc M′

  ξ-case : ∀ {x L L′ M N}
    → L —→ L′
      -----------------------------------------------------------------
    → case L [zero⇒ M |suc x ⇒ N ] —→ case L′ [zero⇒ M |suc x ⇒ N ]

  β-zero : ∀ {x M N}
      ----------------------------------------
    → case `zero [zero⇒ M |suc x ⇒ N ] —→ M

  β-suc : ∀ {x V M N}
    → Value V
      ---------------------------------------------------
    → case `suc V [zero⇒ M |suc x ⇒ N ] —→ N [ x := V ]

  β-μ : ∀ {x M}
      ------------------------------
    → μ x ⇒ M —→ M [ x := μ x ⇒ M ]

我们小心地设计这些归约规则，使得一个项的子项在整项被归约之前先被归约。 这被称为传值（Call-by-value）归约。

除此之外，我们规定归约的顺序是从左向右的。 这意味着归约是确定的（Deterministic）：对于任何一个项，最多存在一个可以被归约至的项。 换句话说，我们的归约关系 —→ 实际上是一个函数。

这种解释项的含义的方法叫做小步操作语义（Small-step Operational Semantics）。 如果 M —→ N，我们称之为项 M 归约至项 N，也称之为项 M 步进（Step to）至项 N。 每条兼容性规则以另一条归约规则作为前提；因此每一步都会用到一条 β-规则，用零或多条兼容性规则进行调整。

小测验

下面的项步进至哪一项？

(ƛ "x" ⇒ ` "x") · (ƛ "x" ⇒ ` "x")  —→  ???
  1. (ƛ "x" ⇒ ` "x")
  2. (ƛ "x" ⇒ ` "x") · (ƛ "x" ⇒ ` "x")
  3. (ƛ "x" ⇒ ` "x") · (ƛ "x" ⇒ ` "x") · (ƛ "x" ⇒ ` "x")

下面的项步进至哪一项？

(ƛ "x" ⇒ ` "x") · (ƛ "x" ⇒ ` "x") · (ƛ "x" ⇒ ` "x")  —→  ???
  1. (ƛ "x" ⇒ ` "x")
  2. (ƛ "x" ⇒ ` "x") · (ƛ "x" ⇒ ` "x")
  3. (ƛ "x" ⇒ ` "x") · (ƛ "x" ⇒ ` "x") · (ƛ "x" ⇒ ` "x")

下面的项步进至哪一项？（twoᶜ 和 sucᶜ 如之前的定义）

twoᶜ · sucᶜ · `zero  —→  ???
  1. sucᶜ · (sucᶜ · `zero)
  2. (ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")) · `zero
  3. `zero

自反传递闭包

步进并不是故事的全部。 总的来说，对于一个封闭的项，我们想要对它反复地步进，直到归约至一个值。 这样可以用定义步进关系 —→ 的自反传递闭包 —↠ 来完成。

我们以一个零或多步的步进关系的序列来定义这样的自反传递闭包，这样的形式与 Equality 章节中的等式链论证形式相似：

infix  2 _—↠_
infix  1 begin_
infixr 2 _—→⟨_⟩_
infix  3 _∎

data _—↠_ : Term → Term → Set where
  _∎ : ∀ M
      ---------
    → M —↠ M

  step—→ : ∀ L {M N}
    → M —↠ N
    → L —→ M
      ---------
    → L —↠ N

pattern _—→⟨_⟩_ L L—→M M—↠N = step—→ L M—↠N L—→M

begin_ : ∀ {M N}
  → M —↠ N
    ------
  → M —↠ N
begin M—↠N = M—↠N

我们如下理解这个关系：

  • 对于项 M，我们可以一步也不归约而得到类型为 M —↠ M 的步骤，写作 M ∎。
  • 对于项 L，我们可以使用 L —→ M 类型步进一步，再使用 M —↠ N 类型步进零或多步， 得到类型为 L —↠ N 的步骤，写作 L —→⟨ L—→M ⟩ M—↠N。其中， L—→M 和 M—↠N 是相应类型的步骤。

在下一部分我们可以看到，这样的记法可以让我们用清晰的步骤来表示归约的例子。

我们曾在 (Equality)[Equality] 一章中用 step-≡ 和一个反转了实参顺序的语法声明定义了等式链， 这里我们同样以反转了实参顺序的模式声明来引入 step—→。 和之前一样，这能让 Agda 更高效地执行类型推断。我们后面会用到很长的归约链， 因此效率是很重要的。

我们也可以用包括 —→ 的最小的自反传递关系来定义：

data _—↠′_ : Term → Term → Set where

  step′ : ∀ {M N}
    → M —→ N
      -------
    → M —↠′ N

  refl′ : ∀ {M}
      -------
    → M —↠′ M

  trans′ : ∀ {L M N}
    → L —↠′ M
    → M —↠′ N
      -------
    → L —↠′ N

这样的三个构造子分别表示 —↠′ 包含了 —→、自反和传递的性质。 证明两者是等价的是一个很好的练习。（的确，一者嵌入了另一者）

练习 —↠≲—↠′ （习题）

证明自反传递闭包的第一种记法嵌入了第二种记法。 为什么它们不是同构的？

-- 请将代码写在此处

合流性

在讨论归约关系时，有一个重要的性质是合流性（Confluence）。 如果项 L 归约至两个项 M 和项 N，那么它们都可以归约至同一个项 P。 我们可以用下面的图来展示这个性质：

           L
          / \
         /   \
        /     \
       M       N
        \     /
         \   /
          \ /
           P

图中，L、M 和 N 由全称量词涵盖，而 P 由存在量词涵盖。 如果图中的每条线代表了零或多步归约步骤，这样的性质被称为合流性。 如果上面的两条线代表一步归约步骤，下面的两条线代表零或多步归约步骤， 这样的性质被称为菱形性质（Diamond Property）。用符号表示为：

postulate
  confluence : ∀ {L M N}
    → ((L —↠ M) × (L —↠ N))
      --------------------
    → ∃[ P ] ((M —↠ P) × (N —↠ P))

  diamond : ∀ {L M N}
    → ((L —→ M) × (L —→ N))
      --------------------
    → ∃[ P ] ((M —↠ P) × (N —↠ P))

在本章中我们讨论的归约系统是确定的。用符号表示为：

postulate
  deterministic : ∀ {L M N}
    → L —→ M
    → L —→ N
      ------
    → M ≡ N

我们可以简单地证明任何确定的归约关系满足菱形性质， 任何满足菱形性质的归约关系满足合流性。 因此，我们研究的归约系统平凡地满足了合流性。

例子

我们用一个简单的例子开始。Church 数二应用于后继函数和零可以得到自然数二：
_ : twoᶜ · sucᶜ · `zero —↠ `suc `suc `zero
_ =
  begin
    twoᶜ · sucᶜ · `zero
  —→⟨ ξ-·₁ (β-ƛ V-ƛ) ⟩
    (ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")) · `zero
  —→⟨ β-ƛ V-zero ⟩
    sucᶜ · (sucᶜ · `zero)
  —→⟨ ξ-·₂ V-ƛ (β-ƛ V-zero) ⟩
    sucᶜ · `suc `zero
  —→⟨ β-ƛ (V-suc V-zero) ⟩
    `suc (`suc `zero)
  ∎
下面的例子中我们归约二加二至四：
_ : plus · two · two —↠ `suc `suc `suc `suc `zero
_ =
  begin
    plus · two · two
  —→⟨ ξ-·₁ (ξ-·₁ β-μ) ⟩
    (ƛ "m" ⇒ ƛ "n" ⇒
      case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ])
        · two · two
  —→⟨ ξ-·₁ (β-ƛ (V-suc (V-suc V-zero))) ⟩
    (ƛ "n" ⇒
      case two [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ])
         · two
  —→⟨ β-ƛ (V-suc (V-suc V-zero)) ⟩
    case two [zero⇒ two |suc "m" ⇒ `suc (plus · ` "m" · two) ]
  —→⟨ β-suc (V-suc V-zero) ⟩
    `suc (plus · `suc `zero · two)
  —→⟨ ξ-suc (ξ-·₁ (ξ-·₁ β-μ)) ⟩
    `suc ((ƛ "m" ⇒ ƛ "n" ⇒
      case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ])
        · `suc `zero · two)
  —→⟨ ξ-suc (ξ-·₁ (β-ƛ (V-suc V-zero))) ⟩
    `suc ((ƛ "n" ⇒
      case `suc `zero [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ])
        · two)
  —→⟨ ξ-suc (β-ƛ (V-suc (V-suc V-zero))) ⟩
    `suc (case `suc `zero [zero⇒ two |suc "m" ⇒ `suc (plus · ` "m" · two) ])
  —→⟨ ξ-suc (β-suc V-zero) ⟩
    `suc `suc (plus · `zero · two)
  —→⟨ ξ-suc (ξ-suc (ξ-·₁ (ξ-·₁ β-μ))) ⟩
    `suc `suc ((ƛ "m" ⇒ ƛ "n" ⇒
      case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ])
        · `zero · two)
  —→⟨ ξ-suc (ξ-suc (ξ-·₁ (β-ƛ V-zero))) ⟩
    `suc `suc ((ƛ "n" ⇒
      case `zero [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ])
        · two)
  —→⟨ ξ-suc (ξ-suc (β-ƛ (V-suc (V-suc V-zero)))) ⟩
    `suc `suc (case `zero [zero⇒ two |suc "m" ⇒ `suc (plus · ` "m" · two) ])
  —→⟨ ξ-suc (ξ-suc β-zero) ⟩
    `suc (`suc (`suc (`suc `zero)))
  ∎
我们用 Church 数归约同样的例子：
_ : plusᶜ · twoᶜ · twoᶜ · sucᶜ · `zero —↠ `suc `suc `suc `suc `zero
_ =
  begin
    (ƛ "m" ⇒ ƛ "n" ⇒ ƛ "s" ⇒ ƛ "z" ⇒ ` "m" · ` "s" · (` "n" · ` "s" · ` "z"))
      · twoᶜ · twoᶜ · sucᶜ · `zero
  —→⟨ ξ-·₁ (ξ-·₁ (ξ-·₁ (β-ƛ V-ƛ))) ⟩
    (ƛ "n" ⇒ ƛ "s" ⇒ ƛ "z" ⇒ twoᶜ · ` "s" · (` "n" · ` "s" · ` "z"))
      · twoᶜ · sucᶜ · `zero
  —→⟨ ξ-·₁ (ξ-·₁ (β-ƛ V-ƛ)) ⟩
    (ƛ "s" ⇒ ƛ "z" ⇒ twoᶜ · ` "s" · (twoᶜ · ` "s" · ` "z")) · sucᶜ · `zero
  —→⟨ ξ-·₁ (β-ƛ V-ƛ) ⟩
    (ƛ "z" ⇒ twoᶜ · sucᶜ · (twoᶜ · sucᶜ · ` "z")) · `zero
  —→⟨ β-ƛ V-zero ⟩
    twoᶜ · sucᶜ · (twoᶜ · sucᶜ · `zero)
  —→⟨ ξ-·₁ (β-ƛ V-ƛ) ⟩
    (ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")) · (twoᶜ · sucᶜ · `zero)
  —→⟨ ξ-·₂ V-ƛ (ξ-·₁ (β-ƛ V-ƛ)) ⟩
    (ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")) · ((ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")) · `zero)
  —→⟨ ξ-·₂ V-ƛ (β-ƛ V-zero) ⟩
    (ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")) · (sucᶜ · (sucᶜ · `zero))
  —→⟨ ξ-·₂ V-ƛ (ξ-·₂ V-ƛ (β-ƛ V-zero)) ⟩
    (ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")) · (sucᶜ · (`suc `zero))
  —→⟨ ξ-·₂ V-ƛ (β-ƛ (V-suc V-zero)) ⟩
    (ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")) · (`suc `suc `zero)
  —→⟨ β-ƛ (V-suc (V-suc V-zero)) ⟩
    sucᶜ · (sucᶜ · `suc `suc `zero)
  —→⟨ ξ-·₂ V-ƛ (β-ƛ (V-suc (V-suc V-zero))) ⟩
    sucᶜ · (`suc `suc `suc `zero)
  —→⟨ β-ƛ (V-suc (V-suc (V-suc V-zero))) ⟩
   `suc (`suc (`suc (`suc `zero)))
  ∎

下一章节中，我们研究如何计算这样的归约序列。

练习 plus-example （习题）

使用归约序列，证明一加一得二。

-- 请将代码写在此处

类型的语法

我们只有两种类型：

  • 函数：A ⇒ B
  • 自然数：`ℕ

和之前一样，我们需要使用与 Agda 不一样的名称来防止混淆。

下面是类型的 BNF 形式语法：

A, B, C  ::=  A ⇒ B | `ℕ

下面是用 Agda 的形式化：

infixr 7 _⇒_

data Type : Set where
  _⇒_ : Type → Type → Type
  `ℕ : Type

优先级

与 Agda 中一致，两个或多个参数的函数以柯里化的形式表示。 以右结合的方式定义 _⇒_、左结合的方式定义 _·_ 更加方便。 因此：

  • (`ℕ ⇒ `ℕ) ⇒ `ℕ ⇒ `ℕ 表示 ((`ℕ ⇒ `ℕ) ⇒ (`ℕ ⇒ `ℕ))。
  • plus · two · two 表示 (plus · two) · two。

小测验

  • 下面给出的项的类型是什么？

    ƛ "s" ⇒ ` "s" · (` "s" · `zero)

    1. (`ℕ ⇒ `ℕ) ⇒ (`ℕ ⇒ `ℕ)
    2. (`ℕ ⇒ `ℕ) ⇒ `ℕ
    3. `ℕ ⇒ (`ℕ ⇒ `ℕ)
    4. `ℕ ⇒ `ℕ ⇒ `ℕ
    5. `ℕ ⇒ `ℕ
    6. `ℕ

    在适当的情况下，可以给出多于一个答案。

  • 下面给出的项的类型是什么？

    (ƛ "s" ⇒ ` "s" · (` "s" · `zero)) · sucᶜ

    1. (`ℕ ⇒ `ℕ) ⇒ (`ℕ ⇒ `ℕ)
    2. (`ℕ ⇒ `ℕ) ⇒ `ℕ
    3. `ℕ ⇒ (`ℕ ⇒ `ℕ)
    4. `ℕ ⇒ `ℕ ⇒ `ℕ
    5. `ℕ ⇒ `ℕ
    6. `ℕ

    在适当的情况下，可以给出多于一个答案。

赋型

语境

在归约时，我们只讨论封闭的项，但是在赋型时，我们必须考虑带有自由变量的项。 给一个项赋型时，我们必须先给它的子项赋型。而在给一个抽象的抽象体赋型时， 抽象的约束变量在抽象体内部是自由的。

语境（Context）将变量和类型联系在一起。 我们用 Γ 和 Δ 来表示语境。 我们用 ∅ 表示空的语境，用 Γ , x ⦂ A 表示扩充 Γ ，将变量 x 对应至类型 A。 例如：

  • ∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ

这个语境将变量 "s" 对应至类型 `ℕ ⇒ `ℕ， 将变量 "z" 对应至类型 `ℕ。

语境如下形式化：

infixl 5  _,_⦂_

data Context : Set where
  ∅     : Context
  _,_⦂_ : Context → Id → Type → Context

练习 Context-≃ （习题）

证明 Context 与 List (Id × Type) 同构。

例如，如下的语境

∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ

和如下的列表相关。

[ ⟨ "z" , `ℕ ⟩ , ⟨ "s" , `ℕ ⇒ `ℕ ⟩ ]
-- 请将代码写在此处

查询判断

我们使用两种判断。第一种写作

Γ ∋ x ⦂ A

表示在语境 Γ 中变量 x 的类型是 A。这样的判断叫做查询（Lookup）判断。 例如，

  • ∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ ∋ "z" ⦂ `ℕ
  • ∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ ∋ "s" ⦂ `ℕ ⇒ `ℕ

分别给出了变量 "z" 和 "s" 对应的类型。 我们使用符号 ∋ （读作 “ni”，反写的 “in”），因为 Γ ∋ x ⦂ A 与查询 x ⦂ A 是否在与 Γ 对应的列表中存在相似。

如果语境中有相同名称的两个变量，那么查询会返回被约束的最近的变量，它遮盖（Shadow） 了另一个变量。例如：

  • ∅ , "x" ⦂ `ℕ ⇒ `ℕ , "x" ⦂ `ℕ ∋ "x" ⦂ `ℕ.

在这里 "x" ⦂ `ℕ ⇒ `ℕ 被 "x" ⦂ `ℕ 遮盖了。

我们如下形式化查询：
infix  4  _∋_⦂_

data _∋_⦂_ : Context → Id → Type → Set where

  Z : ∀ {Γ x A}
      ------------------
    → Γ , x ⦂ A ∋ x ⦂ A

  S : ∀ {Γ x y A B}
    → x ≢ y
    → Γ ∋ x ⦂ A
      ------------------
    → Γ , y ⦂ B ∋ x ⦂ A

构造子 Z 和 S 大致与列表包含关系 _∈_ 的 here 和 there 构造子对应。 但是构造子 S 多取一个参数，来保证查询时我们不会查询一个被遮盖的同名变量。

用 S 构造子会比较麻烦，因为每次都需要提供 x ≢ y 的证明。例如：

_ : ∅ , "x" ⦂ `ℕ ⇒ `ℕ , "y" ⦂ `ℕ , "z" ⦂ `ℕ ∋ "x" ⦂ `ℕ ⇒ `ℕ
_ = S (λ()) (S (λ()) Z)

取而代之的是，我们在类型检查时可以使用以互映证明来检查不等性的「智慧构造子」：

S′ : ∀ {Γ x y A B}
   → {x≢y : False (x ≟ y)}
   → Γ ∋ x ⦂ A
     ------------------
   → Γ , y ⦂ B ∋ x ⦂ A

S′ {x≢y = x≢y} x = S (toWitnessFalse x≢y) x

赋型判断

第二种判断写作

Γ ⊢ M ⦂ A

表示在语境 Γ 中，项 M 有类型 A。 语境 Γ 为 M 中的所有自由变量提供了类型。 例如：

  • ∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ ⊢ ` "z" ⦂ `ℕ
  • ∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ ⊢ ` "s" ⦂ `ℕ ⇒ `ℕ
  • ∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ ⊢ ` "s" · ` "z" ⦂ `ℕ
  • ∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ ⊢ ` "s" · (` "s" · ` "z") ⦂ `ℕ
  • ∅ , "s" ⦂ `ℕ ⇒ `ℕ ⊢ ƛ "z" ⇒ ` "s" · (` "s" · ` "z") ⦂ `ℕ ⇒ `ℕ
  • ∅ ⊢ ƛ "s" ⇒ ƛ "z" ⇒ ` "s" · (` "s" · ` "z") ⦂ (`ℕ ⇒ `ℕ) ⇒ `ℕ ⇒ `ℕ
赋型可以如下形式化：
infix  4  _⊢_⦂_

data _⊢_⦂_ : Context → Term → Type → Set where

  -- Axiom
  ⊢` : ∀ {Γ x A}
    → Γ ∋ x ⦂ A
      -----------
    → Γ ⊢ ` x ⦂ A

  -- ⇒-I
  ⊢ƛ : ∀ {Γ x N A B}
    → Γ , x ⦂ A ⊢ N ⦂ B
      -------------------
    → Γ ⊢ ƛ x ⇒ N ⦂ A ⇒ B

  -- ⇒-E
  _·_ : ∀ {Γ L M A B}
    → Γ ⊢ L ⦂ A ⇒ B
    → Γ ⊢ M ⦂ A
      -------------
    → Γ ⊢ L · M ⦂ B

  -- ℕ-I₁
  ⊢zero : ∀ {Γ}
      --------------
    → Γ ⊢ `zero ⦂ `ℕ

  -- ℕ-I₂
  ⊢suc : ∀ {Γ M}
    → Γ ⊢ M ⦂ `ℕ
      ---------------
    → Γ ⊢ `suc M ⦂ `ℕ

  -- ℕ-E
  ⊢case : ∀ {Γ L M x N A}
    → Γ ⊢ L ⦂ `ℕ
    → Γ ⊢ M ⦂ A
    → Γ , x ⦂ `ℕ ⊢ N ⦂ A
      -------------------------------------
    → Γ ⊢ case L [zero⇒ M |suc x ⇒ N ] ⦂ A

  ⊢μ : ∀ {Γ x M A}
    → Γ , x ⦂ A ⊢ M ⦂ A
      -----------------
    → Γ ⊢ μ x ⇒ M ⦂ A

赋型规则由对应的项的构造子来命名。

大多数规则有第二个名字，从逻辑中的惯例得到。规则的名称也可以用类型的连接符中得到， 引入和消去连接符分别用 -I 和 -E 表示。 我们从上往下阅读时，引入和消去的规则一目了然：前者引入了一个带有连接符的式子， 其出现在结论中，而不是条件中；后者消去了带有连接符的式子，其出现在条件中，而不是结论中。 引入规则表示了如何构造一个给定类型的值（抽象产生函数、零和后继产生自然数），而消去规则 表示了如何解构一个给定类型的值（应用使用函数，匹配表达式使用自然数）。

另外需要注意的是有三处地方（⊢ƛ、⊢case 和 ⊢μ），语境被 x 和相应的类型 所扩充，对应着三处约束变量的引入。

这些规则是确定的，对于每一项至多有一条规则使用。

类型推导的例子

类型推导对应着树。在非正式的记法中，下面是 Church 数二的类型推导：

                        ∋s                     ∋z
                        ------------------ ⊢`  -------------- ⊢`
∋s                      Γ₂ ⊢ ` "s" ⦂ A ⇒ A     Γ₂ ⊢ ` "z" ⦂ A
------------------ ⊢`   ------------------------------------- _·_
Γ₂ ⊢ ` "s" ⦂ A ⇒ A      Γ₂ ⊢ ` "s" · ` "z" ⦂ A
---------------------------------------------- _·_
Γ₂ ⊢ ` "s" · (` "s" · ` "z") ⦂ A
-------------------------------------------- ⊢ƛ
Γ₁ ⊢ ƛ "z" ⇒ ` "s" · (` "s" · ` "z") ⦂ A ⇒ A
------------------------------------------------------------- ⊢ƛ
Γ ⊢ ƛ "s" ⇒ ƛ "z" ⇒ ` "s" · (` "s" · ` "z") ⦂ (A ⇒ A) ⇒ A ⇒ A

其中 ∋s 和 ∋z 是下面两个推导的简写：

             ---------------- Z
"s" ≢ "z"    Γ₁ ∋ "s" ⦂ A ⇒ A
----------------------------- S       ------------- Z
Γ₂ ∋ "s" ⦂ A ⇒ A                       Γ₂ ∋ "z" ⦂ A

其中 Γ₁ = Γ , "s" ⦂ A ⇒ A、Γ₂ = Γ , "s" ⦂ A ⇒ A , "z" ⦂ A。 给出的推导对于任意的 Γ 和 A 有效，例如， 我们可以取 Γ 为 ∅ 和 A 为 `ℕ。

上面的推导可以如下用 Agda 形式化：
Ch : Type → Type
Ch A = (A ⇒ A) ⇒ A ⇒ A

⊢twoᶜ : ∀ {Γ A} → Γ ⊢ twoᶜ ⦂ Ch A
⊢twoᶜ = ⊢ƛ (⊢ƛ (⊢` ∋s · (⊢` ∋s · ⊢` ∋z)))
  where
  ∋s = S′ Z
  ∋z = Z
下面是针对二加二的赋型：
⊢two : ∀ {Γ} → Γ ⊢ two ⦂ `ℕ
⊢two = ⊢suc (⊢suc ⊢zero)

⊢plus : ∀ {Γ} → Γ ⊢ plus ⦂ `ℕ ⇒ `ℕ ⇒ `ℕ
⊢plus = ⊢μ (⊢ƛ (⊢ƛ (⊢case (⊢` ∋m) (⊢` ∋n)
         (⊢suc (⊢` ∋+ · ⊢` ∋m′ · ⊢` ∋n′)))))
  where
  ∋+  = S′ (S′ (S′ Z))
  ∋m  = S′ Z
  ∋n  = Z
  ∋m′ = Z
  ∋n′ = S′ Z

⊢2+2 : ∅ ⊢ plus · two · two ⦂ `ℕ
⊢2+2 = ⊢plus · ⊢two · ⊢two

与之前的例子不同，我们以任意语境，而不是空语境来赋型。 这让我们能够在其他除了顶层之外的语境中使用这个推导。 这里的查询判断 ∋m 和 ∋m′ 指代两个变量 "m" 的绑定。 作为对比，查询判断 ∋n 和 ∋n′ 指代同一个变量 "n" 的绑定，但是查询的语境不同， 第一次 "n" 出现在在语境的最后，第二次在 "m" 之后。

对 Church 数赋型的余下推导如下：
⊢plusᶜ : ∀ {Γ A} → Γ  ⊢ plusᶜ ⦂ Ch A ⇒ Ch A ⇒ Ch A
⊢plusᶜ = ⊢ƛ (⊢ƛ (⊢ƛ (⊢ƛ (⊢` ∋m · ⊢` ∋s · (⊢` ∋n · ⊢` ∋s · ⊢` ∋z)))))
  where
  ∋m = S′ (S′ (S′ Z))
  ∋n = S′ (S′ Z)
  ∋s = S′ Z
  ∋z = Z

⊢sucᶜ : ∀ {Γ} → Γ ⊢ sucᶜ ⦂ `ℕ ⇒ `ℕ
⊢sucᶜ = ⊢ƛ (⊢suc (⊢` ∋n))
  where
  ∋n = Z

⊢2+2ᶜ : ∅ ⊢ plusᶜ · twoᶜ · twoᶜ · sucᶜ · `zero ⦂ `ℕ
⊢2+2ᶜ = ⊢plusᶜ · ⊢twoᶜ · ⊢twoᶜ · ⊢sucᶜ · ⊢zero

与 Agda 交互

可以交互式地构造类型推导。 从声明开始：

⊢sucᶜ : ∅ ⊢ sucᶜ ⦂ `ℕ ⇒ `ℕ
⊢sucᶜ = ?

使用 C-c C-l 让 Agda 创建一个洞，并且告诉我们期望的类型：

⊢sucᶜ = { }0
?0 : ∅ ⊢ sucᶜ ⦂ `ℕ ⇒ `ℕ

现在使用 C-c C-r 来填补这个洞。Agda 注意到 sucᶜ 最外层的项是 ƛ，应该使用 ⊢ƛ 来赋型。 ⊢ƛ 规则需要一个变量，用一个新的洞表示：

⊢sucᶜ = ⊢ƛ { }1
?1 : ∅ , "n" ⦂ `ℕ ⊢ `suc ` "n" ⦂ `ℕ

再次使用 C-c C-r 来填补洞：

⊢sucᶜ = ⊢ƛ (⊢suc { }2)
?2 : ∅ , "n" ⦂ `ℕ ⊢ ` "n" ⦂ `ℕ

再来一次：

⊢sucᶜ = ⊢ƛ (⊢suc (⊢` { }3))
?3 : ∅ , "n" ⦂ `ℕ ∋ "n" ⦂ `ℕ

再次尝试使用 C-c C-r 得到下面的消息：

Don't know which constructor to introduce of Z or S

我们使用填入 Z。如果我们使用 C-c C-space，Agda 证实我们完成了：

⊢sucᶜ = ⊢ƛ (⊢suc (⊢` Z))

我们也可以使用 C-c C-a，用 Agsy 来自动完成。

在 Inference 章节中，我们会展示如何使用 Agda 来直接计算出类型推导。

查询是函数

查询关系 Γ ∋ x ⦂ A 是一个函数。 对于所有的 Γ 和 x， 至多有一个 A 满足这个判断：

∋-functional : ∀ {Γ x A B} → Γ ∋ x ⦂ A → Γ ∋ x ⦂ B → A ≡ B
∋-functional Z        Z          =  refl
∋-functional Z        (S x≢ _)   =  contradiction refl x≢
∋-functional (S x≢ _) Z          =  contradiction refl x≢
∋-functional (S _ ∋x) (S _ ∋x′)  =  ∋-functional ∋x ∋x′

赋型关系 Γ ⊢ M ⦂ A 不是一个函数。例如，在任何 Γ 中 项 ƛ "x" ⇒ ` "x" 有类型 A ⇒ A，A 为任何类型。

非例子

我们也可以证明一些项不是可赋型的。例如，我们接下来证明项 `zero · `suc `zero 是不可赋型的。 原因在于我们需要使得 `zero 既是一个函数又是一个自然数。

nope₁ : ∀ {A} → ¬ (∅ ⊢ `zero · `suc `zero ⦂ A)
nope₁ (() · _)

第二个例子，我们证明项 ƛ "x" ⇒ ` "x" · ` "x" 是不可赋型的。 原因在于我们需要满足 A ⇒ B ≡ A 的两个类型 A 和 B：

nope₂ : ∀ {A} → ¬ (∅ ⊢ ƛ "x" ⇒ ` "x" · ` "x" ⦂ A)
nope₂ (⊢ƛ (⊢` ∋x · ⊢` ∋x′))  = impossible (∋-functional ∋x ∋x′)
  where
  impossible : ∀ {A B} → ¬ (A ⇒ B ≡ A)
  impossible ()

小测验

对于下面的每一条，如果可以推导，给出类型 A，否则说明为什么这样的 A 不存在。

  1. ∅ , "y" ⦂ `ℕ ⇒ `ℕ , "x" ⦂ `ℕ ⊢ ` "y" · ` "x" ⦂ A
  2. ∅ , "y" ⦂ `ℕ ⇒ `ℕ , "x" ⦂ `ℕ ⊢ ` "x" · ` "y" ⦂ A
  3. ∅ , "y" ⦂ `ℕ ⇒ `ℕ ⊢ ƛ "x" ⇒ ` "y" · ` "x" ⦂ A

对于下面的每一条，如果可以推导，给出类型 A、B 和 C，否则说明为什么这样的类型 不存在。

  1. ∅ , "x" ⦂ A ⊢ ` "x" · ` "x" ⦂ B
  2. ∅ , "x" ⦂ A , "y" ⦂ B ⊢ ƛ "z" ⇒ ` "x" · (` "y" · ` "z") ⦂ C

练习 ⊢mul （推荐）

使用你之前写出的项 mul，给出其良类型的推导。

-- 请将代码写在此处

练习 ⊢mulᶜ （习题）

使用你之前写出的项 mulᶜ，给出其良类型的推导。

-- 请将代码写在此处

Unicode

本章中使用了以下 Unicode：

⇒  U+21D2  RIGHTWARDS DOUBLE ARROW (\=>)
ƛ  U+019B  LATIN SMALL LETTER LAMBDA WITH STROKE (\Gl-)
·  U+00B7  MIDDLE DOT (\cdot)
≟  U+225F  QUESTIONED EQUAL TO (\?=)
—  U+2014  EM DASH (\em)
↠  U+21A0  RIGHTWARDS TWO HEADED ARROW (\rr-)
ξ  U+03BE  GREEK SMALL LETTER XI (\Gx or \xi)
β  U+03B2  GREEK SMALL LETTER BETA (\Gb or \beta)
Γ  U+0393  GREEK CAPITAL LETTER GAMMA (\GG or \Gamma)
≠  U+2260  NOT EQUAL TO (\=n or \ne)
∋  U+220B  CONTAINS AS MEMBER (\ni)
∅  U+2205  EMPTY SET (\0)
⊢  U+22A2  RIGHT TACK (\vdash or \|-)
⦂  U+2982  Z NOTATION TYPE COLON (\:)
😇  U+1F607  SMILING FACE WITH HALO
😈  U+1F608  SMILING FACE WITH HORNS

我们用短划 — 和箭头 → 来构造归约 —→。 自反传递闭包 —↠ 也类似。