| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
Ackermann's Function Is Not Primitive Recursive
| Title: | Ackermann's Function Is Not Primitive Recursive |
| Author: | Lawrence C. Paulson |
| Submission date: | 2022-03-23 |
| Abstract: | Ackermann's function is defined in the usual way and a number of its elementary properties are proved. Then, the primitive recursive functions are defined inductively: as a predicate on the functions that map lists of numbers to numbers. It is shown that every primitive recursive function is strictly dominated by Ackermann's function. The formalisation follows an earlier one by Nora Szasz. |
| BibTeX: |
@article{Ackermanns_not_PR-AFP,
author = {Lawrence C. Paulson},
title = {Ackermann's Function Is Not Primitive Recursive},
journal = {Archive of Formal Proofs},
month = mar,
year = 2022,
note = {\url{https://isa-afp.org/entries/Ackermanns_not_PR.html},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |
| Older releases: None |