[racket] Does Redex have support for multi-hole evaluation contexts?
On 7/8/12 3:12 PM, Ryan Newton wrote:
> Thanks for the example!
>
> Masako Takahashi "Parallel Reductions in λ-Calculus", Information
> and Computation 118(1), 1995.
>
> (A lovely paper that is not so easy to find in PDF.)
>
>
> Ah, good to see you cite that paper. We've been using it as one of our
> references, and did manage to find a PDF for it somewhere. We indeed
> are using a similar multistep relation.
>
> This marking trick is a neat thing to add to the redex toolbelt, and it
> looks like we could adapt it to CBV just by tweaking the mark function.
Yes, here's my interpretation of what CBV means in this setting:
(define-language Λ
[X variable]
[V (λ X E)]
[P E] ; side-condition: closed
[E (λ X E) (E E) X]
[F (% (λ X E) F) (λ X E) (F F)])
;; Mark all redexes
(define-metafunction Λ
mark : P -> F
[(mark ((λ X E) V))
(% (λ X E) V)]
[(mark (E_1 E_2))
((mark E_1) (mark E_2))]
[(mark E) E])
;; Reduce all marked redexes
(define-metafunction Λ
rinse&repeat : F -> P
[(rinse&repeat E) E]
[(rinse&repeat (% (λ X E) V))
(rinse&repeat (subst X V E))]
[(rinse&repeat (F_1 F_2))
((rinse&repeat F_1)
(rinse&repeat F_2))])
(define step
(reduction-relation
Λ #:domain E
(--> E (rinse&repeat (mark E)))))
My original example doesn't demonstrate any parallelism in this
language, but this one does:
(traces step (term (((λ X X) (λ Y Y))
((λ P P) (λ Q Q)))))
> However, it evaluates the maximum number of possible redexes in each
> step, which is fine if you already know you've got Church-Rosser. But
> there's a bit of a circularity here and what we really want is a redex
> model that we can use in two different modes for two different purposes:
>
> * Full mode - explore all (or many) thread interleavings, to help us
> convince ourselves that CR does hold for our language. FYI our
> language is parallel CBV with no reduction under lambdas and it does
> have limited effects.
> * Quick mode - explore many fewer (or one) thread interleaving just to
> get to the answer quickly.
>
> What Lindsey's done currently is to come up with a semantics using
> *define-judgment-form* for which we can swap out a couple rules to
> switch between these two modes -- well, at least between
> all-interleavings and our specific lockstep-interleaving (it would be
> nice to explore random orders, as suggested in Robby's message).
I think you could similarly parameterize the `mark' by an oracle that
tells you which redexes to select. Quick = all, full = any. You could
randomly test the CR property with a random oracle selecting two sets
then doing all subsequent reductions looking for a match.
David