Böhm Theorem

Bohm theorem was already used whenever it was asked to find a $\Delta$ that satisfies a certain condition, since it gives a general method to solve this kind of problems.

$\eta$-equivalence (extensional equivalence) tells us that $M{=}_{\eta }\lambda x.x$ if $x$ is not a free variable of $M$.

This tells us that if $M$ is a function, than the behavior is the same as $\lambda x.x$ if they’re extensionally equivalent. This is important in the context of Bohm Theorem.

This can be seen as an equivalence, but also as a reduction rule (you can reduce the right term with the left term).

terminology Closed-normal form means that the term cannot be reduced anymore (normal form) and so it doesn’t contain any redex. Closed means that it doesn’t contain any free variable. It’s noted as $\Lambda °\text{-}nf$.

Let $M,N\in \Lambda °\text{-}nf$ such that $M{\ne }_{\eta }N$, then it exists a $\Delta$ such that:

$$\begin{array}{r}\Delta M=y_1\\ \Delta N=y_2\end{array}$$

todo continue this

Böhm Tree

Böhm Three is a nice tree representation of a normal form. Every node of the three is a Normal Form (not necessarily a closed normal form).

Various cases and the Böhm-out technique

todo continue

Rotators

Rotators $R_k$ (Family of combinators) that allow us to solve the last most difficult case of the Böhm-out technique, in which the same variable appears multiple times in the same path.

Example of rotators:

$$\begin{array}{r}{R}_1=\lambda x.x\\ R_2=\lambda xy.yx\\ R_3=\lambda xyz.zxy\end{array}$$

In order to solve the problem, we need to substitute the repeating variable $x$ with $R_k$ where $k$ is the maximum number of arguments of $x$, plus $1$.

---

tags: lambda-calculus