Wellfounded recursion with copatterns
- 25 September 2013
- conference paper
- conference paper
- Published by Association for Computing Machinery (ACM) in Proceedings of the 18th ACM SIGPLAN international conference on Functional programming
- Vol. 48 (9), 185-196
- https://doi.org/10.1145/2500365.2500591
Abstract
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.Keywords
This publication has 13 references indexed in Scilit:
- CopatternsPublished by Association for Computing Machinery (ACM) ,2013
- Type-Based Termination, Inflationary Fixed-Points, and Mixed Inductive-Coinductive TypesElectronic Proceedings in Theoretical Computer Science, 2012
- Polarised subtyping for sized typesMathematical Structures in Computer Science, 2008
- Type-Based Termination with Sized ProductsLecture Notes in Computer Science, 2008
- Combining Typing and Size Constraints for Checking the Termination of Higher-Order Conditional Rewrite SystemsLecture Notes in Computer Science, 2006
- Semi-continuous Sized Types and TerminationLecture Notes in Computer Science, 2006
- A Type-Based Termination Criterion for Dependently-Typed Higher-Order Rewrite SystemsLecture Notes in Computer Science, 2004
- Type-based termination of recursive definitionsMathematical Structures in Computer Science, 1999
- Intuitionistic sets and ordinalsThe Journal of Symbolic Logic, 1996
- On the productivity of recursive list definitionsACM Transactions on Programming Languages and Systems, 1989