On Sun, Jul 8, 2012 at 11:06 AM, David Van Horn <dvanh...@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. ____________________ Racket Users list: http://lists.racket-lang.org/users
