Distinguishing pure, closed lambda terms

Question

Let $M$ be a full model of the simply typed lambda calculus, over some collection of base types, with the constraint that $|D_\sigma|\geq 2$ for each base type $\sigma$.

Let $a$ and $b$ be two closed and pure lambda terms (terms constructed from $\lambda$ and variables only -- that is, no constants) such that $[a ]_M = [b]_M$. Does it follow that $a$ and $b$ are $\beta\eta$ equivalent?

In other words, does every non-trivial model semantically distinguish between non-equivalent pure lambda terms?

Answer 1

I believe the answer is 'no': roughly none of the Church numerals of type $(o\to o)\to o\to o$ are $\beta\eta$ equivalent, but in a model where $o$ has only two elements, $(o\to o)\to o\to o$ is finite, and so some of the Church numerals coincide in extension.

In more detail, consider the setting with one base type, $o$. Let $y$ be of type $o$ and $x$ of type $o\to o$. Write $x^0y$ for $y$ and $x^{n+1}y$ for $x(x^ny)$

For each $n,m$ such that $n\not= m$ we can find a model $M$ in which $[\lambda xy.x^ny]_M \not= [\lambda xy.x^my]_M$ (any model in which $o$ is infinite will do. For example, if $o$ are the naturals, then these two terms deliver different values when fed the successor function). So these terms are not $\beta\eta$ equivalent. However, since there are infinitely many of them, some pair must coincide in extension in any model in which $(o\to o)\to o\to o$ is finite (such as when $o$ is of cardinality 2).

Answer 2

If $a$ and $b$ are not $\beta\eta$-equivalent, by Bohm’s Theorem there exists a context separating them. Let's call these two new terms $A$ and $B$, with $A \neq B$. Since $[a]_M = [b]_M$, we have also $[A]_M = [B]_M$ by compositionality.

Now think of the term

"$T \equiv \lambda v .$ if $v = A$ then true else if $v = B$ then false".

So the denotation of true ($TA$) and false ($TB$) have to coincide in $M$. Using similar conditionals you can then identify any two values in your model.