| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
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 |
| Status: [ok] | This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |