# [plt-scheme] redex is great

 From: Jos Koot (jos.koot at telefonica.net) Date: Sat Feb 21 09:55:59 EST 2009 Previous message: [plt-scheme] redex is great Next message: [plt-scheme] redex is great Messages sorted by: [date] [thread] [subject] [author]

```This does not reduce T in (x T) and (λ x T), I think
You probably get a head normal form, but not a normal form, I think
Jos

----- Original Message -----
From: "Robby Findler" <robby at eecs.northwestern.edu>
To: "Jos Koot" <jos.koot at telefonica.net>
Cc: <plt-scheme at list.cs.brown.edu>
Sent: Saturday, February 21, 2009 3:41 PM
Subject: Re: [plt-scheme] redex is great

On Sat, Feb 21, 2009 at 8:22 AM, Jos Koot <jos.koot at telefonica.net> wrote:
> Suppose we have a language and a reductor that uses in-hole. Then if term
> T
> matches the in-hole clause, the term (T T) has two matches. As far as I
> can
> see both matches are returned by apply-reduction-relation (which in
> general
> is nice, of course, but here I am talking about leftmost reduction). Hence
> this reductor does not limit itself to leftmost redices only.

I'm not completely sure I'm getting your meaning above, but consider
this grammar:

T = (λ x T) | (T T) | x
E = hole | ((λ x T) E) | (E T)
x = variables

with this rule:

(--> (in-hole E ((λ x T_1) (λ x T_2)))
(in-hole E (subst x T_1 T_2)))

and this example input:

(((λ x x) (λ y y))
((λ p p) (λ q q)))

It reduces to this:

((λ y y)
((λ p p) (λ q q)))

but it does not reduce to this:

(((λ x x) (λ y y))
(λ q q))

because the decomposition of the term does not allow the hole to be on
the second application. That is, the context is restricting
applicability of the rule to only a subset of the places where it
might otherwise apply.

I didn't go thru the exercise and try it out myself, but reading over
your definition of nf? and reduction-step, you should be able to
formulate them as contexts. nf? could clearly be formulated as a
non-terminal in the grammar that matches only things that nf? returns
true for, and then reduction-step can be turned into a definition of a
context that has the hole at the point where (in the definition of
reduction-step) you call subst (ie, case 3).

Robby

```

 Posted on the users mailing list. Previous message: [plt-scheme] redex is great Next message: [plt-scheme] redex is great Messages sorted by: [date] [thread] [subject] [author]