Partiality and Recursion in Interactive Theorem Provers
associated with ITP
PAR-2010 workshop is a venue for researchers developing new approaches to cope with partial functions and terminating general recursion in (interactive) theorem provers.
Interactive theorem provers (ITPs) with inductive types provide a restricted programming language together with a formal meta-theory for reasoning about the language. Because propositions are represented as types and proofs as programs, we cannot allow non-terminating proofs as they may lead to inconsistency. There is also another technical reason for the termination requirement: to decide type-checking of dependent types we need to be able to reduce type expressions to normal form.
When it comes to recursion, termination is syntactically ensured by imposing that the recursive calls must be made on structurally smaller arguments, nowadays known as structural recursion. However, many interesting terminating functions are not structurally recursive, and thus the existing methods used for ensuring termination in ITPs are too restrictive.
Many ITPs also support coinductive types. Coinductive datatypes provide a way to represent infinite data objects; for example, streams of data can be viewed as infinite lists. Coinductive datatypes introduce corecursive objects, on which we can define functions. Termination is not required for these functions, but termination still plays a role since every finite value should still be computable in finite time, even if the computation involves an interaction with a corecursive (possibly infinite) object. This constraint boils down to the concept of productivity. Roughly speaking, infinite sequences of recursive calls where no data is being produced must be avoided. For recursive programs, productivity is undecidable for the same reason that termination is. Therefore, a restrictive criterion, guardedness, is used to describe those productive corecursive functions that are legitimate in ITPs.
The challenge to widen the range of recursive and corecursive functions allowed in ITPs is one of the main theoretical challengies the developers of ITPs have to tackle. And we hope that PAR-10 will provide an opportunity to discuss the issues.
More information can be found here.
- Alexander Krauss, Technische Universitat Muenchen. Recursive Definitions of Monadic Functions.
- Conor McBride, University of Strathclyde. Djinn, monotonic.