patternMinor
Are two terms where one is without a $\lambda\beta$ normal form unconvertible in $\lambda\beta$?
Viewed 0 times
withoutareunconvertiblewherenormalbetatwooneformterms
Problem
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?
$$\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?
Solution
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)$$
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)$$
Context
StackExchange Computer Science Q#6624, answer score: 2
Revisions (0)
No revisions yet.