Skip to main content
CSIRO Logo Data 61 logo

Recursive function definition for types with binders

Authors

Michael Norrish

NICTA

Australian National University

Abstract

This work describes the proof and uses of a theorem allowing definition of recursive functions over the type of λ-calculus terms, where terms with bound variables are identified up to α-equivalence. The theorem embodies what is effectively a principle of primitive recursion, and the analogues of this theorem for other types with binders are clear. The theorem’s side-conditions require that the putative definition be well-behaved with respect to fresh name generation and name permutation. A number of examples over the type of λ-calculus terms illustrate the use of the new principle.

BibTeX Entry

  @inproceedings{Norrish_04,
    author           = {Norrish, Michael},
    doi              = {10.1007/978-3-540-30142-4_18},
    editor           = {{Konrad Slind and Annette Bunker and Ganesh Gopalakrishnan}},
    month            = sep,
    year             = {2004},
    title            = {Recursive Function Definition for Types with Binders},
    address          = {Park City, Utah, United States},
    pages            = {241---256},
    booktitle        = {International Conference on Theorem Proving in Higher Order Logics},
    paperurl         = {https://ts.data61.csiro.au/publications/nicta_full_text/6610.pdf},
    publisher        = {Springer},
    slides           = {/publications/nicta_slides/6610.pdf}
  }

Download