General Recursion and Formal Topology

TL;DR

This paper introduces a novel approach to express general recursion within Martin-Löf's type theory by leveraging inductively generated formal topologies, addressing longstanding limitations in representing recursive functions.

Contribution

The paper proposes a new method using inductively generated formal topologies to incorporate general recursion into type theory while preserving termination guarantees.

Findings

Successfully models general recursion within type theory.

Maintains termination of recursive computations.

Provides a formal framework for recursive definitions.

Abstract

It is well known that general recursion cannot be expressed within Martin-Loef's type theory and various approaches have been proposed to overcome this problem still maintaining the termination of the computation of the typable terms. In this work we propose a new approach to this problem based on the use of inductively generated formal topologies.