1
$\begingroup$

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.

enter image description here

$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$

enter image description here

enter image description here

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.

enter image description here

$\endgroup$
3
  • $\begingroup$ What is your question? $\endgroup$
    – D.W.
    Commented Jul 15, 2022 at 17:46
  • $\begingroup$ What are $L_0, L_1,...$ to distinguish $x$ and $y$? $\endgroup$
    – Oleg Dats
    Commented Jul 16, 2022 at 13:41
  • 1
    $\begingroup$ 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. $\endgroup$
    – D.W.
    Commented Nov 3, 2022 at 17:59

1 Answer 1

2
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.