PasteRack.org
Paste # 44574
2016-09-06 13:36:32

Fork as a new paste.

Paste viewed 129 times.


Embed:

redex ambiguous reduction

  1. #lang racket
  2. (require redex)
  3.  
  4. (define-language simple
  5.   (σ (begin σ ...)
  6.      (define v e))
  7.   (e v
  8.      number
  9.      (+ e e))
  10.   (v variable-not-otherwise-mentioned))
  11.  
  12. (define-extended-language simple+lifted simple
  13.   (e ....
  14.      (lifted v e)))
  15.  
  16. (define-extended-language simple+lifted+hole+temp simple+lifted
  17.   (e ....
  18.      (lift-temp (v e) e))
  19.   (C hole
  20.      (begin σ ... C σ ...)
  21.      (define v C)
  22.      (+ C e)
  23.      (+ e C)))
  24.  
  25. (define simple+lifted→simple
  26.   (reduction-relation
  27.    simple+lifted+hole+temp
  28.    (--> (in-hole C (lifted v e))
  29.         (in-hole C (lift-temp (v e) v))
  30.         create-bubble)
  31.    (--> (in-hole C (+ (lift-temp (v e_lifted) e_a) e_b))
  32.         (in-hole C (lift-temp (v e_lifted) (+ e_a e_b)))
  33.         bubble-up-1)
  34.    (--> (in-hole C (+ e_a (lift-temp (v e_lifted) e_b)))
  35.         (in-hole C (lift-temp (v e_lifted) (+ e_a e_b)))
  36.         bubble-up-2)
  37.    (--> (in-hole C (define v (lift-temp (v_lifted e_lifted) e)))
  38.         (in-hole C (begin (define v_lifted e_lifted)
  39.                           (define v e)))
  40.         inject-lifted)
  41.    (--> (in-hole C (begin σ_a ... (begin σ_b ...) σ_c ...))
  42.         (in-hole C (begin σ_a ... σ_b ... σ_c ...))
  43.         splice-begin)))
  44.  
  45. (apply-reduction-relation* simple+lifted→simple
  46.                            (term (define result (+ (lifted x 1)
  47.                                                    (lifted y 2)))))
  48. ;; => '((begin (define x 1) (define y 2) (define result (+ x y)))
  49. ;;      (begin (define y 2) (define x 1) (define result (+ x y))))

=>