[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