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 i8U4pkGK011064; Thu, 30 Sep 2004 00:51:46 -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 i8U4pj9n005647; Thu, 30 Sep 2004 00:51:45 -0400 (EDT) Message-ID: <415B90E0.8060505@cs.bu.edu> Date: Thu, 30 Sep 2004 00:51:44 -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 <yq@cs.bu.edu>, cs520 Course Account <cs520@cs.bu.edu> Subject: Re: renaming References: <200409300008.i8U0889o026108@cs.bu.edu> In-Reply-To: <200409300008.i8U0889o026108@cs.bu.edu> Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit X-Spam-HitLevel: xx X-Spam-DCC: dcc.uncw.edu: cs3.bu.edu 1201; 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: 411f69ec00000de3
Quan Yuan wrote:
>Professor,
>For the implementation part of this assignment,
>1. Do we just report error and exit when there are unbounded variables, like the implementation by Piece?
>
>
It is a fair to assume that all input terms will be *closed*, i.e., they
do not contain free variable occurrences. But once you start
manipulating such terms, you cannot avoid subterms that are *open*,
i.e., containing free variable occurrences.
>2. When we have a command like " \lambda y. (\lambda y. \lambda x. yx) y",
>do we need to rename the y inside the paranthese?
>
If the preceding term is applied to an argument (call it t), thus
creating a beta-redex, it is probably a good strategy to rename the
inner y (inside the parentheses), so that when you substitute t for y
you only substitute for occurrences of y that are in the scope of the
outer lambda-binding.
>It seems we can use this term
>in an application without variable capturing as long as there is no unbounded variables.
>
>according to the substitution rules on top of [Piece, page 71],
>
> (\lambda y. (\lambda y. \lambda x. yx) y) (\lambda w.w)
>=> (\lambda y. \lambda x. yx) (\lambda w.w)
>=> \lambda x. (\lambda w. w) x
>
>
The preceding evaluation is correct.
Assaf
>
>
>Thanks,
>
>Quan
>
>
>
>
This archive was generated by hypermail 2b29 : Fri Nov 19 2004 - 17:00:43 EST