前阵子正看着 HoTT Book 中 1.12 节,即讲述 identity type 与 path induction 之类的概念,透过 Agda 对其研究与学习之后决定写一篇文章记录下有关这些概念的一些理解,以巩固一下自己对这些概念的认识。

引言

在 Agda 中,我们或多或少在一些需要证明命题等价性的 module 中可能会看到 {-# OPTIONS --without-K #-} 这么一个 language extension,但在此之前我对 Axiom K 也是一知半解,仅局限于知道这个概念其实来自于 MLTT。当然在仔细阅读以及实际地编写过代码去研究后便很快对这东西建立起直觉了,这东西其实也就是 "homogeneous" identity type 的 induction 写法而已!那么你也许会问 homogeneous,induction,identity type 又是什么?为了让读者能够通畅地了解 Axiom K,所以我们先从它的前置概念 induction 开始吧。

什么是 Induction(归纳)?

通俗地说,在逻辑领域中的 induction 指的就是把我们对某一些局部知识的认知,归纳为对整体,全局的一个认识而已,打个比方,我们知道了如今世界中能在空中飞行动物包含了 鸟类,还有昆虫类动物(比方说蜻蜓,蜜蜂 等...)/ 哺乳类(蝙蝠)/ 两栖类,那么就可以归纳出对于所有能在空中飞行的动物种类,它们必定是鸟类,昆虫类,哺乳类,两栖类动物中的任意一种。而对应到 Agda 的代码中,便可以这么表示:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
open import Data.Bool using (true; false; Bool)

data AnimalType : Set where
birds : AnimalType
insects : AnimalType
mammals : AnimalType
amphibian : AnimalType
fish : AnimalType
reptile : AnimalType

canFly : AnimalType → Bool
canFly birds = true
canFly insects = true
canFly mammals = true
canFly amphibian = true
canFly other = false

现在就能透过 canFly 判断到究竟是什么类型的动物能够飞翔了。但由于在 Agda 中的 data type 在理论上本身也只是一个带 dependent type 的 sum type(coproduct type),而 sum type 在 pattern match 时其实就可以以函数的形式表达出来。所以从理论角度来观察,导致看上去好像并不很形式化地定义出来的命题,那么如何能够把这种写法变得更加 formalize 呢?让我们接着往下看!

对于上面 “可飞行的动物种类” 这个例子中,若果把它转换成 natural deduction(自然演绎)的形式化地写出来,那么便有: \[ {\frac { \Gamma \vdash birds \quad \Gamma \vdash insects \quad \Gamma \vdash mammals \quad \Gamma \vdash amphibian \quad \Gamma \vdash fish \quad \Gamma \vdash reptile } { \Gamma \vdash AnimalType : Type } } \] 以及: \[ canFlyInd= {\frac { \Gamma \vdash C : Set \quad \Gamma \vdash m_{1..6} : C } { \Gamma \vdash canFly' : AnimalType \to Bool } } \] 那么对于 judgment \(canFlyInd\) 便是:我们有匹配不同动物种类的函数,即类型 \(C : Type\) 以及 \(m_{1...6} : C\) 作为 premises(前提),那么便能得到 \(canFly'\) 这个 conclusion(结论) 。

而透过 Curry-howard isomorphism(CH-同构),我们便可以把相应的这种命题以及其证明对应到编程语言上,例如:

1
2
3
4
5
6
7
8
9
10
11
canFlyInd : {C : Set}
→ (m₁ : C) (m₂ : C) (m₃ : C)
(m₄ : C) (m₅ : C) (m₆ : C)
→ (AnimalType → C)
canFlyInd m₁ m₂ m₃ m₄ m₅ m₆ t with t
... | birds = m₁
... | insects = m₂
... | mammals = m₃
... | amphibian = m₄
... | fish = m₅
... | reptile = m₆

然后我们便能写出 canFly',即 canFly 的 induction (principle) 版本:

1
2
canFly' : AnimalType → Bool
canFly' = canFlyInd true true true true false false

Induction 与 Pattern matching 的关系

由于在 formal 的 logical inference 中,并不能像 Haskell / Agda / Idris 等这些语言直接地利用语言特性进行 pattern matching,因此定义出 induction 并作用于此是至关重要的。而 pattern matching 对于编程语言来说表面看似是语言特性,但相信读过类型论,或着了解过上面例子的各位肯定就明白这只不过是 induction 的 “语法糖” 而已。更准确的说:“induction principle” 在 patten matching 上的体现其实就是 “proof by case analysis”!

一些 Agda 中 Induction 的例子

当然,除上述的简单例子以外,在 Agda 中由于是带有 dependent type 的,所以还得观察一下更为复杂的一点例子帮助我们消化。

修改 universe 的定义

为了更加贴合 HoTT Book 中对于 universe 的定义,我们不使用 Agda 中的 Set 作为代表 universe 的符号,而是变更为:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
{-# OPTIONS --without-K --exact-split --safe #-}
module Universes where

open import Agda.Primitive public
renaming ( Level to Universe -- We speak of universes rather than of levels.
; lzero to 𝓤₀ -- Our first universe is called 𝓤₀
; lsuc to _⁺ -- The universe after 𝓤 is 𝓤 ⁺
; Setω to 𝓤ω -- There is a universe 𝓤ω strictly above 𝓤₀, 𝓤₁, ⋯ , 𝓤ₙ, ⋯
)
using (_⊔_) -- Least upper bound of two universes, e.g. 𝓤₀ ⊔ 𝓤₁ is 𝓤₁

Type = λ ℓ → Set ℓ

infix 1 _̇

_̇ : (𝓤 : Universe) → Type (𝓤 ⁺)
𝓤 ̇ = Type 𝓤

Dependent pair types(\(\Sigma\)-types)

对于 \(\Sigma\)-types 而言,并不像上述例子般直接返回泛参 C 即可,我们首先要考虑对于 dependent type 的情况,即类型依赖于值,那么这里所返回的泛参 C 也可能依赖于某种 terms,比方说 \(p\) ,那么便有 \(C(p)\) 。以下是 \(\Sigma\)-types 在 Agda 上的定义:

1
2
3
4
5
6
7
8
-- Dependent sum type
record Σ {𝓤 𝓥} {A : 𝓤 ̇} (B : A → 𝓥 ̇) : (𝓤 ⊔ 𝓥) ̇ where
constructor _,_
field
pr₁ : A
pr₂ : B pr₁

open Σ

而根据 \(\Sigma\)-types 的实际情况,pattern matching 时只有一种可能的 case,即透过唯一的 constructor _,_ 建构 record type \(\Sigma\) ,想要定义 Σ-induction 首先要写出构建 C(x, y) 这个分支的 conclusion 的 type families:

1
{A : 𝓤 ̇} {B : A → 𝓥 ̇} (C : Σ B → 𝓦 ̇)

然后是唯一的构造过程:

1
∀ (x : A) (y : B x) → C (x , y)

在 case 的构造定义完毕后,现在我们只需要给出需要被 pattern match 的 \(\Sigma\)-types,即:

1
p : Σ B

和结论,而这个结论(type family) C 本身依赖于类型为 Σ B 的值 p

1
C p

最终将一整个命题合并在一起,并证出,便有:

1
2
3
4
5
Σ-induction : {A : 𝓤 ̇} {B : A → 𝓥 ̇} (C : Σ B → 𝓦 ̇)
→ (∀ (x : A) (y : B x) → C (x , y))
→ (p : Σ B)
→ C p
Σ-induction C g (x , y) = g x y

在 conclusion 中带有 dependent type 的 induction term 亦被称为 (dependent) eliminator

Product types

由于 product type 的 induction term 可以直接透过 dependent pair types 的 special case(即把上面的 type family C 变成一个 constant type C : 𝓦 ̇)定义出来,那么便有:

1
2
Σ-recursion : {A : 𝓤 ̇} {x : A} {B : A → 𝓥 ̇} (C : 𝓦 ̇) → C → Σ B → C
Σ-recursion C c x = Σ-induction (λ _ → C) (λ _ _ → c) x

这种只有 constant type 作为 conclusion 的 induction term 则被称为 non-dependent eliminator

Coproduct types

Coproduct type 的定义,由于非常直观而不做过多阐述:

1
2
3
4
5
6
-- Binary sum type
infixl 20 _+_

data _+_ {𝓤 𝓥} (A : 𝓤 ̇) (B : 𝓥 ̇) : Set (𝓤 ⊔ 𝓥) where
inl : (x : A) → A + B
inr : (y : B) → A + B

同样地,对 coproduct 观察后会看见其是一个 data type,并且有两个 cases,分别是 inl 以及 inr,这意味着我们的 eliminator 将会包含了对这两条分支的 case analysis。现在让我们先定义出所需用到的 type families:

1
{A : 𝓤 ̇} {B : 𝓥 ̇} (C : A + B → 𝓦 ̇)

然后分别是对两条分支进行构造的过程:

1
(∀ (a : A) → C (inl a))
1
(∀ (b : B) → C (inr b))

以及最后需要被 matching 的 coproduct type 和最终的 conclusion:

1
(x : A + B) → C x

那么整个命题连带证明过程写出来便有:

1
2
3
4
5
6
+-induction : {A : 𝓤 ̇} {B : 𝓥 ̇} (C : A + B → 𝓦 ̇)
→ (∀ (a : A) → C (inl a))
→ (∀ (b : B) → C (inr b))
→ (x : A + B) → C x
+-induction C f g (inl x) = f x
+-induction C f g (inr y) = g y

其 non-dependent eliminator 的版本则是:

1
2
+-recursion : {A : 𝓤 ̇} {B : 𝓥 ̇} {C : 𝓦 ̇} → (A → C) → (B → C) → A + B → C
+-recursion {𝓤} {𝓥} {𝓦} {A} {B} {C} = +-induction (λ _ → C)

Identity types(等价类型)

当谈到如何证明两个 terms 之间的命题是等价的,无可避免地必需提及的一个概念就是 identity types(等价类型),即在类型论上定义的等价关系。而在数学中,对于最普通的情况,这种等价关系一般分为了 propositional equality(命题等价)judgemental equality(判定等价) 以及 definitional equality(定义等价) 这三种,而对于这些情况,透过 curry-howard isomorphism(CH-同构)对应到计算机编程上表达时则为:

  • Propositional equality 是指在 types 上表达等价的意思,即等价关系的类型。
  • Judgemental equality 是指在 terms 上表达等价的意思,即该如何透过某些 terms 构造出等价类型,例如最简单的方式就是透过 Reflexive(自反性) 去定义。
  • Definitional equality 是指对于任意两个 terms,它们的含义是相等的。即例如说有 S(S(0))S 是某个自然数的前驱) 以及 2,很明显都是表达同一个数字的意思,而在定义 identity type 时无须用到。

所以当我们想在编程语言中定义等价时,便需要定义一种描述相应概念的方法,而对于 propositional equality,这种方法在类型论中被称为 type formation rules,其定义如下: \[ \frac{\Gamma \vdash A:Type} {\Gamma, x:A, y:A \vdash Id_A(x,y):Type} \] 以及透过 reflexive 的方式定义 judgemental equality 的概念,即是 term introduction rules,有: \[ \frac{\Gamma \vdash A:Type} {\Gamma, x:A \vdash refl(x) : Id_A(x,x)} \] 而在 Agda 中,则可用 data type 表达出来,有:

1
2
data Id (A : 𝓤 ̇) : A → A → 𝓤 ̇ where
refl : ∀ (x : A) → Id A x x

再把 (x : A) 部分简化并调至 data type 的参数上,再加上方便我们使用的等价符号,最终得出:

1
2
3
4
5
data Id (A : 𝓤 ̇) (x : A) : A → 𝓤 ̇ where
refl : Id A x x

_≡_ : ∀ {A : 𝓤 ̇} (x y : A) → 𝓤 ̇
_≡_ {A = A} x y = Id A x y

然后就可以这么去证明命题,例如直接使用 refl 证出 1 = 1:

1
2
3
4
5
6
proof′ : Id ℕ (suc zero) (suc zero)
proof′ = refl

-- 使用 _≡_ notation 的情况,可以直接忽略 ℕ 这个类型
proof : suc zero ≡ suc zero
proof = refl

Axiom K

现在终于进入正题了!Axiom K 其实算是个很别扭的名字,因为从它的名字你没法很直观的感知到这个公理到底是干嘛的,实际上它也只是 identity types 的 induction term(即对 identity type 进行 pattern matching,值得注意的是,在只有经典类型论或着 MLTT 的情况下,matching case 只有 refl 这么一种的情况才可能证出 identity type)。

现在让我们尝试先把它构造出来吧,首先提供一个在构造 identity type induction 所使用到的 type family C : x ≡ x → 𝓥 ̇

1
{A : 𝓤 ̇} {x : A} {C : x ≡ x → 𝓥 ̇}

然后考虑 pattern matching 时 cases 的具体情况,这里只有 refl 这么一种,那么就是:

1
C refl

再之后是需要被 matching 的 term p,以及最终的结论 C p

1
(p : x ≡ x) → C p

现在便可以完整地得到一整个 Axiom K 的式子:

1
2
𝕂 : {A : 𝓤 ̇} {x : A} {C : x ≡ x → 𝓥 ̇} → (C refl) → (p : x ≡ x) → C p
𝕂 c refl = c

Homogeneous(同质)与 Heterogeneous(异质)

J-rules

J-rules,HoTT Book 里又称 path induction,以及衍生概念 base path induction

现在让我们来尝试构造出 J-rules 吧!

Axiom UIP

Uniqueness of identity proofs(等价唯一性证明)

与 Univalence axiom 的关系