Checking correctness for recursive definitions with mixed inductive and coinductive types
Pierre Hyvernat
LAMA, Université Savoie Mont Blanc
https://www.lama.univ-savoie.fr/pagesmembres/hyvernat/
Date(s) : 04/07/2019 iCal
11h00 - 12h30
The Size-Change Principle (SCP) is a simple algorithm giving a partial termination test for recursive definitions. If the language is lazy, it also gives (by duality) a partial productivity test for recursive functions involving coinductive types. This is what is used in Agda.
Unfortunately, when inductive and coinductive types are nested, this is unsound: there are « well typed » and terminating recursive definitions producing terms in empty types. Such definitions make Agda inconsistent.
Using ideas from L. Santocanale about circular proof and parity games, I’ll show how the SCP can be used to check « totality » of recursive definitions. Besides the SCP, the main ingredient is a more informative of notion call-graph, and I’ll sketch the proof of correctness by defining their « untyped » semantics using power domains.
Catégories
