Re: Re: Top level variable bindings

From: Quan Yuan (yq@cs.bu.edu)
Date: Thu Sep 30 2004 - 13:14:47 EDT


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