;;; $Id: combinator-tools.scm,v 1.3 2006/01/05 22:24:09 leavens Exp $
;;; The algorithms toCombinators and toLambda are
;; from Hindley, Lercher and Seldin's book
;;; "Introduction to Combinatory Logic", Cambridge, 1972)
(module combinator-tools (lib "typedscm.ss" "typedscm")
(provide toCombinators interpret lambda-calculus-rep toLambda)
(require
;; For the input grammar, , see the following file:
(lib "combinator-lambda-1-exp.scm" "lib342")
;; For the output grammar, , see the following file:
(lib "combinator-term-mod.scm" "lib342"))
;;; Examples:
;;; (unparse-combinator-term
;;; (toCombinators (parse-expression '(lambda (x) (lambda (y) x)))))
;;; ==> k
;;; (unparse-combinator-term
;;; (toCombinators (parse-expression '(lambda (x) (lambda (y) y)))))
;;; ==> (k i)
(deftype toCombinators (-> (expression) combinator-term))
(define toCombinators
(lambda (exp)
(cases expression exp
(var-exp (id) (var id))
(app-exp (rator rand)
(capp (toCombinators rator) (toCombinators rand)))
(lambda-exp (formal body)
(if (not (occurs-free-in? formal body))
(capp (K) (toCombinators body))
(let ((outer-formal formal))
(cases expression body
(var-exp (id) (I)) ; because formal == id here
(lambda-exp (inner-formal inner-body)
(toCombinators
(lambda-exp outer-formal
(toLambda (toCombinators body)))))
(app-exp (rator rand)
(if (and (equal? rand (var-exp outer-formal))
(not (occurs-free-in? outer-formal rator)))
(toCombinators rator) ; eta rule
(capp
(capp (S)
(toCombinators
(lambda-exp outer-formal rator)))
(toCombinators (lambda-exp outer-formal rand)))))
(else (toCombinators body))))))
(LI () (I))
(LS () (S))
(LK () (K))
(else (error "bad expression: " exp)))))
(deftype interpret (-> (combinator-term) combinator-term))
(define interpret
(lambda (trm)
;; ENSURES LIBERALLY: result is the normal form of trm
(displayln (unparse-combinator-term trm) " ==> ")
(cond
((capp-of-I? trm) (interpret (capp->rand trm)))
((capp-of-K? trm) (interpret (capp->rand (capp->rator trm))))
((capp-of-S? trm)
(interpret (capp
(capp (capp->rand (capp->rator (capp->rator trm)))
(capp->rand trm))
(capp (capp->rand (capp->rator trm))
(capp->rand trm)))))
(else trm))))
(deftype capp-of-I? (-> (combinator-term) boolean))
(define capp-of-I?
(lambda (trm)
(and (capp? trm)
(I? (capp->rator trm)))))
(deftype capp-of-K? (-> (combinator-term) boolean))
(define capp-of-K?
(lambda (trm)
(and (capp? trm)
(capp? (capp->rator trm))
(K? (capp->rator (capp->rator trm))))))
(deftype capp-of-S? (-> (combinator-term) boolean))
(define capp-of-S?
(lambda (trm)
(and (capp? trm)
(capp? (capp->rator trm))
(capp? (capp->rator (capp->rator trm)))
(S? (capp->rator (capp->rator (capp->rator trm)))))))
(deftype lambda-calculus-rep (-> () poof))
(define lambda-calculus-rep
(lambda ()
;; EFFECT: read, interpret, and print lambda calculus expressions.
;; You can enter combinator terms directly by using LS, LK, and LI.
;; You can quit by typing in something that doesn't parse, like
;; (quit)
(display "lambda-calculus> ")
(force-output) ; SCM specific
(pretty-print
(unparse-combinator-term
(interpret
(toCombinators
(parse-expression
(read))))))
(newline)
(lambda-calculus-rep)))
;;; The toLambda function is used internally above;
;;; it does not attempt to recover the initial forma of a lambda term,
;;; which would (in general) be impossible anyway.
(deftype toLambda (-> (combinator-term) expression))
(define toLambda
(lambda (ctrm)
(cases combinator-term ctrm
(I () (LI))
(K () (LK))
(S () (LS))
(var (symbol) (var-exp symbol))
(capp (rator rand) (app-exp (toLambda rator) (toLambda rand)))
)))
(deftype occurs-free-in? (-> (symbol expression) boolean))
(define occurs-free-in?
(lambda (sym trm)
;; ENSURES: result is true just when sym occurs free in trm
(cases expression trm
(var-exp (id) (eq? sym id))
(lambda-exp (formal body)
(and (not (eq? sym formal)) (occurs-free-in? sym body)))
(app-exp (rator rand)
(or (occurs-free-in? sym rator)
(occurs-free-in? sym rand)))
(else #f))))
) ;; end module