模式匹配

模式匹配是一种借助分类讨论的思路定义映射的手法, 常用但不限于类型论中.

1基本思路

通过分析映射的输入部分的格式, 将输入直接分解为一组数据 (而不是将输入作为一个 “变量” 看待) 而定义映射的方式就是模式匹配. 比如, 取出一个二元向量的第一个分量可以用如下两种写法定义:

$$\begin{array}{rl}f& (x)=x_1\\ f& (⟨x,y⟩)=x\end{array}$$

前者没有使用模式匹配, 而后者在使用模式匹配.

若输入存在多种可能的分解, 则需要一一列出, 比如模式匹配的写法定义归纳法就需要处理 $0$ 和其它自然数的情况:

$$\begin{array}{rl}\mathrm{ind}& (0)=x\\ \mathrm{ind}& (s(n))=f(n,\mathrm{ind}(n))\end{array}$$

其中 $f$ 表示任意函数. 这也是自然数类型的消去规则的另一种写法.

在类型论中

•	归纳类型的消去规则基本可以看作是对它的构造规则进行模式匹配, 再将这个过程中出现的数据全部作为某个函数的参数, 最后得到的函数.

•	余归纳类型的构造规则可以看作是对它的消去规则进行模式匹配.

•	高阶归纳类型的消去规则需要额外处理对一个相等类型应用一个函数的特殊情况, 但基本思想和归纳类型一致.

2语义

模式匹配有多种可能的语义, 最经典的便是将其认为是归纳类型的消去规则的直观写法, 即 “写作模式匹配, 读作消去规则”. 这一般是模式匹配标准的理解方式.

作为计算规则

模式匹配的写法很容易让人代入重写系统的思维去理解, 认为模式匹配的每一条语句都是一种计算规则, 然而这并不符合标准的语义, 如下便是一个反例.

例 2.1. 如下函数试图计算两个自然数中较大的一个: $$\begin{array}{rl}\max & :\mathbb{N}\to \mathbb{N}\to \mathbb{N}\\ \max & (0,n)=n\\ \max & (n,0)=n\\ \max & (s(a),s(b))=s(\max (a,b))\end{array}$$该函数可以简易地改写为使用消去规则实现的形式, 但无论如何都无法直接使得它的前两条语句变成计算规则. 换言之, 如下两等式只能有一个成立: $$\begin{array}{rl}\max & (0,n)=n\\ \max & (n,0)=n\end{array}$$当然, 这两个等式之间用相等类型表达的相等关系是可以证明的.

若将每一条语句视为计算规则, 那么可以让类型论中有更多的等式, 但就不能保证所有函数都是由消去规则定义的, 极大地增强了类型论的表达力、且能简化部分证明, 但也破坏了类型论原本较为模块化的规则 (即, 所有构造、消去规则都是附加在一个类型上的).

除此之外, 这样做还有一个显然的问题. 考虑如下定义:

$$\begin{array}{rl}f(n,0)& =1\\ f(0,n)& =2\end{array}$$

若存在这样的函数, 那么有 $f(0,0)=1=2$, 矛盾! 因此, 我们需要确保每一条计算规则之间重叠的部分都是相等的. 这类似于在重写系统中保证合流性.

这样的模式匹配叫做重叠但无序的.

3相关概念

•	消去规则
•	简化归纳族

术语翻译

模式匹配 • 英文 pattern matching

重叠但无序 • 英文 overlapping and order-independent