Authors: Kašterović, SimonaGhilezan, 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 URL: http://imft.ftn.uns.ac.rs/math/cms/uploads/Main/2021_LAP_FORMALS_BoA.pdf Abstract: Typed combinatory logic found its application in various fields of computerscience, e.g. program synthesis , machine learning, e.g.  and artificial intelligence, e.g. , etc. Developments of these fields urge for further researchand development of typed combinatory logic. Although combinatory logic, bothtyped and untyped, has been subject of many studies, to the best of our knowledge none of them investigate combining typed combinatory logic with classicalpropositional logic in order to capture inference of type assignment statements.We introduce in this paper a classical propositional logic for reasoning aboutsimply typed combinatory logic, called logic of combinatory logic, and denotedby LCL.First, we revisit a syntax of simply typed combinatory logic [5, 4, 6]. Termsof untyped combinatory logic, called CL-terms, are generated by the followingsyntaxM,N := x |S |K |I |MNwhere x belongs to a countable set of term variables. The constants S,K,I arecalled primitive combinators. We are mostly interested in typed terms, moreprecisely we are interested in simply typed terms. Simple types are generatedby 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 typedcombinatory terms.We propose extending simply typed combinatory logic with classical logicalconnectives of negation and conjunction. The obtained system is called logic ofcombinatory logic and it is denoted by LCL. The language of the logic LCL isgenerated by the following syntaxα,β := M : σ |¬α |α ∧βWe see that logic LCL is actually obtained from classical propositional logicby replacing propositional letters with type assignment statements M : σ. Weargue that logic LCL is a first step towards formalization of meta-language ofsimply 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 ruleis given in Figure 1. It has emerged as combination of the axiomatic systemfor classical propositional logic and type assignment system for simply typedcombinatory 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 LCLThe first five axiom schemes correspond to axioms and rules of type assignmentsystem for simply typed combinatory logic and the last three axiom schemes areaxiom schemes of classical propositional logic. The axiomatic system has oneinference 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 extendedwith special elements corresponding to primitive combinators. The main resultsof the paper are the soundness and completeness of the axiomatic system withrespect 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

#### Page view(s)

9
checked on Sep 26, 2021 