和我签订契约，成为函数式魔法少女吧！
——胡振江（伪） in 《函数式魔法少女》

写这个系列博文的目的是整理我在《函数式程序设计》课程中的一些笔记，以及对 Agda 和 Verified Programming 的一些理解。

这篇文章主要介绍了在 Agda 中的 Internal Verification （内生证明）的数据结构，以及相关的“内生证明”思想。

这是“内生证明”的第一篇文章，我们将会介绍 Vector 的 Internal Verification ，但是内生证明在 Vector 中还是很浅层的，应用也不是很明显，下一篇将会讲到 BST 和 B-Tree 的 Internal Verification ，这时我们就会看到 Internal Verification 的一些更加深入的应用。

但是，下一节将会更加烧脑，所以这一章就权当过渡，休息休息脑子罢！

Agda，启动！

参考资料：

《函数式程序设计》课件

《Verified Programming in Agda》

提示:阅读本文章可能需要一定的 FP 基础（例如 Haskell），并掌握 Agda Mode 的基本使用方法

本文章含有 Github Copilot 生成的内容，但作者进行了正确性检查，因而文责自负，如有错误的地方欢迎斧正。

Internal Verification

Internal Verification （内生证明） 是一种 Verified Programming 的方法，它的思想是将证明和程序结合在一起，这样就可以在程序中使用证明，而不是在程序外部使用证明。

我们先来比较一下 Internal Verification 和 External Verification （外部证明）的区别。

在 External Verification 中，我们需要在程序外部写出证明，比如说我们先定义一些函数，然后再证明一些和这些函数有关的定理。

一般我们会使用 External Verification 来证明一些和程序无关的定理，例如数学/代数定理，例如我们之前一些章节中讲过的 Boolean Algebra , Natural Number , List Theory 都是用 External Verification 来证明的。

而在 Internal Verification 中，我们将证明和程序结合在一起，这样我们就可以在程序中使用证明，而不是在程序外部使用证明。

我们利用 Internal Verification 书写的函数会含有更多的 argument ，这些 argument 用来传入证明。

Internal Verification 有以下的特点：

  • 可以用于数据类型的基本不变量
  • 可以更容易的用于设计复杂的程序而不发生错误
  • 更难以阅读

更难以阅读

接下来就让我们看一下 Internal Verification 的一些例子。

Vector with Internal Verification

在当时使用 C++ 的时候，我就想过，如果我们能够在编译的时候就知道 Vector 的长度，那么我们就可以在编译的时候就知道 Vector 的越界错误，这样就可以避免很多的错误。

如果我们的 Vector 自带一个长度，而不需要每次都去计算长度，那么我们就会有更多的信息，也可以基于此做一些内生证明。

在 Agda 中，我们可以这样定义一个 Vector：

1
2
3
4
5
data vector (A : Set) : ℕ → Set where
  []  : vector A zero
  _∷_ : ∀ {n} → A → vector A n → vector A (suc n)

infixr 5 _∷_

我们再写一个具体的例子：

1
2
v : vector ℕ 3
v = 1 ∷ 2 ∷ 3 ∷ []

Vector 的一些函数

连接两个 Vector 的函数：

1
2
3
_++v_ : ∀ {A n m} → vector A n → vector A m → vector A (n + m)
[] ++v ys = ys
(x ∷ xs) ++v ys = x ∷ (xs ++v ys)

上面我们还没有看出什么不同，但是接下来我们就可以看到 Internal Verification 的一些用处了。

取 Vector 的第一个元素：

我们为了取 Vector 的第一个元素，我们需要证明 Vector 的长度不为 0，这样我们才能够取出 Vector 的第一个元素，而此时我们并不需要从外部传入证明，而是在函数内部进行证明。

1
2
headv : ∀ {A n} → vector A (suc n) → A
headv (x ∷ xs) = x

在这里，我们使用 head 函数时，定义域就排除掉了长度为 0 的 Vector，这样我们就不需要在函数外部传入证明了。

取 Vector 的尾部：

1
2
3
tailv : ∀ {A n} → vector A n → vector A (pred n)
tailv [] = []
tailv (x ∷ xs) = xs

map 函数：

1
2
3
mapv : ∀ {A B n} → (A → B) → vector A n → vector B n
mapv f [] = []
mapv f (x ∷ xs) = f x ∷ mapv f xs

concat 函数：

1
2
3
concatv : ∀ {A n m} → vector (vector A m) n → vector A (n * m)
concatv [] = []
concatv (xs ∷ xss) = xs ++v concatv xss

取出 Vector 的第 n 个元素：

1
2
3
4
5
nthv : ∀ {A : Set} {m : ℕ} → (n : ℕ) → (n <ℕ m) ≡ true → vector A m → A
nthv zero _ (x ∷ xs) = x
nthv (suc n) p (x ∷ xs) = nthv n p xs
nthv (suc n) () []
nthv zero () []

我们使用了 Absurd Pattern 来处理不可能的情况（它们超出了函数的定义域）

重复一个元素 n 次：

1
2
3
repeatv : ∀ {A : Set} → (n : ℕ) → A → vector A n
repeatv zero x = []
repeatv (suc n) x = x ∷ repeatv n x

Vector 的一些应用

造一个 n * m 的矩阵：

1
2
3
4
5
6
7
_by_matrix : (n m : ℕ) → Set
n by m matrix = vector (vector ℕ m) n

-- ==========================
-- example: 2 by 3 matrix = vector (vector ℕ 3) 2
-- (6 :: 5 :: 4 :: []) :: (3 :: 2 :: 1 :: [])
-- ==========================

基本的矩阵构造：

零矩阵：

1
2
3
4
5
6
7
8
-- helper functions
zero-vec : (n : ℕ) → vector ℕ n
zero-vec zero = []
zero-vec (suc n) = zero ∷ zero-vec n
--
zero-matrix : (n m : ℕ) → n by m matrix
zero-matrix zero m = []
zero-matrix (suc n) m = zero-vec m ∷ zero-matrix n m

对角矩阵和单位矩阵：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
gen-vec : (n : ℕ) → (d : ℕ) → (pos : ℕ) → vector ℕ n
gen-vec zero d pos = []
gen-vec (suc n) d pos with pos =ℕ n
... | true = d ∷ gen-vec n d pos
... | false = zero ∷ gen-vec n d pos

diag-calculation : (n : ℕ) → (m : ℕ) → (d : ℕ) -> m by n matrix
diag-calculation n zero d = []
diag-calculation n (suc m) d = gen-vec n d m ∷ diag-calculation n m d
-- 
diagonal-matrix : (n : ℕ) → (d : ℕ) → n by n matrix
diagonal-matrix n d = diag-calculation n n d

identity-matrix : (n : ℕ) → n by n matrix
identity-matrix n = diagonal-matrix n (suc zero)

一些有点考验代码能力，值得讲一讲的矩阵基本运算计算编程：

取出矩阵的 (i, j) 位置的元素：

1
2
3
4
5
6
7
8
9
10
11
12
13
vector-elt : {n : ℕ} → vector ℕ n → (i : ℕ) → i <ℕ n ≡ true → ℕ
vector-elt {(suc n)} (x ∷ xs) zero p = x
vector-elt {(suc n)} (x ∷ xs) (suc i) p = vector-elt {n} xs i p
-- 
-- begin from 0,0 end in (n-1,m-1)
matrix-elt : {n m : ℕ}
  → n by m matrix
  → (i j : ℕ)
  → i <ℕ n ≡ true
  → j <ℕ m ≡ true
  → ℕ
matrix-elt {n} {m} (x ∷ xs) zero j p q = vector-elt x j q
matrix-elt {(suc n)} {m} (x ∷ xs) (suc i) j p q = matrix-elt {n} {m} xs i j p q

在这个问题中，我们对矩阵逐层“剥皮”处理，先找到第 i 行，然后再在第 i 行中找到第 j 个元素。

我们通过在函数中传入证明来保证 i 和 j 的范围在矩阵的范围内。

矩阵转置：

如果你天真地认为在 Agda 中写一个矩阵转置函数是很简单的，那么你就错了。

如果你更加天真地想要使用上文中的 matrix-elt 函数来写一个矩阵转置函数，那么你就会走进一个无底洞。

家人们，我们还是回忆一下过去在 Haskell 中学到的一些列表操作吧。

1
2
3
4
5
6
7
8
9
10
11
zipWith : ∀  {A : Set } {B : Set } {C : Set }{n : ℕ} → (A → B → C) → vector A n → vector B n → vector C n
zipWith f [] [] = []
zipWith f (x ∷ xs) (y ∷ ys) = (f x y) ∷ (zipWith f xs ys)

repeat-vec : ∀  {A : Set } → (x : A) → (n : ℕ) → vector A n
repeat-vec x zero = []
repeat-vec x (suc n) = x ∷ (repeat-vec x n) 

transpose : {n m : ℕ} → n by m matrix → m by n matrix
transpose {n} {m} [] = repeat-vec [] m
transpose (x ∷ xs) = zipWith (λ x y → x ∷ y) x (transpose xs)

在这里，我们使用了 zipWith 函数，它的作用是将两个 Vector 中的元素两两配对，然后再使用一个函数对这两个元素进行操作。

我们用 repeat-vec 函数来处理矩阵的边界情况，从而保证我们转置函数的正确性。

在取转置的过程中，我们用 zipWith 函数将矩阵的每一行的元素和转置后的矩阵的每一行的元素进行配对，然后再将这一行的每一个元素分别地插入到转置后的矩阵的每一行的元素的前面，相当于插入到第一列，试着动笔画一画，我们是不是完成了矩阵的转置呢？

然后此时你尝试递归到边界情况，然后你就会发现我们为什么要使用 repeat-vec 将一个空的 Vector 重复 m 次，这样实际上构成了一个 m * 0 的矩阵，这样我们就可以将这个 m * 0 的矩阵和我们的取出来的每一行进行 zipWith 操作了。

小练习：尝试证明你的转置函数的正确性
Hint：你可能需要回到定义中去比较任意 (i, j) 位置的元素和转置后的 (j, i) 位置的元素相等
我也没有写过这个证明，如果你写出来了，欢迎在评论区分享你的证明，当然寒假我也会视情况进行一些探索。

点积：

很显然吧，不需要解释罢。

1
2
3
_∙_ : {n : ℕ} → (x y : vector ℕ n) → ℕ
(x ∷ xs) ∙ (y ∷ ys) = x * y + (xs ∙ ys)
[] ∙ [] = 0

在写到点积的时候，我回想起今天上课的时候讲到的 foldr fusion，我们是否也可以用类似的方式来对点积的函数进行 formalization，然后写出一个更加一般化和优美的形式呢？

这里小留一个坑，等我寒假有空了再来填吧。

完整参考代码

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
module internal where

open import natural
open import Data.Bool using (true; false; Bool; if_then_else_)
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong)
open Eq.≡-Reasoning using (begin_; step-≡; step-≡˘; _≡⟨⟩_; _∎)
open import Data.List hiding (zipWith)


data vector (A : Set) : ℕ → Set where
  []  : vector A zero
  _∷_ : ∀ {n} → A → vector A n → vector A (suc n)

infixr 5 _∷_

_++v_ : ∀ {A n m} → vector A n → vector A m → vector A (n + m)
[] ++v ys = ys
(x ∷ xs) ++v ys = x ∷ (xs ++v ys)

headv : ∀ {A n} → vector A (suc n) → A
headv (x ∷ xs) = x

tailv : ∀ {A n} → vector A n → vector A (pred n)
tailv [] = []
tailv (x ∷ xs) = xs

mapv : ∀ {A B n} → (A → B) → vector A n → vector B n
mapv f [] = []
mapv f (x ∷ xs) = f x ∷ mapv f xs

concatv : ∀ {A n m} → vector (vector A m) n → vector A (n * m)
concatv [] = []
concatv (xs ∷ xss) = xs ++v concatv xss

nthv : ∀ {A : Set} {m : ℕ} → (n : ℕ) → (n <ℕ m) ≡ true → vector A m → A
nthv zero _ (x ∷ xs) = x
nthv (suc n) p (x ∷ xs) = nthv n p xs
nthv (suc n) () []
nthv zero () []

repeatv : ∀ {A : Set} → (n : ℕ) → A → vector A n
repeatv zero x = []
repeatv (suc n) x = x ∷ repeatv n x

_by_matrix : (n m : ℕ) → Set
n by m matrix = vector (vector ℕ m) n

-- ==========================
-- example: 2 by 3 matrix = vector (vector ℕ 3) 2
-- (6 :: 5 :: 4 :: []) :: (3 :: 2 :: 1 :: [])
-- ==========================

-- helper functions
zero-vec : (n : ℕ) → vector ℕ n
zero-vec zero = []
zero-vec (suc n) = zero ∷ zero-vec n
--
zero-matrix : (n m : ℕ) → n by m matrix
zero-matrix zero m = []
zero-matrix (suc n) m = zero-vec m ∷ zero-matrix n m

gen-vec : (n : ℕ) → (d : ℕ) → (pos : ℕ) → vector ℕ n
gen-vec zero d pos = []
gen-vec (suc n) d pos with pos =ℕ n
... | true = d ∷ gen-vec n d pos
... | false = zero ∷ gen-vec n d pos

diag-calculation : (n : ℕ) → (m : ℕ) → (d : ℕ) -> m by n matrix
diag-calculation n zero d = []
diag-calculation n (suc m) d = gen-vec n d m ∷ diag-calculation n m d
-- 
diagonal-matrix : (n : ℕ) → (d : ℕ) → n by n matrix
diagonal-matrix n d = diag-calculation n n d


identity-matrix : (n : ℕ) → n by n matrix
identity-matrix n = diagonal-matrix n (suc zero)

vector-elt : {n : ℕ} → vector ℕ n → (i : ℕ) → i <ℕ n ≡ true → ℕ
vector-elt {(suc n)} (x ∷ xs) zero p = x
vector-elt {(suc n)} (x ∷ xs) (suc i) p = vector-elt {n} xs i p
-- 
-- begin from 0,0 end in (n-1,m-1)
matrix-elt : {n m : ℕ}
  → n by m matrix
  → (i j : ℕ)
  → i <ℕ n ≡ true
  → j <ℕ m ≡ true
  → ℕ
matrix-elt {n} {m} (x ∷ xs) zero j p q = vector-elt x j q
matrix-elt {(suc n)} {m} (x ∷ xs) (suc i) j p q = matrix-elt {n} {m} xs i j p q

zipWith : ∀  {A : Set } {B : Set } {C : Set }{n : ℕ} → (A → B → C) → vector A n → vector B n → vector C n
zipWith f [] [] = []
zipWith f (x ∷ xs) (y ∷ ys) = (f x y) ∷ (zipWith f xs ys)

repeat-vec : ∀  {A : Set } → (x : A) → (n : ℕ) → vector A n
repeat-vec x zero = []
repeat-vec x (suc n) = x ∷ (repeat-vec x n) 

transpose : {n m : ℕ} → n by m matrix → m by n matrix
transpose {n} {m} [] = repeat-vec [] m
transpose (x ∷ xs) = zipWith (λ x y → x ∷ y) x (transpose xs)

_∙_ : {n : ℕ} → (x y : vector ℕ n) → ℕ
(x ∷ xs) ∙ (y ∷ ys) = x * y + (xs ∙ ys)
[] ∙ [] = zero