On adding (ξ) to weak equality in combinatory logic

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


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



    Upload a copy of this work     Papers currently archived: 92,261

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library


Added to PP

81 (#207,875)

6 months
33 (#103,772)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

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