Authors: Kašterović, Simona
Ghilezan, Silvia 
Affiliations: Mathematics 
Title: Towards Logic of Combinatory Logic
First page: 34
Last page: 36
Related Publication(s): Book of Abstracts of the 10th International Conference Logic and Applications, LAP 2021
Conference: 10th International Conference Logic and Applications, LAP 2021, September 20 - 24, 2020, Dubrovnik, Croatia
Issue Date: Sep-2021
Rank: M34
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
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.
Keywords: combinatory logic | classical propositional logic | simple types | axiomatization | semantics | soundness | completeness
Publisher: University Center Dubrovnik, Croatia,
Project: Advanced artificial intelligence techniques for analysis and design of system components based on trustworthy BlockChain technology - AI4TrustBC 

Show full item record

Page view(s)

checked on Sep 26, 2021

Google ScholarTM


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.