= Approximation theorem for the graph model
{title2=$\llbracket M\rrbracket_\rho=\bigcup_{A\in\mathcal A(M)}\llbracket A\rrbracket_\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>.
Back to article page
