Widened version of buggy PDCFA

toy-wide.rkt

#lang racket
(require redex)

(define-language L
  [e x (e e) lam (let ([x e]) e)]
  [lam (λf (x) e)]
  [λf λ lambda]
  [x variable-not-otherwise-mentioned]
  ;; Machine
  [ρ (side-condition (name ρ any) (hash? (term ρ)))]
  [σ (side-condition (name σ any) (hash? (term σ)))]  
  [δ ((a vs) ...)]
  [a (x any)] ;; addresses
  [v (lam ρ) (many vs)]
  [vs (side-condition (name vs any) (set? (term vs)))]
  [· (e ρ)] ;; a point is a closed expression
  ;; continuations are lists of frames terminated by mt or a return
  [ϕ (ar ·) (lt x e ρ) (fn v)]
  [k (rt ·) mt (ϕ k)]
  ;; returns are threaded through a table
  [Ξ (side-condition (name Ξ any) (hash? (term Ξ)))]
  [ς (· k) (v k)]
  [Σ (side-condition (name Σ any) (set? (term Σ)))]
  [S (Σ σ Ξ)])

(define-metafunction L
  [(alloc x ς) (x ())]) ;; 0CFA for now.

(define-metafunction L
  [(lookup σ ρ x) ,(hash-ref (term σ) (hash-ref (term ρ) (term x)))])
(define-metafunction L
  [(extend ρ x a) ,(hash-set (term ρ) (term x) (term a))])
(define-metafunction L
  [(σextend σ a (many vs))
   ,(hash-set (term σ) (term a)
              (set-union (hash-ref (term σ) (term a) (set)) (term vs)))]
  [(σextend σ a v)
   ,(hash-set (term σ) (term a)
              (set-add (hash-ref (term σ) (term a) (set)) (term v)))])

(define-metafunction L
  [(unmany (many vs)) vs]
  [(unmany v) ,(set (term v))])
(define-metafunction L
  [(from-many v) ,(set->list (term (unmany v)))])

(define-metafunction L
  [(bind ς σ ρ x v)
   (ρ_1 ((a (unmany v))))
   (where a (alloc x ς))
   (where ρ_1 (extend ρ x a))])

(define-metafunction L
  [(push Ξ · k) ((· ,(set (term k))))])
(define-metafunction L
  [(pop Ξ ·)
   ,(set->list (hash-ref (term Ξ) (term ·)))])

(define-metafunction L
  [(injectW e) (,(set (term ((e #hash()) mt))) #hash() #hash())])

(define (join σ₀ σ₁)
  (for/fold ([σ σ₀]) ([(a vs) (in-hash σ₁)])
    (hash-set σ a (set-union (hash-ref σ a (set)) vs))))

(define R
  (reduction-relation L
    #:arrow -->
    ;; Variable reference
    [--> ({(x ρ) k} σ Ξ)
         ({(many (lookup σ ρ x)) k} () ())]
    ;; Evaluate application
    [--> ({((e_0 e_1) ρ) k} σ Ξ)
         ({(e_0 ρ) ((ar (e_1 ρ)) k)} () ())]
    ;; Evaluate let binding
    [--> ({((let ([x e_0]) e_1) ρ) k} σ Ξ)
         ({(e_0 ρ) ((lt x e_1 ρ) k)} () ())]
    ;; Function done. Evaluate argument
    [--> ({v ((ar ·) k)} σ Ξ)
         ({· ((fn v) k)} () ())]
    ;; Function call
    [--> ((name ς {v ((fn v_f) k)}) σ_0 Ξ)
         ({· (rt ·)} δ (push Ξ · k))
         (where (v_p ... ((λf (x) e) ρ_0) v_s ...) (from-many v_f))
         (where (ρ_1 δ) (bind ς σ_0 ρ_0 x v))       
         (where · (e ρ_1))]
    ;; Let binding
    [--> ((name ς {v ((lt x e ρ_0) k)}) σ_0 Ξ)
         ({· k} δ ())
         (where (ρ_1 δ) (bind ς σ_0 ρ_0 x v))
         (where · (e ρ_1))]
    ;; "Return"
    [--> ({v (rt ·)} σ Ξ)
         ({v k} () ())
         (where (k_0 ... k k_1 ...) (pop Ξ ·))]
    ;; Answers self-reduce.
    [--> ({v mt} σ Ξ) ({v_0 mt} () ())
         (where (v_p ... v_0 v_s ...) (from-many v))]))

(define W
  (reduction-relation L
    [--> (Σ σ Ξ)
         ,(step-system (term Σ) (term σ) (term Ξ))]))

(define (applyΔ h δ)
  (for/fold ([h h]) ([pair (in-list δ)])
    (match pair
      [`(,k ,v) (hash-set h k (set-union (hash-ref h k (set)) v))])))

(define (step-system Σ σ Ξ)
  (define-values (Σ* δ δΞ)
    (for/fold ([Σ* Σ]
               [δ '()]
               [δΞ '()])
        ([ς (in-set Σ)])
      (for/fold ([Σ* Σ*] [δ δ] [δΞ δΞ])
          ([ςσΞ (in-list (apply-reduction-relation R (term (,ς ,σ ,Ξ))))])
        (match ςσΞ
          [`(,ς ,δ* ,δΞ*)
           (values (set-add Σ* ς) (append δ* δ) (append δΞ* δΞ))]))))
  (define σ* (applyΔ σ δ))
  (define Ξ* (applyΔ Ξ δΞ))
  (if (and (equal? Σ Σ*)
           (equal? σ σ*)
           (equal? Ξ Ξ*))
      (term (,(for/set ([ς (in-set Σ)]
                        #:when (redex-match L (v mt) ς))
                (first ς))
             ,σ))
      (term (,Σ* ,σ* ,Ξ*))))

(define count-down
  (term (let ([Yf (lambda (f)
                    ((lambda (g0) (f (lambda (x0) ((g0 g0) x0))))
                     (lambda (g1) (f (lambda (x1) ((g1 g1) x1))))))])
          (let ([pred
                 (lambda (n)
                   (lambda (rf)
                     (lambda (rx)
                       (((n (lambda (g2) (lambda (h) (h (g2 rf)))))
                         (lambda (ignored) rx))
                        (lambda (id) id)))))])
            (let ([church3 (lambda (f3) (lambda (x3) (f3 (f3 (f3 x3)))))])
              (let ([true (lambda (xt) (lambda (yt) (xt (lambda (dummy0) dummy0))))])
                (let ([false (lambda (xf) (lambda (yf) (yf (lambda (dummy1) dummy1))))])
                 (let ([church0? (lambda (z) ((z (lambda (zx) false)) true))])
                    (let ([count-down
                           (Yf
                            (λ (count-down)
                              (λ (m)
                                (((church0? m) (λ (dummy2) true))
                                 (λ (dummy3)
                                   (count-down (pred m)))))))])
                      (count-down church3))))))))))
#;(traces W (term (injectW ,count-down))
        #:format first)

(apply-reduction-relation* W (term (injectW ,count-down)))