sign in
english version rss feed

inria-00277075, version 2

Inductive and Coinductive Components of Corecursive Functions in Coq

Yves Bertot () 1, Ekaterina Komendantskaya () 1

Coalgebraic Methods in Computer Science (2008)

Abstract: In Constructive Type Theory, recursive and corecursive definitions are subject to syntactic restrictions which guarantee termination for recursive functions and productivity for corecursive functions. However, many terminating and productive functions do not pass the syntactic tests. Bove proposed in her thesis an elegant reformulation of the method of accessibility predicates that widens the range of terminative recursive functions formalisable in Constructive Type Theory. In this paper, we pursue the same goal for productive corecursive functions. Notably, our method of formalisation of coinductive definitions of productive functions in Coq requires not only the use of ad-hoc predicates, but also a systematic algorithm that separates the inductive and coinductive parts of functions.

  • Domain : Computer Science/Logic in Computer Science
    Computer Science/Computer Science and Game Theory
  • Keywords : Coq – Induction – Coinduction – Productiveness – Guardedness – Accessibility Predicates.
  • Available versions :  v1 (2008-05-05) v2 (2008-07-09)
 
  • inria-00277075, version 2
  • oai:hal.inria.fr:inria-00277075
  • From: 
  • Submitted on: Wednesday, 9 July 2008 12:31:12
  • Updated on: Wednesday, 9 July 2008 21:16:37
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...