Ah, I see.
Those are the VT and TT I want, but then I also want to define:
(C ::= VT TT)
and take the context-closure of C.
(see attached)
Can I get my hands on the generated VT and TT easily, or would I need to tweak
Redex internals to automate this?
--
William J. Bowman
On Fri, May 03, 2019 at 07:52:09PM -0500, Robby Findler wrote:
> (thunk TT) isn't a TT, tho? It will reduce only in a TT.
>
> Robby
>
> On Fri, May 3, 2019 at 7:16 PM William J. Bowman <[email protected]>
> wrote:
> >
> > That looks like the contexts I want, but it doesn't seem to reduce under a
> > (thunk TT) in my example model.
> >
> > --
> > Sent from my phoneamajig
> >
> > > On May 3, 2019, at 20:02, Robby Findler <[email protected]> wrote:
> > >
> > > Redex, when asked to create the compatible closure, creates a context
> > > and then uses that. In this case, it will create a context something
> > > like this:
> > >
> > > TT ::= hole | (\ (x) TT) | (TT v) | (t VT) | (force VT) | (return VT)
> > > VT ::= (thunk TT)
> > >
> > > If you want something else (I'm not sure of an algorithm to handle
> > > this kind of thing without coming with something like that), it might
> > > be simplest to write out the contexts that you want directly and use
> > > context-closure.
> > >
> > > Robby
> > >
> > >> On Fri, May 3, 2019 at 6:42 PM William J. Bowman
> > >> <[email protected]> wrote:
> > >>
> > >> Hello all,
> > >>
> > >> I'm trying to define a model in Redex where values and terms are separate
> > >> nonterminals, and then define a reduction relation using
> > >> `compatible-closure`
> > >> to lift the small steps to the, well, compatible closure.
> > >> Unfortunately, it doesn't do what I expect, presumably because the
> > >> nonterminals
> > >> for values and terms are mutually defined, but `compatible-closure` takes
> > >> exactly one nonterminal.
> > >>
> > >> Is there a way to do what I want?
> > >> See attached.
> > >>
> > >> --
> > >> William J. Bowman
> > >>
> > >> --
> > >> You received this message because you are subscribed to the Google
> > >> Groups "Racket Users" group.
> > >> To unsubscribe from this group and stop receiving emails from it, send
> > >> an email to [email protected].
> > >> For more options, visit https://groups.google.com/d/optout.
> >
> > --
> > You received this message because you are subscribed to the Google Groups
> > "Racket Users" group.
> > To unsubscribe from this group and stop receiving emails from it, send an
> > email to [email protected].
> > For more options, visit https://groups.google.com/d/optout.
>
> --
> You received this message because you are subscribed to the Google Groups
> "Racket Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to [email protected].
> For more options, visit https://groups.google.com/d/optout.
--
You received this message because you are subscribed to the Google Groups
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
For more options, visit https://groups.google.com/d/optout.
#lang racket/base
(require
redex/reduction-semantics)
(define-language λvL
(x ::= variable-not-otherwise-mentioned)
(v w ::= (thunk t) () x)
(t u ::= (λ (x) t) (t v) (force v) (return v))
(TT ::= hole (λ (x) TT) (TT v) (t VT) (force VT) (return VT))
(VT ::= (thunk TT))
(C ::= VT TT)
;; How do I tell redex to compatible-close over both v and t?
(anyterm ::= v t)
#:binding-forms
(λ (x) any_1 #:refers-to x))
(define λv-->
(reduction-relation
λvL
(--> ((λ (x) t) v)
(substitute t x v)
"β")
(--> (force (thunk t)) t
"force")))
(define λv-->*
(context-closure λv--> λvL C))
(test-->
λv-->
(term ((λ (x) (force (thunk (return x)))) ()))
(term (force (thunk (return ())))))
(test-->>
λv-->*
(term ((λ (x) (force (thunk (return x)))) ()))
(term (return ())))
(test-->>
λv-->*
(term (λ (x) (force (thunk (return x)))))
(term (λ (x) (return x))))
;; Fails, since thunk is a v, not a t.
(test-->>
λv-->*
(term (thunk (λ (x) (force (thunk (return x))))))
(term (thunk (λ (x) (return x)))))
