Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Ackermann's Function Is Not Pr...


view this post on Zulip Email Gateway (Mar 24 2022 at 07:19):

From: Tobias Nipkow <nipkow@in.tum.de>
Ackermann's Function Is Not Primitive Recursive
Lawrence C. Paulson

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.

https://www.isa-afp.org/entries/Ackermanns_not_PR.html

This formalization was moved to the AFP from the distribution (HOL/Examples/)

Enjoy!
smime.p7s


Last updated: Jul 15 2022 at 23:21 UTC