[racket-dev] composing contexts in Redex?

From: Casey Klein (clklein at eecs.northwestern.edu)
Date: Tue May 3 10:10:31 EDT 2011

On Mon, May 2, 2011 at 8:45 PM, Stephen Chang <stchang at ccs.neu.edu> wrote:
> Hmm, or maybe you've found a bug in my model. Either way, thanks for
> looking into this.

I couldn't resist taking another look.

Here's how I'd like to define it:

(define-language unfortunate-loop
    (L hole
       (in-hole (L e) (λ x hole)))
    (A hole
       (in-hole L A)))

An L is one level of applications. Its second production extends an L
with one application on the outside and one lambda on the inside,
thereby maintaining balance. An A is zero or more nested Ls.

Unfortunately, this definition sends the Redex matcher into a loop.
Matching term t against pattern A will use the second production of A
and the first production of L to get back to where it started,
matching t against A. (As Robby pointed out, maybe it should consider
these choices a failure and turn to the other productions.)

This definition can be salvaged by forcing A's second production to
consume some input before consuming a possibly empty L:

(define-language no-loop
    (A hole
        (in-hole (L e) (λ x A)))
    (L hole
        (in-hole (L e) (λ x hole))))

The second A production wraps the L in an application and consequently
expects an extra lambda before the next A.

Alternatively, we could make L slightly unbalanced and account for the
extra lambda in A's second production:

(define-language also-no-loop
    (A hole
       (in-hole (L e) A))
    (L (λ x hole)
       (in-hole (L e) (λ x hole))))

I'm not happy with either of these definitions, though; they require
too much thinking about how the matching algorithm will behave. I'm
starting to think I was wrong when I suggested that we should make
these definitions syntax errors and be done with it.

Posted on the dev mailing list.