import of pattern-specializer examples

[specializable.git] / examples / lambda-calculus.lisp

diff --git a/examples/lambda-calculus.lisp b/examples/lambda-calculus.lisp
new file mode 100644 (file)
index 0000000..2073db0
--- /dev/null
+++ b/examples/lambda-calculus.lisp
@@ -0,0 +1,134 @@
+;;;; lambda-calculus.lisp --- Untyped lambda calculus based on pattern specializers.
+;;;;
+;;;; Copyright (C) 2014 Jan Moringen
+;;;;
+;;;; Author: Jan Moringen <jmoringe@techfak.uni-bielefeld.DE>
+
+;;;; Partially based on idea from
+;;;;
+;;;; [1] Benjamin C. Pierce (2002): Types and Programming languages
+
+(cl:defpackage #:pattern-specializer.examples.lambda-calculus
+  (:use
+   #:cl
+   #:pattern-specializer)
+
+  (:shadow
+   #:abs)
+
+  (:import-from #:optima
+   #:guard))
+
+(cl:in-package #:pattern-specializer.examples.lambda-calculus)
+
+;;; Syntax
+;;;
+;;;        ,- app   ,- const
+;;;       /        /
+;;; term ---- val ---- abs
+;;;       \
+;;;        `- var
+
+(defstruct term) ; abstract
+
+(defstruct (val (:include term))) ; abstract
+
+(defstruct (const (:include val) (:constructor make-const (value)))
+  (value nil))  ; TODO val?
+
+(defstruct (var (:include term) (:constructor make-var (name)))
+  (name nil :type symbol))
+
+(defstruct (abs (:include val) (:constructor make-abs (var body)))
+  (var nil :type var)
+  (body nil :type term))
+
+(defstruct (app (:include term) (:constructor make-app (fun arg)))
+  (fun nil :type term)
+  (arg nil :type val))
+
+;;; Parse
+
+(defgeneric parse (form)
+  (:generic-function-class pattern-generic-function))
+
+(defmethod parse ((form integer))
+  (make-const form))
+
+(defmethod parse ((form symbol))
+  (make-var form))
+
+(defmethod parse ((form (pattern (list 'λ (guard name (symbolp name)) body))))
+  (make-abs (parse name) (parse body)))
+
+(defmethod parse ((form (pattern (list func arg))))
+  (make-app (parse func) (parse arg)))
+
+;;; Substitution
+
+(defgeneric substitute1 (term var val))
+
+(defmethod substitute1 ((term val) (var var) (val val))
+  term)
+
+;; [1 Page 69]
+(defmethod substitute1 ((term var) (var var) (val val))
+  (if (equalp term var) val term))
+
+;; [1 Page 69]
+(defmethod substitute1 ((term abs) (var var) (val val))
+  ;; TODO capture
+  (make-abs (abs-var term) (substitute1 (abs-body term) var val)))
+
+;; [1 Page 69]
+(defmethod substitute1 ((term app) (var var) (val val))
+  (make-app (substitute1 (app-fun term) var val)
+            (substitute1 (app-arg term) var val)))
+
+;;; Evaluation
+
+(defgeneric eval1 (term)
+  (:generic-function-class pattern-generic-function))
+
+(defmethod eval1 ((term val))
+  term)
+
+;; Reduce function to value
+;;
+;;      t_1 -> t_1'
+;; ---------------------
+;;  t_1 t_2 -> t_1' t_2
+;;
+;; [1 Page 72; Figure 5.3]
+(defmethod eval1 ((term (pattern (app fun arg))))
+  (eval1 (make-app (eval1 fun) arg)))
+
+;; Reduce argument to value
+;;
+;;      t_2 -> t_2'
+;; ---------------------
+;;  v_1 t_2 -> v_1 t_2'
+;;
+;; [1 Page 72; Figure 5.3]
+(defmethod eval1 ((term (pattern (app (fun (and fun (val))) arg))))
+  (eval1 (make-app fun (eval1 arg))))
+
+;; Application
+;;
+;; (λx.t_{12}) v_2 -> [x -> v_2] t_{12}
+;;
+;; [1 Page 72; Figure 5.3]
+(defmethod eval1 ((term (pattern (app (fun (abs var body)) (arg (and arg (val)))))))
+  (let ((arg-value (eval1 arg)))
+    (eval1 (substitute1 body var arg-value))))
+
+;;; Test
+
+(eval1 (make-const 1))
+
+(eval1 (make-abs (make-var 'x) (make-const 1)))
+
+(eval1 (make-app (make-abs (make-var 'x) (make-var 'x)) (make-const 1)))
+;; => #S(CONST :VALUE 1)
+
+(eval1 (parse '(((λ z (λ y z)) 5) 6)))