1 ;;;; lambda-calculus.lisp --- Untyped lambda calculus based on pattern specializers.
3 ;;;; Copyright (C) 2014 Jan Moringen
5 ;;;; Author: Jan Moringen <jmoringe@techfak.uni-bielefeld.DE>
7 ;;;; Partially based on idea from
9 ;;;; [1] Benjamin C. Pierce (2002): Types and Programming languages
11 (cl:defpackage #:pattern-specializer.examples.lambda-calculus
14 #:pattern-specializer)
19 (:import-from #:optima
22 (cl:in-package #:pattern-specializer.examples.lambda-calculus)
28 ;;; term ---- val ---- abs
32 (defstruct term) ; abstract
34 (defstruct (val (:include term))) ; abstract
36 (defstruct (const (:include val) (:constructor make-const (value)))
37 (value nil)) ; TODO val?
39 (defstruct (var (:include term) (:constructor make-var (name)))
40 (name nil :type symbol))
42 (defstruct (abs (:include val) (:constructor make-abs (var body)))
44 (body nil :type term))
46 (defstruct (app (:include term) (:constructor make-app (fun arg)))
52 (defgeneric parse (form)
53 (:generic-function-class pattern-generic-function))
55 (defmethod parse ((form integer))
58 (defmethod parse ((form symbol))
61 (defmethod parse ((form (pattern (list 'λ (guard name (symbolp name)) body))))
62 (make-abs (parse name) (parse body)))
64 (defmethod parse ((form (pattern (list func arg))))
65 (make-app (parse func) (parse arg)))
69 (defgeneric substitute1 (term var val))
71 (defmethod substitute1 ((term val) (var var) (val val))
75 (defmethod substitute1 ((term var) (var var) (val val))
76 (if (equalp term var) val term))
79 (defmethod substitute1 ((term abs) (var var) (val val))
81 (make-abs (abs-var term) (substitute1 (abs-body term) var val)))
84 (defmethod substitute1 ((term app) (var var) (val val))
85 (make-app (substitute1 (app-fun term) var val)
86 (substitute1 (app-arg term) var val)))
90 (defgeneric eval1 (term)
91 (:generic-function-class pattern-generic-function))
93 (defmethod eval1 ((term val))
96 ;; Reduce function to value
99 ;; ---------------------
100 ;; t_1 t_2 -> t_1' t_2
102 ;; [1 Page 72; Figure 5.3]
103 (defmethod eval1 ((term (pattern (app fun arg))))
104 (eval1 (make-app (eval1 fun) arg)))
106 ;; Reduce argument to value
109 ;; ---------------------
110 ;; v_1 t_2 -> v_1 t_2'
112 ;; [1 Page 72; Figure 5.3]
113 (defmethod eval1 ((term (pattern (app (fun (and fun (val))) arg))))
114 (eval1 (make-app fun (eval1 arg))))
118 ;; (λx.t_{12}) v_2 -> [x -> v_2] t_{12}
120 ;; [1 Page 72; Figure 5.3]
121 (defmethod eval1 ((term (pattern (app (fun (abs var body)) (arg (and arg (val)))))))
122 (let ((arg-value (eval1 arg)))
123 (eval1 (substitute1 body var arg-value))))
127 (eval1 (make-const 1))
129 (eval1 (make-abs (make-var 'x) (make-const 1)))
131 (eval1 (make-app (make-abs (make-var 'x) (make-var 'x)) (make-const 1)))
132 ;; => #S(CONST :VALUE 1)
134 (eval1 (parse '(((λ z (λ y z)) 5) 6)))