Finite Generation and Presentation Problems for Lambda Calculus and Combinatory Logic

2021 ◽  
pp. 316-326
Author(s):  
Rick Statman
Keyword(s):  
Lambda Calculus ◽  
Combinatory Logic ◽  
Finite Generation

scholarly journals Systems of illative combinatory logic complete for first-order propositional and predicate calculus

1993 ◽  
Vol 58 (3) ◽  
pp. 769-788 ◽  
Author(s):  
Henk Barendregt ◽  
Martin Bunder ◽  
Wil Dekkers
Keyword(s):  
Lambda Calculus ◽  
Predicate Calculus ◽  
Combinatory Logic ◽  
Consistent System ◽  
First Order ◽  
Base Logic

AbstractIllative combinatory logic consists of the theory of combinators or lambda calculus extended by extra constants (and corresponding axioms and rules) intended to capture inference. The paper considers systems of illative combinatory logic that are sound for first-order propositional and predicate calculus. The interpretation from ordinary logic into the illative systems can be done in two ways: following the propositions-as-types paradigm, in which derivations become combinators or, in a more direct way, in which derivations are not translated. Both translations are closely related in a canonical way. The two direct translations turn out to be complete. The paper fulfills the program of Church [1932], [1933] and Curry [1930] to base logic on a consistent system of λ-terms or combinators. Hitherto this program had failed because systems of ICL were either too weak (to provide a sound interpretation) or too strong (sometimes even inconsistent).

scholarly journals COMBINATORY LOGIC AND $ lambda $-CALCULUS FOR CLASSICAL LOGIC

10.5109/13496 ◽  
2000 ◽  
Vol 32 (2) ◽  
pp. 105-122
Author(s):  
Kensuke Baba ◽  
Yukiyoshi Kameyama ◽  
Sachio Hirokawa
Keyword(s):  
Classical Logic ◽  
Lambda Calculus ◽  
Combinatory Logic

Categorical models for non-extensional λ-calculi and combinatory logic

1992 ◽  
Vol 2 (3) ◽  
pp. 327-357 ◽  
Author(s):  
Simone Martini
Keyword(s):  
Lambda Calculus ◽  
Second Order ◽  
Combinatory Logic ◽  
Cartesian Closed Category ◽  
Closed Category ◽  
Simple Generalization ◽  
Categorical Models ◽  
Closed Structure ◽  
Cartesian Closed

The notions of weak Cartesian closed category and very weak CCC are introduced by dropping the extensionality (and the naturality) requirements in the adjunction defining the closed structure of a CCC. A number of specific examples of these categories are given. The weak notions are shown to be equivalent from both the semantic and syntactic standpoint to the typed non-extensional lambda-calculus and to the typed Combinatory Logic, extended with surjective pairs. Type-free models are characterized as reflexive objects in wCCCs. Finally, categorical models for the second-order non-extensional calculus are defined, by introducing a simple generalization of the notion of PL-category.

REGULAR SYSTEMS OF EQUATIONS IN λ-CALCULUS

1990 ◽  
Vol 01 (03) ◽  
pp. 325-339 ◽  
Author(s):  
ADOLFO PIPERNO ◽  
ENRICO TRONCI
Keyword(s):  
Lambda Calculus ◽  
Combinatory Logic ◽  
Systems Of Equations ◽  
Equational Theories ◽  
Solvability Problem

Many problems arising in equational theories like Lambda-calculus and Combinatory Logic can be expressed by combinatory equations or systems of equations. However, the solvability problem for an arbitrarily given class of systems is in general undecidable. In this paper we shall focus our attention on a decidable class of systems, which will be called regular systems, and we shall analyse some classical problems and well-known properties of Lambda-calculus that can be described and solved by means of regular systems. The significance of such class will be emphasized showing that for slight extensions of it the solvability problem turns out to be undecidable.

scholarly journals Completeness of the propositions-as-types interpretation of intuitionistic logic into illative combinatory logic

1998 ◽  
Vol 63 (3) ◽  
pp. 869-890 ◽  
Author(s):  
Wil Dekkers ◽  
Martin Bunder ◽  
Henk Barendregt
Keyword(s):  
Intuitionistic Logic ◽  
Predicate Logic ◽  
Lambda Calculus ◽  
Preceding Paper ◽  
Predicate Calculus ◽  
Combinatory Logic ◽  
First Order ◽  
Two Systems

AbstractIllative combinatory logic consists of the theory of combinators or lambda calculus extended by extra constants (and corresponding axioms and rules) intended to capture inference. In a preceding paper, [2], we considered 4 systems of illative combinatory logic that are sound for first order intuitionistic propositional and predicate logic. The interpretation from ordinary logic into the illative systems can be done in two ways: following the propositions-as-types paradigm, in which derivations become combinators, or in a more direct way, in which derivations are not translated. Both translations are closely related in a canonical way. In the cited paper we proved completeness of the two direct translations. In the present paper we prove that also the two indirect translations are complete. These proofs are direct whereas in another version, [3], we proved completeness by showing that the two corresponding illative systems are conservative over the two systems for the direct translations. Moreover we shall prove that one of the systems is also complete for predicate calculus with higher type functions.

Combinatory logic

2018 ◽  
Author(s):  
David Charles McCarty
Keyword(s):  
Computer Science ◽  
Lambda Calculus ◽  
Combinatory Logic ◽  
Close Relative ◽  
Syntactic Category ◽  
Central Figure ◽  
Formal Systems ◽  
Functional Models ◽  
Crucial Property ◽  
Further Development

Combinatory logic comprises a battery of formalisms for expressing and studying properties of operations constitutive to contemporary logic and its applications. The sole syntactic category in combinatory logic is that of the applicative term. Closed terms are called ‘combinators’; there is no binding of variables. Systems containing the basic combinators S and K exhibit the crucial property of combinatorial completeness: every routine expressible in the system can be captured by a term composed of these two combinators alone. Combinatory logic is a close relative of Church’s lambda calculus. M. Schönfinkel first introduced and defined basic combinators in 1920 in assaying foundations for mathematics that avoid bound variables and take operations, rather than sets, as fundamental. H. Curry later rediscovered the combinators (and coined the term ‘combinatory logic’) independently of Schönfinkel. Curry constructed various formal systems for combinatory logic and, throughout most of the subject’s history, was the central figure in the research. In 1969, D. Scott succeeded in constructing set-theoretic, functional models for the lambda calculus and combinatory logic. Since then semantic studies of combinatory systems, together with research on their applications to computer science and further development as foundational systems, have dominated the field.

scholarly journals Ticket Entailment is decidable

2012 ◽  
Vol 23 (3) ◽  
pp. 568-607 ◽  
Author(s):  
VINCENT PADOVANI
Keyword(s):  
Lambda Calculus ◽  
Relevance Logic ◽  
Combinatory Logic ◽  
Equivalent Problem ◽  
Typed Lambda Calculus ◽  
Ticket Entailment

We prove the decidability of the logic T→ of Ticket Entailment. This issue was first raised by Anderson and Belnap within the framework of relevance logic, and is equivalent to the question of the decidability of type inhabitation in simply typed combinatory logic with the partial basis BB′IW. We solve the equivalent problem of type inhabitation for the restriction of simply typed lambda calculus to hereditarily right-maximal terms.

scholarly journals Preface

1999 ◽  
Vol 9 (4) ◽  
pp. 321-321
Author(s):  
MARIANGIOLA DEZANI-CIANCAGLINI ◽  
GIUSEPPE LONGO ◽  
JONATHAN P. SELDIN
Keyword(s):  
Computer Science ◽  
Type System ◽  
Lambda Calculus ◽  
Combinatory Logic ◽  
Subsequent Work ◽  
Mathematical Structures ◽  
Type Assignment ◽  
The Face ◽  
The Subject ◽  
The University

This special double issue of Mathematical Structures in Computer Science is in honour of Roger Hindley and is devoted to the topic of lambda-calculus and logic.It is a great pleasure for us to greet Roger Hindley on the occasion of his retirement from the University of Wales, Swansea, and his 60th birthday. We have known Roger for many years and we have had the chance to collaborate with him and appreciate his intellectual standard, his remarkable mathematical rigor, and his inexhaustible sense of humour. This has enabled Roger to step back critically even in the face of a difficult mathematical task and help to solve it by a new way of looking at it.Roger Hindley's dissertation concerned the Church–Rosser Theorem and was a significant contribution to the topic. His subsequent work spanned many aspects of lambda-calculus, covering both its models and applications. To mention just a few, he produced work on axioms for Curry's strong (eta) reduction, comparing lambda and combinatory reductions (and models), models for type assignment, and formulas as types for some nonstandard systems (intersection types, BCK systems, etc.).Roger Hindley collaborated with Jonathan Seldin on two well-known introductory books on the subject (Bruce Lercher also collaborated as an author on the first of these). More recently, he has published an introduction to type assignment. He was also co-author with H. B. Curry and J. Seldin on Combinatory Logic, vol. II, which is an important research publication on the subject.Roger has played an important role in the lambda-calculus community over the years as that community has grown; in particular, he has been an active organiser of many conferences on the topic. In fact, his success in disseminating knowledge about the lambda calculus, particularly in the United Kingdom, means that Roger may be considered a ‘Godfather’ of ML and its type system.(In preparing this special issue of Mathematical Structures in Computer Science, we have been fortunate enough to receive too many excellent papers for one double issue. As a result, additional papers by colleagues who wish to honour Roger will appear in future issues of this journal.)

Sign in / Sign up

Export Citation Format

Share Document