# Implementing the Goodstein Function in &lambda;-Calculus

 Title: Implementing the Goodstein Function in λ-Calculus Author: Bertram Felgenhauer (int-e /at/ gmx /dot/ de) Submission date: 2020-02-21 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. BibTeX: @article{Goodstein_Lambda-AFP, author = {Bertram Felgenhauer}, title = {Implementing the Goodstein Function in λ-Calculus}, journal = {Archive of Formal Proofs}, month = feb, year = 2020, note = {\url{http://isa-afp.org/entries/Goodstein_Lambda.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License