3
$\begingroup$

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?

|cite|improve this question
$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – cody Nov 12 '12 at 17:38
  • $\begingroup$ 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? $\endgroup$ – Callum Rogers Nov 12 '12 at 17:49
  • $\begingroup$ 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. $\endgroup$ – cody Nov 12 '12 at 19:56
2
$\begingroup$

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

|cite|improve this answer
$\endgroup$
  • $\begingroup$ 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? $\endgroup$ – Gilles 'SO- stop being evil' Nov 13 '12 at 19:44
  • $\begingroup$ @Gilles: That's a very creative interpretation of what is written. $\endgroup$ – Dave Clarke Nov 13 '12 at 20:09

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.