Typing in reflective combinatory logic

DOI10.1016/J.APAL.2005.11.004MaRDI QIDQ2498910zbMATH OpenOpenAlexFDO

Authors Nikolai Krupski

Publication date 16 August 2006

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.apal.2005.11.004

zbMATH Keywords

complexity, cut elimination derivability proof theory reflective combinatory logic typing well-formed formula

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Cut-elimination and normal-form theorems (03F05)

Review text

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.

Recommendations

Cites work

Cited in

(8)

This page was built for publication: Typing in reflective combinatory logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2498910)