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 i9141gfQ032671; Fri, 1 Oct 2004 00:01:42 -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 i9141fSZ012041; Fri, 1 Oct 2004 00:01:41 -0400 (EDT) Message-ID: <415CD6A7.8040603@cs.bu.edu> Date: Fri, 01 Oct 2004 00:01:43 -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: Quan <Yuan@cs.bu.edu>, cs520 Course Account <cs520@cs.bu.edu> Subject: Re: Top level variable bindings References: <200410010342.i913ghSZ008724@cs.bu.edu> In-Reply-To: <200410010342.i913ghSZ008724@cs.bu.edu> Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit X-Spam-HitLevel: xx X-Spam-DCC: dmv.com: cs3.bu.edu 1181; 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: 411f69ec00000e47
Yes, it is full-beta reduction, not call-by-value. You can say that,
under evaluation of *closed* terms under call-by-value, you do not need
to worry about variable capture -- if you also decide to explicitly
substitute a copy of the argument (or actual parameter) for every
occurrence of the formal parameter. But is this the only way to carry
out call-by-value (and other evaluation strategies)? Why would you not,
for example, create an environment (or a table) instead, where you keep
a pairing of the formal parameter and the corresponding argument which
will be looked up only when needed?
Assaf
Quan wrote:
>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