= Complete development of a lambda term
{title2=$M^\bullet$}
Define $x^\bullet=x$, $(\lambda x.M)^\bullet=\lambda x.M^\bullet$, and develop an application by contracting its root when that root is syntactically a <beta-redex>: $((\lambda x.M)N)^\bullet=M^\bullet[x:=N^\bullet]$. Otherwise $(MN)^\bullet=M^\bullet N^\bullet$. Newly created root redexes need not be contracted. Induction with the substitution lemma proves that if $M\Rightarrow N$, then $N\Rightarrow M^\bullet$. Thus any two parallel reducts share this reduct.
Back to article page
