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