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
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
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
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
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
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
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
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
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 (λ
(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
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
11 matches
Mail list logo
