coq - 为什么依赖类型语言使用弱头范式来比较可转换性

Question

据我了解，几乎所有依赖类型的语言都使用弱头范式进行转换。为什么会这样？为什么检查可兑换性就足够了（对我来说似乎还不够）？你有什么推荐阅读的？

score 3 · Accepted Answer

弱头归一化对于基本情况来说是足够且更有效的。

x1 = x1 : t
x1 = x2 : t, x1 ≠ x2
x1 t1 ... tn = x2 : t,
x1 t1 ... tn = x2 s1 ... sn : t, x1 ≠ x2

对于递归情况，无论如何都会在子项对上调用该函数(ti, si)，因此无需急切地减少它们。

x1 t1 ... tn = x1 s1 ... sn : t

您可以在 Benjamin Pierce 编辑的类型和编程语言中的高级主题第 230 页阅读更多相关信息。您还可以在网上找到很多关于纯类型系统的类型推断和规范化的论文。

这是理论计算机科学的一个问题。

score 1 · Accepted Answer

版主可以将此答案与上述答案合并。这些是按字母顺序排列的。

2 回答 2