[plt-scheme] redex is great

 From: Robby Findler (robby at eecs.northwestern.edu) Date: Sat Feb 21 09:41:34 EST 2009 Previous message: [plt-scheme] redex is great Next message: [plt-scheme] redex is great Messages sorted by: [date] [thread] [subject] [author]

```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]