[racket] Does Redex have support for multi-hole evaluation contexts?

 From: David Van Horn (dvanhorn at ccs.neu.edu) Date: Sun Jul 8 15:52:43 EDT 2012 Previous message: [racket] Does Redex have support for multi-hole evaluation contexts? Next message: [racket] Does Redex have support for multi-hole evaluation contexts? Messages sorted by: [date] [thread] [subject] [author]

```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

```

 Posted on the users mailing list. Previous message: [racket] Does Redex have support for multi-hole evaluation contexts? Next message: [racket] Does Redex have support for multi-hole evaluation contexts? Messages sorted by: [date] [thread] [subject] [author]