<div class="gmail_quote"><div>Thanks for the example!</div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div> Masako Takahashi "Parallel Reductions in ë-Calculus", Information</div>
and Computation 118(1), 1995. </blockquote><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
(A lovely paper that is not so easy to find in PDF.)<br></blockquote><div><br></div><div>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.</div>
<div><br></div><div>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. 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:</div>
<div><ul><li>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.</li>
<li>Quick mode - explore many fewer (or one) thread interleaving just to get to the answer quickly.</li></ul><div>What Lindsey's done currently is to come up with a semantics using <span style="color:rgb(34,34,34);font-size:13px;font-family:arial,sans-serif"><b>define-judgment-form</b> 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).</span></div>
</div><div><span style="color:rgb(34,34,34);font-size:13px;font-family:arial,sans-serif"><br></span></div><div><span style="color:rgb(34,34,34);font-size:13px;font-family:arial,sans-serif">Cheers,</span></div>
<div><span style="color:rgb(34,34,34);font-size:13px;font-family:arial,sans-serif"> -Ryan</span></div><div><br></div><div><br></div></div>