Formalizing computability theory via partial recursive functions

TL;DR

This paper extends the Lean theorem prover's mathlib library to formalize computability theory using primitive and partial recursive functions, including a universal function and halting problem undecidability.

Contribution

It introduces a constructive encoding of partial functions and leverages type class inference for G"odel numberings, enhancing formalization and executable reasoning.

Findings

Construction of a universal partial recursive function

Proof of the undecidability of the halting problem

Executable encoding of partial functions

Abstract

We present an extension to the $\mathtt{mathlib}$ library of the Lean theorem prover formalizing the foundations of computability theory. We use primitive recursive functions and partial recursive functions as the main objects of study, and we use a constructive encoding of partial functions such that they are executable when the programs in question provably halt. Main theorems include the construction of a universal partial recursive function and a proof of the undecidability of the halting problem. Type class inference provides a transparent way to supply G\"{o}del numberings where needed and encapsulate the encoding details.