lambda calculus: delta rules
Author Message lambda calculus: delta rules

Hi,

I'm currently reading Chris Hankin's _Lambda Calculi: A Guide for
Computer Scientists_.  When  introducing delta rules he writes:

# An example, introduced by Church is:
#
#   deltaC MN -> lambda xy.x if M,N element-of beta-deltaC-nf0
#                            and M and N are equivalent
#   deltaC MN -> lambda xy.y if M,N element-of beta-deltaC-nf0
#                            and M and N are not equivalent
#
# [...] It is important that the delta-rules specify closed terms to
# avoid inconsistency:
#
#   (lambda xy.deltaC xy)II ->> deltaC II -> lambda xy.x
#
# but if deltaC can be applied to open terms then we also have:
#
#   (lambda xy.deltaC xy)II -> (lambda xyzw.w)II ->> lambda zw.w

I don't understand this last line at all.  How can you get from
`(lambda xy.deltaC xy)II' to `(lambda xyzw.w)II'?

Hopefully, someone can help me out here.

Thanks,
Boris

--

Sun, 30 Mar 2003 07:42:33 GMT  lambda calculus: delta rules

Quote:

> Hi,

> I'm currently reading Chris Hankin's _Lambda Calculi: A Guide for
> Computer Scientists_.  When  introducing delta rules he writes:

> # An example, introduced by Church is:
> #
> #   deltaC MN -> lambda xy.x if M,N element-of beta-deltaC-nf0
> #                            and M and N are equivalent
> #   deltaC MN -> lambda xy.y if M,N element-of beta-deltaC-nf0
> #                            and M and N are not equivalent
> #
> # [...] It is important that the delta-rules specify closed terms to
> # avoid inconsistency:
> #
> #   (lambda xy.deltaC xy)II ->> deltaC II -> lambda xy.x
> #
> # but if deltaC can be applied to open terms then we also have:
> #
> #   (lambda xy.deltaC xy)II -> (lambda xyzw.w)II ->> lambda zw.w

> I don't understand this last line at all.  How can you get from
> `(lambda xy.deltaC xy)II' to `(lambda xyzw.w)II'?

Simply by redycing deltaC x y first.

deltaC x y -> lambda xy. y
(which, by alpha) = lambda zw . w

so, using the usual rules for lambda reduction,

(lambda xy.deltaC xy)II -> (lambda xy. lambda zw. w)II
\_______/
\____________this bit reduced first

which can be written (lambda xyzw . w)II

When not using delta rules, it's perfectly OK to reduce in any order.

--

Sun, 30 Mar 2003 03:00:00 GMT  lambda calculus: delta rules

| > I don't understand this last line at all.  How can you get from
| > `(lambda xy.deltaC xy)II' to `(lambda xyzw.w)II'?
|
| Simply by redycing deltaC x y first.
|
|    deltaC x y -> lambda xy. y
|    (which, by alpha) = lambda zw . w

Well,

deltaC x y -> lambda xy.y
only if x is not syntactically equivalent to y.

I think I'm missing something completely here.  To me x and y seem to
be syntactically equivalent in the above reductions and if they indeed
are syntactically equivalent, then the complete form would reduce like
this:

(lambda xy.deltaC x y)II -> (lambda xyzw.z)II ->> lambda zw.z

which would be correct.

Although, I think a related example proves the point that you must not
apply delta rules to open terms:

(lambda xy.deltaC x y)IK -> (lambda xyzw.z)IK -> lambda zw.z

which is clearly incorrect, since I is not equivalent to K.

Still not getting the original example and probably completely
misunderstanding something,

Boris

--

To err is human,
To purr feline.
-- Robert Byrne

Sun, 30 Mar 2003 03:00:00 GMT  lambda calculus: delta rules

Quote:

> Well,

>   deltaC x y -> lambda xy.y
>   only if x is not syntactically equivalent to y.

> I think I'm missing something completely here.  To me x and y seem to
> be syntactically equivalent in the above reductions

Syntactically equivalent means "the same up to alpha conversion" (ie
are the same without doing any reduction), which the terms x and y are
not.  \x.x is syntactically equivalent to \y.y, because x and y are
both bound, permitting renaming.

I suppose there's a case for "syntactically equivalent" meaning "the
same" (without any form of translation), but that wouldn't affect the
lack of equivalence between x and y.  You may be confusing syntactical
equivalence with "belonging to the same syntactic category" or
something.

Jn

--

Sun, 30 Mar 2003 03:00:00 GMT  lambda calculus: delta rules

| Syntactically equivalent means "the same up to alpha conversion" (ie
| are the same without doing any reduction), which the terms x and y
| are not.  \x.x is syntactically equivalent to \y.y, because x and y
| are both bound, permitting renaming.

Thank you, this clears things up for me.

--

Everything should be built top-down, except the first time.

Tue, 01 Apr 2003 03:00:00 GMT

 Page 1 of 1 [ 5 post ]

Relevant Pages