A syntactical proof of the operational equivalence of two λ-terms
classification
🧮 math.LO
keywords
lambdaequivalenceoperationalproofsyntacticalexpansioninfinitepurely
read the original abstract
In this paper we present a purely syntactical proof of the operational equivalence of $I=\lambda xx$ and the $\lambda$-term $J$ that is the $\eta$-infinite expansion of $I$.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.