Indexed lambda term
= Indexed lambda term
{title2=$\Lambda_\bot^{\mathbb N}$}
An indexed <lambda term> assigns a natural number to every subterm occurrence; one also admits a constant $\bot$ with empty interpretation. In the <graph model of lambda calculus>, every syntax constructor is interpreted as usual and then intersected with $\{0,\ldots,n\}$ at its occurrence index $n$. All indexed interpretations are finite subsets of the unindexed interpretation, and their directed union recovers that interpretation.