Return-Path: <Yuan@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 i913gjsn028744 for <kfoury@cs3.bu.edu>; Thu, 30 Sep 2004 23:42:45 -0400 Received: from whoamI (dip14-ppp-162.bu.edu [168.122.14.162]) (authenticated bits=0) by cs.bu.edu (8.12.2/8.12.2) with ESMTP id i913ghSZ008724 for <kfoury@cs.bu.edu>; Thu, 30 Sep 2004 23:42:44 -0400 (EDT) Message-Id: <200410010342.i913ghSZ008724@cs.bu.edu> Date: Thu, 30 Sep 2004 23:42:48 -0500 From: "Quan" <Yuan@cs.bu.edu> To: "Assaf J. Kfoury" <kfoury@cs.bu.edu> Subject: Re: Re: Top level variable bindings X-mailer: Foxmail 5.0 [cn] Content-Type: text/plain; charset="gb2312" Content-Transfer-Encoding: 7bit X-Spam-HitLevel: xxxx X-Spam-DCC: SdV: cs3.bu.edu 1179; Body=1 Fuz1=1 Fuz2=1 X-Spam-Checker-Version: SpamAssassin 2.64 (2004-01-11) on cs3.bu.edu X-Spam-Level: **** X-Spam-Status: No, hits=4.6 required=10.0 tests=AWL,MSGID_FROM_MTA_BACKUP, RCVD_IN_DSBL,RCVD_IN_NJABL_DUL,RCVD_IN_NJABL_PROXY,RCVD_IN_SORBS_DUL, RCVD_IN_SORBS_MISC autolearn=no version=2.64 X-Spam-Pyzor: Reported 0 times. Status: RO X-Mozilla-Status: 8011 X-Mozilla-Status2: 00000000 X-UIDL: 411f69ec00000e45
But this is full-beta reduction instead of call-by-value, isn't it?
======= 2004-09-30 17:25:59 =======
>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