A syntactical proof of the operational equivalence of two $\lambda$-terms

TL;DR

This paper provides a purely syntactical proof demonstrating the operational equivalence of the identity lambda-term and its eta-infinite expansion, contributing to the theoretical understanding of lambda calculus.

Contribution

It introduces a novel syntactical proof of operational equivalence between two lambda-terms, expanding the theoretical framework of lambda calculus.

Findings

Proves the operational equivalence syntactically

Shows the eta-infinite expansion is equivalent to the identity

Enhances understanding of lambda-term transformations

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$.