Return-Path: <tvashwin@cs.bu.edu> Received: from csa.bu.edu (csa [128.197.12.3]) by cs3.bu.edu (8.12.11/8.12.11) with ESMTP id i8U5EUlX014961; Thu, 30 Sep 2004 01:14:30 -0400 Received: from localhost (tvashwin@localhost) by csa.bu.edu (8.10.1/8.10.1) with ESMTP id i8U5EU120753; Thu, 30 Sep 2004 01:14:30 -0400 (EDT) X-Authentication-Warning: csa.bu.edu: tvashwin owned process doing -bs Date: Thu, 30 Sep 2004 01:14:30 -0400 (EDT) From: ashwin thangali <tvashwin@cs.bu.edu> X-Sender: tvashwin@csa.bu.edu To: Assaf Kfoury <kfoury@cs.bu.edu> cc: Quan Yuan <yq@cs.bu.edu>, cs520 Course Account <cs520@cs.bu.edu> Subject: Re: renaming In-Reply-To: <415B90E0.8060505@cs.bu.edu> Message-ID: <Pine.SOL.4.20.0409300111090.28051-100000@csa.bu.edu> Content-Type: TEXT/PLAIN; charset=US-ASCII X-Spam-HitLevel: X-Spam-DCC: dcc.uncw.edu: cs3.bu.edu 1201; Body=2 Fuz1=2 Fuz2=2 X-Spam-Checker-Version: SpamAssassin 2.64 (2004-01-11) on cs3.bu.edu X-Spam-Level: X-Spam-Status: No, hits=0.0 required=10.0 tests=none autolearn=ham version=2.64 X-Spam-Pyzor: Reported 0 times. Status: RO X-Mozilla-Status: 8013 X-Mozilla-Status2: 00000000 X-UIDL: 411f69ec00000de6
asaf,
can you provide a set of interesting test cases so that we can check
our implementation? this would be useful since some of us may overlook
some peculiar cases.
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
On Thu, 30 Sep 2004, Assaf Kfoury wrote:
> 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