Bruce Lercher. Strong reduction and normal form in combinatory logic. The journal of symbolic logic, vol. 32 (1967), pp. 213–223.

1971 ◽  
Vol 36 (1) ◽  
pp. 171-171
Author(s):  
Luis E. Sanchis
Keyword(s):  
Normal Form ◽  
Combinatory Logic ◽  
Symbolic Logic ◽  
Strong Reduction

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

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.

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

John T. Kearns. Combinatory logic with discriminators. The journal of symbolic logic, vol. 34 (1969), pp. 561–575.

1973 ◽  
Vol 38 (2) ◽  
pp. 339-340
Author(s):  
Jonathan P. Seldin
Keyword(s):  
Combinatory Logic ◽  
Symbolic Logic
Sign in / Sign up

Export Citation Format

Share Document