More: 简单类型 λ-演算的更多构造
module plfa.part2.More where
到此，我们主要集中于一门基于 Plotkin 的 PCF 的相对轻便的语言，包括了函数、自然数和不动点。 在本章中，我们将扩展我们的演算，来支持下列特性：
- 原语数字
- let 绑定
- 积
- 积的替代表示方法
- 和
- 单元类型
- 单元类型的替代表示方法
- 空类型
- 列表
所有上述数据类型和本书第一部分描述的相近。 对于 let 和数据类型的「替代表示方法」，我们展示如何将它们翻译至演算中其他的构造。 介绍的大部分将由非形式化的方式展示。 我们展示如何形式化前四种构造，并将其余留给读者作为习题。
非形式化的表述会以类似于 Lambda 章节中的形式，使用外在类型的项给出。 而形式化的表述会以类似于 DeBruijn 章节中的形式，使用内在类型的项给出。
到现在，使用符号来解释应该可以比文字更简洁、更精确、更易于跟随。 对于每一种构造，我们给出它的语法、赋型、归约和例子。 在需要的时候，我们也会给出构造的翻译；在下个章节我们会正式地证明翻译的正确性。
原语数字
我们定义 Nat 类型，等同于内置的自然数类型，并定义乘法作为数字的基本运算：
语法
A, B, C ::= ... 类型
Nat 原语自然数
L, M, N ::= ... 项
con c 常量
L `* M 乘法
V, W ::= ... 值
con c 常量赋型
con 规则的前提不同寻常，它指代了一个 Agda 的赋型判断，而不是 我们定义的演算中的赋型判断。
c : ℕ
--------------- con
Γ ⊢ con c : Nat
Γ ⊢ L : Nat
Γ ⊢ M : Nat
---------------- _`*_
Γ ⊢ L `* M : Nat归约
直接定义原语的规则，例如下面的最后一条规则，被称为 δ 规则。 这里的 δ 规则使用 Agda 标准库中的自然数乘法来定义原语数字的乘法。
L —→ L′
----------------- ξ-*₁
L `* M —→ L′ `* M
M —→ M′
----------------- ξ-*₂
V `* M —→ V `* M′
----------------------------- δ-*
con c `* con d —→ con (c * d)例子
下面是一个求立方的函数的例子：
cube : ∅ ⊢ Nat ⇒ Nat
cube = ƛ x ⇒ x `* x `* xLet 绑定
Let 绑定只影响项的语法；不引入新的值或者类型：
语法
L, M, N ::= ... 项
`let x `= M `in N let赋型
Γ ⊢ M ⦂ A
Γ , x ⦂ A ⊢ N ⦂ B
------------------------- `let
Γ ⊢ `let x `= M `in N ⦂ B归约
M —→ M′
--------------------------------------- ξ-let
`let x `= M `in N —→ `let x `= M′ `in N
--------------------------------- β-let
`let x `= V `in N —→ N [ x := V ]下面是一个求十次方的函数：
exp10 : ∅ ⊢ Nat ⇒ Nat
exp10 = ƛ x ⇒ `let x2 `= x `* x `in
`let x4 `= x2 `* x2 `in
`let x5 `= x4 `* x `in
x5 `* x5翻译
我们可以将每个 let 项翻译成一个抽象：
(`let x `= M `in N) † = (ƛ x ⇒ (N †)) · (M †)此处的 M † 代表了将项 M 从带有此构造的演算到不带此构造演算的翻译。
积
语法
A, B, C ::= ... 类型
A `× B 积类型
L, M, N ::= ... 项
`⟨ M , N ⟩ 有序对
`proj₁ L 投影第一分量
`proj₂ L 投影第二分量
V, W ::= ... 值
`⟨ V , W ⟩ 有序对赋型
Γ ⊢ M ⦂ A
Γ ⊢ N ⦂ B
----------------------- `⟨_,_⟩ 或 `×-I
Γ ⊢ `⟨ M , N ⟩ ⦂ A `× B
Γ ⊢ L ⦂ A `× B
---------------- `proj₁ 或 `×-E₁
Γ ⊢ `proj₁ L ⦂ A
Γ ⊢ L ⦂ A `× B
---------------- `proj₂ 或 `×-E₂
Γ ⊢ `proj₂ L ⦂ B归约
M —→ M′
------------------------- ξ-⟨,⟩₁
`⟨ M , N ⟩ —→ `⟨ M′ , N ⟩
N —→ N′
------------------------- ξ-⟨,⟩₂
`⟨ V , N ⟩ —→ `⟨ V , N′ ⟩
L —→ L′
--------------------- ξ-proj₁
`proj₁ L —→ `proj₁ L′
L —→ L′
--------------------- ξ-proj₂
`proj₂ L —→ `proj₂ L′
---------------------- β-proj₁
`proj₁ `⟨ V , W ⟩ —→ V
---------------------- β-proj₂
`proj₂ `⟨ V , W ⟩ —→ W例子
下面是一个交换有序对中分量的函数：
swap× : ∅ ⊢ A `× B ⇒ B `× A
swap× = ƛ z ⇒ `⟨ `proj₂ z , `proj₁ z ⟩积的替代表示方法
与其使用两种消去积类型的方法，我们可以使用一个匹配表达式来同时绑定两个变量， 作为积的替代表示方法。 我们重复完整的语法，但只给出新的赋型和归约规则：
语法
A, B, C ::= ... 类型
A `× B 积累性
L, M, N ::= ... 项
`⟨ M , N ⟩ 有序对
case× L [⟨ x , y ⟩⇒ M ] 匹配
V, W ::= 值
`⟨ V , W ⟩ 有序对赋型
Γ ⊢ L ⦂ A `× B
Γ , x ⦂ A , y ⦂ B ⊢ N ⦂ C
------------------------------- case× 或 ×-E
Γ ⊢ case× L [⟨ x , y ⟩⇒ N ] ⦂ C归约
L —→ L′
--------------------------------------------------- ξ-case×
case× L [⟨ x , y ⟩⇒ N ] —→ case× L′ [⟨ x , y ⟩⇒ N ]
--------------------------------------------------------- β-case×
case× `⟨ V , W ⟩ [⟨ x , y ⟩⇒ N ] —→ N [ x := V ][ y := W ]下面是用新记法重写的交换有序对中分量的函数：
swap×-case : ∅ ⊢ A `× B ⇒ B `× A
swap×-case = ƛ z ⇒ case× z
[⟨ x , y ⟩⇒ `⟨ y , x ⟩ ]翻译
我们可以将替代表示方法翻译到用投影的表示方法：
(case× L [⟨ x , y ⟩⇒ N ]) †
=
`let z `= (L †) `in
`let x `= `proj₁ z `in
`let y `= `proj₂ z `in
(N †)这里 z 是一个不在 N 中以自由变量出现的变量。 我们将这样的变量叫做新鲜（Fresh）的变量。
可能有人认为我们可以使用下面更紧凑的翻译：
-- 错误
(case× L [⟨ x , y ⟩⇒ N ]) †
=
(N †) [ x := `proj₁ (L †) ] [ y := `proj₂ (L †) ]但是这样的话它们表现的不一样。 第一项总是在归约 N 之前归约 L，它只计算 `proj₁ 和 `proj₂一次。 第二项在归约 N 之前不先将 L 归约至值，取决于 x 和 y 在 N 中出现的次数， 它将归约 L 很多次或者根本不归约，因此它会计算 `proj₁ 和 `proj₂ 很多次或者根本不计算。
我们也可以反向的翻译：
(`proj₁ L) ‡ = case× (L ‡) [⟨ x , y ⟩⇒ x ]
(`proj₂ L) ‡ = case× (L ‡) [⟨ x , y ⟩⇒ y ]和
语法
A, B, C ::= ... 类型
A `⊎ B 和类型
L, M, N ::= ... 项
`inj₁ M 注入第一分量
`inj₂ N 注入第二分量
case⊎ L [inj₁ x ⇒ M |inj₂ y ⇒ N ] 匹配
V, W ::= ... 值
`inj₁ V 注入第一分量
`inj₂ W 注入第二分量赋型
Γ ⊢ M ⦂ A
-------------------- `inj₁ 或 ⊎-I₁
Γ ⊢ `inj₁ M ⦂ A `⊎ B
Γ ⊢ N ⦂ B
-------------------- `inj₂ 或 ⊎-I₂
Γ ⊢ `inj₂ N ⦂ A `⊎ B
Γ ⊢ L ⦂ A `⊎ B
Γ , x ⦂ A ⊢ M ⦂ C
Γ , y ⦂ B ⊢ N ⦂ C
----------------------------------------- case⊎ 或 ⊎-E
Γ ⊢ case⊎ L [inj₁ x ⇒ M |inj₂ y ⇒ N ] ⦂ C归约
M —→ M′
------------------- ξ-inj₁
`inj₁ M —→ `inj₁ M′
N —→ N′
------------------- ξ-inj₂
`inj₂ N —→ `inj₂ N′
L —→ L′
---------------------------------------------------------------------- ξ-case⊎
case⊎ L [inj₁ x ⇒ M |inj₂ y ⇒ N ] —→ case⊎ L′ [inj₁ x ⇒ M |inj₂ y ⇒ N ]
--------------------------------------------------------- β-inj₁
case⊎ (`inj₁ V) [inj₁ x ⇒ M |inj₂ y ⇒ N ] —→ M [ x := V ]
--------------------------------------------------------- β-inj₂
case⊎ (`inj₂ W) [inj₁ x ⇒ M |inj₂ y ⇒ N ] —→ N [ y := W ]例子
下面是交换和的两个分量的函数：
swap⊎ : ∅ ⊢ A `⊎ B ⇒ B `⊎ A
swap⊎ = ƛ z ⇒ case⊎ z
[inj₁ x ⇒ `inj₂ x
|inj₂ y ⇒ `inj₁ y ]单元类型
对于单元类型来说，有一种方法引入单元类型，但是没有消去单元类型的方法。 单元类型没有归约规则。
语法
A, B, C ::= ... 类型
`⊤ 单元类型
L, M, N ::= ... 项
`tt 单元值
V, W ::= ... 值
`tt 单元值赋型
------------ `tt 或 ⊤-I
Γ ⊢ `tt ⦂ `⊤归约
（无）
例子
下面是 A 和 A `× `⊤的同构：
to×⊤ : ∅ ⊢ A ⇒ A `× `⊤
to×⊤ = ƛ x ⇒ `⟨ x , `tt ⟩
from×⊤ : ∅ ⊢ A `× `⊤ ⇒ A
from×⊤ = ƛ z ⇒ `proj₁ z单元类型的替代表达方法
与其没有消去单元类型的方法，我们可以使用一个匹配表达式来绑定零个变量， 作为单元类型的替代表示方法。 我们重复完整的语法，但只给出新的赋型和归约规则：
语法
A, B, C ::= ... 类型
`⊤ 单元类型
L, M, N ::= ... 项
`tt 单元值
`case⊤ L [tt⇒ N ] 匹配
V, W ::= ... 值
`tt 单元值赋型
Γ ⊢ L ⦂ `⊤
Γ ⊢ M ⦂ A
------------------------ case⊤ 或者 ⊤-E
Γ ⊢ case⊤ L [tt⇒ M ] ⦂ A归约
L —→ L′
------------------------------------- ξ-case⊤
case⊤ L [tt⇒ M ] —→ case⊤ L′ [tt⇒ M ]
----------------------- β-case⊤
case⊤ `tt [tt⇒ M ] —→ M下面是用新记法重新 A 和 A ‵× `⊤ 的同构的一半：
from×⊤-case : ∅ ⊢ A `× `⊤ ⇒ A
from×⊤-case = ƛ z ⇒ case× z
[⟨ x , y ⟩⇒ case⊤ y
[tt⇒ x ] ]翻译
我们可以将替代表示方法翻译到用没有匹配式的表示方法：
(case⊤ L [tt⇒ M ]) † = `let z `= (L †) `in (M †)此处 z 是一个在 M 中不以自由变量出现的变量。
空类型
对于空类型来说，只有一种消去此类型的值的方法，但是没有引入此类型的值的方法。 没有空类型的值，也没有归约规则，但是有 β 规则。 case⊥ 构造和 Agda 中的 ⊥-elim 的作用相似：
语法
A, B, C ::= ... 类型
`⊥ 空类型
L, M, N ::= ... 项
case⊥ L [] 匹配赋型
Γ ⊢ L ⦂ `⊥
------------------ case⊥ 或 ⊥-E
Γ ⊢ case⊥ L [] ⦂ A归约
L —→ L′
------------------------- ξ-case⊥
case⊥ L [] —→ case⊥ L′ []例子
下面是 A 和 A `⊎ `⊥ 的同构：
to⊎⊥ : ∅ ⊢ A ⇒ A `⊎ `⊥
to⊎⊥ = ƛ x ⇒ `inj₁ x
from⊎⊥ : ∅ ⊢ A `⊎ `⊥ ⇒ A
from⊎⊥ = ƛ z ⇒ case⊎ z
[inj₁ x ⇒ x
|inj₂ y ⇒ case⊥ y
[] ]列表
语法
A, B, C ::= ... 类型
`List A 列表类型
L, M, N ::= ... 项
`[] 空列表
M `∷ N 构造列表
caseL L [[]⇒ M | x ∷ y ⇒ N ] 匹配
V, W ::= ... 值
`[] 空列表
V `∷ W 构造列表赋型
----------------- `[] 或 List-I₁
Γ ⊢ `[] ⦂ `List A
Γ ⊢ M ⦂ A
Γ ⊢ N ⦂ `List A
-------------------- _`∷_ 或 List-I₂
Γ ⊢ M `∷ N ⦂ `List A
Γ ⊢ L ⦂ `List A
Γ ⊢ M ⦂ B
Γ , x ⦂ A , xs ⦂ `List A ⊢ N ⦂ B
-------------------------------------- caseL 或 List-E
Γ ⊢ caseL L [[]⇒ M | x ∷ xs ⇒ N ] ⦂ B归约
M —→ M′
----------------- ξ-∷₁
M `∷ N —→ M′ `∷ N
N —→ N′
----------------- ξ-∷₂
V `∷ N —→ V `∷ N′
L —→ L′
--------------------------------------------------------------- ξ-caseL
caseL L [[]⇒ M | x ∷ xs ⇒ N ] —→ caseL L′ [[]⇒ M | x ∷ xs ⇒ N ]
------------------------------------ β-[]
caseL `[] [[]⇒ M | x ∷ xs ⇒ N ] —→ M
--------------------------------------------------------------- β-∷
caseL (V `∷ W) [[]⇒ M | x ∷ xs ⇒ N ] —→ N [ x := V ][ xs := W ]例子
下面是列表的映射函数：
mapL : ∅ ⊢ (A ⇒ B) ⇒ `List A ⇒ `List B
mapL = μ mL ⇒ ƛ f ⇒ ƛ xs ⇒
caseL xs
[[]⇒ `[]
| x ∷ xs ⇒ f · x `∷ mL · f · xs ]形式化
我们接下来展示如何形式化：
- 原语数字
- let 绑定
- 积
- 积的替代表示方法
其余构造的形式化作为练习留给读者。
导入
import Relation.Binary.PropositionalEquality as Eq open Eq using (_≡_; refl) open import Data.Empty using (⊥; ⊥-elim) open import Data.Nat using (ℕ; zero; suc; _*_; _<_; _≤?_; z≤n; s≤s) open import Relation.Nullary using (¬_) open import Relation.Nullary.Decidable using (True; toWitness)
语法
infix 4 _⊢_ infix 4 _∋_ infixl 5 _,_ infixr 7 _⇒_ infixr 9 _`×_ infix 5 ƛ_ infix 5 μ_ infixl 7 _·_ infixl 8 _`*_ infix 8 `suc_ infix 9 `_ infix 9 S_ infix 9 #_
类型
data Type : Set where `ℕ : Type _⇒_ : Type → Type → Type Nat : Type _`×_ : Type → Type → Type
语境
data Context : Set where ∅ : Context _,_ : Context → Type → Context
变量及查询判断
data _∋_ : Context → Type → Set where Z : ∀ {Γ A} --------- → Γ , A ∋ A S_ : ∀ {Γ A B} → Γ ∋ B --------- → Γ , A ∋ B
项以及赋型判断
data _⊢_ : Context → Type → Set where -- 变量 `_ : ∀ {Γ A} → Γ ∋ A ----- → Γ ⊢ A -- 函数 ƛ_ : ∀ {Γ A B} → Γ , A ⊢ B --------- → Γ ⊢ A ⇒ B _·_ : ∀ {Γ A B} → Γ ⊢ A ⇒ B → Γ ⊢ A --------- → Γ ⊢ B -- 自然数 `zero : ∀ {Γ} ------ → Γ ⊢ `ℕ `suc_ : ∀ {Γ} → Γ ⊢ `ℕ ------ → Γ ⊢ `ℕ case : ∀ {Γ A} → Γ ⊢ `ℕ → Γ ⊢ A → Γ , `ℕ ⊢ A ----- → Γ ⊢ A -- 不动点 μ_ : ∀ {Γ A} → Γ , A ⊢ A ---------- → Γ ⊢ A -- 原语数字 con : ∀ {Γ} → ℕ ------- → Γ ⊢ Nat _`*_ : ∀ {Γ} → Γ ⊢ Nat → Γ ⊢ Nat ------- → Γ ⊢ Nat -- let `let : ∀ {Γ A B} → Γ ⊢ A → Γ , A ⊢ B ---------- → Γ ⊢ B -- 积 `⟨_,_⟩ : ∀ {Γ A B} → Γ ⊢ A → Γ ⊢ B ----------- → Γ ⊢ A `× B `proj₁ : ∀ {Γ A B} → Γ ⊢ A `× B ----------- → Γ ⊢ A `proj₂ : ∀ {Γ A B} → Γ ⊢ A `× B ----------- → Γ ⊢ B -- 积的替代表示方法 case× : ∀ {Γ A B C} → Γ ⊢ A `× B → Γ , A , B ⊢ C -------------- → Γ ⊢ C
缩减 de Bruijn 因子
length : Context → ℕ length ∅ = zero length (Γ , _) = suc (length Γ) lookup : {Γ : Context} → {n : ℕ} → (p : n < length Γ) → Type lookup {(_ , A)} {zero} (s≤s z≤n) = A lookup {(Γ , _)} {(suc n)} (s≤s p) = lookup p count : ∀ {Γ} → {n : ℕ} → (p : n < length Γ) → Γ ∋ lookup p count {_ , _} {zero} (s≤s z≤n) = Z count {Γ , _} {(suc n)} (s≤s p) = S (count p) #_ : ∀ {Γ} → (n : ℕ) → {n∈Γ : True (suc n ≤? length Γ)} -------------------------------- → Γ ⊢ lookup (toWitness n∈Γ) #_ n {n∈Γ} = ` count (toWitness n∈Γ)
重命名
ext : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ∋ A) --------------------------------- → (∀ {A B} → Γ , A ∋ B → Δ , A ∋ B) ext ρ Z = Z ext ρ (S x) = S (ρ x) rename : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ∋ A) ----------------------- → (∀ {A} → Γ ⊢ A → Δ ⊢ A) rename ρ (` x) = ` (ρ x) rename ρ (ƛ N) = ƛ (rename (ext ρ) N) rename ρ (L · M) = (rename ρ L) · (rename ρ M) rename ρ (`zero) = `zero rename ρ (`suc M) = `suc (rename ρ M) rename ρ (case L M N) = case (rename ρ L) (rename ρ M) (rename (ext ρ) N) rename ρ (μ N) = μ (rename (ext ρ) N) rename ρ (con n) = con n rename ρ (M `* N) = rename ρ M `* rename ρ N rename ρ (`let M N) = `let (rename ρ M) (rename (ext ρ) N) rename ρ `⟨ M , N ⟩ = `⟨ rename ρ M , rename ρ N ⟩ rename ρ (`proj₁ L) = `proj₁ (rename ρ L) rename ρ (`proj₂ L) = `proj₂ (rename ρ L) rename ρ (case× L M) = case× (rename ρ L) (rename (ext (ext ρ)) M)
同时代换
exts : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ⊢ A) → (∀ {A B} → Γ , A ∋ B → Δ , A ⊢ B) exts σ Z = ` Z exts σ (S x) = rename S_ (σ x) subst : ∀ {Γ Δ} → (∀ {C} → Γ ∋ C → Δ ⊢ C) → (∀ {C} → Γ ⊢ C → Δ ⊢ C) subst σ (` k) = σ k subst σ (ƛ N) = ƛ (subst (exts σ) N) subst σ (L · M) = (subst σ L) · (subst σ M) subst σ (`zero) = `zero subst σ (`suc M) = `suc (subst σ M) subst σ (case L M N) = case (subst σ L) (subst σ M) (subst (exts σ) N) subst σ (μ N) = μ (subst (exts σ) N) subst σ (con n) = con n subst σ (M `* N) = subst σ M `* subst σ N subst σ (`let M N) = `let (subst σ M) (subst (exts σ) N) subst σ `⟨ M , N ⟩ = `⟨ subst σ M , subst σ N ⟩ subst σ (`proj₁ L) = `proj₁ (subst σ L) subst σ (`proj₂ L) = `proj₂ (subst σ L) subst σ (case× L M) = case× (subst σ L) (subst (exts (exts σ)) M)
单个和双重代换
_[_] : ∀ {Γ A B} → Γ , B ⊢ A → Γ ⊢ B --------- → Γ ⊢ A _[_] {Γ} {A} {B} N M = subst {Γ , B} {Γ} σ {A} N where σ : ∀ {A} → Γ , B ∋ A → Γ ⊢ A σ Z = M σ (S x) = ` x _[_][_] : ∀ {Γ A B C} → Γ , A , B ⊢ C → Γ ⊢ A → Γ ⊢ B ------------- → Γ ⊢ C _[_][_] {Γ} {A} {B} N V W = subst {Γ , A , B} {Γ} σ N where σ : ∀ {C} → Γ , A , B ∋ C → Γ ⊢ C σ Z = W σ (S Z) = V σ (S (S x)) = ` x
值
data Value : ∀ {Γ A} → Γ ⊢ A → Set where -- 函数 V-ƛ : ∀ {Γ A B} {N : Γ , A ⊢ B} --------------------------- → Value (ƛ N) -- 自然数 V-zero : ∀ {Γ} ----------------- → Value (`zero {Γ}) V-suc_ : ∀ {Γ} {V : Γ ⊢ `ℕ} → Value V -------------- → Value (`suc V) -- 原语数字 V-con : ∀ {Γ n} ----------------- → Value (con {Γ} n) -- 积 V-⟨_,_⟩ : ∀ {Γ A B} {V : Γ ⊢ A} {W : Γ ⊢ B} → Value V → Value W ---------------- → Value `⟨ V , W ⟩
在给出的参数无法确定隐式参数时，我们需要给出隐式参数。
归约
infix 2 _—→_ data _—→_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where -- 函数 ξ-·₁ : ∀ {Γ A B} {L L′ : Γ ⊢ A ⇒ B} {M : Γ ⊢ A} → L —→ L′ --------------- → L · M —→ L′ · M ξ-·₂ : ∀ {Γ A B} {V : Γ ⊢ A ⇒ B} {M M′ : Γ ⊢ A} → Value V → M —→ M′ --------------- → V · M —→ V · M′ β-ƛ : ∀ {Γ A B} {N : Γ , A ⊢ B} {V : Γ ⊢ A} → Value V -------------------- → (ƛ N) · V —→ N [ V ] -- 自然数 ξ-suc : ∀ {Γ} {M M′ : Γ ⊢ `ℕ} → M —→ M′ ----------------- → `suc M —→ `suc M′ ξ-case : ∀ {Γ A} {L L′ : Γ ⊢ `ℕ} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A} → L —→ L′ ------------------------- → case L M N —→ case L′ M N β-zero : ∀ {Γ A} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A} ------------------- → case `zero M N —→ M β-suc : ∀ {Γ A} {V : Γ ⊢ `ℕ} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A} → Value V ---------------------------- → case (`suc V) M N —→ N [ V ] -- 不动点 β-μ : ∀ {Γ A} {N : Γ , A ⊢ A} ---------------- → μ N —→ N [ μ N ] -- 原语数字 ξ-*₁ : ∀ {Γ} {L L′ M : Γ ⊢ Nat} → L —→ L′ ----------------- → L `* M —→ L′ `* M ξ-*₂ : ∀ {Γ} {V M M′ : Γ ⊢ Nat} → Value V → M —→ M′ ----------------- → V `* M —→ V `* M′ δ-* : ∀ {Γ c d} --------------------------------- → con {Γ} c `* con d —→ con (c * d) -- let ξ-let : ∀ {Γ A B} {M M′ : Γ ⊢ A} {N : Γ , A ⊢ B} → M —→ M′ --------------------- → `let M N —→ `let M′ N β-let : ∀ {Γ A B} {V : Γ ⊢ A} {N : Γ , A ⊢ B} → Value V ------------------- → `let V N —→ N [ V ] -- 积 ξ-⟨,⟩₁ : ∀ {Γ A B} {M M′ : Γ ⊢ A} {N : Γ ⊢ B} → M —→ M′ ------------------------- → `⟨ M , N ⟩ —→ `⟨ M′ , N ⟩ ξ-⟨,⟩₂ : ∀ {Γ A B} {V : Γ ⊢ A} {N N′ : Γ ⊢ B} → Value V → N —→ N′ ------------------------- → `⟨ V , N ⟩ —→ `⟨ V , N′ ⟩ ξ-proj₁ : ∀ {Γ A B} {L L′ : Γ ⊢ A `× B} → L —→ L′ --------------------- → `proj₁ L —→ `proj₁ L′ ξ-proj₂ : ∀ {Γ A B} {L L′ : Γ ⊢ A `× B} → L —→ L′ --------------------- → `proj₂ L —→ `proj₂ L′ β-proj₁ : ∀ {Γ A B} {V : Γ ⊢ A} {W : Γ ⊢ B} → Value V → Value W ---------------------- → `proj₁ `⟨ V , W ⟩ —→ V β-proj₂ : ∀ {Γ A B} {V : Γ ⊢ A} {W : Γ ⊢ B} → Value V → Value W ---------------------- → `proj₂ `⟨ V , W ⟩ —→ W -- 积的替代表示方式 ξ-case× : ∀ {Γ A B C} {L L′ : Γ ⊢ A `× B} {M : Γ , A , B ⊢ C} → L —→ L′ ----------------------- → case× L M —→ case× L′ M β-case× : ∀ {Γ A B C} {V : Γ ⊢ A} {W : Γ ⊢ B} {M : Γ , A , B ⊢ C} → Value V → Value W ---------------------------------- → case× `⟨ V , W ⟩ M —→ M [ V ][ W ]
自反传递闭包
infix 2 _—↠_ infix 1 begin_ infixr 2 _—→⟨_⟩_ infix 3 _∎ data _—↠_ {Γ A} : (Γ ⊢ A) → (Γ ⊢ A) → Set where _∎ : (M : Γ ⊢ A) ------ → M —↠ M step—→ : (L : Γ ⊢ A) {M N : Γ ⊢ A} → M —↠ N → L —→ M ------ → L —↠ N pattern _—→⟨_⟩_ L L—→M M—↠N = step—→ L M—↠N L—→M begin_ : ∀ {Γ A} {M N : Γ ⊢ A} → M —↠ N ------ → M —↠ N begin M—↠N = M—↠N
值不再归约
V¬—→ : ∀ {Γ A} {M N : Γ ⊢ A} → Value M ---------- → ¬ (M —→ N) V¬—→ V-ƛ () V¬—→ V-zero () V¬—→ (V-suc VM) (ξ-suc M—→M′) = V¬—→ VM M—→M′ V¬—→ V-con () V¬—→ V-⟨ VM , _ ⟩ (ξ-⟨,⟩₁ M—→M′) = V¬—→ VM M—→M′ V¬—→ V-⟨ _ , VN ⟩ (ξ-⟨,⟩₂ _ N—→N′) = V¬—→ VN N—→N′
可进性
data Progress {A} (M : ∅ ⊢ A) : Set where step : ∀ {N : ∅ ⊢ A} → M —→ N ---------- → Progress M done : Value M ---------- → Progress M progress : ∀ {A} → (M : ∅ ⊢ A) ----------- → Progress M progress (` ()) progress (ƛ N) = done V-ƛ progress (L · M) with progress L ... | step L—→L′ = step (ξ-·₁ L—→L′) ... | done V-ƛ with progress M ... | step M—→M′ = step (ξ-·₂ V-ƛ M—→M′) ... | done VM = step (β-ƛ VM) progress (`zero) = done V-zero progress (`suc M) with progress M ... | step M—→M′ = step (ξ-suc M—→M′) ... | done VM = done (V-suc VM) progress (case L M N) with progress L ... | step L—→L′ = step (ξ-case L—→L′) ... | done V-zero = step β-zero ... | done (V-suc VL) = step (β-suc VL) progress (μ N) = step β-μ progress (con n) = done V-con progress (L `* M) with progress L ... | step L—→L′ = step (ξ-*₁ L—→L′) ... | done V-con with progress M ... | step M—→M′ = step (ξ-*₂ V-con M—→M′) ... | done V-con = step δ-* progress (`let M N) with progress M ... | step M—→M′ = step (ξ-let M—→M′) ... | done VM = step (β-let VM) progress `⟨ M , N ⟩ with progress M ... | step M—→M′ = step (ξ-⟨,⟩₁ M—→M′) ... | done VM with progress N ... | step N—→N′ = step (ξ-⟨,⟩₂ VM N—→N′) ... | done VN = done (V-⟨ VM , VN ⟩) progress (`proj₁ L) with progress L ... | step L—→L′ = step (ξ-proj₁ L—→L′) ... | done (V-⟨ VM , VN ⟩) = step (β-proj₁ VM VN) progress (`proj₂ L) with progress L ... | step L—→L′ = step (ξ-proj₂ L—→L′) ... | done (V-⟨ VM , VN ⟩) = step (β-proj₂ VM VN) progress (case× L M) with progress L ... | step L—→L′ = step (ξ-case× L—→L′) ... | done (V-⟨ VM , VN ⟩) = step (β-case× VM VN)
求值
record Gas : Set where constructor gas field amount : ℕ data Finished {Γ A} (N : Γ ⊢ A) : Set where done : Value N ---------- → Finished N out-of-gas : ---------- Finished N data Steps {A} : ∅ ⊢ A → Set where steps : {L N : ∅ ⊢ A} → L —↠ N → Finished N ---------- → Steps L eval : ∀ {A} → Gas → (L : ∅ ⊢ A) ----------- → Steps L eval (gas zero) L = steps (L ∎) out-of-gas eval (gas (suc m)) L with progress L ... | done VL = steps (L ∎) (done VL) ... | step {M} L—→M with eval (gas m) M ... | steps M—↠N fin = steps (L —→⟨ L—→M ⟩ M—↠N) fin
例子
cube : ∅ ⊢ Nat ⇒ Nat cube = ƛ (# 0 `* # 0 `* # 0) _ : cube · con 2 —↠ con 8 _ = begin cube · con 2 —→⟨ β-ƛ V-con ⟩ con 2 `* con 2 `* con 2 —→⟨ ξ-*₁ δ-* ⟩ con 4 `* con 2 —→⟨ δ-* ⟩ con 8 ∎ exp10 : ∅ ⊢ Nat ⇒ Nat exp10 = ƛ (`let (# 0 `* # 0) (`let (# 0 `* # 0) (`let (# 0 `* # 2) (# 0 `* # 0)))) _ : exp10 · con 2 —↠ con 1024 _ = begin exp10 · con 2 —→⟨ β-ƛ V-con ⟩ `let (con 2 `* con 2) (`let (# 0 `* # 0) (`let (# 0 `* con 2) (# 0 `* # 0))) —→⟨ ξ-let δ-* ⟩ `let (con 4) (`let (# 0 `* # 0) (`let (# 0 `* con 2) (# 0 `* # 0))) —→⟨ β-let V-con ⟩ `let (con 4 `* con 4) (`let (# 0 `* con 2) (# 0 `* # 0)) —→⟨ ξ-let δ-* ⟩ `let (con 16) (`let (# 0 `* con 2) (# 0 `* # 0)) —→⟨ β-let V-con ⟩ `let (con 16 `* con 2) (# 0 `* # 0) —→⟨ ξ-let δ-* ⟩ `let (con 32) (# 0 `* # 0) —→⟨ β-let V-con ⟩ con 32 `* con 32 —→⟨ δ-* ⟩ con 1024 ∎ swap× : ∀ {A B} → ∅ ⊢ A `× B ⇒ B `× A swap× = ƛ `⟨ `proj₂ (# 0) , `proj₁ (# 0) ⟩ _ : swap× · `⟨ con 42 , `zero ⟩ —↠ `⟨ `zero , con 42 ⟩ _ = begin swap× · `⟨ con 42 , `zero ⟩ —→⟨ β-ƛ V-⟨ V-con , V-zero ⟩ ⟩ `⟨ `proj₂ `⟨ con 42 , `zero ⟩ , `proj₁ `⟨ con 42 , `zero ⟩ ⟩ —→⟨ ξ-⟨,⟩₁ (β-proj₂ V-con V-zero) ⟩ `⟨ `zero , `proj₁ `⟨ con 42 , `zero ⟩ ⟩ —→⟨ ξ-⟨,⟩₂ V-zero (β-proj₁ V-con V-zero) ⟩ `⟨ `zero , con 42 ⟩ ∎ swap×-case : ∀ {A B} → ∅ ⊢ A `× B ⇒ B `× A swap×-case = ƛ case× (# 0) `⟨ # 0 , # 1 ⟩ _ : swap×-case · `⟨ con 42 , `zero ⟩ —↠ `⟨ `zero , con 42 ⟩ _ = begin swap×-case · `⟨ con 42 , `zero ⟩ —→⟨ β-ƛ V-⟨ V-con , V-zero ⟩ ⟩ case× `⟨ con 42 , `zero ⟩ `⟨ # 0 , # 1 ⟩ —→⟨ β-case× V-con V-zero ⟩ `⟨ `zero , con 42 ⟩ ∎
练习 More （推荐和实践）
形式化本章中定义的剩余构造。 修改本文件来完成你的改动。 求值每一个例子，如果需要时将其应用于数据，来确认它返回期待的答案：
- 和（推荐）
- 单元类型（实践）
- 单元类型的替代表示方法（实践）
- 空类型（推荐）
- 列表（实践）
用下面的分隔符来标出你添加的代码：
-- begin
-- end练习 double-subst（延伸）
证明双重代换等同于两个单独代换。
postulate double-subst : ∀ {Γ A B C} {V : Γ ⊢ A} {W : Γ ⊢ B} {N : Γ , A , B ⊢ C} → N [ V ][ W ] ≡ (N [ rename S_ W ]) [ V ]
注意到我们需要交换参数，而且 W 的语境需要用重命名来调整，使得右手边的项保持良类型。
测试例子
我们重复 DeBruijn 章节中的测试例子， 来保证我们在扩展基本演算时没有破坏原演算的任何性质。
two : ∀ {Γ} → Γ ⊢ `ℕ two = `suc `suc `zero plus : ∀ {Γ} → Γ ⊢ `ℕ ⇒ `ℕ ⇒ `ℕ plus = μ ƛ ƛ (case (# 1) (# 0) (`suc (# 3 · # 0 · # 1))) 2+2 : ∀ {Γ} → Γ ⊢ `ℕ 2+2 = plus · two · two Ch : Type → Type Ch A = (A ⇒ A) ⇒ A ⇒ A twoᶜ : ∀ {Γ A} → Γ ⊢ Ch A twoᶜ = ƛ ƛ (# 1 · (# 1 · # 0)) plusᶜ : ∀ {Γ A} → Γ ⊢ Ch A ⇒ Ch A ⇒ Ch A plusᶜ = ƛ ƛ ƛ ƛ (# 3 · # 1 · (# 2 · # 1 · # 0)) sucᶜ : ∀ {Γ} → Γ ⊢ `ℕ ⇒ `ℕ sucᶜ = ƛ `suc (# 0) 2+2ᶜ : ∀ {Γ} → Γ ⊢ `ℕ 2+2ᶜ = plusᶜ · twoᶜ · twoᶜ · sucᶜ · `zero
Unicode
本章中使用了以下 Unicode：
σ U+03C3 GREEK SMALL LETTER SIGMA (\Gs or \sigma)
† U+2020 DAGGER (\dag)
‡ U+2021 DOUBLE DAGGER (\ddag)