[racket-dev] composing contexts in Redex?
Is there any way to compose contexts in Redex? I want to represent a context where, at each level, the leftmost term is an arbitrary number of nested lambdas, and the hole is in the body of the innermost lambda. A ::= hole | (\x_1...\x_n.A) e_1 .. e_n Below is my (stripped down) attempt at representing this in redex, but trying to match (term hole) to an A context goes into an infinite loop. #lang racket (require redex) (define-language test (e x (λ x e) (e e)) (x variable-not-otherwise-mentioned) (F hole (λ x F)) (L hole (L e)) (A hole (in-hole L (in-hole F A _ For list-related administrative tasks: http://lists.racket-lang.org/listinfo/dev
Re: [racket-dev] composing contexts in Redex?
On Mon, May 2, 2011 at 2:43 PM, Stephen Chang stch...@ccs.neu.edu wrote: Why not just: A ::= hole | ((lambda x A) e) That doesnt cover something like (((lambda y (lambda x hole)) e_1) e_2) Oh, right. Sorry. Robby _ For list-related administrative tasks: http://lists.racket-lang.org/listinfo/dev
Re: [racket-dev] composing contexts in Redex?
2011/5/2 Stephen Chang stch...@ccs.neu.edu: Oh, but this simpler definition seems to be equivalent: (define-language test (e x (λ x e) (e e)) (x variable-not-otherwise-mentioned) (A hole (λ x A) (A e))) Yes, you are right. But I left out a part of my grammar, which is that I need the number of nested lambdas and the number of arguments to be equal. I couldnt figure out a way to define that with only one context. Here's what I'm currently working with: (F (λ x hole) (λ x F)) (L (hole e) (L e)) (A hole (side-condition (in-hole L_1 (in-hole F_1 A)) (= (term (num-λs F_1)) (term (num-args L_1) (define-language test (e x (λ x e) (e e)) (x variable-not-otherwise-mentioned) (A hole (in-hole (A e) (λ x A (redex-match test A (term hole)) `(,(make-match `(,(make-bind 'A (make-hole) (redex-match test A (term (((λ y (λ x hole)) a) b))) `(,(make-match `(,(make-bind 'A `(((λ y (λ x ,(make-hole))) a) b) (redex-match test A (term (((λ y hole) a) b))) false (redex-match test A (term ((λ y (λ x hole)) a))) false (redex-match test A (term ((λ x (((λ y (λ z hole)) a) b)) c))) `(,(make-match `(,(make-bind 'A `((λ x (((λ y (λ z ,(make-hole))) a) b)) c) (redex-match test A (term ((λ x ((λ y (λ z hole)) a)) b))) false _ For list-related administrative tasks: http://lists.racket-lang.org/listinfo/dev
Re: [racket-dev] composing contexts in Redex?
2011/5/2 Casey Klein clkl...@eecs.northwestern.edu: (define-language test (e x (λ x e) (e e)) (x variable-not-otherwise-mentioned) (A hole (in-hole (A e) (λ x A (redex-match test A (term hole)) `(,(make-match `(,(make-bind 'A (make-hole) (redex-match test A (term (((λ y (λ x hole)) a) b))) `(,(make-match `(,(make-bind 'A `(((λ y (λ x ,(make-hole))) a) b) (redex-match test A (term (((λ y hole) a) b))) false (redex-match test A (term ((λ y (λ x hole)) a))) false (redex-match test A (term ((λ x (((λ y (λ z hole)) a) b)) c))) `(,(make-match `(,(make-bind 'A `((λ x (((λ y (λ z ,(make-hole))) a) b)) c) (redex-match test A (term ((λ x ((λ y (λ z hole)) a)) b))) false (Oops, hit Send before typing the rest of my message.) Does that work? _ For list-related administrative tasks: http://lists.racket-lang.org/listinfo/dev
Re: [racket-dev] composing contexts in Redex?
(define-language test (e x (λ x e) (e e)) (x variable-not-otherwise-mentioned) (A hole (in-hole (A e) (λ x A Cool, that works! I didnt think to do that with in-hole. Can you explain how it keeps the number of lambdas and arguments the same though? I'm cant quite figure out what's going on. _ For list-related administrative tasks: http://lists.racket-lang.org/listinfo/dev
Re: [racket-dev] composing contexts in Redex?
Hmm, or maybe you've found a bug in my model. Either way, thanks for looking into this. 2011/5/2 Casey Klein clkl...@eecs.northwestern.edu: On Mon, May 2, 2011 at 3:30 PM, Stephen Chang stch...@ccs.neu.edu wrote: (define-language test (e x (λ x e) (e e)) (x variable-not-otherwise-mentioned) (A hole (in-hole (A e) (λ x A Cool, that works! I didnt think to do that with in-hole. Can you explain how it keeps the number of lambdas and arguments the same though? I'm cant quite figure out what's going on. I spent some time trying to come up with a convincing explanation. I didn't get anywhere. It turns out my problem was that it doesn't actually work: (redex-match test A (term (((λ x ((λ y (λ z hole)) a)) b) c))) `(,(make-match `(,(make-bind 'A `(((λ x ((λ y (λ z ,(make-hole))) a)) b) c) One of these days maybe I'll learn that the redex-check step comes before the email step (and way before the paper publishing step). _ For list-related administrative tasks: http://lists.racket-lang.org/listinfo/dev
