Some properties of $β$-$η$-normal forms in $λ$-K-calculus (Alcune proprietá delle forme $β$-$η$-normali nel $λ$-K-calcolo)
Corrado Böhm, Chun Tian
TL;DR
The paper analyzes β-η-normal forms in the λ-K-calculus, establishing a constructive framework to distinguish distinct normal forms through substitutions and finite-argument contexts. It introduces a principled equivalence relation on normal forms and a finite-case analysis that yields explicit witnesses (contexts) separating non-equal forms, with a constructive algorithm for building the witness terms. It further derives inversion-style results: for any normal form with a variable, there exist left and right combinators $\Delta$ and $\nabla$ such that $\Delta\circ F\circ\nabla = I$, and it explores the algebraic consequences for the combinator semigroup, including cases where nontrivial inverses exist and implications for the codomain cardinality. Overall, the work provides a detailed, constructive account of the separability and invertibility properties of β-η-normal forms in λ-K-calculus, with several corollaries on the structure and behavior of combinators beyond canonical normal forms.
Abstract
This is a plain English translation of [Böh68], originally in Italian, by Chun Tian. All footnotes (and citations only found in footnotes, of course) are added by the translator.