1 results
On adding (ξ) to weak equality in combinatory logic
-
- Journal:
- The Journal of Symbolic Logic / Volume 54 / Issue 2 / June 1989
- Published online by Cambridge University Press:
- 12 March 2014, pp. 590-607
- Print publication:
- June 1989
-
- Article
- Export citation
-
Because the main difference between combinatory weak equality and λβ-equality is that the rule
is 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.
