Combinatory logic

Routledge Encyclopedia of Philosophy ◽

10.4324/9780415249126-y013-1 ◽

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.

Download Full-text

Preface

Mathematical Structures in Computer Science ◽

10.1017/s0960129598009682 ◽

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.)

Download Full-text

Arts and Branches of Science Significantly Contributing to Cyber and Cyber Security

Cyber Security and Threats ◽

10.4018/978-1-5225-5634-3.ch048 ◽

2018 ◽

pp. 977-994

Author(s):

Margarita Levin Jaitner ◽

Áine MacDermott

Keyword(s):

Computer Science ◽

Cyber Security ◽

Physical World ◽

Colleges And Universities ◽

The Past ◽

Academic Exchange ◽

Further Development

Academia plays an important role in shaping a country's cyber readiness. In the past years, nations have started investing in new cyber-related programs at colleges and universities. This also includes promoting academic exchange with partner countries, as well as putting effort into improved cooperation between industries and scholars in the area of cyber. In many cases the efforts focus largely on computer science and closely related branches of science. However, the very nature of the cyberspace as both a continuation and a reflection of the physical world require a broader perspective on academic assets required to create and sustain sound cyber defines capabilities. Acknowledging this premise, this paper sets out to map branches of science that significantly contribute to the domain known as ‘cyber' and searches for new aspects for further development.

Download Full-text

Projecting the Impact of Information Technology on Work and Skills in the 2030s

10.1093/oxfordhb/9780199655366.013.26 ◽

2017 ◽

Cited By ~ 1

Author(s):

Stuart W. Elliott

Keyword(s):

Information Technology ◽

Computer Science ◽

Preliminary Analysis ◽

Research Literature ◽

It Capabilities ◽

Recent Computer ◽

The Impact ◽

Near Future ◽

Further Development ◽

Future Effect

The research literature in computer science provides a way of understanding the growing capabilities of information technology (IT) and anticipating their future effect on work and skills. This chapter reviews a set of recent computer science articles to identify the IT capabilities that have been demonstrated in research settings. These capabilities are compared to information on occupational ability requirements to identify occupations that are potentially vulnerable to displacement as demonstrated IT capabilities are refined and applied over the next couple decades. The chapter’s preliminary analysis suggests that occupations representing 82 percent of current employment will be potentially vulnerable to displacement by IT in the near future. More rigorous versions of the chapter’s preliminary analysis should be carried out once or twice each decade to track the further development of IT capabilities and regularly update our understanding of their likely consequences for work and skills.

Download Full-text

A weak absolute consistency proof for some systems of illative combinatory logic

Journal of Symbolic Logic ◽

10.2307/2273470 ◽

1983 ◽

Vol 48 (3) ◽

pp. 771-776 ◽

Cited By ~ 5

Author(s):

M.W. Bunder

Keyword(s):

Set Theory ◽

Combinatory Logic ◽

Weak Consistency ◽

Consistency Proof ◽

First Order ◽

Formal Systems ◽

Elementary Methods ◽

Order Arithmetic ◽

Strongly Consistent ◽

Order Predicate Calculus

A large number of formal systems based on combinatory logic or λ-calculus have been extended to include first order predicate calculus. Several of these however have been shown to be inconsistent, all, as far as the author knows, in the strong sense that all well formed formulas (which here include all strings of symbols) are provable. We will call the corresponding consistency notion—an arbitrary wff ⊥ is provable—weak consistency. We will say that a system is strongly consistent if no formula and its negation are provable.Now for some systems, such as that of Kuzichev [11], the strong and weak consistency notions are equivalent, but in the systems of [5] and [6], which we will be considering, they are not. Each of these systems is strong enough to have all of ZF set theory, except Grounding and Choice, interpretable in it, and the system of [5] can also encompass first order arithmetic (see [7]). It therefore seems unlikely that a strong consistency result could be proved for these systems using elementary methods. In this paper however, we prove the weak consistency of both these systems by means that could be formulated, at least within the theory of [5]. The method also applies to the typed systems of Curry, Hindley and Seldin [10] and to Seldin's generalised types [12].

Download Full-text

Using typed lambda calculus to implement formal systems on a machine

Journal of Automated Reasoning ◽

10.1007/bf00245294 ◽

1992 ◽

Vol 9 (3) ◽

pp. 309-354 ◽

Cited By ~ 46

Author(s):

Arnon Avron ◽

Furio Honsell ◽

Ian A. Mason ◽

Robert Pollack

Keyword(s):

Lambda Calculus ◽

Formal Systems ◽

Typed Lambda Calculus

Download Full-text

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

Journal of Symbolic Logic ◽

10.2307/2275096 ◽

1993 ◽

Vol 58 (3) ◽

pp. 769-788 ◽

Cited By ~ 7

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).

Download Full-text

From Magic to Deity, Matter to Persona

10.1093/oso/9780198767022.003.0003 ◽

2018 ◽

Author(s):

Bihani Sarkar

Keyword(s):

Indian Philosophy ◽

Causal Power ◽

Active Material ◽

Central Figure ◽

Classical Indian Philosophy ◽

Further Development

The first chapter of the Devīmāhātmya, a collection of myths about the warrior goddess Durgā, mentions a mysterious figure of magic and causal power, the goddess Mahāmāyā who is the personified sleep of Viṣṇu. Though tightly enmeshed with Durgā, Mahāmāyā is charged with a complex symbolism distinguishing her from Durgā. Focusing on Mahāmāyā, this chapter turns from myth to classical Indian philosophy to probe her origin and to trace her further development and exaltation from a metaphysical concept into a deity of worship. It assesses the notion of māyā as magic, illusion and the principle of active material causation in metaphysics preceding the Devīmāhātmya, from which Mahāmāyā as a religious icon drew her varied signification It is particularly within the cosmogonic speculations of Sadyojyotiḥ and Bhaṭṭa Rāmakaṇṭha, early writers of the Śaiva Siddhānta, that Māyā is turned into a central figure in the understanding of how reality is formed.

Download Full-text