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

## Download