Typing in reflective combinatory logic (Q2498910)

This paper is about Artemov's reflective combinatory logic \(RCL_\to\). In \(RCL_\to\) combinators \(k\) and \(s\) are assigned their usual Curry-Howard types, but as the system has no combinatory reduction or conversion, the combinators here are no more than labels applied to the theorems of intuitionistic implicational logic. \(RCL_\to\) also has other typed constants \(d^{()}, \;o^{()}\) and \(c^{()}\) as well as an operator ! that are not explained in the current paper. For this and a clearer understanding of these constants and their rules the reader has to go to [\textit{S. Artëmov}, ``Kolmogorov and Gödel's approach to intuitionistic logic, and investigations in this direction in the last decade'', Russ. Math. Surv. 59, No. 2, 203--229 (2004); translation from Usp. Mat. Nauk 59, No. 2, 9--36 (2003; Zbl 1074.03029)]. A strange feature of \(RCL_\to\) is that if \(F\) is a formula and \(t:F\) (\(t\) is a term of type \(F\)) then also \(tt:F, t(tt):F, \ldots \) ! The author proves that every well formed term in \(RCL_\to\) has a unique type, that typability testing and detailed type restoration can be done in polynomial time and that the derivability relation for \(RCL_\to\) is decidable and PSPACE complete.