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 (cl:in-package #:pattern-specializer.examples.lambda-calculus)
  17
  18 ;;; Syntax
  19
  20 (defstruct term)
  21
  22 (defstruct (value (:include term) (:constructor make-value (value)))
  23   (value nil)) ; TODO val?
  24
  25 (defstruct (var (:include term) (:constructor make-var (name)))
  26   (name nil :type symbol))
  27
  28 (defstruct (abst (:include value) (:constructor make-abst (var body)))
  29   (var nil :type var)
  30   (body nil :type term))
  31
  32 (defstruct (app (:include term) (:constructor make-app (func arg)))
  33   (func nil :type term)
  34   (arg nil :type term))
  35
  36 ;;; Parse
  37
  38 (defgeneric parse (from)
  39   (:generic-function-class pattern-generic-function))
  40
  41 (defmethod parse ((form (pattern (optima:guard value (integerp value))))) ; TODO just (form integer)
  42   (make-value value))
  43
  44 (defmethod parse ((form (pattern (optima:guard name (symbolp name))))) ; TODO just (form symbol)
  45   (make-var form))
  46
  47 (defmethod parse ((form (pattern (list 'λ (optima:guard name (symbolp name)) body))))
  48   (make-abst (parse name) (parse body)))
  49
  50 (defmethod parse ((form (pattern (list func arg))))
  51   (make-app (parse func) (parse arg)))
  52
  53 ;;; Substitution
  54
  55 (defgeneric substitute1 (term var val))
  56
  57 (defmethod substitute1 ((term value) (var var) (val value))
  58   term)
  59
  60 ;; [1 Page 69]
  61 (defmethod substitute1 ((term var) (var var) (val value))
  62   (if (equalp term var) val term))
  63
  64 ;; [1 Page 69]
  65 (defmethod substitute1 ((term abst) (var var) (val value))
  66   ;; TODO capture
  67   (make-abst (abst-var term) (substitute1 (abst-body term) var val)))
  68
  69 ;; [1 Page 69]
  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)))
  73
  74 ;;; Evaluation
  75
  76 (defgeneric eval1 (term)
  77   (:generic-function-class pattern-generic-function))
  78
  79 (defmethod eval1 ((term (pattern (value)))) ; TODO does not need pattern
  80   term)
  81
  82 ;; Reduce function to value
  83 ;;
  84 ;;      t_1 -> t_1'
  85 ;; ---------------------
  86 ;;  t_1 t_2 -> t_1' t_2
  87 ;;
  88 ;; [1 Page 72; Figure 5.3]
  89 (defmethod eval1 ((term (pattern (app func arg))))
  90   (eval1 (make-app (eval1 func) arg)))
  91
  92 ;; Reduce argument to value
  93 ;;
  94 ;;      t_2 -> t_2'
  95 ;; ---------------------
  96 ;;  v_1 t_2 -> v_1 t_2'
  97 ;;
  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))))
 101
 102 ;; Application
 103 ;;
 104 ;; (λx.t_12) v_2 -> [x -> v_2] t_12
 105 ;;
 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))))
 110
 111 ;;; Test
 112
 113 (eval1 (make-value 1))
 114
 115 (eval1 (make-abst (make-var 'x) (make-value 1)))
 116
 117 (eval1 (make-app (make-abst (make-var 'x) (make-var 'x)) (make-value 1)))
 118 ;; => S#(VALUE)
 119
 120 (eval1 (parse '(((λ z (λ y z)) 5) 6)))