Return-Path: <yq@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 i8UHC89O029665 for <kfoury@cs3.bu.edu>; Thu, 30 Sep 2004 13:12:08 -0400 Received: from JELLYFISH (cumm111-0b01-dhcp167.bu.edu [128.197.11.167]) (authenticated bits=0) by cs.bu.edu (8.12.2/8.12.2) with ESMTP id i8UHC79o024294 for <kfoury@cs.bu.edu>; Thu, 30 Sep 2004 13:12:08 -0400 (EDT) Message-Id: <200409301712.i8UHC79o024294@cs.bu.edu> Date: Thu, 30 Sep 2004 13:14:47 -0400 From: "Quan Yuan" <yq@cs.bu.edu> To: "Assaf Kfoury" <kfoury@cs.bu.edu> Subject: Re: Re: Top level variable bindings X-mailer: Foxmail 5.0 [en] Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: 7bit X-Spam-HitLevel: xx X-Spam-DCC: sonic.net: cs3.bu.edu 1156; 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=2.2 required=10.0 tests=AWL,MSGID_FROM_MTA_BACKUP autolearn=no version=2.64 X-Spam-Pyzor: Reported 0 times. Status: X-Mozilla-Status: 8011 X-Mozilla-Status2: 00000000 X-UIDL: 411f69ec00000e1b
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