The original claim was that a state is reachable in PDCFA iff it is reachable in 0CFA, but that is not true. Ian came up with a counterexample: ``` (let* ((id (lambda (x) ((lambda (q) q) x))) (y (id 0)) (z (id 1))) y) ``` In PDCFA the answer is just {0}, but 0CFA is {0,1}. I verified this in the boiled down models below.

pdcfa-v-0cfa.rkt

#lang racket
(struct vbl (x)       #:transparent)
(struct lam (x e)     #:transparent)
(struct app (e0 e1 l) #:transparent)

(struct mt ()    #:transparent)
(struct ap (e k) #:transparent)
(struct fn (v k) #:transparent)

(define (lookup σ x)
  (hash-ref σ x))

(define (extend σ x v)
  (hash-set σ x
            (set-union (set v)
                       (hash-ref σ x (set)))))

; State -> [Set State]
(define (fs-step ς)
  (match ς
    [(list (vbl x) σ κ)
     (for/set [(v (in-set (lookup σ x)))]
       (list v σ κ))]
    [(list (app e0 e1 l) σ κ)
     (set (list e0 (extend σ l κ) (ap e1 l)))]

    [(list v σ (ap e l))
     (set (list e σ (fn v l)))]

    [(list v σ (fn (lam x e) l))
     (for/set [(κ (in-set (lookup σ l)))]
       (list e (extend σ x v) κ))]

    [_ (set)]))

; State -> [Set State]
(define (pd-step ς)
  (match ς
    [(list (vbl x) σ κ)
     (for/set [(v (in-set (lookup σ x)))]
       (list v σ κ))]

    [(list (app e0 e1 l) σ κ)
     (set (list e0 σ (ap e1 κ)))]

    [(list v σ (ap e κ))
     (set (list e σ (fn v κ)))]

    [(list v σ (fn (lam x e) κ))
     (set (list e (extend σ x v) κ))]

    [_ (set)]))

(define (fix r)
  (λ (ς)
    (let loop ((R (set ς)) (P (set)))
      (if (equal? R P)
          R
          (loop (step r R) R)))))

(define (step r R)
  (apply set-union
         R
         (for/list ([ς (in-set R)])
           (r ς))))

(define (pd-eval e)
  ((fix pd-step) (list e (hash) (mt))))

(define (fs-eval e)
  ((fix fs-step) (list e (hash) (mt))))

(define (final? ς)
  (match ς
    [(list (lam x e) σ (mt)) #t]
    [_ #f]))

(define (final ςs)
  (for/set ([ς (in-set ςs)]
            #:when (final? ς))
    (match ς
      [(list e σ k) e])))

(define (mlet l x e0 e1)
  (app (lam x e1) e0 l))

(define ianj
  (mlet 1 'id (lam 'x (app (lam 'q (vbl 'q)) (vbl 'x) 2))
        (mlet 3 'y (app (vbl 'id) (lam 'zero (vbl 'zero)) 4)
              (mlet 5 'z (app (vbl 'id) (lam 'one (vbl 'one)) 6)
                    (vbl 'y)))))

(final (pd-eval ianj))
(final (fs-eval ianj))