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))
16 (cl:in-package #:pattern-specializer.examples.lambda-calculus)
22 (defstruct (value (:include term) (:constructor make-value (value)))
23 (value nil)) ; TODO val?
25 (defstruct (var (:include term) (:constructor make-var (name)))
26 (name nil :type symbol))
28 (defstruct (abst (:include value) (:constructor make-abst (var body)))
30 (body nil :type term))
32 (defstruct (app (:include term) (:constructor make-app (func arg)))
38 (defgeneric parse (from)
39 (:generic-function-class pattern-generic-function))
41 (defmethod parse ((form (pattern (optima:guard value (integerp value))))) ; TODO just (form integer)
44 (defmethod parse ((form (pattern (optima:guard name (symbolp name))))) ; TODO just (form symbol)
47 (defmethod parse ((form (pattern (list 'λ (optima:guard name (symbolp name)) body))))
48 (make-abst (parse name) (parse body)))
50 (defmethod parse ((form (pattern (list func arg))))
51 (make-app (parse func) (parse arg)))
55 (defgeneric substitute1 (term var val))
57 (defmethod substitute1 ((term value) (var var) (val value))
61 (defmethod substitute1 ((term var) (var var) (val value))
62 (if (equalp term var) val term))
65 (defmethod substitute1 ((term abst) (var var) (val value))
67 (make-abst (abst-var term) (substitute1 (abst-body term) var val)))
70 (defmethod substitute1 ((term app) (var var) (val value))
71 (make-app (substitute1 (app-func term) var val)
72 (substitute1 (app-arg term) var val)))
76 (defgeneric eval1 (term)
77 (:generic-function-class pattern-generic-function))
79 (defmethod eval1 ((term (pattern (value)))) ; TODO does not need pattern
82 ;; Reduce function to value
85 ;; ---------------------
86 ;; t_1 t_2 -> t_1' t_2
88 ;; [1 Page 72; Figure 5.3]
89 (defmethod eval1 ((term (pattern (app func arg))))
90 (eval1 (make-app (eval1 func) arg)))
92 ;; Reduce argument to value
95 ;; ---------------------
96 ;; v_1 t_2 -> v_1 t_2'
98 ;; [1 Page 72; Figure 5.3]
99 (defmethod eval1 ((term (pattern (app (func (and func (value))) arg))))
100 (eval1 (make-app func (eval1 arg))))
104 ;; (λx.t_12) v_2 -> [x -> v_2] t_12
106 ;; [1 Page 72; Figure 5.3]
107 (defmethod eval1 ((term (pattern (app (func (abst var body)) (arg (and arg (value)))))))
108 (let ((arg-value (eval1 arg)))
109 (eval1 (substitute1 body var arg-value))))
113 (eval1 (make-value 1))
115 (eval1 (make-abst (make-var 'x) (make-value 1)))
117 (eval1 (make-app (make-abst (make-var 'x) (make-var 'x)) (make-value 1)))
120 (eval1 (parse '(((λ z (λ y z)) 5) 6)))