Email Gateway (Aug 23 2022 at 08:18): Email Gateway (Aug 23 2022 at 08:18):From: Tobias Nipkow <nipkow@in.tum.de>
Implementing the Goodstein Function in λ-Calculus
Bertram Felgenhauer
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.
https://www.isa-afp.org/entries/Goodstein_Lambda.html
Enjoy!
smime.p7s
Last updated: Apr 24 2024 at 20:16 UTC