提问人: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
下一个:时间序列数据模式识别方法
评论
x
y
z
maj true false z = z
z
maj true false true = true
maj true false false = false
maj true false z = z
z
true
false