From Böhm's Theorem to Observational Equivalences
Mariangiola Dezani-Ciancaglini, Elio Giovannetti · Electronic Notes in Theoretical Computer Science · 2001
There are essentially two ways of looking at the computational behaviours of λ-terms. One consists in putting the term within a context (possibly of λ-calculus extensions) and observing some properties (typically termination). The other consists in reducing the term until some meaningful information is obtained: this naturally leads to a tree representation of the information implicitly contained in the original term. The paper is an informal overview of the role played by Böhm's Theorem in these observations of terms.