Render classical 0CFA as reduction relation

0cfa-reduction.rkt

#lang racket
;; This program attempts to render the results
;; of classical 0CFA as a reduction relation.

;; 0CFA is the refl, trans closure of:

;; e0 ~> \x.e    e1 ~> v
;; ---------------------
;; (e0 e1) ~> e, x ~> e1

(struct ~> (name lhs rhs) #:transparent)

(define (trans-step e edges)
  (match e
    [(~> _ e0 e1)
     (for/set ([e (in-set edges)]
               #:when (equal? (~>-lhs e) e1))
       (~> 'trans e0 (~>-rhs e)))]))

(trans-step (~> '_ 1 2) (set (~> '_ 2 3)
                             (~> '_ 2 7)))

(define (val? e)
  (match e
    [(list 'λ x e) #t]
    [_ #f]))

(define (app-step e edges)
  (match e
    [(~> _ (list e0 e1) _)
     (define funs
       (for/set ([e (in-set edges)]
                 #:when (and (equal? (~>-lhs e) e0)
                             (val? (~>-rhs e))))
         (~>-rhs e)))
     (define args 
       (for/set ([e (in-set edges)]
                 #:when (and (equal? (~>-lhs e) e1)
                             (val? (~>-rhs e))))
         (~>-rhs e)))
     
     (for*/fold ([s (set)])
       ([f (in-set funs)]
        [a (in-set args)])
       (match f
         [(list 'λ x e2)          
          (set-union (set (~> 'app (~>-lhs e) e2)
                          (~> 'app x a))
                     s)]))]
    [_ (set)]))

(app-step (~> 'trans '(f x) '(f x))
          (set (~> '_ 'f '(λ y y))
               (~> '_ 'x '(λ z z))
               (~> '_ 'x '(λ q q))))


(define (refl-close e)
  (match e
     [(list 'λ x e0) 
      (set-add (refl-close e0) (~> 'refl e e))]
     [(list e0 e1) 
      (set-add (set-union (refl-close e0) 
                          (refl-close e1))
               (~> 'refl e e))]
     [x 
      (set (~> 'refl x x))]))

(refl-close '(λ x (λ z (x z))))
   
(define (step s)
  (for/fold ([a (set)])
    ([e (in-set s)])
    (set-union a
               (trans-step e s)
               (app-step e s))))

(define (analyze e)
  (let loop ([s (refl-close e)])
    (define s1 (set-union s (step s)))
    (if (equal? s s1) 
        s
        (loop s1))))
                 
(require redex)

(define-language L
  (M ::= X (M M) (λ X M))
  (X ::= variable-not-otherwise-mentioned)
  (E ::= hole (E M) (M E)))

(define (app? e)
  (match e
    [(~> 'app _ _) #t]
    [_ #f]))
(define (refl? e)
  (match e
    [(~> _ e e) #t]
    [(~> 'refl _ _) #t]
    [_ #f]))


(define (0cfa p)
  (define a (for/list ([e (in-set (analyze p))]
                      #:when (app? e))
              (match e
                [(~> _ e0 e1)
                 (list '~> e0 e1)])))
  
  (reduction-relation 
   L
   (--> M_0 M_1
        (where (_ ... (~> M_0 M_1) _ ...)
               ,a))))

(define (run p)
  (traces (0cfa p) p))

;; Example from NNH
(run '((λ f ((f f) (λ x x))) (λ y y)))

#;
;; Example from PDCFA paper
(run '((λ id ((λ a ((λ b a) (id (λ four four)))) 
                (id (λ three three))))
         (λ x x)))