Verified 马猴烧酒 in Agda 第一篇

和我签订契约，成为魔法少女吧！
——QB in 《魔法少女小圆》

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

选择学习函数式程序设计，就好像选择成为魔法少女，如果你不能真正喜欢并且理解函数式编程、并且为它付出你学习的努力，那么你就会学废，彻彻底底地变成“函数式魔女”。

我还真是个笨蛋。
——美树沙耶香 in 《魔法少女小圆》

这是本系列文章的第一篇，主要介绍为什么我们要学习 Agda 和 Verified Programming，以及我们需要学什么。

我参考了胡振江老师的《函数式程序设计》课程的课件，以及《Verified Programming in Agda》这本书。

《函数式程序设计》课件

《Verified Programming in Agda》

$\color{red}提示:阅读本文章可能需要一定的 FP 基础（例如 Haskell）$

解决问题的一般思路

在学习 Verified Programming 之前，我们先来看看解决问题的一般思路。

一般地，要解决一个具体问题，往往需要分为两步走：

Sepcification 问题分解和抽象
Implementation 问题求解（实现）

Specification

描述问题，描述你的算法需要做什么（what）
表达你的意图
越清晰越好

Implementation

提出实现方法，描述你该如何解决这个问题（how）
描述你的算法的执行过程
在可用的时空资源内尽可能高效地解决问题

联系

这既是 Specification 和 Implementation 的联系，也是一个问题。

如何证明你的 Implementation 满足 Specification，或者说，如何证明你的 Implementation 是正确的？

因此我们需要一个工具来帮助我们证明我们的 Implementation 满足 Specification，这个工具就是 Verified Programming。

成为 Verified まほうしょうじょ in Agda 吧！

如何书写 Specification

谓词逻辑：描述你意向中的在输入和输出之间的关系
函数式：直接地使用函数描述从输入到输出的映射，这种映射是可以直接执行和计算的，但是可能极度低效。

谓词逻辑方法

例子：描述你意向中输入和输出之间的关系

Example: Increase

这是一个 Specification，描述了输入和输出之间的关系。

Increase : ℕ → ℕ
Increase n > Square n

Square : ℕ → ℕ
Square n = n * n

它讲了这么一件事：你要解决的问题（Increase）的输出需要满足严格大于输入的平方（Square）。

我们先尝试给出一个 Implementation，然后证明它满足 Specification。

1 2	Increase : ℕ → ℕ Increase n = Square n + 1

证明过程：

Increase n
= { definition of Increase }
Square n + 1
> { arithmetic property }
Square n

从而我们证明了这个 Implementation 满足 Specification。

小练习：

请给出 Increase 的另一个 Implementation，并证明它满足 Specification。

函数式方法

函数式方法直接地使用函数描述从输入到输出的映射，这种映射是可以直接执行和计算的，但是可能极度低效。

Example: quad

1 2	quad : ℕ → ℕ quad n = n * n * n * n

这是一个 Specification，描述了输入和输出之间的关系。

这个描述非常的直接，我们可以直接使用这个函数来计算，但是这个计算过程非常低效，我们看到，我们使用了三次乘法，这是不必要的。

! 如果你有一定的 OI 基础，那么你在这个问题上应该会有一些感觉，你会联想到快速幂问题吧？

通过函数式的 Specification，我们不必要去单独做出一个 Implementation，因为我们可以直接使用这个函数来计算，在计算的过程中，我们就可以完成证明

我们还可以尝试使用一些数学性质来优化这个函数，例如：

quan n
= { specification of quad }
n * n * n * n
= {since multiplication is associative}
(n * n) * (n * n)
= {definition of square}
Square n * Square n
= {definition of square}
Square Square n

在以后的学习中，我们还会看到更多这样的例子。

小练习：

拓展我们优化 quad 函数的思路至更一般的情况，尝试给出计算 exp(x,n)=x^n 的高效算法。

函数式方法的优点

可直接执行
通过更加基本的函数的组合来直接描述输入到输出的映射
当使用的函数是良构造且具有较好的代数性质的时候，函数式方法更适合推理。

解决问题的方法

举个例子，大家都做过鸡兔同笼的问题吧。

幼儿园的时候我们大约会使用这样的方法来解决这个问题：

枚举所有可能的情况，然后判断是否满足条件。

小学的时候我们大约会使用这样的方法来解决这个问题：

假设全部为鸡，然后得出脚的数量差，然后根据鸡和兔子的脚的数量差来计算鸡和兔子的数量。

中学的时候我们大约会使用这样的方法来解决这个问题：

列方程组，然后解方程组。

我们解决这个问题的方法越来越高级，解决这个问题的难度和复杂度也越低。

从以上的例子可以看出，相同的问题会有不同的难度，取决于我们使用的方法。

许多数学问题，一旦我们用上了方程组背后的等式理论，就会变得非常简单。

那么，解决编程问题的方法又是什么呢？我们有像等式理论一样的方法来构建高效而正确的程序吗？

有的，这就是：

程序演算（Calculational Programming）

程序演算

目前我对这方面还没有太深入的了解，所以这部分就先按下不表了。

以后有机会再补充。