Combinatory logic with polymorphic types

Tree Rewriting Systems, Combinatory Weak Reduction Systems and Type Free Languages1

Fundamenta Informaticae ◽

10.3233/fi-1982-53-404 ◽

1982 ◽

Vol 5 (3-4) ◽

pp. 279-299

Author(s):

Alberto Pettorossi

Keyword(s):

Combinatory Logic ◽

Rewriting Systems ◽

Tree Transducers ◽

Tree Languages ◽

One To One ◽

The One ◽

Weak Reduction

In this paper we consider combinators as tree transducers: this approach is based on the one-to-one correspondence between terms of Combinatory Logic and trees, and on the fact that combinators may be considered as transformers of terms. Since combinators are terms themselves, we will deal with trees as objects to be transformed and tree transformers as well. Methods for defining and studying tree rewriting systems inside Combinatory Weak Reduction Systems and Weak Combinatory Logic are also analyzed and particular attention is devoted to the problem of finiteness and infinity of the generated tree languages (here defined). This implies the study of the termination of the rewriting process (i.e. reduction) for combinators.

Download Full-text

On the likelihood of normalization in combinatory logic

Journal of Logic and Computation ◽

10.1093/logcom/exx005 ◽

2017 ◽

Vol 27 (7) ◽

pp. 2251-2269 ◽

Cited By ~ 1

Author(s):

Maciej Bendkowski ◽

Katarzyna Grygiel ◽

Marek Zaionc

Keyword(s):

Combinatory Logic

Download Full-text

Set Theory based on Combinatory Logic.

Journal of Symbolic Logic ◽

10.2307/2271198 ◽

1970 ◽

Vol 35 (1) ◽

pp. 147

Author(s):

Jonathan P. Seldin ◽

Maarten Wicher Visser Bunder

Keyword(s):

Set Theory ◽

Combinatory Logic

Download Full-text

TERMINATION OF ABSTRACT REDUCTION SYSTEMS

International Journal of Foundations of Computer Science ◽

10.1142/s0129054109006450 ◽

2009 ◽

Vol 20 (01) ◽

pp. 57-82

Author(s):

JEREMY E. DAWSON ◽

RAJEEV GORÉ

Keyword(s):

General Theorem ◽

Combinatory Logic ◽

Rewrite Systems ◽

Path Ordering

We present a general theorem capturing conditions required for the termination of abstract reduction systems. We show that our theorem generalises another similar general theorem about termination of such systems. We apply our theorem to give interesting proofs of termination for typed combinatory logic. Thus, our method can handle most path-orderings in the literature as well as the reducibility method typically used for typed combinators. Finally we show how our theorem can be used to prove termination for incrementally defined rewrite systems, including an incremental general path ordering. All proofs have been formally machine-checked in Isabelle/HOL.

Download Full-text

Higher-Order Illative Combinatory Logic

Journal of Symbolic Logic ◽

10.2178/jsl.7803080 ◽

2013 ◽

Vol 78 (3) ◽

pp. 837-872 ◽

Cited By ~ 2

Author(s):

Łukasz Czajka

Keyword(s):

Strong Consistency ◽

Predicate Logic ◽

Higher Order ◽

Second Order ◽

Model Construction ◽

Partial Answer ◽

Combinatory Logic ◽

First Order ◽

Propositional Quantifiers

AbstractWe show a model construction for a system of higher-order illative combinatory logic thus establishing its strong consistency. We also use a variant of this construction to provide a complete embedding of first-order intuitionistic predicate logic with second-order propositional quantifiers into the system of Barendregt, Bunder and Dekkers, which gives a partial answer to a question posed by these authors.

Download Full-text

Dynamically configurable combinatory logic array as Boolean neural network

Proceedings of 1993 IEEE Conference on Tools with Al (TAI-93) ◽

10.1109/tai.1993.634000 ◽

2002 ◽

Cited By ~ 1

Author(s):

J. Niittylahti ◽

H. Raittinen ◽

K. Kaski

Keyword(s):

Neural Network ◽

Combinatory Logic ◽

Dynamically Configurable ◽

Logic Array

Download Full-text

(In)equational combinatory logic

Combinatory Logic ◽

10.1201/b11046-7 ◽

2011 ◽

pp. 133-144

Keyword(s):

Combinatory Logic

Download Full-text

Applied combinatory logic

Combinatory Logic ◽

10.1201/b11046-10 ◽

2011 ◽

pp. 233-248

Keyword(s):

Combinatory Logic

Download Full-text

A combinatory logic approach to higher-order E-unification

Theoretical Computer Science ◽

10.1016/0304-3975(94)00210-a ◽

1995 ◽

Vol 139 (1-2) ◽

pp. 207-242 ◽

Cited By ~ 3

Author(s):

Daniel J. Dougherty ◽

Patricia Johann

Keyword(s):

Higher Order ◽

Combinatory Logic ◽

Logic Approach

Download Full-text

A combinatory account of internal structure

Journal of Symbolic Logic ◽

10.2178/jsl/1309952521 ◽

2011 ◽

Vol 76 (3) ◽

pp. 807-826 ◽

Cited By ~ 17

Author(s):

Barry Jay ◽

Thomas Given-Wilson

Keyword(s):

Normal Form ◽

Internal Structure ◽

Pattern Matching ◽

Normal Forms ◽

Expressive Power ◽

Combinatory Logic ◽

Natural Numbers ◽

Type Information ◽

Computable Functions

AbstractTraditional combinatory logic uses combinators S and K to represent all Turing-computable functions on natural numbers, but there are Turing-computable functions on the combinators themselves that cannot be so represented, because they access internal structure in ways that S and K cannot. Much of this expressive power is captured by adding a factorisation combinator F. The resulting SF-calculus is structure complete, in that it supports all pattern-matching functions whose patterns are in normal form, including a function that decides structural equality of arbitrary normal forms. A general characterisation of the structure complete, confluent combinatory calculi is given along with some examples. These are able to represent all their Turing-computable functions whose domain is limited to normal forms. The combinator F can be typed using an existential type to represent internal type information.

Download Full-text