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 i8UMcR0l002961; Thu, 30 Sep 2004 18:38:27 -0400 Received: from cs.bu.edu (kfoury@fiddle [128.197.10.114]) (authenticated bits=0) by cs.bu.edu (8.12.2/8.12.2) with ESMTP id i8UMcSSZ023163; Thu, 30 Sep 2004 18:38:28 -0400 (EDT) Sender: kfoury@cs.bu.edu Message-ID: <415C8AE1.5D3154A6@cs.bu.edu> Date: Thu, 30 Sep 2004 18:38:25 -0400 From: "Assaf J. Kfoury" <kfoury@cs.bu.edu> Organization: Boston University X-Mailer: Mozilla 4.78 [en] (X11; U; SunOS 5.8 sun4u) X-Accept-Language: en To: ashwin thangali <tvashwin@cs.bu.edu> CC: Quan Yuan <yq@cs.bu.edu>, cs520 Course Account <cs520@cs.bu.edu> Subject: Re: renaming References: <Pine.SOL.4.20.0409300111090.28051-100000@csa.bu.edu> Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit X-Spam-HitLevel: X-Spam-DCC: MC: cs3.bu.edu 1128; 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=0.1 required=10.0 tests=AWL autolearn=ham version=2.64 X-Spam-Pyzor: Reported 0 times. Status: X-Mozilla-Status: 8011 X-Mozilla-Status2: 00000000 X-UIDL: 411f69ec00000e3a
Here are some examples you may try.
First some abbreviations:
2 = (lambda x. lambda y. x ( x y ) ) -- Church numeral 2.
I = (lambda x. x)
K = (lambda x. lambda y. x)
omega = (lambda x. x x)
Now try various combinations of the previous
terms {2, I, K, omega}. For example, test your
interpreter with
2 I I
2 K
2 2 K
omega omega
K omega
omega I
etc.
Assaf
ashwin thangali wrote:
> 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