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

Abstract
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
Options
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: 52,893
Through your library

References found in this work BETA

Combinatory Logic.Haskell B. Curry, J. Roger Hindley & Jonathan P. Seldin - 1977 - Journal of Symbolic Logic 42 (1):109-110.
The Lambda Calculus. Its Syntax and Semantics.E. Engeler - 1984 - Journal of Symbolic Logic 49 (1):301-303.
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

Analytics

Added to PP index
2009-01-28

Total views
39 ( #246,994 of 2,342,991 )

Recent downloads (6 months)
3 ( #240,294 of 2,342,991 )

How can I increase my downloads?

Downloads

My notes