examples/lambda-calculus.lisp

   1 ;;;; lambda-calculus.lisp --- Untyped lambda calculus based on pattern specializers.
   2 ;;;;
   3 ;;;; Copyright (C) 2014 Jan Moringen
   4 ;;;;
   5 ;;;; Author: Jan Moringen <jmoringe@techfak.uni-bielefeld.DE>
   6
   7 ;;;; Partially based on idea from
   8 ;;;;
   9 ;;;; [1] Benjamin C. Pierce (2002): Types and Programming languages
  10
  11 (cl:defpackage #:pattern-specializer.examples.lambda-calculus
  12   (:use
  13    #:cl
  14    #:pattern-specializer)
  15
  16   (:shadow
  17    #:abs)
  18
  19   (:import-from #:optima
  20    #:guard))
  21
  22 (cl:in-package #:pattern-specializer.examples.lambda-calculus)
  23
  24 ;;; Syntax
  25 ;;;
  26 ;;;        ,- app   ,- const
  27 ;;;       /        /
  28 ;;; term ---- val ---- abs
  29 ;;;       \
  30 ;;;        `- var
  31
  32 (defstruct term) ; abstract
  33
  34 (defstruct (val (:include term))) ; abstract
  35
  36 (defstruct (const (:include val) (:constructor make-const (value)))
  37   (value nil))  ; TODO val?
  38
  39 (defstruct (var (:include term) (:constructor make-var (name)))
  40   (name nil :type symbol))
  41
  42 (defstruct (abs (:include val) (:constructor make-abs (var body)))
  43   (var nil :type var)
  44   (body nil :type term))
  45
  46 (defstruct (app (:include term) (:constructor make-app (fun arg)))
  47   (fun nil :type term)
  48   (arg nil :type val))
  49
  50 ;;; Parse
  51
  52 (defgeneric parse (form)
  53   (:generic-function-class pattern-generic-function))
  54
  55 (defmethod parse ((form integer))
  56   (make-const form))
  57
  58 (defmethod parse ((form symbol))
  59   (make-var form))
  60
  61 (defmethod parse ((form (pattern (list 'λ (guard name (symbolp name)) body))))
  62   (make-abs (parse name) (parse body)))
  63
  64 (defmethod parse ((form (pattern (list func arg))))
  65   (make-app (parse func) (parse arg)))
  66
  67 ;;; Substitution
  68
  69 (defgeneric substitute1 (term var val))
  70
  71 (defmethod substitute1 ((term val) (var var) (val val))
  72   term)
  73
  74 ;; [1 Page 69]
  75 (defmethod substitute1 ((term var) (var var) (val val))
  76   (if (equalp term var) val term))
  77
  78 ;; [1 Page 69]
  79 (defmethod substitute1 ((term abs) (var var) (val val))
  80   ;; TODO capture
  81   (make-abs (abs-var term) (substitute1 (abs-body term) var val)))
  82
  83 ;; [1 Page 69]
  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)))
  87
  88 ;;; Evaluation
  89
  90 (defgeneric eval1 (term)
  91   (:generic-function-class pattern-generic-function))
  92
  93 (defmethod eval1 ((term val))
  94   term)
  95
  96 ;; Reduce function to value
  97 ;;
  98 ;;      t_1 -> t_1'
  99 ;; ---------------------
 100 ;;  t_1 t_2 -> t_1' t_2
 101 ;;
 102 ;; [1 Page 72; Figure 5.3]
 103 (defmethod eval1 ((term (pattern (app fun arg))))
 104   (eval1 (make-app (eval1 fun) arg)))
 105
 106 ;; Reduce argument to value
 107 ;;
 108 ;;      t_2 -> t_2'
 109 ;; ---------------------
 110 ;;  v_1 t_2 -> v_1 t_2'
 111 ;;
 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))))
 115
 116 ;; Application
 117 ;;
 118 ;; (λx.t_{12}) v_2 -> [x -> v_2] t_{12}
 119 ;;
 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))))
 124
 125 ;;; Test
 126
 127 (eval1 (make-const 1))
 128
 129 (eval1 (make-abs (make-var 'x) (make-const 1)))
 130
 131 (eval1 (make-app (make-abs (make-var 'x) (make-var 'x)) (make-const 1)))
 132 ;; => #S(CONST :VALUE 1)
 133
 134 (eval1 (parse '(((λ z (λ y z)) 5) 6)))