重访参数性：归纳类型与命题的一致性
摘要
雷诺兹的参数性理论捕捉了参数多态函数表现一致的性质：它们在相关的实例化上产生相关的结果。在依赖类型编程语言中，此类关系和一致性证明可以在内部表达，并作为程序翻译生成。我们为 Coq 的一个重要片段提出了一种新的参数性翻译。先前对参数多态命题的翻译允许非一致性。例如，在相关的实例化上，函数可能返回逻辑不等价的命题(如 True 和 False)。我们表明，多态命题的一致性一般而言无法实现。尽管如此，我们的翻译产生了证明这两个命题逻辑等价且这些命题的任意两个证明相关的证据。这是以可能需要在实例化上施加更多假设为代价实现的，在最坏情况下要求它们同构。我们的翻译通过携带并组合式地构建关于参数性关系的额外证明，增强了先前的 Coq 翻译。一种用于翻译归纳类型和模式匹配的新方法使之更为容易。该新方法建立并推广了先前针对依赖类型编程语言的此类翻译。利用具体化与反射，我们已将我们的翻译实现为 Coq 程序。我们获得了若干更强的自由定理，适用于一个进行中的编译器正确性项目。先前，其中一些定理的证明需要数小时才能完成。
引用
@article{arxiv.1705.01163,
title = {Revisiting Parametricity: Inductives and Uniformity of Propositions},
author = {Abhishek Anand and Greg Morrisett},
journal= {arXiv preprint arXiv:1705.01163},
year = {2017}
}
备注
Addressed ICFP2017 reviews: better structure (lemmas, sections). correctness of the ISOREL translation. discussion of the necessity of assumptions. new names: weak and strong ISOREL translation. statements of theorems generated by the translations. clarification about the use of axioms, comparison with JMeq. more related work and precise comparison with HoTT