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

On 7/8/12 11:38 AM, Ryan Newton wrote:
> That actually cuts right to the heart of one of our issues.
>
> In our ideal semantics (e1 e2) can step to (e1' e2), (e1 e2'), or (e1'
> e2'), but of course this creates many possible evaluation orders and
> makes redex take a long long time.
>
> Our quick-and-dirty version is to require synchronous steps (e1' e2'),
> and then separately allow one branch to catch up if the other branch is
> a value:
>     (e v) -> (e' v)
>     (v e) -> (v e')
>
> So that would cover your example.  It's still parallelism, but it's an
> unrealistically constrained evaluation order.

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.

Here's a small redex model that does parallel reduction.  On each step 
it takes the set of redexes and reduces them all.  This is done by 
marking redexes, then eliminating them with beta reduction until there 
are no marks left.  The example shows how multiple redexes are reduced 
in parallel on each step.

Maybe there's some idea you could glean from this, and if there is, I'd 
like to hear about it. :)

David


#lang racket
(require redex/reduction-semantics)

(define-language Λ
   [X variable]
   [E (λ X E) (E E) X]
   [F (% (λ X F) F) (λ X F) (F F) X])

;; Mark all redexes
(define-metafunction Λ
   mark : E -> F
   [(mark X) X]
   [(mark ((λ X E_0) E_1))
    (% (λ X (mark E_0)) (mark E_1))]
   [(mark (E_1 E_2))
    ((mark E_1) (mark E_2))]
   [(mark (λ X E))
    (λ X (mark E))])

;; Reduce all marked redexes
(define-metafunction Λ
   rinse&repeat : F -> E
   [(rinse&repeat E) E]
   [(rinse&repeat X) X]
   [(rinse&repeat (% (λ X F_0) F_1))
    (rinse&repeat (subst X F_1 F_0))]
   [(rinse&repeat (F_1 F_2))
    ((rinse&repeat F_1)
     (rinse&repeat F_2))]
   [(rinse&repeat (λ X F))
    (λ X (rinse&repeat F))])

(define step
   (reduction-relation
    Λ #:domain E
    (--> E_0 (rinse&repeat F)
         (where F (mark E_0)))))

(define-metafunction Λ
   subst : X any any -> any
   ;; 1. x_1 bound, so don't continue in λ body
   [(subst X_1 any_1 (λ X_1 any_2))
    (λ X_1 any_2)]
   ;; 2. general purpose capture avoiding case
   [(subst X_1 any_1 (λ X_2 any_2))
    (λ X_new (subst X_1 any_1 (subst-var X_2 X_new any_2)))
    (where X_new ,(variable-not-in (term (X_1 any_1 any_2))
                                   (term X_2)))]
   ;; 3. replace x_1 with e_1
   [(subst X_1 any_1 X_1) any_1]
   ;; 4. x_1 and x_2 are different, so don't replace
   [(subst X_1 any_1 X_2) X_2]
   ;; the last cases cover all other expressions
   [(subst X_1 any_1 (any_2 ...)) ((subst X_1 any_1 any_2) ...)]
   [(subst X_1 any_1 any_2) any_2])

(define-metafunction Λ
   subst-var : X any any -> any
   [(subst-var X_1 any_1 X_1) any_1]
   [(subst-var X_1 any_1 (any_2 ...))
    ((subst-var X_1 any_1 any_2) ...)]
   [(subst-var X_1 any_1 any_2) any_2])


(require redex)
(traces step (term (((λ S (λ Z (S (S (S Z)))))
                      (λ X X))
                     (λ Y Y))))