Wellfounded recursion with copatterns: a unified approach to termination and productivity
Wellfounded recursion with copatterns: a unified approach to termination and productivity
复制标题
具有共同模式的有根据的递归：终止和生产力的统一方法
DOI：
--
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
B. Pientka
中科院分区：
文献类型：
--
作者：
Andreas Abel;B. Pientka
在本文中，我们研究了基于系统F-OMEGA的核心语言的强范围，该系统支持有限和无限结构的编程。在我们先前工作的基础上，有限数据（例如有限列表和树木）是通过构造函数定义的，并通过模式匹配来操纵，而无限数据（例如流和无限树）是通过观测来定义的，并通过Copantern匹配来合成。在这项工作中，我们通过跟踪有关该类型中有限和无限数据的大小信息来采用一种基于类型的方法来进行强归一化。这保证了构图。更重要的是，模式和复制的二元性提供了一个统一的语义概念，这使我们首次可以优雅而均匀地支持有充分根据的诱导和通过单纯的重写来诱导。强有力的标准化是围绕吉拉德（Girard）的可还原性候选者进行的。因此，我们的系统允许非确定性主义，并且不依赖覆盖范围。由于系统F-OMEGA足够笼统，因此可以成为结构计算的汇编的目标，因此这项工作是代表COQ和AGDA等证明助手中以观察为中心数据的重要一步。
In this paper, we study strong normalization of a core language based on System F-omega which supports programming with finite and infinite structures. Building on our prior work, finite data such as finite lists and trees are defined via constructors and manipulated via pattern matching, while infinite data such as streams and infinite trees is defined by observations and synthesized via copattern matching. In this work, we take a type-based approach to strong normalization by tracking size information about finite and infinite data in the type. This guarantees compositionality. More importantly, the duality of pattern and copatterns provide a unifying semantic concept which allows us for the first time to elegantly and uniformly support both well-founded induction and coinduction by mere rewriting. The strong normalization proof is structured around Girard's reducibility candidates. As such our system allows for non-determinism and does not rely on coverage. Since System F-omega is general enough that it can be the target of compilation for the Calculus of Constructions, this work is a significant step towards representing observation-centric infinite data in proof assistants such as Coq and Agda.
影响因子：
0.6
作者：
Ghani N
通讯作者：
Ghani N