Lambda Calchylus test document

Lambda calculus evaluator written with Hy.

DRAFT! 5.9.2017

System configuration


In [1]:
(import hy sys)
(print "Hy version: " hy.__version__)
(print "Python" sys.version)


Hy version:  0.13.0
Python 3.6.2 | packaged by conda-forge | (default, Jul 23 2017, 22:58:45) [MSC v.1900 64 bit (AMD64)]

Main evaluator code


In [2]:
; Copyright (c) Marko Manninen (@markomanninen), 2017
(import hy)
(eval-and-compile
  (setv ; lambda expression macro name
        lambdachr 'L
        ; lambda expression argument and body separator
        separator ',
        ; TODO: these could be constructed by some lambda-term-generator macro
        forms ["CONST" "IDENT" "TRUE" "FALSE" "REPLACE" "OMIT"
               "PAIR" "HEAD" "TAIL" "FIRST" "SECOND" "NIL" "NIL?" "is_NIL"
               "ZERO" "ZERO?" "is_ZERO" "NUM" 
               "ONE" "TWO" "THREE" "FOUR" "FIVE" "SIX" "SEVEN" "EIGHT" "NINE" "TEN"
               "COND" "AND" "OR" "NOT" "XOR"
               "ADD" "PRED" "SUCC" "EXP" "SUM" "PROD" "SUB"
               "EQ?" "is_EQ" "LEQ?" "is_LEQ" "SELF" "YCOMB"
               "SUMMATION" "FACTORIAL" "FIBONACCI"])
  ; is gensym?
  (defn gensym? [x] (or (= (first x) ":") (= (first x) "\ufdd0")))
  ; pretty print utility
  (defn pprint [expr]
    (if-not (coll? expr) (str expr)
      (% "(%s)" (.join " " (list-comp (pprint x) [x expr])))))
  ; safe get index for the first occurrence of the x
  ; (index (, 1 2) 0) ; -> -1
  (defn index [l x]
    (try (.index l x)
         (except [e [ValueError AttributeError]]
           -1)))
  ; extend and return list instead of .extend list in place
  ; provide a as a copy (.copy a) in cases where strange 
  ; recursive error behaviour is occurring
  (defn extend [a &rest b]
    (for [c b] (.extend a c)) a)
  ; church number body generator helper (N 3 m n) ; -> (m (m (m n)))
  ;(defn N [n x y]
  ;  (if (zero? n) y
  ;      (% "(%s %s%s" (, x  (N (dec n) x y) ")"))))
  ; is expr(ession) a suitable macro form?
  (defn macro-form? [expr] (and (symbol? expr) (in expr forms)))
  ; is expr(ession) or the firs sub expression a suitable macro form
  (defn form? [expr]
    (or (macro-form? expr)
        (and (coll? expr) (macro-form? (first expr)))))
  ; is expr(ession) a lambda expression i.e. starts with lambdachr: (L ...)?
  (defn L? [expr]
    (and (coll? expr)
         (symbol? (first expr))
         (= (first expr) lambdachr)))
  ; make lambda expression from body and other parts
  (defn build-lambda [body &optional [args []] [vals []]]
    (hy.HyExpression (extend [lambdachr] args [separator] body vals)))
  ; substitute lambda sub expr(ession). it requires special handler
  ; because of variable shadowing and not-coll body
  (defn substitute* [a b expr] ; (print 's2 a b expr)
    (setv p (extract-parts expr)
          args (get p "args")
          body (get p "body")
          vals (get p "vals")
          free (drop (len args) vals))
    ; first substitute a to b in possible values
    (if-not (empty? vals) (setv vals (substitute a b vals)))
    ; shadow arguments, don't substitute if a is in new arguments
    (if (in a args) expr
        (build-lambda
          ; only coll body can be iterated
          (if (coll? body)
              [(substitute a b body)]
              [(if (= a body) b body)])
          args vals)))
  ; substitute a with b in expr
  (defn substitute [a b expr] ; (print 's1 a b expr)
    (if (coll? expr)
        ; if e is lambda expression, call special handler
        (if (L? expr) (substitute* a b expr)
            ; else substitute all sub expressions
            ((type expr) (genexpr (substitute a b e) [e expr])))
        ; return substitute (b), if match is found
        (if (= a expr) b expr)))
  ; shift arguments inside functions in application expressions
  ; ((L x , x) a b) -> (L x , x a b) -> (a b)
  ; ((TRUE) TRUE FALSE) -> (TRUE TRUE FALSE) -> TRUE
  ; this is required to convert and evaluate substituted function forms
  ; (L x y z , ((x) y z) TRUE a b) -> ((TRUE) a b) -> (TRUE a b) -> a
  (defn shift-arguments [expr]
    (if-not (coll? expr) expr 
      (do
        (setv f (first expr))
        ;(print 'shift-arguments-1 (pprint expr))
        (if (or (L? f) (and (coll? f) (form? f)))
            (setv expr (extend ((type f) (.copy f)) (tuple (rest expr)))))
        ;(print 'shift-arguments-2 (pprint expr))
        ((type expr) (genexpr (shift-arguments e) [e expr])))))
  ; alpha renaming / compile argument names if name collision occurs
  (defn name-collision* [args expr]
    (if (coll? expr) 
        (do (setv p False)
            (for [e expr]
              (if (name-collision* args e)
                (do (setv p True)
                    (break)))) p)
        (in expr args)))
  ; alpha renaming / compile argument names if name collision occurs
  (defn name-collision [vals args e]
    (setv p False)
    (for [e vals]
      (if (coll? e)
          (if (name-collision* args e)
              (do (setv p True)
                  (break)))
          (if (in e args)
              (do (setv p True)
                  (break))))) p)
  ; get lambda expression parts
  ; body: (x x), args: (x), values (y), and params: ([x y])
  (defn extract-parts [expr]
    (setv idx (index expr separator)
          ; expression might start with L: (L x , x ...)
          ; or without L: (x , x ...)
          ldx (if (L? expr) 1 0))
    ; if separator index is less than expected
    ; lambda expression is possibly malformed, just return the expression
    (if (< idx ldx) {"body" (if (coll? expr) (first expr) expr) "args" [] "vals" [] "params" []}
        (do
          (setv body (cut expr (inc idx))
                bodyb (first body)
                args (cut expr ldx idx)
                ; args 2 for alpha conversion
                args2 (tuple (map (fn [x] (if (gensym? (name x)) x (gensym x))) args))
                vals (tuple (rest body)))
          ; alpha conversion / variable renaming
          ; this is a brute force method. name collision should not occur because
          ; all variable names are changed and replaced. other way around would be to find out,
          ; if there are name collisions, and replace only those variable names.
          ; this might however require several loops and argument carrying for each variable and expression...
          ;(if (name-collision vals args bodyb)
          (for [[a b] (zip args args2)]
            (setv bodyb (substitute a b bodyb)))
          ; return body, args, vals, and key-value pairs based on args-vals
          {"body" bodyb "args" args2 "vals" vals "params" (zip args2 vals)})))
  ; handle macro forms extra
  (defn expand-form* [body]
    (if-not (coll? body) body
        (if (macro-form? (first body))
            (eval body)
            ((type body) (genexpr (expand-form* e) [e body])))))
  ; helper function to expand form that has custom lambda macros / forms
  ; used after everything else for the lambda form evaluation is done
  (defn expand-forms [expr]
    (if-not (none? expr)
      (if (or (symbol? expr) (coll? expr) (iterable? expr))
          (pprint (expand-form* (read-str expr)))
          expr)))
  ; are evaluated lambda forms same and there are no free values
  ; inside the form. because, if there are, we can still reduce the form
  (defn B? [body bodyx]
    (setv p (extract-parts body))
    (and (empty? (get p "vals")) (= body bodyx)))
  ; convert generated machine variable names to normal forms
  (defn human-readable [expr]
    (if (coll? expr)
        (genexpr (human-readable e) [e expr])
        (if (gensym? (name expr))
            (do
               (setv idx (inc (index (name expr) ":")))
               (cut (name expr) idx (inc idx)))
            expr)))
  ; beta reduction helper
  (defn beta-reduction* [expr]
    (setv p (extract-parts expr)
          body (get p "body")
          bodyx body
          ; rest of the free arguments that are not in params
          free (list (drop (len (get p "args")) (get p "vals"))))
    ; substitute bound arguments
    ;(print 'before-substitute-body: (pprint body) (get p "params"))
    (for [[a b] (get p "params")]
      (setv body (substitute a b body)))
    ;(print 'after-substitute-body: (pprint body))
    ; shift application arguments
    (if (coll? body) (setv body (shift-arguments body)))
    ;(print 'after-shift-arguments: (pprint body))
    ; extend body
    (if (and (L? body) (not (empty? free)))
        (setv body (extend body free)))
    ;(print 'after-extend-body: (pprint body) (not (coll? body)) (= body bodyx))
    (if (form? body)
        (if (coll? body)
            (eval (if (empty? free) body (extend body free)))
            (if (empty? free) (human-readable body) 
                (eval (hy.HyExpression (extend [body] free)))))
        (if (or (not (coll? body)) (B? body bodyx))
            (if (empty? (get p "args")) (beta-reduction body)
                (if (empty? (get p "vals")) (human-readable expr)
                    (if (empty? free) (human-readable body)
                        (human-readable (extend [body] free)))))
            (if (L? body)
                (beta-reduction body)
                ((type body) (genexpr (beta-reduction x) [x (if (empty? free) body (extend [body] free))]))))))
  ; main form beta / eta reduction steps
  (defn beta-reduction [expr]
    ;(print)
    ;(print 'beta-reduction: (pprint expr))
    ; TODO: should we try to shift argument before everything else is done?
    ;(if (and (coll? expr)) (setv expr (shift-arguments expr)))
    ; if the form (expr) is not lambda for i.e. starting with L
    ; we still want to seek if there are sub lambda expressions
    ; (x (x (L x , x y))) should return (x (x y))
    (if (L? expr) 
        (beta-reduction* expr)
        (if (coll? expr)
            ((type expr) (genexpr (beta-reduction x) [x expr]))
            (human-readable expr))))
  ; reformulate expression, because by using L macro, L is naturally left out from the expression
  ; beta-reduction functions on the other hand relys on the L in the beginning of the expression!
  ; then pass parameters and possibly expand macro form later
  (defn evaluate-lambda-expression [expr]
    (setv expr (beta-reduction (hy.HyExpression (extend [lambdachr] expr))))
    (if (or (coll? expr) (symbol? expr))
        ; symbols and expression should be pretty "printed"
        (pprint expr)
        ; numbers for example get passed as they are
        ; this is not exactly included on lambda calculus but just a way
        ; to keep data types existing for hy and later usage
        expr)))

; shorthand to evaluate lambda form and expand the result
; it still has some cases, where expansion is not working as expected,
; for example: #Ÿ(SUM (SUM ONE ONE) ZERO) ; -> (x (x (ZERO x y)))
(defsharp Ÿ [expr] `(expand-forms (L , ~expr)))

; lambda expression main macro
(defmacro L [&rest expr]
  ; try except is not working alone on macro body!
  (if-not (empty? expr)
    (try 
      (evaluate-lambda-expression expr)
      (except [e [RecursionError hy.errors.HyMacroExpansionError]]
        (print (str e) "for lambda expression:" (pprint expr))))))

; church number generator: (NUM 3) ; -> (L x y , (x (x (x y))))
; launch application: (NUM 3 a b) ; -> (a (a (a b)))
;(defmacro NUM [n &rest args]
;  `(L x y , ~(read_str (N n 'x 'y)) ~@args))
; Tuukka Turto (@tuturto), 2017
(defmacro NUM [n &rest args]
  (if (< n 0) (macro-error n (% "For NUM n needs to be zero or more, was: %s" n))
      (= n 0) `(L x y , y ~@args)
      (> n 0) (do (setv expr `(x y))
                  (for [i (range (dec n))]
                    (setv expr `(x ~expr)))
                  `(L x y , ~expr ~@args))))


Out[2]:
<function _hy_anon_fn_23 at 0x000002109BB62378>

Predefined Lambda forms

These are the usual Lambda forms from textbooks. Macros are created for shorthands. They are used to make Lambda terms shorter and more comprehensible.


In [3]:
; constant, doesn't take any arguments, will return given "static" value
(defmacro CONST  [&rest args] `(L , ~@args))
; identity, return passed argument as it is
(defmacro IDENT  [&rest args] `(L a , a ~@args))
; booleans
; true, take two arguments, return the first and omit the second
(defmacro TRUE   [&rest args] `(L a b , a ~@args))
; false, take two arguments, return the second and omit the first
(defmacro FALSE  [&rest args] `(L a b , b ~@args))
; replace next argument with false, take one argument, but return a static FALSE value
; if two arguments are given, then FALSE will return the latter, in a way this is similar
; giving two arguments to FALSE
;(defmacro REPLACE [&rest args] `(L a , FALSE ~@args))
(defmacro REPLACE [&rest args] `(L a , (L a b , b) ~@args))
; omit next
(defmacro OMIT   [&rest args] `(L a , b ~@args))
; lists
(defmacro NIL    [&rest args] `(FALSE ~@args))
(defmacro PAIR   [&rest args] `(L a b s , (s a b) ~@args))
(defmacro FIRST  [&rest args] `(TRUE ~@args))
(defmacro SECOND [&rest args] `(FALSE ~@args))
(defmacro HEAD   [&rest args] `(L s , (s TRUE) ~@args))
(defmacro TAIL   [&rest args] `(L s , (s FALSE) ~@args))
(defmacro NIL?   [&rest args] `(L s , (s FALSE TRUE) ~@args))
; zero things
(defmacro ZERO  [&rest args] `(FALSE ~@args))
;(defmacro ZERO? [&rest args] `(L f , (f (L x , FALSE) TRUE) ~@args))
;(defmacro ZERO? [&rest args] `(L f , (f REPLACE TRUE) ~@args))
(defmacro ZERO? [&rest args] `(L f , (f (L a , (L a b , b)) (L a b , a)) ~@args))
; logic
(defmacro COND  [&rest args] `(L p a b , (p a b) ~@args))
(defmacro AND   [&rest args] `(L a b , (a b FALSE) ~@args))
;(defmacro AND2  [&rest args] `(L a b , (a b a) ~@args))
(defmacro OR    [&rest args] `(L a b , (a TRUE b) ~@args))
;(defmacro OR2   [&rest args] `(L a b , (a a b) ~@args))
(defmacro NOT   [&rest args] `(L p , (p FALSE TRUE) ~@args))
;(defmacro NOT2  [&rest args] `(L p a b , (p b a) ~@args))?
(defmacro XOR   [&rest args] `(L a b , (a (NOT b) b) ~@args))
; positive "church" numerals
;(defmacro ONE   [&rest args] `(L x y , (x y) ~@args))
(defmacro ONE   [&rest args] `(NUM 1 ~@args))
;(defmacro TWO   [&rest args] `(L x y , (x (x y)) ~@args))
(defmacro TWO   [&rest args] `(NUM 2 ~@args))
;(defmacro THREE [&rest args] `(L x y , (x (x (x y))) ~@args))
(defmacro THREE [&rest args] `(NUM 3 ~@args))
;(defmacro FOUR  [&rest args] `(L x y , (x (x (x (x y)))) ~@args))
(defmacro FOUR  [&rest args] `(NUM 4 ~@args))
;(defmacro FIVE  [&rest args] `(L x y , (x (x (x (x (x y))))) ~@args))
(defmacro FIVE  [&rest args] `(NUM 5 ~@args))
;(defmacro SIX   [&rest args] `(L x y , (x (x (x (x (x (x y)))))) ~@args))
(defmacro SIX   [&rest args] `(NUM 6 ~@args))
;(defmacro SEVEN [&rest args] `(L x y , (x (x (x (x (x (x (x y))))))) ~@args))
(defmacro SEVEN [&rest args] `(NUM 7 ~@args))
;(defmacro EIGHT [&rest args] `(L x y , (x (x (x (x (x (x (x (x y)))))))) ~@args))
(defmacro EIGHT [&rest args] `(NUM 8 ~@args))
;(defmacro NINE  [&rest args] `(L x y , (x (x (x (x (x (x (x (x (x y))))))))) ~@args))
(defmacro NINE  [&rest args] `(NUM 9 ~@args))
;(defmacro TEN   [&rest args] `(L x y , (x (x (x (x (x (x (x (x (x (x y)))))))))) ~@args))
(defmacro TEN   [&rest args] `(NUM 10 ~@args))
; arithmetics
; add one, increase by one
(defmacro ADD   [&rest args] `(L n x y , (n x (x y)) ~@args))
; next / successor = INC = ADD
(defmacro SUCC  [&rest args] `(L n x y , (x (n x y)) ~@args))
; previous / predecessor = DEC
;(defmacro PRED  [&rest args] `(L n x y , (n (L g h , (h (g x))) (L x , y) (L u , u)) ~@args))
;(defmacro PRED  [&rest args] `(L n x y , (n (L g h , (h (g x))) (L x , y) IDENT) ~@args))
(defmacro PRED  [&rest args] `(L n x y , (n (L g h , (h (g x))) (L x , y) (L a , a)) ~@args))
; substract two numbers from each other
;(defmacro SUB   [&rest args] `(L k , (k (L p u , (u (ADD (p TRUE)) (p TRUE))) (L u , u ZERO ZERO)) ~(first args) FALSE ~@(rest args)))
(defmacro SUB   [&rest args] `(L m n , (m PRED n) ~@args))
; sum two numbers together
;(defmacro SUM  [&rest args] `(L m n , (m SUCC n) ~@args))
(defmacro SUM   [&rest args] `(L m n x y , (m x (n x y)) ~@args))
; multiplication, product of two numbers
(defmacro PROD  [&rest args] `(L m n x y , (m (n x) y) ~@args))
; exponent x^y
(defmacro EXP   [&rest args] `(L m n x y , (n m x y) ~@args))
; lesser or equal
(defmacro LEQ?  [&rest args] `(L m n , (ZERO? (n PRED m)) ~@args))
; equal
(defmacro EQ?   [&rest args] `(L m n , (AND (LEQ? m n) (LEQ? n m)) ~@args))
; combinators / applications
(defmacro SELF  [&rest args] `(L f x , (f f x) ~@args))
; TODO!
(defmacro YCOMB [&rest args] `(L f , (L x , (f (f x)) (L x , (f (f x)))) ~@args))
; some math functions
; ∑
(defmacro SUMMATION [&rest args] `(L x , (SELF (L f n , (COND (ZERO? n) ZERO (SUM n (f f (PRED n))))) x) ~@args))
; ∏ TODO: number greater than THREE will mess up the evaluation
; Also if number (n) is give first at: (PROD n (f f (PRED n))) it will mess up the thing
(defmacro FACTORIAL [&rest args] `(L x , (SELF (L f n , (COND (ZERO? n) ONE (PROD (f f (PRED n)) n))) x) ~@args))
; F TODO: implement
(defmacro FIBONACCI [])


Out[3]:
<function <lambda> at 0x000002109BB56AE8>

Sandbox test area


In [4]:
; replace form, one argument
(, (L a , (L a b , b) l) (REPLACE l))


Out[4]:
('(L a b , b)', '(L a b , b)')

In [5]:
; replace form, two arguments
(, (L a , (L a b , b) l m) (REPLACE l m))


Out[5]:
('b', 'b')

In [6]:
; replace form, three arguments
(, (L a , (L a b , b) l m n) (REPLACE l m n))


Out[6]:
('n', 'n')

In [7]:
; infix serial notation!
(ONE ADD TWO ADD THREE ADD FOUR)


Out[7]:
'(x (x (x (x (x (x (x (x (x (x y))))))))))'

Self application


In [8]:
(SELF (L f n , (COND (ZERO? n) ONE (PROD (f f (PRED n)) n))) THREE) ; 1*2*3 = 6


Out[8]:
'(x (x (x (x (x (x y))))))'

In [9]:
; SELF
(L f n , (f f n)
  ; function
  (L f n , 
    ; COND
    (L p a b , (p a b) 
      ; if n is ZERO?
      (L f , (f (L a , (L a b , b)) (L a b , a)) n)
      ; then ONE
      (L x y , (x y))
      ; else PROD 
      (L m n x y , (m (n x) y)
        ; function PRED n
        (f f (L n x y , (n (L g h , (h (g x))) (L x , y) (L a , a)) n))
        ; times n
        n)))
  ; THREE
  (L x y , (x (x (x y))))) ; 1*2*3=6


Out[9]:
'(x (x (x (x (x (x y))))))'

In [10]:
(SELF (L f n , (COND (ZERO? n) ZERO (SUM n (f f (PRED n))))) THREE) ; 1*2*3 = 6


Out[10]:
'(x (x (x (x (x (x y))))))'

In [11]:
; SELF
(L f n , (f f n)
  ; function
  (L f n , 
    ; COND
    (L p a b , (p a b) 
      ; if n is ZERO?
      (L f , (f (L a , (L a b , b)) (L a b , a)) n)
      ; then ZERO
      (L x y , y)
      ; else SUM 
      (L m n x y , (m x (n x y))
        ; function PRED n
        (f f (L n x y , (n (L g h , (h (g x))) (L x , y) (L a , a)) n))
        ; times n
        n)))
  ; THREE
  (L x y , (x (x (x y))))) ; 1*2*3=6


Out[11]:
'(x (x (x (x (x (x y))))))'

In [12]:
#Ÿ(YCOMB a)


Out[12]:
'(a (a (L x , (a (a x)))))'

In [13]:
(YCOMB (L f n , (COND (ZERO? n) ZERO (SUM n (f (PRED n))))) THREE) ; 1*2*3 = 6


Out[13]:
'(x (x (x (x (x ((x (L a , (L a b , b)) (L a b , a)) ZERO (SUM x ((x (L g h , (h (g (L a , (L a b , b))))) (L x , (L a b , a)) (L a , a)) ZERO (SUM (PRED x) (PRED (PRED THREE) (PRED (PRED x)))))) y))))))'

In [14]:
(YCOMB
  (L f n , 
    ; COND
    (L p a b , (p a b) 
      ; if ZERO? n
      (L f , (f (L a , (L a b , b)) (L a b , a)) n) 
      ; then ZERO
      (L x y , y) 
      ; else SUM 
      (L m n x y , (m x (n x y))
         ; function PRED n
         (f (L n x y , (n (L g h , (h (g x))) (L u , y) (L u , u)) n))
         ; times n
         n)))
  (L  x y , (x (x (x y)))))


Out[14]:
'((x (L a , (L a b , b)) (L a b , a)) (L x y , y) ((x (L g h , (h (g (L a , (L a b , b))))) (L u , (L a b , a)) (L u , u)) (L x y , y) ((x (L g h , (h (g (L g h , (h (g (L u , (L u , x) (L g h , (h (g (L n x y , (n (L g h , (h (g x))) (L u , y) (L u , u)) (L n x y , (n (L g h , (h (g x))) (L u , y) (L u , u)) x))))) (L n x y , (n (L g h , (h (g x))) (L u , y) (L u , u)) (L n x y , (n (L g h , (h (g x))) (L u , y) (L u , u)) x))))))))) (L u , (L u , (L n x y , (n (L g h , (h (g x))) (L u , y) (L u , u)) x x y))) (L u , u)) (L u , u)) x (x x y)) (x (x (x (x (x y))))))'

In [15]:
(YCOMB (L f n , (COND (ZERO? n) ONE (PROD (f (PRED n)) n))) THREE) ; 1*2*3 = 6


Out[15]:
'((x (x (x (x (x (x (L a , (L a b , b)))))))) (L a b , a) ONE (PROD ((x (x (x (x (x (x (L g h , (h (g (L a , (L a b , b))))))))))) (L x , (L a b , a)) (L a , a) ONE (PROD (PRED (PRED THREE) (PRED (PRED (PRED THREE (THREE x))))) (PRED (PRED THREE (THREE x))))) (PRED THREE (THREE x))) y)'

In [16]:
(YCOMB
  (L f n , 
    ; COND
    (L p a b , (p a b) 
      ; if ZERO? n
      (L f , (f (L a , (L a b , b)) (L a b , a)) n) 
      ; then ONE
      (L x y , (x y)) 
      ; else PROD 
      (L m n x y , (m (n x) y) 
         ; function PRED n
         (f (L n x y , (n (L g h , (h (g x))) (L u , y) (L u , u)) n))
         ; times n
         n)))
  (L  x y , (x (x (x y)))))


Out[16]:
'((x (x (x (x (x (x (L a , (L a b , b)))))))) (L a b , a) (L x y , (x y)) ((x (x (x (x (x (x (L g h , (h (g (L a , (L a b , b))))))))))) (L u , (L a b , a)) (L u , u) (L x y , (x y)) ((x (x (x (x (x (x (L g h , (h (g (L g h , (h (g (L u , (L u , (L n x y , (n (L g h , (h (g x))) (L u , y) (L u , u)) (L n x y , (n (L g h , (h (g x))) (L u , y) (L u , u)) (L x y , (x (x (x y)))) (L x y , (x (x (x y))) x)) x)) (L g h , (h (g (L n x y , (n (L g h , (h (g x))) (L u , y) (L u , u)) (L n x y , (n (L g h , (h (g x))) (L u , y) (L u , u)) (L n x y , (n (L g h , (h (g x))) (L u , y) (L u , u)) (L x y , (x (x (x y)))) (L x y , (x (x (x y))) x))))))) (L n x y , (n (L g h , (h (g x))) (L u , y) (L u , u)) (L n x y , (n (L g h , (h (g x))) (L u , y) (L u , u)) (L n x y , (n (L g h , (h (g x))) (L u , y) (L u , u)) (L x y , (x (x (x y)))) (L x y , (x (x (x y))) x))))))))))))))))) (L u , (L u , y)) (L u , u) (L u , u)) (x (x (x (x (x (x x)))))) y) y)'

In [17]:
; https://stackoverflow.com/questions/36511989/lambda-calculus-reduction-evaluating-expr
(L f x , (f (f x)) (L y , (y ^ 2)) 5)


Out[17]:
'((5 ^ 2) ^ 2)'

Tests

Function and application constructors


In [18]:
; not lambda expression
(assert (= (, 'x) (, 'x)))
; no body lambda expression
(assert (= (L ,) None))
; constant
(assert (= (L , c) 'c))
; identity, without argument
(assert (= (L x , x) "(L x , x)"))
; identity, with argument
(assert (= (L x , x y) 'y))
; select first, without arguments
(assert (= (L x y , x) "(L x y , x)"))
; select second, without arguments
(assert (= (L x y , y) "(L x y , y)"))
; select first, with arguments
(assert (= (L x y , x 1 0) 1))
; select second, with arguments
(assert (= (L x y , y 1 0) 0))
; function without arguments
(assert (= (L x y z , (x y z)) "(L x y z , (x y z))"))
; nested functions and arguments
(assert (= (L x , (L y , (L z , (z x y) l) k) j) "(l j k)"))
; nested functions, flatten arguments
(assert (= (L x , (L y , (L z , (z x y))) j k l) "(l j k)"))
; flatten functions and arguments
(assert (= (L x y z , (z x y) j k l) "(l j k)"))
; application without arguments
(assert (= (L , ((L x y z , (x y z)))) "(L x y z , (x y z))"))
; application with arguments
(assert (= (L , ((L x y z , (x y z)) a b c)) "(a b c)"))
; free argument
(assert (= (L x , x y z) "(y z)"))
; nested
(assert (= (L , ((L x y z , (x y z) x y z) a b c) 1 2 3) "((x y z) a b c 1 2 3)"))

Alpha conversion


In [19]:
; variable renaming should give right result
; instead of first substituting x with y, and then both y's with z, resulting (2 2)
; this test should give (y z) because y is bound to x and x only. latter y should not replace it
(assert (= (L x y , (x y) y z) "(y z)"))
; same should apply to deeper values too
(assert (= (L x y , (x y) (y (y z)) z) "((y (y z)) z)"))

Basic shorthand forms


In [20]:
; special macros for main lambda terms / forms
; constant
(assert (= (CONST x) 'x))
; identity, without arguments
(assert (= (IDENT) "(L a , a)"))
; identity, with arguments
(assert (= (IDENT 1) 1))
; identity, nested
(assert (= (IDENT (IDENT 1)) 1))
; boolean macros
(assert (= (, (TRUE) (TRUE 1 0) 
              (FALSE) (FALSE 1 0)) 
           (, "(L a b , a)" 1 
              "(L a b , b)" 0)))

List shorthand forms


In [21]:
; lists
(assert (= (NIL) "(L a b , b)"))
; pair constructor
(assert (= (PAIR TRUE NIL) "(s TRUE NIL)"))
; selector
(assert (= (PAIR TRUE NIL FIRST) 'TRUE))
; head and tail
(assert (= (, (HEAD (PAIR TRUE NIL)) 
              (TAIL (PAIR TRUE NIL))) 
           (, 'TRUE 'NIL)))
; is nil, simple
(assert (= (, (NIL? NIL) (NIL? TRUE)) (, 'TRUE 'FALSE)))
; is nil, head and tail
(assert (= (, (NIL? (HEAD (PAIR TRUE NIL))) 
              (NIL? (TAIL (PAIR TRUE NIL)))) 
           (, 'FALSE 'TRUE)))
; nested pairs and heads and tails
(assert (=
   (, (HEAD (PAIR TRUE (PAIR TRUE NIL))) 
      (HEAD (TAIL (PAIR TRUE (PAIR TRUE NIL))))
      (TAIL (TAIL (PAIR TRUE (PAIR TRUE NIL)))))
   (, 'TRUE 'TRUE 'NIL)))
; nil? for nested pairs
(assert (=
  (, (NIL? (TAIL (TAIL (PAIR TRUE (PAIR TRUE NIL))))) 
     (NIL? (HEAD (TAIL (PAIR TRUE (PAIR TRUE NIL))))))
  (, 'TRUE 'FALSE)))
; selectors for pairs
(assert (=  (, (PAIR (PAIR TRUE FALSE FIRST) NIL FIRST)
               (PAIR (PAIR TRUE FALSE SECOND) NIL FIRST)
               (PAIR (PAIR TRUE FALSE FIRST) NIL SECOND)
               (PAIR (PAIR TRUE FALSE SECOND) NIL SECOND)
               (PAIR TRUE (PAIR TRUE NIL FIRST) FIRST)
               (PAIR TRUE (PAIR TRUE NIL SECOND) FIRST)
               (PAIR TRUE (PAIR TRUE NIL FIRST) SECOND)
               (PAIR TRUE (PAIR TRUE NIL SECOND) SECOND))
            (, 'TRUE 'FALSE 'NIL 'NIL
               'TRUE 'TRUE 'TRUE 'NIL)))
; simple condition
(assert (=
    (, (COND TRUE TRUE FALSE) 
       (COND FALSE TRUE FALSE))
    (, 'TRUE 'FALSE)))
; number nil? conditions
(assert (=
    (, (COND (NIL? (NUM 0)) TRUE FALSE)
       (COND (NIL? (NUM 1)) TRUE FALSE)
       (COND (NIL? (NUM 10)) TRUE FALSE))
    (, 'TRUE 'FALSE 'FALSE)))
; nil tail/head pair condition
(assert (=
    (, (COND (NIL? (TAIL (PAIR (NUM 1) NIL))) TRUE FALSE)
       (COND (NIL? (HEAD (PAIR (NUM 1) NIL))) TRUE FALSE))
    (, 'TRUE 'FALSE)))

Church numerals shorthands


In [22]:
; church numeral general generator, without arguments
(assert (= (NUM 3) "(L x y , (x (x (x y))))"))
; church numeral, general generator, with arguments
(assert (= (NUM 3 m n) "(m (m (m n)))"))
; church numeral, zero
(assert (= (ZERO) "(L a b , b)"))
; church numeral, zero with arguments
(assert (= (ZERO a b) 'b))
;(assert (= (, (ZERO) (ZERO a b) (ONE) #𝜆(TWO x y) (THREE m n))
           ;('(L a b , b)', 'b', '(L x y , (x y))', '(x (x y))', '(m (m (m n)))')
;           (, "(L a b , b)" "b", "(L x y , (x y))" "(x (x y))" "(m (m (m n)))")))

Logic operator shorthands


In [23]:
; and tests
(assert (=
  (, (AND TRUE TRUE) (AND TRUE FALSE)
     (AND FALSE TRUE) (AND FALSE FALSE))
  (, 'TRUE 'FALSE 'FALSE 'FALSE)))
; or tests
(assert (=
  (, (OR TRUE TRUE) (OR TRUE FALSE)
     (OR FALSE TRUE) (OR FALSE FALSE))
  (, 'TRUE 'TRUE 'TRUE 'FALSE)))
; not tests
(assert (= (, (NOT TRUE) (NOT FALSE)) (, 'FALSE 'TRUE)))
; xor tests
(assert (= 
  (, (XOR TRUE TRUE) (XOR TRUE FALSE)
     (XOR FALSE TRUE) (XOR FALSE FALSE))
  (, 'FALSE 'TRUE 'TRUE 'FALSE)))
; logic condition
(assert (= (COND (AND (NOT (XOR FALSE FALSE)) (OR TRUE FALSE)) TRUE FALSE) 'TRUE))
; eval read str
(assert (= (eval (read-str "(TRUE)")) "(L a b , a)"))
; less or equal
(assert (= (, (LEQ? ONE TWO) (LEQ? TWO ONE)  (LEQ? ONE ONE) 
           (, 'TRUE 'FALSE 'TRUE))))
; equal
(assert (= (, (EQ? ONE TWO) (EQ? TWO ONE)  (EQ? ONE ONE) 
           (, 'FALSE 'FALSE 'TRUE))))

In [24]:
; math operations
; next, inc, successive
(assert (= #Ÿ(SUCC ONE) "(x (x y))"))
; add is same as succ
(assert (= (ADD ONE) "(x (x y))"))
; infix notation
(assert (= (ONE ADD ONE ADD ONE) "(x (x (x y)))"))
; previous, dec, predecessive
(assert (= (PRED THREE) "(x (x y))"))
; previous, dec, predecessor, with arguments
(assert (= (PRED THREE a b) "(a (a b))"))
; nested predecessor
(assert (= (PRED (PRED (PRED FOUR))) "(x y)"))
; previous + next is same
(assert (= #Ÿ(SUCC (PRED TWO)) "(x (x y))"))
; previous + next is same for zero
(assert (= (PRED (SUCC ZERO)) 'y))
; but previous + next is one for zero!
(assert (= #Ÿ(SUCC (PRED ZERO)) "(x y)"))
; sum two values
(assert (= #Ÿ(SUM TWO TWO) "(x (x (x (x y))))"))
; substract two x from y
(assert (= (, (SUB ONE TWO) (SUB ONE ONE) (SUB TWO ONE))
           (, "(x y)" 'y 'y)))
(assert (= (, #Ÿ(EXP TWO TWO) #Ÿ(EXP TEN ZERO) #Ÿ(EXP ZERO ZERO))
           (, "(x (x (x (x y))))" "(x y)" "(x y)")))
(assert (= (, #Ÿ(PROD ZERO ONE a b) #Ÿ(PROD ONE ONE a b) #Ÿ(PROD TWO TWO a b))
           (, 'b "(a b)" "(a (a (a (a b))))")))
; self application
(assert (= (SELF (L x , x) 1) 1))
; self application, fixed point
;count down to zero
(assert (= (SELF (L f n , (COND (ZERO? n) ZERO (f f (PRED n)))) THREE) 'ZERO))
; count down to one with lesser or equal comparison
(assert (= (SELF (L f n , (COND (LEQ? n ONE) n (f f (PRED n)))) FOUR) "(x y)"))
; count down to one with equal comparison
(assert (= (SELF (L f n , (COND (EQ? n ONE) n (f f (PRED n)))) FOUR) "(x y)"))

Math function shorthands


In [25]:
; summation sequence, with plain number
(assert (= (SUMMATION (L x y , (x (x (x y))))) "(x (x (x (x (x (x y))))))"))
; summation sequence, with number macro form
(assert (= (SUMMATION THREE) "(x (x (x (x (x (x y))))))"))
; product sequence, with plain number
(assert (= (FACTORIAL (L x y , (x (x (x y))))) "(x (x (x (x (x (x y))))))"))
; product sequence, with number macro form
(assert (= (FACTORIAL THREE) "(x (x (x (x (x (x y))))))"))

Infinite loop


In [26]:
; self application recursive loop
(setv result (L x , (x x) (L x , (x x))))
(assert (none? result))


maximum recursion depth exceeded while calling a Python object for lambda expression: (x , (x x) (L x , (x x)))

The MIT License

Copyright (c) 2017 Marko Manninen