Re: renaming

From: ashwin thangali (tvashwin@cs.bu.edu)
Date: Thu Sep 30 2004 - 01:14:30 EDT


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