On Adding $(\xi)$ to Weak Equality in Combinatory Logic
Bunder, Martin W. ; Hindley, J. Roger ; Seldin, Jonathan P.
J. Symbolic Logic, Tome 54 (1989) no. 1, p. 590-607 / Harvested from Project Euclid
Because the main difference between combinatory weak equality and $\lambda\beta$-equality is that the rule \begin{equation*}\tag{\xi} X = Y \vdash \lambda x.X = \lambda x.Y\end{equation*} is valid for the latter but not the former, it is easy to assume that another way of defining combinatory $\beta$-equality is to add rule $(\xi)$ to the postulates for weak equality. However, to make this true, one must choose the definition of combinatory abstraction in $(\xi)$ very carefully. If one tries to use one of the more common abstraction algorithms, the result will be an equality, $=_\xi$, that is either equivalent to $\beta\eta$-equality (and so strictly stronger than $\beta$-equality) or else strictly weaker than $\beta$-equality. This paper will study the relations $=_\xi$ for several commonly used abstraction algorithms, distinguish between them, and axiomatize them.
Publié le : 1989-06-14
Classification: 
@article{1183742929,
     author = {Bunder, Martin W. and Hindley, J. Roger and Seldin, Jonathan P.},
     title = {On Adding $(\xi)$ to Weak Equality in Combinatory Logic},
     journal = {J. Symbolic Logic},
     volume = {54},
     number = {1},
     year = {1989},
     pages = { 590-607},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1183742929}
}
Bunder, Martin W.; Hindley, J. Roger; Seldin, Jonathan P. On Adding $(\xi)$ to Weak Equality in Combinatory Logic. J. Symbolic Logic, Tome 54 (1989) no. 1, pp.  590-607. http://gdmltest.u-ga.fr/item/1183742929/