<div>Ah, thanks again!  This is for a paper submission (and we&#39;ll post the draft soon) so there isn&#39;t time to change our current model too much at the moment, but I&#39;m very interested in exploring this parameterized-mark proposal after that.</div>

<div><br></div><div>For one thing I hope we&#39;ll then get to dig a bit more into redex performance issues -- i.e. compare this version vs. our define-judgement formulation.  We would like to maxmize the number of paths/sec we can explore.</div>

<div><br></div><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
I think you could similarly parameterize the `mark&#39; 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.</blockquote>

<div><br></div><div>  -Ryan </div><div><br></div><div>P.S. Oops I misspoke before -- not that it&#39;s important but our current model isn&#39;t multistep like Takahashi.  Rather it&#39;s still single step but allows multiple individual reductions to happen simultaneously on disjoint parts of the expression.  That makes it more directly comparable to the proposal by David.</div>

<div><br></div></div>