提问人：user11718766 提问时间：10/27/2023 更新时间：10/27/2023 访问量：63
为什么一些不相交和详尽的模式不能表示为定义上的等式？
Why can some disjoint and exhaustive patterns not be represented as definitional equalities?
问：
我目前正在阅读 Ulf Norell 的博士论文，他在论文中描述了 Agda 的实现。
在第 2.2 章（第 41 页）中，他关注的是与依赖类型的模式匹配，他指出，有些模式——即使它们是不相交的和详尽的——也不能表示为底层核心类型理论中的定义等式。他用下面的例子来说明这一点：
maj : Bool → Bool → Bool → Bool
maj true true true = true
maj true false z = z
maj false y true = y
maj x true false = x
maj false false false = false
不幸的是，他没有证明或激励这一说法。凭直觉，我认为这是真的，因为我们可能无法真正使用核心理论来“计数”，但我没有找到任何适当的论据来说服我这个陈述的真实性。
这里有人可以解释一下，为什么某些不相交和详尽的模式不能表示为定义等式——也许使用上面的例子？
答：
1赞
Jesper
10/27/2023
#1
我们在 ESOP 2014 （https://jesper.cx/files/overlapping-and-order-independent-patterns.pdf） 的论文“重叠和顺序无关模式”中对此示例进行了广泛的讨论。
基本上，大多数证明助手通过模式匹配将定义转换为案例树（有时甚至进一步转换为消除器），但是没有办法将函数忠实地表示为案例树。这样做的原因是，案例树迫使你决定首先匹配哪个参数，但是一旦你匹配任何参数，该参数是变量的等式就不再具有定义相等性。maj
下一个：时间序列数据模式识别方法
评论
xyzmaj true false z = zzmaj true false true = truemaj true false false = falsemaj true false z = zztruefalse