= Indexed beta reduction
Use the binary finite-set encoding $e_k$ and Cantor code $\langle k,t\rangle$. Contracting $(\lambda x.P^n)^{m+1}Q^p$ gives the substituted body with its root index lowered by taking the minimum with $\min(m,n)$, replacing each occurrence $x^r$ by a copy of $Q$ with root index $\min(m,p,r)$. A zero-indexed abstraction instead substitutes $\bot$ and gives the body root index zero. Indices strictly budget the argument information that can be used by application. Finite-witness inequalities for the pairing code prove that indexed reduction increases the interpretation, although it can decrease the underlying <Böhm tree>.
Back to article page
