Applicative theories for logarithmic complexity classes (Q2346995)

Two theories for logarithmic space are presented. The first formalises a new two-sorted algebra that is very similar to Cook and Bellantoni's two-sorted algebra \(B\) for polynomial time [\textit{S. Bellantoni} and \textit{S. Cook}, Comput. Complexity 2, No. 2, 97--110 (1992; Zbl 0766.68037)]. The second theory describes logarithmic space by formalising concatenation- and sharply bounded recursion. The theories are inspired by Cantini's theories formalising \(B\) [\textit{A. Cantini}, Arch. Math. Logic 41, No. 2, 169--189 (2002; Zbl 1042.03015)].