Hostname: page-component-745bb68f8f-g4j75 Total loading time: 0 Render date: 2025-01-12T10:09:16.138Z Has data issue: false hasContentIssue false
  • English
  • Français

A predicative analysis of structural recursion

Published online by Cambridge University Press:  09 January 2002

ANDREAS ABEL  and
THORSTEN ALTENKIRCH
ANDREAS ABEL
Affiliation:
Department of Computer Science, University of Munich, 80538 Munich, Germany; (e-mail: [email protected])
THORSTEN ALTENKIRCH
Affiliation:
School of Computer Science & Information Technology, University of Nottingham, Nottingham NG8 1BB, UK; (e-mail: [email protected])
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

We introduce a language based upon lambda calculus with products, coproducts and strictly positive inductive types that allows the definition of recursive terms. We present the implementation (foetus) of a syntactical check that ensures that all such terms are structurally recursive, i.e. recursive calls appear only with arguments structurally smaller than the input parameters of terms considered. To ensure the correctness of the termination checker, we show that all structurally recursive terms are normalizing with respect to a given operational semantics. To this end, we define a semantics on all types and a structural ordering on the values in this semantics and prove that all values are accessible with regard to this ordering. Finally, we point out how to do this proof predicatively using set based operators.

Type
Research Article
Information
Journal of Functional Programming , Volume 12 , Issue 1 , January 2002 , pp. 1 - 41
Copyright
© 2002 Cambridge University Press
Submit a response

Discussions

No Discussions have been published for this article.