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 i8U4dw9k008932; Thu, 30 Sep 2004 00:39:58 -0400 Received: from cs.bu.edu (h000c41248e2b.ne.client2.attbi.com [24.34.20.189]) (authenticated bits=0) by cs.bu.edu (8.12.2/8.12.2) with ESMTP id i8U4dv9n004035; Thu, 30 Sep 2004 00:39:57 -0400 (EDT) Message-ID: <415B8E1C.7090308@cs.bu.edu> Date: Thu, 30 Sep 2004 00:39:56 -0400 From: Assaf Kfoury <kfoury@cs.bu.edu> Organization: Boston University User-Agent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.6) Gecko/20040413 Debian/1.6-5 X-Accept-Language: en To: ashwin thangali <tvashwin@cs.bu.edu> CC: cs520 Course Account <cs520@cs.bu.edu> Subject: Re: Top level variable bindings References: <Pine.SOL.4.20.0409292337200.28051-100000@csa.bu.edu> In-Reply-To: <Pine.SOL.4.20.0409292337200.28051-100000@csa.bu.edu> Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit X-Spam-HitLevel: xx X-Spam-DCC: meer: cs3.bu.edu 1086; 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=2.4 required=10.0 tests=AWL,RCVD_IN_DSBL, RCVD_IN_NJABL_PROXY autolearn=no version=2.64 X-Spam-Pyzor: Reported 0 times. Status: RO X-Mozilla-Status: 8011 X-Mozilla-Status2: 00000000 X-UIDL: 411f69ec00000de2
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