search

lawrencecpaulson / lawrencecpaulson.github.io

the blog "Machine Logic"
13 stars 0 forks source link

https://lawrencecpaulson.github.io/2022/08/31/Ackermann-not-PR-I.html #29

Open utterances-bot opened 1 year ago

utterances-bot commented 1 year ago

Ackermann's function is not primitive recursive, I

https://lawrencecpaulson.github.io/2022/08/31/Ackermann-not-PR-I.html

adrilow commented 1 year ago

Hi! Very nice to see the theory of the Ackermann function development in the AFP. A few years ago I needed some facts about it and its inverse (it is the complexity bound of the union find data structure) and I formalized them following a Coq development. Maybe it is of interest:

https://github.com/adrilow/Proof-of-the-amortized-time-complexity-of-the-Union-Find-data-structure-in-Isabelle-HOL/blob/master/Ackermann.thy

lawrencecpaulson commented 1 year ago

I'd love to see your inverse Ackermann development in the AFP. Preferably with less usage of apply, but regardless!