Approximation theorem for the graph model ($[[M{]]}_{\rho }={\bigcup }_{A\in \mathcal{A}(M)}[[A{]]}_{\rho }$)

The interpretation of a lambda term in the graph model of lambda calculus is the union of the interpretations of all its finite Böhm approximants. Every finite indexed interpretation reduces monotonically to an indexed normal approximant. Taking the union over all occurrence indices gives one inclusion; replacing subterms by bottom and using beta soundness gives the other. This identifies denotational information with finite observable parts of a Böhm tree.