Definition 2.1.3 (Takahashi Translation). The Takahashi translation $M^{\ast }$ of a $\lambda$-term $M$ is recursively defined as follows:

• (1)
  $x^{\ast }:=x$, for $x$ a variable;
• (2)
  If $M=(\lambda x.P)Q$ is a redex, then $M^{\ast }:=P^{\ast }[x:=Q^{\ast }]$;
• (3)
  If $M=PQ$ is a $\lambda$-application, then $M^{\ast }:=P^{\ast }{Q}^{\ast }$;
• (4)
  If $M=\lambda x.P$ is a $\lambda$-abstraction, then $M^{\ast }:=\lambda x.P^{\ast }$.

These rules are numbered by order of precedence, in case of ambiguity. We also define $M^{0\ast }:=M$ and $M^{(n+1)\ast }:={(M^{n\ast })}^{\ast }$.