From Proof Polynomials to Reflexive Combinators
by
Sergei Artemov
Moscow University and the Graduate Center of the City University of New York

The Logic of Proofs LP was introduced in [1, 2] to answer questions concerning the intended provability semantics of Gödel's provability calculus (a.k.a. the modal logic S4) and of the intuitionistic logic. These problems were first discussed by Heyting, Kolmogorov and Gödel in the 1930s; see [2] for a total account. In this talk we will introduce Reflexive Combinatory Logic RCL built on the basis of LP. RCL substantially extends the traditional Combi natory Logic by new combinators capable of handling iterated type assertions.

The Logic of Proofs LP operates with propositions and proof terms called ``proof polynomials'', built from variables and constants by three operations: ``·'' - application, ``!'' - proof checker and ``+'' - union. Along with the usual propositional atoms it has also formulas of form \lctF, where F is a formula and t a proof polynomial. Constants denote proofs of instances of axioms of the system, variables stand for unspecified proofs of open assumptions. A proof polynomial p(x, y, z, ... ) represents a proof from open assumptions, corresponding to x, y, z, ... . The exact arithmetical provability semantics of LP can be found in [1, 2]. The system LP contains axioms and rules:

A0. Axioms (and rules) of the classical propositional logic,

A1. \lctF\implies F reflection,

A2. \lct(F\implies G) \implies (\lcsF\implies \lc(t·s)G) application,

A3. \lctF \implies \lc!t(\lctF) proof checker,

A4. \lcsF \implies \lc(s+t)F,     \lctF \implies \lc(s+t)F union.

Rule: if c is a constant and A an axiom from A0 - A4, infer \lccA.

The typed combinatory logic may be regarded as a fragment of LP in the language with ``\imps'' as a sole connective, with ``·'' as the only term formation operation and with the intuitionistic logic on the background. Proof polynomials show the way of building a new sort of \lambda-calculus with arbitrary nesting of type assertions: reflexive \lambda-calculus \lambda^\infty from [3]. The system \lambda^\infty contains intuitionistic logic as its type calcul us fragment (level 0), propositional combinations of types and type assertions for typed \lambda-terms on level 1, etc. and enjoys the Internalization Property (IP): if A₁, A₂, ... , A_n\vdash B then

\lcx1A1, \lcx2A2, ... , \lcxnAn\vdash\lct(x1, x2, ... , xn)B

for some term t(x₁, x₂, ... , x_n). Note that the Curry-Howard isomorphism of logic derivations and typed \lambda-terms corresponds to IP applied to level 0.

The Reflexive Combinatory Logic RCLOn RCL combinators see also postings on my Fall 2002 lectures on Computational Logic at the CUNY Graduate Center and of Spring 2003 at Moscow University on http://www.cs.gc.cuny.edu/ ~ sartemov/.ecasts \lambda^\infty to the Combinatory Logic format. There are good reasons why RCL has the right to co-exist with \lambda^\infty: RCL is much more compact and manageable than \lambda^\infty, embedding of RCL to LP does not need coding, etc. Characteristic features of RCL are the Combinatory Logic format, a Church style rigid typing, the implicational intuitionistic logic on level 0, and the Internalization Property. Among the RCL combinators there are

\lck[A\imps(B\imps A)]	old combinator k
\lcs[(A\imps(B\imps C))\imp((A\imps B)\imps(A\imps C))]	old combinator s
\lcd[\lctF\implies F]	DENOTATE
\lco[\lct(F\implies G) \implies (\lcsF\implies \lc(t·s)G)]	INTERPRETER
\lcc[\lctF \implies \lc!t(\lctF)]	CODING

The set-theoretical semantics of types, where functional types are interpreted as sets of functions, naturally extends to RCL. In this semantics some objects have constructive counterparts names, e.g. computable functions have names, which are programs that compute them. \lctF is interpreted as a name (program) of type F. Under this reading

\lcd[\lctF\implies F] - realizes a fundamental denotational correspondence name - object, in particular, program - function.

\lco[\lct(F\implies G) \implies (\lcsF\implies \lc(t·s)G)] represents an interpreter, which maps a program t and input s to the result t·s.

\lcc[\lctF \implies \lc!t(\lctF)] maps a program into its code (alias, name, etc.).

[1] S. Artemov, ``Operational Modal Logic, '' Tech. Rep. MSI 95-29, Cornell University, 1995.

[2] S. Artemov, ``Explicit provability and constructive semantics'', The Bulletin for Symbolic Logic, v.7, No. 1, pp. 1-36, 2001.

[3] J. Alt and S. Artemov, ``Reflective lambda-calculus'', In Springer Lecture Notes in Computer Science; v. 2183, Proceedings of the Dagstuhl-Seminar on Proof Theory in Computer Science, 2001.

Footnotes:

On RCL combinators see also postings on my Fall 2002 lectures on Computational Logic at the CUNY Graduate Center and of Spring 2003 at Moscow University on http://www.cs.gc.cuny.edu/ ~ sartemov/.r

Date received: June 1, 2003