Write a Blog >>
Mon 20 Jan 2020 15:56 - 16:18 at Maurepas - Decidability and complexity Chair(s): Kathrin Stark

We implement in Gallina a hierarchy of functions that calculate the upper inverses to the hyperoperation/Ackermann hierarchy. Our functions run in $\Theta(b)$ for inputs expressed in unary, and in $O(b^2)$ for inputs expressed in binary (where $b$ = bitlength). We use our inverses to define linear-time functions—$\Theta(b)$ for both unary-represented and binary-represented inputs—that compute the upper inverse of the diagonal Ackermann function $\mathcal{A}(n)$. We show that these functions are consistent with the usual definition of the inverse Ackermann function $\alpha(n)$.

Mon 20 Jan

CPP-2020-papers
15:35 - 16:40: CPP 2020 - Decidability and complexity at Maurepas
Chair(s): Kathrin StarkSaarland University, Germany
CPP-2020-papers15:35 - 15:56
Talk
Yannick ForsterSaarland University, Fabian KunzeSaarland University, Maximilian WuttkeSaarland University
DOI Pre-print Media Attached
CPP-2020-papers15:56 - 16:18
Talk
Linh TranNational University of Singapore, Anshuman MohanNational University of Singapore, Aquinas HoborNational University of Singapore
DOI Pre-print Media Attached
CPP-2020-papers16:18 - 16:40
Talk
Simon SpiesSaarland University, Yannick ForsterSaarland University
DOI Pre-print Media Attached