An indexed lambda term assigns a natural number to every subterm occurrence; one also admits a constant with empty interpretation. In the graph model of lambda calculus, every syntax constructor is interpreted as usual and then intersected with at its occurrence index . All indexed interpretations are finite subsets of the unindexed interpretation, and their directed union recovers that interpretation.
New to topics? Read the docs here!