# Are two terms where one is without a $\lambda\beta$ normal form unconvertible in $\lambda\beta$?

I know that if you try and make the theory

$$\lambda\beta+\{s = t\ |\text{ s, t are terms without }\lambda\beta\text{ normal forms}\}$$

then that theory becomes inconsistent. Are two terms where one is without a $\lambda\beta$ normal form also unconvertible in $\lambda\beta$, ie can it ever be true that $\lambda\beta \vdash s=t$ if $s$ dosen't have a normal form?

-
I'm not sure I understand your question: First, you may add s=t for certain terms s,t without normal form to the lambda calculus without breaking consistency: this is the notion of meaningless term that was widely studied in the 60s and 70s. The rest of your question is poorly worded, I'm afraid. – cody Nov 12 '12 at 17:38
Maybe poorly worded - I just have very little idea what I'm talking about, only having studied lambda calculus for 3 weeks! By meaningless term do you mean unsolvable term? The real question is if you are given a term s that is not normalisable and any term t, is it always the case that you can never equate them using the rules of lambda beta? – Callum Rogers Nov 12 '12 at 17:49
Yes I'm sorry I meant unsolvable (meaningless is a more general definition given for terms). Also, I'm still not clear on your question: why can't you take s=t (modulo alpha) for example? In that case s can be anything. – cody Nov 12 '12 at 19:56

It is trivially the case that two terms can be $\beta$-convertible even though they do not have a normal form.

Consider:

$$((\lambda x.x)\ (\lambda x.x\ x))\ (\lambda x.x\ x)$$

and

$$(\lambda x.x\ x)\ (\lambda x.x\ x).$$

In one step we have $$((\lambda x.x)\ (\lambda x.x\ x))\ (\lambda x.x\ x)\to (\lambda x.x\ x)\ (\lambda x.x\ x)$$

-
You're answering a rather boring interpretation of the question. I think what was really meant is: if $s \neq_\beta t$ and neither $s$ nor $t$ has a normal form, is the equational theory of $\beta \cup \{s=t\}$ inconsistent? – Gilles Nov 13 '12 at 19:44
@Gilles: That's a very creative interpretation of what is written. – Dave Clarke Nov 13 '12 at 20:09