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