← All papers
Formalizing Computability Theory via Partial Recursive Functions
cs.LO
Oct 19, 2018 · v3
TL;DR
Formalizes computability theory in Lean's mathlib including the halting problem undecidability.
Abstract
We present an extension to the 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, employing a constructive encoding of partial functions such that they are executable when the programs in question provably halt. The main results 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ödel numberings where needed and encapsulate the encoding details.
Problem
The foundations of computability theory (partial recursive functions, universal functions, undecidability of halting) had not been formalized in Lean's mathlib library.
Approach
The authors formalize computability theory using primitive recursive functions and partial recursive functions in Lean. Partial functions use a constructive encoding that makes them executable when programs provably halt. Type class inference supplies Goedel numberings transparently where needed.
Results
The formalization constructs a universal partial recursive function and proves the undecidability of the halting problem. The work is contributed to Lean's mathlib library.