Implementing the Goodstein Function in λ-Calculus

Bertram Felgenhauer 📧

February 21, 2020

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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


Session Goodstein_Lambda