[FOM] lambda calculus/Barendregt
pax0 at seznam.cz
pax0 at seznam.cz
Thu Feb 7 13:33:23 EST 2013
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).
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
">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
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)
> 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.
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...
More information about the FOM