A Proof-Theoretic Account of Primitive Recursion and Primitive Iteration

Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperJournal articleResearchpeer-review

  • Luca Cherabini, Universit`a degli Studi di Parma, Italy
  • Olivier Danvy
We revisit both the usual ``going-up'' induction principle and Manna and Waldinger's ``going-down'' induction principle for primitive recursion,`a la Goedel, and primitive iteration, `a la Church. We use 'Kleene's trick' to show that primitive recursion and primitive iiteration are as expressive as the other, even in the presence of accumulators. As a result, we can directly extract a variety of recursive and iterative functional programs of the kind usually written or optimized by hand.
Original languageEnglish
JournalJournal of Formalized Reasoning
Volume4
Issue1
Pages (from-to)85-109
Number of pages25
ISSN1972-5787
Publication statusPublished - 2011

See relations at Aarhus University Citationformats

ID: 44448902