Implementing the Goodstein Function in Λ-Calculus

Bertram Felgenhauer 📧

February 21, 2020

Abstract

In this formalization, we develop an implementation of the Goodstein function G in plain λ-calculus, linked to a concise, self-contained specification. The implementation works on a Church-encoded representation of countable ordinals. The initial conversion to hereditary base 2 is not covered, but the material is sufficient to compute the particular value G(16), and easily extends to other fixed arguments.
BSD License

Topics

Theories of Goodstein_Lambda