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

On Sun, Jul 8, 2012 at 11:06 AM, David Van Horn <dvanhorn at ccs.neu.edu> wrote:
> I doubt that this helps, but just in case... another notion of parallel
> reduction is the one used in simple proofs of Church-Rosser, e.g.
>
>    Masako Takahashi "Parallel Reductions in λ-Calculus", Information
>    and Computation 118(1), 1995.
>
> (A lovely paper that is not so easy to find in PDF.)
>
> In this approach you can define a notion of a step E => E' which does
> beta-reduction on any subset of the redexes in E in parallel.  The =>
> relation is nice because it enjoys the diamond property, unlike one-step
> reduction.

Hi David,

I'm very glad you brought this up, because I've been wondering how to
deal with expressing reflexive rules in Redex!

The relation in Takahashi is reminiscent of the one defined on p. 55
of the Redex book.  In particular, both of them have a reflexive rule,
M --> M, and a parallel application rule, M N --> M' N'.  The
semantics that we want to express in Redex has both of those features.

The trouble I've been having is that the reflexive rules don't seem to
play nicely with the test infrastructure in Redex.  In particular,
`test-->>` finds all irreducible terms reachable from a given term,
but with reflexive reduction rules, there are no terms that are
irreducible.  Using `test-->>E` might work, but since the property we
are most interested in testing for is determinism, we would really
like to be able to know not only that there exists a path from one
term to another, but that *all* possible reductions take us from the
first term to the second.

We ended up leaving the reflexive rules out of our Redex model, and
instead adding application rules M N --> M N' and M N --> M' N in
addition to the parallel application rule.  But if there's a standard
way of accounting for reflexive rules in Redex, I'm curious what it
is!

Best,
Lindsey

P.S. Ryan, I had been assuming that "one-step" meant "small-step", but
now I think that by "one-step" David means a relation that doesn't
reduce redexes in parallel.  So, in fact, ours *is* multi-step because
it *does* reduce in parallel.