06113695

j

06113695 Kristiansen, Lars Mender, Bedeho Mesghina Wolde Non-determinism in G\"odel's system $T$. Theory Comput. Syst. 51, No. 1, 85-105 (2012). 2012 Springer-Verlag, New York, NY EN complexity theory non-determinism G\"odel's System $T$ denotational semantics

doi:10.1007/s00224-011-9377-9

Summary: The calculus $T^-$ is a successor-free version of G\"odel's $T$. It is well known that a number of important complexity classes, like e.g. the classes LOGSPACE, P, LINSPACE, ETIME and PSPACE, are captured by natural fragments of $T^-$ and related calculi. We introduce the calculus $T^{\backsim}$, which is a non-deterministic variant of $T^-$, and compare the computational power of $T^{\backsim}$ and $T^-$. First, we provide a denotational semantics for $T^{\backsim}$ and prove this semantics to be adequate. Furthermore, we prove that LINSPACE $\subseteq \mathcal {G}^{\backsim}_0\subseteq$ NLINSPACE and ETIME $\subseteq \mathcal {G}^{\backsim}_1 \subseteq$ ESPACE where $\mathcal {G}^{\backsim}_0$ and $\mathcal {G}^{\backsim}_1$ are classes of problems decidable by certain fragments of $T^{\backsim}$. (It is proved elsewhere that the corresponding fragments of $T^-$ equal respectively LINSPACE and ETIME.) Finally, we show a way to interpret $T^{\backsim}$ in $T^-$.