Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New AFP entry: Implementing the Goodstein Func...

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: Nov 21 2024 at 12:39 UTC