Simple but buggy PDCFA

toyPDCFA.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 (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
  [(from-many (many vs)) ,(set->list (term vs))]
  [(from-many v) (v)])

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

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

(define-metafunction L
  [(inject e) ({(e #hash()) #hash() mt} #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 -->
#;
    [==> (Σ σ Ξ)
         ,(step-system (term Σ) (term σ) (term Ξ))]
    ;; 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 σ_0 ((fn v_f) k)}) Ξ)
         ({· σ_1 (rt ·)} (push Ξ · k))
         (where (v_p ... ((λf (x) e) ρ_0) v_s ...) (from-many v_f))
         (where (ρ_1 σ_1) (bind ς σ_0 ρ_0 x v))       
         (where · (e ρ_1))]
    ;; Let binding
    [--> ((name ς {v σ_0 ((lt x e ρ_0) k)}) Ξ)
         ({· σ_1 k} Ξ)
         (where (ρ_1 σ_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 (step-system Σ σ Ξ)
  (for/fold ([Σ* (set)]
             [σ* σ]
             [Ξ Ξ])
      ([ς (in-set Σ)])
    ...todo...))

(define count-down
  (term (let ([Yf (lambda (f)
                    ((lambda (g) (f (lambda (x) ((g g) x))))
                     (lambda (g) (f (lambda (x) ((g g) x))))))])
          (let ([pred
                 (lambda (n)
                   (lambda (rf)
                     (lambda (rx)
                       (((n (lambda (g) (lambda (h) (h (g rf)))))
                         (lambda (ignored) rx))
                        (lambda (id) id)))))])
            (let ([church3 (lambda (f3) (lambda (x3) (f3 (f3 (f3 x3)))))])
              (let ([true (lambda (x) (lambda (y) (x (lambda (dummy) dummy))))])
                (let ([false (lambda (x) (lambda (y) (y (lambda (dummy) dummy))))])
                  (let ([church0? (lambda (z) ((z (lambda (zx) false)) true))])
                    (let ([count-down
                           (Yf
                            (λ (count-down)
                              (λ (m)
                                (((church0? m) (λ (dummy) true))
                                 (λ (dummy)
                                   (count-down (pred m)))))))])
                      (count-down church3))))))))))
(redex-match L ({(e ρ) σ k} Ξ) (term (inject ,count-down)))
(traces R (term (inject ,count-down)))
;; This just runs and runs!
;(apply-reduction-relation* R (term (inject ,count-down)))