Translating between lambda and BSCI calculus

bsci.ss

;; Notes on "Learning Programs: A Hierarchical Bayesian Approach"

;; I was confused by the routing terminology and the tree transformation
;; figures in the paper.  In particular I was not exactly sure what were the
;; general rules behind translating (S (B * I) I) to the square function.

;; B, C combinators are known as the "Turner combinators."
;; See http://c2.com/cgi/wiki?EssAndKayCombinators
;; where the translations of lambda calculus to "BSCI" calculus are given:

;; \x.(p q) = (B p \x.q) if x does not occur free in p
;; \x.(p q) = (C \x.p q) if x does not occur free in q
;; \x.(p q) = (S \x.p \x.q) if x occurs free in both p and q

;; This allows us to write simple translators from (a subset of) Scheme code
;; to (a subset of) the combinator language used in the paper.

;; Example:
;; Paper Fig 1 (with currying):
;; `(lambda (x) ( (+ ((* x) x)) 1))
;; Compositional translation to combinator logic:

;; x not present in the right subtree -> C
;; (C [[(lambda (x) (+ ((* x) x)))]] 1)
;; ;; x not present in the left subtree -> B
;; (C (B + [[(lambda (x) ((* x) x))]]) 1)
;; ;; x not free in in either subtree -> S
;; (C (B + (S ([[(lambda (x) (* x))]]1 [[(lambda (x) x)]]2))) 1)
;; ;; reduction 1: x not present in the left subtree -> B
;; (C (B + (S (B * [[(lambda (x) x)]]3) [[(lambda (x) x)]]2)) 1)
;; ;; reduction 3: identity (I)
;; (C (B + (S (B * I) [[(lambda (x) x)]]2)) 1)
;; ;; reduction 2: identity (I)
;; (C (B + (S (B * I) I)) 1)

;; Generally:

(define (tagged-list? e t)
  (and (pair? e) (list? e) 
       (equal? t (car e))))

(define (app? expr) (pair? expr))
(define (lam? expr) (tagged-list? expr 'lambda))
(define (prim? expr) (or (symbol? expr)
                         (number? expr)
                         (string? expr)))

(define (extend v b env) (cons (cons v b) env))
(define (lookup v env) (cdr (assoc v env)))

;; assumes the expression has no variable capture

(define (bound? v expr)
  (cond [(lam? expr) (bound? v (caddr expr))]
        [(app? expr) (or (bound? v (car expr))
                         (bound? v (cadr expr)))]
        [(prim? expr) (equal? v expr)]))

;; The translator

(define (L->BSCI expr route-var)
  (cond [(lam? expr) (let ([next-route-var (car (cadr expr))]) ;;assume one var for now
                       (L->BSCI (caddr expr) next-route-var))]
        [(app? expr) 
         (if 
           route-var
           (let* ([l-bound (bound? route-var (car expr))]
                  [r-bound (bound? route-var (cadr expr))])
             (cond [(and l-bound r-bound)
                    `(S ,(L->BSCI (car expr) route-var) 
                        ,(L->BSCI (cadr expr) route-var))]
                   [l-bound
                     `(C ,(L->BSCI (car expr) route-var)
                         ,(cadr expr))]
                   [r-bound
                     `(B ,(car expr)
                         ,(L->BSCI (cadr expr) route-var))]
                   [else expr]))
           expr)]
        [(prim? expr) (if 
                        (equal? route-var expr) 
                        'I
                        expr)]))

;; Translation back to lambda calculus: basically go backwards?

;; [[(C (B + (S (B * I) I)) 1)]]
;; C-rule
;; (C X Y) => (lambda (x) (([[X]] x) [[Y]]))
;; B-rule
;; (B X Y) => (lambda (x) (([[X]] ([[Y]] x))))
;; S-rule
;; (S X Y) => (lambda (x) (([[X]] x) ([[Y]] x)))
;; I-rule
;; I => (lambda (x) x)

;; Is there any use in introducing the intermediate lambdas?

;; Example
;; (C (B + (S (B * I) I)) 1)
;; 
;; (lambda (x) (
;;              ([[(B + (S (B * I) I))]] x) 
;;              1))
;; 
;; (lambda (x) (
;;              ((lambda (x1)
;;                 (+ ([[(S (B * I) I)]] x1)))
;;               x)
;;              1))
;; 
;; (lambda (x) (
;;              ((lambda (x1)
;;                 (+ 
;;                   (lambda (x2)
;;                     (([[(B * I)]] x2)
;;                      ([[I]] x2)))
;;                   x1))
;;               x)
;;              1))
;; 
;; (lambda (x) (
;;              ((lambda (x1)
;;                 (+ 
;;                   (lambda (x2)
;;                     (((lambda (x3) (* ((lambda (x5) x5) x3))) x2)
;;                      ((lambda (x4) x4) x2)))
;;                   x1))
;;               x)
;;              1))
;;              

(define (B? e) (tagged-list? e 'B))
(define (C? e) (tagged-list? e 'C))
(define (S? e) (tagged-list? e 'S))
(define (I? e) (equal? e 'I))

;; The translator itself

;; Use higher-order abstract syntax to get rid of the intermediate redexes
;; Express distinction between B, C, S as actual dropping of argument in Scheme

(define (BSCI->L expr)
  `(lambda (x)
     ,((BSCI->L* expr) 'x)))

(define (BSCI->L* expr)
  (lambda (v)
    (cond [(or (C? expr) (B? expr) (S? expr))
           ((lambda (x) `(,((BSCI->L* (cadr expr)) x) 
                           ,((BSCI->L* (caddr expr)) x)))
            v)]
          [(I? expr) v]
          [else expr])))

;; Tests

(import (printing))

(pretty-print '(L->BSCI '(lambda (x) ((+ ((* x) x)) 1)) #f))
(pretty-print (L->BSCI '(lambda (x) ((+ ((* x) x)) 1)) #f))
(pretty-print '(BSCI->L '(C (B + (S (B * I) I)) 1)))
(pretty-print (BSCI->L '(C (B + (S (B * I) I)) 1)))