Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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?

share|cite|improve this question
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.


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


$$(\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)$$

share|cite|improve this answer
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

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

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