Roger Hindley. Axioms for strong reduction in combinatory logic. The journal of symbolic logic, vol. 32 (1967), pp. 224–236. - Bruce Lercher. The decidability of Hindley's axioms for strong reduction. The journal of symbolic logic, vol. 32 (1967), pp. 237–239.

1971 ◽  
Vol 36 (1) ◽  
pp. 171-172
Author(s):  
Haskell B. Curry
Keyword(s):  
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.

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

The decidability of hindley's axioms for strong reduction

1967 ◽  
Vol 32 (2) ◽  
pp. 237-239 ◽  
Author(s):  
Bruce Lercher
Keyword(s):  
Finite Number ◽  
Infinite System ◽  
Combinatory Logic ◽  
Strong Reduction

In his paper [3] Hindley shows that strong reduction in combinatory logic (see [1] for the basic discussion of this notion) cannot be axiomatized with a finite number of axiom schemes, and then he presents an infinite system of axiom schemes for strong reduction. Hindley lists one axiom and six axiom schemes, together with a method (clause (viii) below) for generating further axiom schemes from these. The results of this note are that different applications of clause (viii) yield different axiom schemes, and that the property of being an axiom is decidable.

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
Sign in / Sign up

Export Citation Format

Share Document