Implementing the Goodstein Function in λ-Calculus (Q7361484)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry Goodstein_Lambda
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Implementing the Goodstein Function in λ-Calculus |
AFP entry Goodstein_Lambda |
Statements
21 February 2020
0 references
Bertram Felgenhauer
0 references
Implementing the Goodstein Function in λ-Calculus (English)
0 references
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.
0 references
