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
Times are displayed in time zone: Saskatchewan, Central America change

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