Re: [racket-dev] composing contexts in Redex?
2011/5/5 Stephen Chang stch...@ccs.neu.edu: So I'm struggling with redex again and I cant figure out a way to utilize any of the previously mentioned tricks. I just included what I have below and I described what I'm trying to do. Hopefully someone will have some time to take a look? :) I'm not quite sure what you're going for, but I have some guesses below. I have a context A, where the focus is in the body of the lambda(s) of an application, and for every lambda, there is an argument to match. I'm using Casey's definition from earlier in this thread (you did uncover a bug in my model, thanks for that!). (A hole (in-hole (A e) (λ x A))) However, I also want to be able to split A's so that other stuff can go in between, Can you define an other stuff non-terminal O: (O hole ) and sprinkle some Os in A: (A hole (in-hole (in-hole O ((in-hole O A) e)) (λ x (in-hole O A ? I'm not sure if I have the Os in the right spots, but this should be OK termination-wise as long as O does not have any productions that lead directly to A (e.g., the production A, a production B where B is a non-terminal with production A, etc.). If it does, then the outermost in-hole O would need to be reworked. so I defined a more general context C and a metafunction balance where if (balance C) = 0, then C \in A. The balance fn (defined below) returns the number of extra unmatched args available in a C, and #f otherwise (ie - if there's too many lambdas). (C hole (λ x C) (C e)) Finally, I have evaluation contexts E that use the previous definitions: (E ;; hole (E e) (in-hole A E) (side-condition (in-hole C_1 E) (term (balance C_1))) ... other Es ...) I'd like to be able to use the (commented out) productions on the first line of E, but I was getting infinite loops. Then I realized that the productions on the first line are equivalent to a subset of C that have a nonnegative balance, so I tried using the production on the second line instead, thinking it would work bc I got rid of the hole in E, but it still infinite loops when trying to match hole. There would be no loop if C didn't include hole: (L (λ x hole) (hole e)) (C L (in-hole L C)) Can you still define what you want using this C? Finally, I want to be able to use these contexts in conjunction with other, more complicated E productions. I included the relevant snippets of my language definition below: (define-language test (e x (λ x e) (e e)) (x (variable-except e λ v a A n C E hole any)) (n integer) (C hole (λ x C) (C e)) (A hole (in-hole (A e) (λ x A))) ; via Casey (E #;hole #;(E e) #;(in-hole A E) (side-condition (in-hole C_1 E) (term (balance C_1))) (side-condition (in-hole C_1 ((in-hole A_1 (λ x_1 (in-hole C_2 (in-hole E x_1 E)) (and (redex-match test A (term (in-hole C_1 C_2))) (not (member (term x_1) (term (bound-vars-C C_2))) ) (define-metafunction test ; balance : C - n or #f [(balance C) (balance_ C 0 0)]) (define-metafunction test ; balance_ : C n n - n or #f [(balance_ hole n_1 n_2) ,(- (term n_2) (term n_1))] [(balance_ (C e) n_1 n_2) (balance_ C n_1 ,(add1 (term n_2)))] [(balance_ (λ x C) n_1 n_2) ,(if ( (term n_1) (term n_2)) (term (balance_ C ,(add1 (term n_1)) n_2)) #f)]) ;; bound-vars ;; compute the set/list of bound variables in a given term (define-metafunction test bound-vars-C : C - (x ...) [(bound-vars-C (λ x C)) (x ,@(term (bound-vars-C C)))] [(bound-vars-C (C e)) (bound-vars-C C)] [(bound-vars-C hole) ()]) _ For list-related administrative tasks: http://lists.racket-lang.org/listinfo/dev
Re: [racket-dev] composing contexts in Redex?
Can you define an other stuff non-terminal O: (O hole ) and sprinkle some Os in A: (A hole (in-hole (in-hole O ((in-hole O A) e)) (λ x (in-hole O A Something along this line could work. But I would need side conditions to make sure that the O doesnt mess up the A-ness property of the A. Being able to split A's is only part of the problem though. I think ultimately, the problem is that I still want to be able to combine context definitions. For example, I need A to be one possible case in another context definition E. There would be no loop if C didn't include hole: (L (λ x hole) (hole e)) (C L (in-hole L C)) Can you still define what you want using this C? C must be able to be a hole in the code I have. But maybe it doesnt have to with your O idea above. Thanks for the ideas! _ For list-related administrative tasks: http://lists.racket-lang.org/listinfo/dev
Re: [racket-dev] composing contexts in Redex?
So I'm struggling with redex again and I cant figure out a way to utilize any of the previously mentioned tricks. I just included what I have below and I described what I'm trying to do. Hopefully someone will have some time to take a look? :) I have a context A, where the focus is in the body of the lambda(s) of an application, and for every lambda, there is an argument to match. I'm using Casey's definition from earlier in this thread (you did uncover a bug in my model, thanks for that!). (A hole (in-hole (A e) (λ x A))) However, I also want to be able to split A's so that other stuff can go in between, so I defined a more general context C and a metafunction balance where if (balance C) = 0, then C \in A. The balance fn (defined below) returns the number of extra unmatched args available in a C, and #f otherwise (ie - if there's too many lambdas). (C hole (λ x C) (C e)) Finally, I have evaluation contexts E that use the previous definitions: (E ;; hole (E e) (in-hole A E) (side-condition (in-hole C_1 E) (term (balance C_1))) ... other Es ...) I'd like to be able to use the (commented out) productions on the first line of E, but I was getting infinite loops. Then I realized that the productions on the first line are equivalent to a subset of C that have a nonnegative balance, so I tried using the production on the second line instead, thinking it would work bc I got rid of the hole in E, but it still infinite loops when trying to match hole. Finally, I want to be able to use these contexts in conjunction with other, more complicated E productions. I included the relevant snippets of my language definition below: (define-language test (e x (λ x e) (e e)) (x (variable-except e λ v a A n C E hole any)) (n integer) (C hole (λ x C) (C e)) (A hole (in-hole (A e) (λ x A))) ; via Casey (E #;hole #;(E e) #;(in-hole A E) (side-condition (in-hole C_1 E) (term (balance C_1))) (side-condition (in-hole C_1 ((in-hole A_1 (λ x_1 (in-hole C_2 (in-hole E x_1 E)) (and (redex-match test A (term (in-hole C_1 C_2))) (not (member (term x_1) (term (bound-vars-C C_2))) ) (define-metafunction test ; balance : C - n or #f [(balance C) (balance_ C 0 0)]) (define-metafunction test ; balance_ : C n n - n or #f [(balance_ hole n_1 n_2),(- (term n_2) (term n_1))] [(balance_ (C e) n_1 n_2)(balance_ C n_1 ,(add1 (term n_2)))] [(balance_ (λ x C) n_1 n_2) ,(if ( (term n_1) (term n_2)) (term (balance_ C ,(add1 (term n_1)) n_2)) #f)]) ;; bound-vars ;; compute the set/list of bound variables in a given term (define-metafunction test bound-vars-C : C - (x ...) [(bound-vars-C (λ x C)) (x ,@(term (bound-vars-C C)))] [(bound-vars-C (C e)) (bound-vars-C C)] [(bound-vars-C hole) ()]) _ For list-related administrative tasks: http://lists.racket-lang.org/listinfo/dev
Re: [racket-dev] composing contexts in Redex?
2011/5/5 Stephen Chang stch...@ccs.neu.edu: So I'm struggling with redex again and I cant figure out a way to utilize any of the previously mentioned tricks. I just included what I have below and I described what I'm trying to do. Hopefully someone will have some time to take a look? :) I have a context A, where the focus is in the body of the lambda(s) of an application, and for every lambda, there is an argument to match. I'm using Casey's definition from earlier in this thread (you did uncover a bug in my model, thanks for that!). (A hole (in-hole (A e) (λ x A))) However, I also want to be able to split A's so that other stuff can go in between, so I defined a more general context C and a metafunction balance where if (balance C) = 0, then C \in A. The balance fn (defined below) returns the number of extra unmatched args available in a C, and #f otherwise (ie - if there's too many lambdas). (C hole (λ x C) (C e)) Finally, I have evaluation contexts E that use the previous definitions: (E ;; hole (E e) (in-hole A E) (side-condition (in-hole C_1 E) (term (balance C_1))) ... other Es ...) I'd like to be able to use the (commented out) productions on the first line of E, but I was getting infinite loops. Then I realized that the productions on the first line are equivalent to a subset of C that have a nonnegative balance, so I tried using the production on the second line instead, thinking it would work bc I got rid of the hole in E, but it still infinite loops when trying to match hole. Even without the productions on the first line, the one on the second line is enough to send the matcher into a loop. Since C_1 matches hole, matching (in-hole C_1 E) loops back to matching E without consuming any input. I'll take a closer look tomorrow and hopefully have a more production suggestion. Finally, I want to be able to use these contexts in conjunction with other, more complicated E productions. I included the relevant snippets of my language definition below: (define-language test (e x (λ x e) (e e)) (x (variable-except e λ v a A n C E hole any)) (n integer) (C hole (λ x C) (C e)) (A hole (in-hole (A e) (λ x A))) ; via Casey (E #;hole #;(E e) #;(in-hole A E) (side-condition (in-hole C_1 E) (term (balance C_1))) (side-condition (in-hole C_1 ((in-hole A_1 (λ x_1 (in-hole C_2 (in-hole E x_1 E)) (and (redex-match test A (term (in-hole C_1 C_2))) (not (member (term x_1) (term (bound-vars-C C_2))) ) (define-metafunction test ; balance : C - n or #f [(balance C) (balance_ C 0 0)]) (define-metafunction test ; balance_ : C n n - n or #f [(balance_ hole n_1 n_2) ,(- (term n_2) (term n_1))] [(balance_ (C e) n_1 n_2) (balance_ C n_1 ,(add1 (term n_2)))] [(balance_ (λ x C) n_1 n_2) ,(if ( (term n_1) (term n_2)) (term (balance_ C ,(add1 (term n_1)) n_2)) #f)]) ;; bound-vars ;; compute the set/list of bound variables in a given term (define-metafunction test bound-vars-C : C - (x ...) [(bound-vars-C (λ x C)) (x ,@(term (bound-vars-C C)))] [(bound-vars-C (C e)) (bound-vars-C C)] [(bound-vars-C hole) ()]) _ 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 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
[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
