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 racket-users+unsubscr...@googlegroups.com.
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))
;; 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")))
; This ought to reduce under vs, as well ts, since they are mutually defined.
; But it only uses t.
(define λv-->*
(compatible-closure λv--> λvL t))
; Doesn't work, but in a different way.
#;(define λv-->*
(compatible-closure λv--> λvL anyterm))
(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)))))
