# What are distinguishable terms in Bohm theorem?

I have just started to study "Lambda-Calculus and Combinators, an Introduction" by Roger Hindley.

There is a formulation of B ̈ohm’s theorem that I can not understand.

$$M$$ and $$N$$ are terms in bn-normal form. Based on the description I assume that $$M$$ could be equal to λ-term $$x$$ and $$N=y$$. $$x≠y$$. Both $$x$$ and $$y$$ do not have b-redexes and n-redexes. I do not understand how to distinguish between $$M=x$$ and $$N=y$$.

$$xL_1..L_nxy => x$$

$$yL_1..L_nxy => y$$

I have found another formulation of this theorem where everything is clear. A function is applied to terms rather than terms ($$M$$ and $$N$$) are applied to combinators.

• What is your question?
– D.W.
Commented Jul 15, 2022 at 17:46
• What are $L_0, L_1,...$ to distinguish $x$ and $y$? Commented Jul 16, 2022 at 13:41
• Please don't write your question or put clarifications in the comments. Instead, edit the question to incorporate all relevant information in the question, and make sure it reads well for someone who encounters it for the first time.
– D.W.
Commented Nov 3, 2022 at 17:59

## 1 Answer

I believe the word "combinator" in your first statement of Böhm's theorem means a closed λ-term, i.e. one which has no free variables (as is the case here for instance); this is consistent with the fact that the statement at the end of your question mentions closed normal forms. Thus your example terms $$M$$ and $$N$$ are not combinators because $$fv(M) = \{x\}$$ and $$fv(N) = \{y\}$$, so they don't satisfy the assumption of Böhm's theorem.