Return-Path: <kfoury@cs.bu.edu> Received: from cs.bu.edu (cs [128.197.12.2]) by cs3.bu.edu (8.12.11/8.12.11) with ESMTP id i8UMQ2Ol000540; Thu, 30 Sep 2004 18:26:02 -0400 Received: from cs.bu.edu (kfoury@fiddle [128.197.10.114]) (authenticated bits=0) by cs.bu.edu (8.12.2/8.12.2) with ESMTP id i8UMQ3SZ021355; Thu, 30 Sep 2004 18:26:03 -0400 (EDT) Sender: kfoury@cs.bu.edu Message-ID: <415C87F7.D180FD60@cs.bu.edu> Date: Thu, 30 Sep 2004 18:25:59 -0400 From: "Assaf J. Kfoury" <kfoury@cs.bu.edu> Organization: Boston University X-Mailer: Mozilla 4.78 [en] (X11; U; SunOS 5.8 sun4u) X-Accept-Language: en To: Quan Yuan <yq@cs.bu.edu>, cs520@cs.bu.edu Subject: Re: Top level variable bindings References: <200409301712.i8UHC79o024294@cs.bu.edu> Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit X-Spam-HitLevel: X-Spam-DCC: SPAMCHECK.NET: cs3.bu.edu 1168; Body=19 Fuz1=19 Fuz2=19 X-Spam-Checker-Version: SpamAssassin 2.64 (2004-01-11) on cs3.bu.edu X-Spam-Level: X-Spam-Status: No, hits=0.1 required=10.0 tests=AWL autolearn=ham version=2.64 X-Spam-Pyzor: Reported 0 times. Status: X-Mozilla-Status: 8011 X-Mozilla-Status2: 00000000 X-UIDL: 411f69ec00000e38
Just adjust my example a little in order to get
variable capture. For example, how about the
following:
lambda y. (lambda x. lambda y. x ( x y )) (lambda a. a y)
Assaf
Quan Yuan wrote:
> Professor,
> In the example (lambda x. lambda y. x ( x y )) (lambda a. a) (lambda b. b). Although lambda y. x ( x y) is open, but the argument (lambda a. a) is closed, it doesn't have the problem of variable capture.
>
> Quan
>
> ======= At 2004-09-30, 00:39:56 you wrote: =======
>
> >Why do you say that "top level bindings for variables" is not part of
> >pure untyped lambda calculus? A term of the form (lambda x. x) w is
> >certainly legal in the pure untyped lambda calculus.
> >
> >Are you perhaps thinking that your implementation should work on
> >*closed* terms? This is a fair assumption to make. So, for example, you
> >implementation should be able to work on an input term of the form:
> >
> >(lambda x. lambda y. x ( x y )) (lambda a. a) (lambda b. b)
> >
> >But then you will have to work with subterms that are not closed. For
> >example, the leftmost reduction step for the preceding term requires
> >that you substitute (lambda a. a) for every free occurrence of x in the
> >subterm
> >
> >lambda y. x ( x y)
> >
> >I hope this helps a little.
> >
> >Assaf
> >
> >ashwin thangali wrote:
> >
> >> Pierce's implementation allows top level bindings for variables. an
> >>example of this is given on line3 in test.f. This is not a part of pure
> >>untyped lambda calculus. do we need to implement this feature?
> >>
> >>without this, a command like,
> >>
> >>(lamda x. x) w
> >>
> >>would be illegal. but if top level binding is provided before this command
> >>then the command is legal.
> >>
> >>thanks,
> >>ashwin
> >>
> >>
> >>Ashwin V. Thangali
> >>111 Cummington Street,MCS 263,
> >>Computer Science Dept,
> >>Boston University,
> >>Boston, MA 02215
> >>Office: 617 358 1139
> >>Home: 617 734 6209
> >>Homepage: http://cs-people.bu.edu/tvashwin
> >>
> >>
> >>
> >>
> >>
> >.
>
> = = = = = = = = = = = = = = = = = = = =
>
This archive was generated by hypermail 2b29 : Fri Nov 19 2004 - 17:00:43 EST