Constructing Recursion Operators in Intuitionistic Type Theory

TL;DR

This paper develops a theory of well-founded relations within intuitionistic type theory, enabling formal derivation of recursion and induction schemes for complex relations, facilitating theorem proving in systems like Nuprl.

Contribution

It introduces a comprehensive framework for recursion over well-founded relations in intuitionistic type theory, extending primitive recursion to higher types and complex relations.

Findings

Formal derivation of induction and recursion schemes for well-founded relations

Application to natural numbers, inverse images, addition, multiplication, and exponentiation

Comparison with ordinal recursion over higher types

Abstract

Martin-L\"of's Intuitionistic Theory of Types is becoming popular for formal reasoning about computer programs. To handle recursion schemes other than primitive recursion, a theory of well-founded relations is presented. Using primitive recursion over higher types, induction and recursion are formally derived for a large class of well-founded relations. Included are < on natural numbers, and relations formed by inverse images, addition, multiplication, and exponentiation of other relations. The constructions are given in full detail to allow their use in theorem provers for Type Theory, such as Nuprl. The theory is compared with work in the field of ordinal recursion over higher types.