Strong reduction and normal form in combinatory logic

1967 ◽  
Vol 32 (2) ◽  
pp. 213-223 ◽  
Author(s):  
Bruce Lercher
Keyword(s):  
Normal Form ◽  
Combinatory Logic ◽  
Strong Reduction ◽  
The Church

The notion of strong reduction is introduced in Curry and Feys' book Combinatory logic [1] as an analogue, in the theory of combinatore, to reduction (more exactly, βη-reduction) in the theory of λ-conversion. The existence of an analogue and its possible importance are suggested by an equivalence between the theory of combinatore and λ-conversion, and the Church-Rosser theorem in λ-conversion. This theorem implies that if a formula X is convertible to a formula X* which cannot be further reduced—is irreducible, or in normal form—then X is convertible to X* by a reduction alone. Moreover, the reduction may be performed in a certain prescribed order.

scholarly journals The Church Rosser theorem for strong reduction in combinatory logic.

1968 ◽  
Vol 9 (4) ◽  
pp. 299-302 ◽  
Author(s):  
Kenneth Loewen
Keyword(s):  
Combinatory Logic ◽  
Strong Reduction ◽  
The Church

scholarly journals A combinatory account of internal structure

2011 ◽  
Vol 76 (3) ◽  
pp. 807-826 ◽  
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.

Arithmetic based on the Church numerals in illative combinatory logic

Studia Logica ◽  
1988 ◽  
Vol 47 (2) ◽  
pp. 129-143
Author(s):  
M. W. Bunder
Keyword(s):  
Combinatory Logic ◽  
The Church

Some consistency proofs and a characterization of inconsistency proofs in illative combinatory logic

1987 ◽  
Vol 52 (1) ◽  
pp. 89-110 ◽  
Author(s):  
M. W. Bunder
Keyword(s):  
Normal Form ◽  
Propositional Calculus ◽  
Weak Form ◽  
Combinatory Logic ◽  
Major Premise ◽  
Elimination Rule ◽  
Introduction Rule ◽  
Consistency Proofs ◽  
Arbitrary Term

It is well known that combinatory logic with unrestricted introduction and elimination rules for implication is inconsistent in the strong sense that an arbitrary term Y is provable. The simplest proof of this, now usually called Curry's paradox, involves for an arbitrary term Y, a term X defined by X = Y(CPy).The fact that X = PXY = X ⊃ Y is an essential part of the proof.The paradox can be avoided by placing restrictions on the implication introduction rule or on the axioms from which it can be proved.In this paper we determine the forms that must be taken by inconsistency proofs of systems of propositional calculus based on combinatory logic, with arbitrary restrictions on both the introduction and elimination rules for the connectives. Generally such a proof will involve terms without normal form and cut formulas, i.e. formulas formed by an introduction rule that are immediately removed by an elimination with at most some equality steps intervening. (Such a sequence of steps we call a “cut”.)The above applies not only to the strong form of inconsistency defined above, but also to the weak form of inconsistency defined by: all propositions are provable, if this can be represented in the system.Any inconsistency proof of this kind of system can be reduced to one where the major premise of the elimination rule involved in the cut and its deduction must also appear in the deduction of the minor premise involved in the cut.We can, using this characterization of inconsistency proofs, put appropriate restrictions on certain introduction rules so that the systems, including a full classical propositional one, become provably consistent.

Axioms for strong reduction in combinatory logic

1967 ◽  
Vol 32 (2) ◽  
pp. 224-236 ◽  
Author(s):  
Roger Hindley
Keyword(s):  
Binary Relation ◽  
Equivalence Relation ◽  
Combinatory Logic ◽  
Strong Reduction ◽  
Image Position ◽  
Weak Reduction

In combinatory logic there is a system of objects which intuitively represent functions, and a binary relation between these objects, which represents the process of evaluating the result of applying a function to an argument. (This is explained fully in [1].) From this relation called weak reduction, “≥,” an equivalence relation is defined by saying that X is weakly equivalent to Y if and only if there exist n (with 0 ≤ n) and X0,…,Xη such that It turns out that equivalent objects represent the same function, but two objects representing the same function need not be equivalent.

The Church-Rosser property in symmetric combinatory logic

2005 ◽  
Vol 70 (2) ◽  
pp. 536-556 ◽  
Author(s):  
Katalin Bimbó
Keyword(s):  
Fixed Point ◽  
Place Identity ◽  
Combinatory Logic ◽  
Left And Right ◽  
The One ◽  
The Church

AbstractSymmetic combinatory logic with the symmetric analogue of a combinatorially complete base (in the form of symmetric λ-calculus) is known to lack the Church-Rosser property. We prove a much stronger theorem that no symmetric combinatory logic that contains at least two proper symmetric combinatory has the Church-Rosser property. Although the statement of the result looks similar to an earlier one concerning dual combinatory logic, the proof is different because symmetric combinators may form redexes in both left and right associated terms. Perhaps surprisingly, we are also able to show that certain symmetric combinatory logics that include just one particular constant are not confluent. This result (beyond other differences) clearly sets apart symmetric combinatory logic from dual combinatory logic, since all dual combinatory systems with a single combinator or a single dual combinator are Church-Rosser. Lastly, we prove that a symmetric combinatory logic that contains the fixed point and the one-place identity combinator has the Church-Rosser property.

scholarly journals Modified strong reduction in combinatory logic.

1968 ◽  
Vol 9 (3) ◽  
pp. 265-270 ◽  
Author(s):  
Kenneth Loewen
Keyword(s):  
Combinatory Logic ◽  
Strong Reduction
Sign in / Sign up

Export Citation Format

Share Document