On adding (?) to weak equality in combinatory logic

Autor: Bunder, Martin W., Hindley, J. Roger, Seldin, Jonathan P.
Zdroj: Journal of Symbolic Logic; June 1989, Vol. 54 Issue: 2 p590-607, 18p
Abstrakt: AbstractBecause the main difference between combinatory weak equality and ?ß-equality is that the ruleis valid for the latter but not the former, it is easy to assume that another way of defining combinatory ß-equality is to add rule (?) to the postulates for weak equality. However, to make this true, one must choose the definition of combinatory abstraction in (?) very carefully. If one tries to use one of the more common abstraction algorithms, the result will be an equality, =?, that is either equivalent to ß?-equality (and so strictly stronger than ß-equality) or else strictly weaker than ß-equality. This paper will study the relations =?for several commonly used abstraction-algorithms, distinguish between them, and axiomatize them.
Databáze: Supplemental Index