1
$\begingroup$

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?

$\endgroup$
1
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Thank you. I figured that Bohm's theorem would be the key, but I only know of the theorem in the untyped setting. In the typed setting it appears to be slightly weaker (see theorem 6.1 in mi.sanu.ac.rs/~kosta/KRIT1.pdf). Do you a have a reference for the version you're appealing to? $\endgroup$ – Andrew Bacon Feb 15 '16 at 17:05
  • $\begingroup$ @AndrewBacon You're right, I completely forgot the typed setting... But your reference is good, and apparently you can still apply the reasoning with the typed version. $\endgroup$ – Graffitics Feb 15 '16 at 21:54
  • $\begingroup$ Right, but the theorem in the paper I linked to is crucially weaker than Bohm's theorem: it only says if $a$ and $b$ are not $\beta\eta$ equivalent you can find type instances of them that are separated by a context. So I don't think you're reasoning works. I actually now think the claim in the question is false: see my other answer. $\endgroup$ – Andrew Bacon Feb 16 '16 at 17:35
0
$\begingroup$

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).

$\endgroup$
  • $\begingroup$ I now think I didn't understand your question. Did you mean: suppose that $[a]_M=[b]_M$ for typed terms $a$ and $b$, then do $a$ and $b$ have to be $\beta\eta$ equivalent as untyped $\lambda$-terms? In which case your answer is the correct one. $\endgroup$ – Graffitics Feb 17 '16 at 14:47
  • $\begingroup$ I actually meant: are they $\beta\eta$-equivalent in the simply typed lambda calculus. But I'm not actually seeing the difference between that and your question. If a and b are untyped terms that are typable, then the reduction of them both to $\beta\eta$ normal form will be correct in both the typed and untyped setting. So they have the same $\beta\eta$ normal form in the typed calculus iff they have the same $\beta\eta$ normal form in the untyped calculus. $\endgroup$ – Andrew Bacon Feb 17 '16 at 16:07
  • $\begingroup$ But then your example makes you able to apply the same trick: "$\lambda x.$ if $x>m$ then true", "$\lambda x.$ if $x<m$ then false". You don't have true Church numerals if $o$ is finite. $\endgroup$ – Graffitics Feb 17 '16 at 17:03
  • $\begingroup$ It doesn't matter whether the terms really correspond to "true" numbers or not. The point is we have infinitely many terms that are not $\beta\eta$-equivalent but such that some agree in extension in the model described. (I don't know how the notion of "greater than" which you use above is being defined precisely, but in a finite model it won't order the denotations of the Church numerals like the natural numbers.) $\endgroup$ – Andrew Bacon Feb 17 '16 at 20:51
  • $\begingroup$ But then on a finite ground type, your "Church numerals" are provably equivalent (because of SN) even if not $\beta\eta$-equivalent in the general case. I'll check with other researchers tomorrow, as I'm pretty ignorant on the type case, and in general people consider infinite ground types avoiding your problem altogether. $\endgroup$ – Graffitics Feb 18 '16 at 0:57

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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