[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.
"
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>
More information about the FOM
mailing list