Implementing the Goodstein Function in λ-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