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

【问题标题】：Why dependently typed languages use weak head normal form to compare for convertibility为什么依赖类型语言使用弱头范式来比较可转换性
【发布时间】：2014-03-24 17:08:42
【问题描述】：

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

【问题讨论】：

您必须记住，归一化会导致指数级爆炸。如果头构造函数已经不同，则无需花费所有时间计算。

标签： coq agda dependent-type idris

【解决方案1】：

Weak-head 归一化对于基本情况已经足够且更有效。

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 页阅读更多相关信息。您还可以在网络上找到很多关于纯类型系统的类型推断和规范化的论文。

这是Theoretical Computer Science 的问题。

【讨论】：

谢谢！你能给我几个关于这些主题的好文章的链接吗？我没有问数学和理论 cs，因为这里回答 dep 类型问题的人比那里多。

【解决方案2】：

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

http://www.informatik.uni-trier.de/~ley/pers/hd/j/Jutting:L=_S=_van_Benthem
http://www.informatik.uni-trier.de/~ley/pers/hd/p/Pagano:Miguel
http://www.cs.le.ac.uk/people/ps56/publications.xml
http://www.lix.polytechnique.fr/~vsiles/papers/
http://www.cs.rhul.ac.uk/home/zhaohui/type.html

【讨论】：

作为对上述答案的编辑会更好。因为它基本上是一个链接唯一的答案。