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
____________________
Racket Users list:
http://lists.racket-lang.org/users
