Formalization of the perturbative λ-calculus in Redex

lam-T.ss

#lang racket
(require redex)

(define-language λT
  ;; Terms
  (e x
     (λ (x) e)
     (e e)
     0
     (+ e ...)
     (T e)
     (pi-1 e)
     (pi-2 e)
     (iota-1 e)
     (iota-2 e))
  ;; Contexts
  (E (λ (x) E)
     (E e)
     (e E)
     (+ e ... E e ...)
     (T E)
     (pi-1 E)
     (pi-2 E)
     (iota-1 E)
     (iota-2 E)
     hole)
  ;; Variables
  (x variable-not-otherwise-mentioned))

(define reduction
  (reduction-relation
   λT

   (--> (in-hole E (+))
        (in-hole E 0)
        "empty +")
   (--> (in-hole E (+ e))
        (in-hole E e)
        "unary +")
   (--> (in-hole E (+ e_1 ... (+ e_2 ...) e_3 ...))
        (in-hole E (+ e_1 ... e_2 ... e_3 ...))
        "flatten")
   (--> (in-hole E (+ e_1 ... 0 e_2 ...))
        (in-hole E (+ e_1 ... e_2 ...))
        "drop 0")

   (--> (in-hole E (λ (x) 0))
        (in-hole E 0)
        "λ0")
   (--> (in-hole E (λ (x) (+ e ...)))
        (in-hole E (+ (λ (x) e) ...))
        "λ+")
   (--> (in-hole E (0 e))
        (in-hole E 0)
        "0@")
   (--> (in-hole E ((+ e_1 ...) e_2))
        (in-hole E (+ (e_1 e_2) ...))
        "+@")
   (--> (in-hole E (T 0))
        (in-hole E 0)
        "T0")
   (--> (in-hole E (T (+ e ...)))
        (in-hole E (+ (T e) ...))
        "T+")
   (--> (in-hole E (pi-1 0))
        (in-hole E 0)
        "pi-1 0")
   (--> (in-hole E (pi-1 (+ e ...)))
        (in-hole E (+ (pi-1 e) ...))
        "pi-1 +")
   (--> (in-hole E (pi-2 0))
        (in-hole E 0)
        "pi-2 0")
   (--> (in-hole E (pi-2 (+ e ...)))
        (in-hole E (+ (pi-2 e) ...))
        "pi-2 +")
   (--> (in-hole E (iota-1 0))
        (in-hole E 0)
        "iota-1 0")
   (--> (in-hole E (iota-1 (+ e ...)))
        (in-hole E (+ (iota-1 e) ...))
        "iota-1 +")
   (--> (in-hole E (iota-2 0))
        (in-hole E 0)
        "iota-2 0")
   (--> (in-hole E (iota-2 (+ e ...)))
        (in-hole E (+ (iota-2 e) ...))
        "iota-2 +")

   (--> (in-hole E (pi-1 (iota-1 e)))
        (in-hole E e)
        "pi-1 iota-1")
   (--> (in-hole E (pi-2 (iota-2 e)))
        (in-hole E e)
        "pi-2 iota-2")
   (--> (in-hole E (pi-1 (iota-2 e)))
        (in-hole E 0)
        "pi-1 iota-2")
   (--> (in-hole E (pi-2 (iota-1 e)))
        (in-hole E 0)
        "pi-2 iota-1")

   (--> (in-hole E ((λ (x) e_1) e_2))
        (in-hole E (substitute x e_2 e_1))
        "beta")

   (--> (in-hole E (T (λ (x) e)))
        (in-hole E (λ (x) (push-forward x e)))
        "T")))

;; Capture-avoiding substitution of a term for free occurrences
;; of a variable in another term.
(define-metafunction λT
  substitute : x e e -> e
  ((substitute x e_1 (λ (x) e_2))
   (λ (x) e_2))
  ((substitute x e_1 (λ (x_bound) e_2))
   (λ (x_fresh)
     (substitute x e_1
                 (rename-variable x_bound x_fresh e_2)))
   (where x_fresh
          ,(variable-not-in
            (term (+ x x_bound e_1 e_2))
            (term x_bound))))
  ((substitute x e_1 x) e_1)
  ((substitute x e_1 x_other) x_other)
  ((substitute x e_1 (e_2 e_3))
   ((substitute x e_1 e_2)
    (substitute x e_1 e_3)))
  ((substitute x e_1 0) 0)
  ((substitute x e_1 (+ e_2 ...))
   (+ (substitute x e_1 e_2) ...))
  ((substitute x e_1 (T e_2))
   (T (substitute x e_1 e_2)))
  ((substitute x e_1 (pi-1 e_2))
   (pi-1 (substitute x e_1 e_2)))
  ((substitute x e_1 (pi-2 e_2))
   (pi-2 (substitute x e_1 e_2)))
  ((substitute x e_1 (iota-1 e_2))
   (iota-1 (substitute x e_1 e_2)))
  ((substitute x e_1 (iota-2 e_2))
   (iota-2 (substitute x e_1 e_2))))

;; Rename every occurrence (whether free, bound, or binding)
;; of x_old in a given expression as x_new.
(define-metafunction λT
  rename-variable : x x e -> e
  ((rename-variable x_old x_new x_old) x_new)
  ((rename-variable x_old x_new x) x)
  ((rename-variable x_old x_new (λ (x_old) e))
   (λ (x_new) (rename-variable x_old x_new e)))
  ((rename-variable x_old x_new (λ (x) e))
   (λ (x) (rename-variable x_old x_new e)))
  ((rename-variable x_old x_new (e_1 e_2))
   ((rename-variable x_old x_new e_1)
    (rename-variable x_old x_new e_2)))
  ((rename-variable x_old x_new 0) 0)
  ((rename-variable x_old x_new (+ e ...))
   (+ (rename-variable x_old x_new e) ...))
  ((rename-variable x_old x_new (T e))
   (T (rename-variable x_old x_new e)))
  ((rename-variable x_old x_new (pi-1 e))
   (pi-1 (rename-variable x_old x_new e)))
  ((rename-variable x_old x_new (pi-2 e))
   (pi-2 (rename-variable x_old x_new e)))
  ((rename-variable x_old x_new (iota-1 e))
   (iota-1 (rename-variable x_old x_new e)))
  ((rename-variable x_old x_new (iota-2 e))
   (iota-2 (rename-variable x_old x_new e))))

(define-metafunction λT
  bundle : e e -> e
  ((bundle e_1 e_2)
   (+ (iota-1 e_1)
      (iota-2 e_2))))

(define-metafunction λT
  <> : e e -> e
  ((<> e_1 e_2)
   (bundle (+ ((pi-1 e_1) (pi-2 e_2))
              (pi-1 ((T (pi-2 e_1)) e_2)))
           ((pi-2 e_1) (pi-2 e_2)))))

(define-metafunction λT
  push-forward-linear : any e -> e
  ((push-forward-linear any e)
   (bundle (any (pi-1 e))
           (any (pi-2 e)))))

(define-metafunction λT
  push-forward : x e -> e
  ((push-forward x x) x)
  ((push-forward x x_other)
   (iota-2 x_other))
  ((push-forward x (λ (x_bound) e))
   (bundle
    (λ (x_fresh) (pi-1 e_transformed))
    (λ (x_fresh) (pi-2 e_transformed)))
   (where x_fresh
          ,(variable-not-in
            (term x)
            (term x_bound)))
   (where e_transformed
          (push-forward x (rename-variable x_bound x_fresh e))))
  ((push-forward x (e_1 e_2))
   (<> (push-forward x e_1)
       (push-forward x e_2)))
  ((push-forward x 0) 0)
  ((push-forward x (+ e ...))
   (+ (push-forward x e) ...))
  ;; WARNING This is a catch-all case that deals with T, pi-n, and
  ;; iota-n, and it should appear last.
  ((push-forward x (any e))
   (push-forward-linear any (push-forward x e))))

;; Reduce redexes randomly until no redexes left.  Print the obtained
;; expression and the number of steps taken.
(define (reduce-randomly relation expression)
  (let loop ((reduction expression)
             (path-length 0))
    (let* ((reduction-list
            (apply-reduction-relation
             relation
             reduction))
           (num-reductions
            (length reduction-list))
           (next-reduction
            (if (zero? num-reductions)
                reduction
                (list-ref reduction-list
                          (random num-reductions)))))
      (if (equal? reduction next-reduction)
          (begin
            (pretty-print reduction)
            (printf "~a steps\n" path-length))
          (loop next-reduction (+ path-length 1))))))

;; Reduce redexes until no redexes left choosing at each step a redex
;; whose reduction leads to the smallest possible term.  If verbose?
;; is #t, print intermediate expressions and names of the reductions.
;; Print the obtained expression and the number of steps taken.
(define (reduce-smallest relation expression [verbose? #f])
  (let loop ((reduction expression)
             (path-length 0))
    (let* ((reduction-list
            (apply-reduction-relation/tag-with-names
             relation
             reduction))
           (num-reductions
            (length reduction-list))
           (next-reduction
            (if (zero? num-reductions)
                reduction
                (minimum-by size reduction-list))))
      (if (equal? reduction next-reduction)
          (begin
            (pretty-print reduction)
            (printf "~a steps\n" path-length))
          (begin
            (when verbose? (pretty-print next-reduction))
            (loop (cadr next-reduction) (+ path-length 1)))))))

;; Return the leftmost element of a list with a smallest value of key
;; function.
(define (minimum-by key lst)
  (let loop ((lst (cdr lst))
             (curr-val (car lst))
             (curr-key (key (car lst))))
    (if (null? lst)
        curr-val
        (let* ((next-val (car lst))
               (next-key (key next-val)))
          (if (< next-key curr-key)
              (loop (cdr lst) next-val next-key)
              (loop (cdr lst) curr-val curr-key))))))

(define (size thing)
  (cond ((pair? thing)
         (+ (size (car thing))
            (size (cdr thing))))
        ((null? thing) 0)
        (else 1)))

(define non-confluence-example
  (term
   (T (λ (x) ((λ (y) ((f x) y)) x)))))

(define non-confluence-example-beta
  (cadr
   (assoc "beta"
          (apply-reduction-relation/tag-with-names
           reduction
           non-confluence-example))))

(define non-confluence-example-T
  (cadr
   (assoc "T"
          (apply-reduction-relation/tag-with-names
           reduction
           non-confluence-example))))

#|
The following session shows that the reduction relation defined here
is non-confluent.

  > (reduce-smallest reduction non-confluence-example-T)
  (+
   (λ (x) (iota-1 ((pi-1 ((T f) x)) (pi-2 x))))
   (λ (x) (iota-1 (pi-1 ((T (f (pi-2 x))) (iota-2 (pi-2 x))))))
   (λ (x) (iota-2 ((f (pi-2 x)) (pi-2 x))))
   (λ (x) (iota-1 ((pi-1 ((T f) (iota-2 (pi-2 x)))) (pi-2 x))))
   (λ (x) (iota-1 (pi-1 ((T (f (pi-2 x))) x)))))
  314 steps

  > (reduce-smallest reduction non-confluence-example-beta)
  (+
   (λ (x) (iota-1 ((pi-1 ((T f) x)) (pi-2 x))))
   (λ (x) (iota-1 (pi-1 ((T (f (pi-2 x))) x))))
   (λ (x) (iota-2 ((f (pi-2 x)) (pi-2 x)))))
  37 steps

The terms of the form

(pi-1 ((T g) (iota-2 (pi-2 x))))

are semantically zero but don't reduce.
|#