[FOM] lambda calculus/Barendregt

[pax0 at seznam.cz]

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.

"



Read lambda*x.SI(Kx) instead here.

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

"



"












 
"




 
"
Ask Barendregt, not me!

> \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>