[racket-dev] composing contexts in Redex?

Thanks for the careful analysis. 

The best solution sounds to me like a form of backtracking so that the
matcher can skip clauses when it reaches cycles.

In the meantime, Stephen can manage with the suggestions below. 

-- Matthias



On May 3, 2011, at 10:10 AM, Casey Klein wrote:

> 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.
> 
> _________________________________________________
>  For list-related administrative tasks:
>  http://lists.racket-lang.org/listinfo/dev