The decidability of hindley's axioms for strong reduction

Publisher Website
Google Scholar
Abstract
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.

This publication has 1 reference indexed in Scilit: