Journal of Symbolic Logic 54 (2):590-607 (1989)

Because the main difference between combinatory weak equality and λβ-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 β-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
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.2307/2274872
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 71,512
Through your library

References found in this work BETA

The Lambda Calculus. Its Syntax and Semantics.E. Engeler - 1984 - Journal of Symbolic Logic 49 (1):301-303.
Combinatory Logic.Haskell B. Curry, J. Roger Hindley & Jonathan P. Seldin - 1977 - Journal of Symbolic Logic 42 (1):109-110.
Introduction to Combinators and Λ-Calculus.J. Roger Hindley & Jonathan P. Seldin - 1988 - Journal of Symbolic Logic 53 (3):985-986.

Add more references

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles


Added to PP index

Total views
45 ( #253,738 of 2,520,896 )

Recent downloads (6 months)
3 ( #205,180 of 2,520,896 )

How can I increase my downloads?


My notes