Towards Logic of Combinatory Logic

Abstract

Typed combinatory logic found its application in various fields of computer science, e.g. program synthesis [1], machine learning, e.g. [2] and artificial intelligence, e.g. [3], etc. Developments of these fields urge for further research and development of typed combinatory logic. Although combinatory logic, both typed and untyped, has been subject of many studies, to the best of our knowledge none of them investigate combining typed combinatory logic with classical propositional logic in order to capture inference of type assignment statements. We introduce in this paper a classical propositional logic for reasoning about simply typed combinatory logic, called logic of combinatory logic, and denoted by LCL. First, we revisit a syntax of simply typed combinatory logic [5, 4, 6]. Terms of untyped combinatory logic, called CL-terms, are generated by the following syntax M,N := x |S |K |I |MN where x belongs to a countable set of term variables. The constants S,K,I are called primitive combinators. We are mostly interested in typed terms, more precisely we are interested in simply typed terms. Simple types are generated by the following syntax σ,τ := a |σ →τ where a belongs to a countable set of type variables. A type assignment statement is of the form M : σ, where M is a CL-term and σ is a simple type. Our goal was to build up a logical system for reasoning about simply typed combinatory terms. We propose extending simply typed combinatory logic with classical logical connectives of negation and conjunction. The obtained system is called logic of combinatory logic and it is denoted by LCL. The language of the logic LCL is generated by the following syntax α,β := M : σ |¬α |α ∧β We see that logic LCL is actually obtained from classical propositional logic by replacing propositional letters with type assignment statements M : σ. We argue that logic LCL is a first step towards formalization of meta-language of simply typed combinatory logic. We give an axiomatic system and propose a semantics for LCL. The ax- iomatic system of LCL consisting of eight axiom schemes and one inference rule is given in Figure 1. It has emerged as combination of the axiomatic system for classical propositional logic and type assignment system for simply typed combinatory logic. Axiom schemes: (Ax 1) S : (σ →(τ →ρ)) →((σ →τ) →(σ →ρ)) (Ax 2) K : σ →(τ →σ) (Ax 3) I : σ →σ (Ax 4) (M : σ →τ) ⇒((N : σ) ⇒(MN : τ)) (Ax 5) M : σ ⇒N : σ, if M = N is provable in EQη (Ax 6) α ⇒(β ⇒α) (Ax 7) (α ⇒(β ⇒γ)) ⇒((α ⇒β) ⇒(α ⇒γ)) (Ax 8) (¬¬α ⇒¬β) ⇒((¬¬α ⇒β) ⇒¬α) Inference rule: α ⇒β α (MP)β Figure 1: Axiomatic system of LCL The first five axiom schemes correspond to axioms and rules of type assignment system for simply typed combinatory logic and the last three axiom schemes are axiom schemes of classical propositional logic. The axiomatic system has one inference rule, called Modus Ponens. Inspired by Kripke-style semantics for typed lambda calculus introduced in [7, 8], we propose semantics for LCL based on applicative structures extended with special elements corresponding to primitive combinators. The main results of the paper are the soundness and completeness of the axiomatic system with respect to the proposed semantics.