[FOM] lambda calculus/Barendregt

pax0 at seznam.cz pax0 at seznam.cz
Thu Feb 7 13:33:23 EST 2013

Hi All,
I have a question about lambda calculus in Barendregt book 1.st edition.
I cannot derive example at the bottom of page 148.
The author writes that S(K(SI))(S(KK)I) can be derived from lambda*x.SI(Kx)
and I derived S(KS)(S(KI)(S(KK)I))
We are both right and in CL+ext these 2 terms can be reduced to SI(Kx).
None of
S(K(SI))(S(KK)I)
S(KS)(S(KI)(S(KK)I))
can be reduced in CL alone.
So my question is, why this non-confluence does not contradict Church-
Rosser's Theorem for CL (without ext!).
Both are derived in CL from the same lambda-term.
Thank you, Jan Pax

"
See below.

"

">I have two questions.
>Why the example is stated before the stronger CL_ext
>is introduced, and is in the scope of CL?
"

May be that both

[A]  S(K(SI))(S(KK)I)
[B] S(KS)(S(KI)(S(KK)I))

can be derived from SI(Kx) but not to SI(Kx).

"

"

Is this the case?

""

If not which from [A], [B] can be derived from SI(Kx)?
I'd say that both.

"

If not both, how then I derived [B] and Barendregt [A]?

If both, this would contradict Church Rosser theorem for CL.

Each possibility is strange; which actually holds?

Thank you, Hynek

"

"

"

"

> \How can I see
> S(K(SI))(S(KK)I)x weakly reduces to SI(Kx)
> and
> S(KS)(S(KP)(S(KK)I))x weakly reduces to SI(Kx).

The rules of weak reduction are:
(S) Replace SXYZ by XZ(YZ),
(K) Replace KXY by X.

Now
S(K(SI))(S(KK)I)x
has form SXYZ, where
X is (K(SI)),
Y is (S(KK)I),
Z is x.
So it reduces to XZ(YZ), which is [I leave you to fill in the details].
This can be reduced further [details omitted].

Barendregt's book is very condensed. To get a "gentler" introduction
to combinatory logic, try the internet. When I looked a couple of
years ago, there were some lecture-notes, although I now forget
where. Perhaps some still survive."
"
"
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20130207/c2361358/attachment-0001.html>