Skip to content

Instantly share code, notes, and snippets.

@dpurjon

dpurjon/core-test.clj

Created September 26, 2017 20:26
Show Gist options
  • Save dpurjon/3254707dbde47896a81d3f61e50b14b0 to your computer and use it in GitHub Desktop.
Save dpurjon/3254707dbde47896a81d3f61e50b14b0 to your computer and use it in GitHub Desktop.
Download ZIP
A walktrough λ-calculus with Clojure
Raw
core-test.clj
(ns lambda.core-test
(:require [clojure.test :refer :all]))
;; A walktrough λ-calculus with Clojure
;; based on Greg Michaelson book "An introduction to to functional programming through lambda calculus"
;; !!! DISCLAIMER !!!
;; ------------------
;; This document is 100% based on Greg Michaelson's book.
;; Most examples of the book have been implemented as runnable Clojure code.
;; Comments around code state my understanding of the concepts of the book
;; in a casual and concise fashion (hard to beat the book though !).
;; So the book is a good complement of this document (probably the inverse).
;; You can buy a copy for less than $20 (it's cheap for a CS book).
;; If you are Greg Michaelson, thank you and sorry for paraphrasing.
;; Resources
;; ---------
;; http://www.inf.fu-berlin.de/lehre/WS03/alpi/lambda.pdf
;; http://www.viksit.com/tags/clojure/practical-applications-y-combinator-clojure/
;; http://www.fatvat.co.uk/2009/04/understanding-y-combinator.html
;; https://gist.github.com/z5h/5102747
;; https://stackoverflow.com/questions/45931279/how-to-implement-iteration-of-lambda-calculus-using-scheme-lisp
;; http://blog.klipse.tech/lambda/2016/08/07/pure-y-combinator-clojure.html
;; https://mvanier.livejournal.com/2897.html?nojs=1
;; !!! RANDOM TIPS !!!
;; -------------------
;; 0. If you can't read Clojure code, create a new project with Leiningen,
;; implement a recusive Fibonacci with unit tests, then come back,
;; you know enough Clojure.
;; 1. You should clone this project
;; 2. Your editor ougth to use a monospaced font
;; 3. Code is not self-sufficient, read all the comments too
;; 4. Tests like to be modified, run, created, deleted, ... that's what they are
;; meant for.
;; >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
;; >>>>>>>> OK! LET'S GO >>>>>>>>
;; >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
;; λ-calculus or "The Smallest Universal Programming Language Of The World"
;; It was introduced in 1930s by Alonzo Church.
;; It's said to be universal because any computable function can be expressed
;; through this formalism. It's equivalent to a Turing machine.
;; The lambda calculus is a system for manipulating λ-expressions
;; An <expression> is either a <name>, a <function>, or an <application>
;; This is all about abstractions :
;; - A <name> identifies an abstraction
;; - A <function> describes an abstraction
;; - An <application> specializes an abstraction (by specializing a function)
;; <name> syntax : in Clojure that would syntactically be any valid symbol.
;; Clojure a special reader notation for creating symbols : the quote, as in 'fred.
;; Otherwise, one has to rely on the symbol function, as in (symbol "33")
(deftest syntax
;; Let's say a name is a Clojure symbol :
(def ->name symbol)
(def name? symbol?)
;; Let's write some names :
(testing "names are any sequence of non blank characters"
(are [name] (name? name) ;; λ-calculus syntax :
'fred ;; fred
'legs-11 ;; legs-11
(->name "19th_nervous_breakdown") ;; 19th_nervous_breakdown
(->name "33") ;; 33
(->name "+") ;; +
(->name "-->"))) ;; -->
;; A λ <funtion> is an abstraction over a λ expression
;; in λ calculus it has the form λ<name>.<body>
;; <name> has the same definition as above and is called the function's **bound variable**
;; <body> is any <expression> (a <name>, <function> or <application>)
;; a <function> doesn't have a name, and has always one and only one argument (<name>)
;; In Clojure the syntax would be (fn [name] <body>) where <body> is a λ-expression
;; Let's write some functions :
(testing "functions"
(are [function] (fn? function) ;; λ-calculus syntax :
(fn [x] x) ;; λx.x
(fn [first] (fn [second] first)) ;; λfirst.λsecond.first
(fn [f] (fn [a] (f a))))) ;; λf.λa.(f a)
;; A function <application> has the form (<function expression> <argument expression>)
;; A function <application> is also named as a **bound pair**
;; <function expression> and <argument expression> are λ-expressions.
;; The <function expression> is said to be **applied** to the <argument expression>
;; The <function expression> should evaluate to return a function (as you'll see nearly everything is a function)
;; There are 2 methods for evaluating an expression :
;; 1) **applicative order** reduction where the expression is evaluated in place
;; Nowadays it's called **call by value**
;; Clojure uses applicative order reduction.
;; 2) **normal order** reduction where the expression evaluation is delayed until it's used
;; Nowadays it's called **call by name**, **lazy evaluation**, **call by reference**
;; Haskell uses (more or less) normal order reduction.
;; The function <application> in λ-calculus syntax is identical to the Clojure syntax
;; Conceptually it's all about manipulating expressions. In applicative order :
;; 1. Evaluate <function expression> such as you get a function λ<name>.<body>
;; 2. Evaluate <argument expression> as an <irreducible expression>
;; 3. Procede to what is called the **beta reduction** :
;; a. In the <body>, replace occurences of bound variable <name> with <irreductible expression>
;; b. remove the 'λname.' part.
;; Finally ! Let's write some applications :
(testing "applications" ;; λ-calculus syntax :
;; The simplest one :
(is (= 'x ((fn [a] a) 'x))) ;; (λa.a x) => x
;; functions equivalence is a CS problem of it's own that clojure doesn't solve.
;; A clojure function is a JVM object that implements equality as object identity equality
;; Hence, 2 functions syntactically the same are unfortunately not equals
(is (not= (fn [a] a) (fn [a] a)))
;; I said that a function does't have a name but I will allow it for 2 reasons:
;; 1) It's a syntactic sugar that avoid writing the same function definition over and over
;; Getting the full expression, is just a matter of replacing the named function by it's definition
;; 2) It solves our problem of function equality
;; Here I name the function λa.λb.a "first" with a let binding
;; but I could have used def or defn :
(let [first (fn [a] (fn [b] a)) ;; def first = λa.λb.a
identity (fn [a] a)]
(is (= first (identity first))) ;; (λa.a first) => first
(is (= identity ((first identity) first))) ;; ((λa.λb.a λa.a) λa.λb.a) =>
#__ ;; (λb.λa.a λa.λb.a) =>
#__ ;; λa.a
)))
;; recap
(def ->name symbol)
(def name? symbol?)
(deftest simple-λ-functions ;; λ-calculus syntax :
;; The functions defined here are some building blocks of a surprising
;; arithmetic that has to come in subsequent scrolls of your screen :)
(testing "IDENTITY function"
;; The identity function returns the argument to which it is applied.
;; In λ-calculus it is written λx.x
(defn identity [x] x) ;; def identity = λx.x
(is (= 'x ((fn [a] a) 'x))) ;; (λa.a x) => x
;; applied to itself, it returns itself
(let [identity-applied-to-identity (identity identity)] ;; (λx.x λx.x)
(is (= identity identity-applied-to-identity)) ;; (λx.x λx.x) => λx.x
(is (= 'x (identity-applied-to-identity 'x))) ;; ((λx.x λx.x) x) => x
))
(testing "SELF-APPLICATION function" ;; λ-calculus syntax
;; The self-application functions returns the application of its argument to its argument
;; Or, more intelligibly λ.s(s s)
(defn self-application [s] (s s)) ;; λs.(s s)
(is (= identity (self-application identity))) ;; (λs.(s s) λx.x) => λx.x
;; Applying self application to itself result in an infinite loop : the premise of a recur function
(is (thrown? StackOverflowError (self-application self-application)))) ;; (λs.(s s) λs.(s s)) => (λs.(s s) λs.(s s)) => ... => (λs.(s s) λs.(s s))
(testing "FUNCTION APPLICATION function"
;; The function application function applies a function to an argument, both passed as argument of functions
;; λfunction.λargument(function argument)
(defn function-application [function] (fn [argument] (function argument))) ;; def function-application = λfuntion.λargument.(function argument)
;; let's apply the function application function to identity and self-application :
(is (= self-application ;; ((λfuntion.λargument.(function argument)) λx.x) λs.(s s)) =>
((function-application identity) self-application))) ;; (λargument.(λx.x argument) λs.(s s)) =>
#__ ;; (λx.x λs.(s s)) => λs.(s s)
)
;; A language would be a useless language if we could't represent data in any form
;; The 3 functions described below are used to make pairs and selecting the first or the second element
;; Mind you! You won't have a handy way like [1 2] to represent a a pair of 2 numbers
;; but rather an abstraction over it (you won't get any data types, only functions).
;; Without further ado :
(testing "SELECT FIRST function"
;; A pair is abstracted over arguments of functions
;; The pair here is made of of the first argument of select-first
;; and the second argument of the function returned in the body of select-first
(defn select-first [first] (fn [second] first)) ;; def select-first = λfirst.λsecond.first
;; here we make a pair abstracted over that contains
(is (= identity ((select-first identity) apply))) ;; ((λfirst.λsecond.first λx.x) λfuntion.λargument.(function argument)) =>
#__ ;; (λsecond.λx.x λfuntion.λargument.(function argument)) =>
#__ ;; λx.x
)
(testing "SELECT SECOND function"
;; select-second is pretty much the same as select-first
(defn select-second [first] (fn [second] second)) ;; def select-second = λfirst.λsecond.second
(is (= apply ((select-second identity) apply))) ;; ((λfirst.λsecond.second λx.x) λfuntion.λargument.(function argument)) =>
#__ ;; (λsecond.second λfuntion.λargument.(function argument)) =>
#__ ;; λfuntion.λargument.(function argument)
;; select-second could also be defined as :
(let [select-second2 (select-first identity)] ;; def select-second2 = (λfirst.λsecond.first λx.x)
(is (= apply ((select-second2 identity) apply))) ;; (λfirst.λsecond.first λx.x) =>
#__ ;; (λsecond.λx.x λx.x)
#__ ;; renaming bound variable second to first and bound variable x to second leads to
#__ ;; λfirst.λsecond.second
)
)
(testing "MAKE PAIR function"
(defn make-pair [first] (fn [second] (fn [func] ((func first) second)))) ;; def make-pair = λfirst.λsecond.λfunc.((func first) second)
;; I really didn't get it the first time and was wondering "where is the pair here".
;; What we really get here after beta reduction
;; is the function (fn [func] ((func first) second))
;; where bound variables first and second are replaced by whatever you want a pair of.
;; And this function is magically a pair (with magic properties) !!
;; Let's build a pair of hands :
(let [pair-of-hands ((make-pair 'left) 'right)] ;; def pair-of-hands = ((λfirst.λsecond.λfunc.((func first) second) left) right) =>
#__ ;; (λsecond.λfunc.((func left) second) right) =>
#__ ;; (λfunc.((func left) right)
;; If we apply select-first on it, we get the left hand
(is (= 'left (pair-of-hands select-first))) ;; (λfunc.((func left) right) select-first) =>
#__ ;; ((select-first left) right) =>
#__ ;; left
;; And if we apply select-second on it, we get the right hand
(is (= 'right (pair-of-hands select-second)))
;; We just made a pair and a way of accessing elements in the purest,
;; the most abstract way that I could have ever imagined. I'm litteraly
;; fascinated and I hope you too !!!
)
)
)
;; recap :
(def identity (fn [x] x))
(def self-application (fn [s] (s s)))
(def function-application (fn [function] (fn [argument] (function argument)))) ;; def function-application = λfuntion.λargument.(function argument)
(def select-first (fn [first] (fn [second] first)))
(def select-second (fn [first] (fn [second] second)))
(def make-pair (fn [first] (fn [second] (fn [func] ((func first) second))))) ;; def make-pair = λfirst.λsecond.λfunc.((func first) second)
;; From now on I'll stop referring to the λ-calculus syntax.
;; I hope that you get the point that I'm mimicing λ-calculus syntax with a subset
;; Clojure syntax, and what I write is fundamentaly λ-calculus not Clojure.
;; As a reminder, I only use :
;; - symbols as names
;; - functions with one and only one parameter
;; - function applications
;; My only syntactic sugar (for now on) :
;; - `var` binding with `def`, `defn` and `let`
(deftest boolean-logic
;; What good a programming language could bring if we couldn't use boolean
;; expressions and if statements ?
;; Remember, this is all about abstractions and we don't have any datatype.
;; The way boolean logic is modeled is a bit tricky and I didn't get it at first :
;; Say select-first means true, and select-second means false
;; After beta reduction of the first and second argument,
;; make-pair gives a function (fn [func] ((func first) second))
;; An if statement in Clojure like `(if condition first second)`
;; is just a generic function that takes the condition as a parameter :
;; - select-first if cond is true
;; - select-second if cond is false
;; So elegant !!!
;; let's rename make-pair cond in order to make the code cleaner
(def cond make-pair)
;; let's also alias select-first and select-second
;; (true and false are reserved keywords hence the capital letter)
(def True select-first)
(def False select-second)
;; name our if statement apply-or-identity which is equivalent to
;; (fn [func] ((func 'left) 'right)
(let [left-or-right ((cond 'left) 'right)]
;; applying True selects the first branch (like a true condition)
(is (= 'left (left-or-right True)))
;; applying False selects the second branch (like a false condition)
(is (= 'right (left-or-right False)))
;; to implement the boolean operator NOT, the bound variable func of the pair
;; must be reduced to a function (fn [x] ((x False) True)) so that if x is True
;; then False is returned, and vice versa.
(def not (fn [x] ((x False) True)))
(is (= False (not True)))
(is (= True (not False)))
;; keep in mind that left-or-right is a function that takes a λ-boolean expression as parameter
(is (= 'left (left-or-right (not False))))
;; To implement the boolean operator AND, the bound variable func must have
;; 2 bound variables x and y and be equivalent to the if Clojure statement :
;; (if x y False)
(def and (fn [x] (fn [y] ((x y) False))))
(are [x y r] (= r ((and x) y))
True True True
True False False
False True False
False False False)
(is (= 'right (left-or-right ((and (not True)) True))))
(is (= 'left (left-or-right ((and True) (not False)))))
;; We implement the OR operator as (if x True y)
(def or (fn [x] (fn [y] ((x True) y))))
(are [x y r] (= r ((or x) y))
True True True
True False True
False True True
False False False)
(is (= 'right (left-or-right ((or False) (not True)))))
(is (= 'left (left-or-right ((or True) (not True)))))
;; we can now compose large boolean expressions such as
;; (not False) && (False || True)
(is (= True ((and (not False)) ((or False) True))))
;; It's quite easy to implement other operators such as NOR
;; (which can be the only building block of a complex processor but that's another story)
(def nor (fn [x] (fn [y] (not ((or x) y)))))
(are [x y r] (= r ((nor x) y))
True True False
True False False
False True False
False False True)
;; Or maybe :
(def nor2 (fn [x] (fn [y] ((x False) (not y)))))
(are [x y r] (= r ((nor2 x) y))
True True False
True False False
False True False
False False True)
;; Let's make XOR (my favorite of all boolean operators, which one is yours?)
(def xor (fn [x] (fn [y] ((x (not y)) y))))
(are [x y r] (= r ((xor x) y))
True True False
True False True
False True True
False False False)))
;; recap
(def cond make-pair)
(def True select-first)
(def False select-second)
(def not (fn [x] ((x False) True)))
(def and (fn [x] (fn [y] ((x y) False))))
(def or (fn [x] (fn [y] ((x True) y))))
(def nor (fn [x] (fn [y] (not ((or x) y)))))
(def xor (fn [x] (fn [y] ((x (not y)) y))))
;; So we have kinda IF statements and boolean expressions.
;; Guess what a computer is missing ? Numbers !
;; Did I already said we don't have any datatypes, only abstractions ?
;; So let's focus about how numbers behave, not what they are.
;; Peano's (a 19th century mathematician) defined natural recursively stating
;; each natural number has a successor and every non-zero natural number has a
;; unique predecessor.
;; This is how we'll define them in λ-calculus.
(deftest natural-numbers
;; Say 0 is the identity function
(def zero identity)
;; The succ function applied to a number n-1 builds a pair (False,n-1)
;; Each number `n` is one of those pair that encapsulates its predecessor (`n-1`).
;; Remember, a pair is a function on wich a selector can be applied
;; (`select-first` or `select-second`)
(def succ (fn [n-1] (fn [s] ((s False) n-1))))
(def one (succ zero))
(def two (succ one))
;; `zero?` tests if `n` is zero.
(def zero? (fn [n] (n select-first)))
;; zero is the identity function. So `zero` applied to `select-first` returns
;; `select-first`, and if you go to the definition of `True` above, it's
;; just an alias for `select-first`
(is (= True (zero? zero)))
;; We said a number n is a pair (False, n-1). So applying `select-first`
;; on this pair returns constantly False
(is (= False (zero? one)))
(is (= False (zero? two)))
;; The `pred` function returns the predecessor
;; We said a number n is a pair (False, n-1). So applying `select-second` on
;; it will return n-1.
(def pred (fn [n] (n select-second)))
(is (= zero (pred one)))
(is (= zero (pred (succ zero))))
(is (= one (pred two)))
;; However there is one glitch with `(pred zero)` that returns `select-second`
;; Unfortunately `select-second` is not a valid number.
(is (not= True (zero? (succ (pred zero)))))
;; So pred should return zero if it's zero, the predecessor otherwise
;; Remember `cond` builds a "generic if" where the condition is passed as parameter.
;; Here the condition is `(zero? n)`
(def pred (fn [n] (((cond zero) (n select-second)) (zero? n))))
(is (= zero (pred zero)))
(is (= zero (pred (pred zero))))
(is (= zero (pred one)))
(is (= one (pred two)))
;; note : pred can be simplified with some λ-gym
(def pred (fn [n] (((zero? n) zero) (n select-second))))
(is (= zero (pred zero)))
(is (= zero (pred (pred zero))))
(is (= zero (pred one)))
(is (= one (pred two))))
;; Recap
(def zero identity)
(def succ (fn [n-1] (fn [s] ((s False) n-1))))
(def one (succ zero))
(def two (succ one))
(def zero? (fn [n] (n select-first)))
(def pred (fn [n] (((zero? n) zero) (n select-second))))
(deftest recursion
;; recursion is the only way to loop in λ-calculus
;; Let's try to implement add in a recursive fashion
;; Adding two numbers a and b can is finding the b-th successor of a
;; So we will apply the `succ` function b times over a
;; for example 1 + 2 <=> (succ (succ 1))
;; add is a function that takes a and b as parameters
;; if b == 0 then returns a otherwise recursively call ((add (succ a)) (pred b))
(def add (fn [a] (fn [b] (((cond a) ((add (succ a)) (pred b))) (zero? b)))))
;; It looks fine but there is 2 caveats here :
;;
;; A. I use a subset of Clojure as lambda-calculus. In the subset I allow
;; the use of `def` for convenience. But lambda-calculus doesn't have such
;; facility. Here I make an **explicit recursion** : in the definition of `add`
;; I explicity call `add`. This is not allowed in lambda-calculus.
;;
;; B. Clojure is a **strict language**, it uses **applicative order**,
;; for argument evaluation. That is to say the inner `((add (succ a)) (pred b))`
;; argument is evaluated before being applied to `(cond a)`. And this inner call to
;; `add` also contains a function application where an application of `add`
;; is an argument which also contains ... until the stack blows up. BOOM !!!
(is (thrown? StackOverflowError ((add zero) zero)))
;; I could try to go for a lenghty explanation that would lead to the
;; solution. But I feel it will be a little off-topic, and I am still
;; inconfortable with some parts of the solution. Here is my personal journey
;; to the solution :
;; 0. Let's fumble, and experience those stack overflows.
;; 1. The wise people use the **Y combinator**, yeah let's do that
;; 2. But Clojure being a strict language, let's use the **Z combinator** instead
;; 3. Oh! and don't forget to wrap branches of conditional in **thunks**
;; (and wonder how your approach of using a Clojure subset as lambda calculus
;; might not be the best idea you had).
;; That probably sounds utterly difficult. It is. On the other hand it is
;; really easy to use !
;; This is the mighty Z combinator
(def Z (fn [f] (self-application (fn [s] (f (fn [arg] ((s s) arg)))))))
;; Here we define `add*`. Please notice:
;; - abstraction at the recursive call with one more parameter `recursive-fn`
;; - the thunks around the branches of conditional
(def add* (fn [recursive-fn]
(fn [a]
(fn [b]
((((zero? b)
(fn [_] a))
(fn [_] ((recursive-fn (succ a)) (pred b))))
'dummy)))))
;; Use Z combinator and `add*`
(def add (Z add*))
;; It seems to work as expected :
(is (= True (zero? ((add zero) zero))))
(is (= one ((add one) zero)))
(is (= True (zero? (pred (pred ((add one) one))))))
;; There is a lot of material on internet that describes the mental process
;; that produces this craziness. I found this one the most pleasant reading :
;; https://mvanier.livejournal.com/2897.html?nojs=1
;; And my own questionments can be found at :
;; https://stackoverflow.com/questions/46061344/how-to-implement-a-recursive-function-in-lambda-calculus-using-a-subset-of-cloju
;; Because we are awesome, it will all makes sense one day !
)
;; Recap
(def Z (fn [f] (self-application (fn [s] (f (fn [arg] ((s s) arg)))))))
(def add (Z (fn [recursive-fn]
(fn [a]
(fn [b]
((((zero? b)
(fn [_] a))
(fn [_] ((recursive-fn (succ a)) (pred b))))
'dummy))))))
(deftest alonzo-test
;; Our code becomes really hard to decypher.
;; Thanks to clojure macro's we can write our own little language called "alonzo"
;; 1. When a function has several arguments, like `add` which have 3
;; let's allow n-parameters functions instead of funtion that
;; returns function that returns function. The macro will rewrite :
;; (fn [a b c] expr) => (fn [a] (fn [b] (fn [c] expr)))
;; 2. When calling a n-parameters function, let's do a single application
;; instead of n. The macro will rewrite :
;; (f a b c) => (((f a) b) c)
(defn curryfy
"(fn [a b c] body) => (fn [a] (fn [b] (fn [c] body)))"
[fn-definition]
(let [[_ args body] fn-definition]
(reduce (fn [expr arg] (list 'fn [arg] expr))
(list 'fn [(last args)] body)
(next (reverse args)))))
(defn apply-one-arg-fn
"(f a b c) => (((f a) b) c)"
[application]
(reduce (fn [acc arg] (list acc arg))
(take 2 application)
(drop 2 application)))
(defn fn? [l] (= 'fn (first l)))
(def fn-definition? (every-pred list? fn?))
(def fn-application? (every-pred list? (complement fn?)))
(defn alonzo->lambda-calculus [l]
(clojure.walk/postwalk
(fn [%]
(clojure.core/cond
(fn-definition? %) (auto-currying %)
(fn-application? %) (apply-one-arg-fn %)
:default %))
l))
(defmacro alonzo [l] (alonzo->lambda-calculus l))
;; Let's rewrite add :
(def add
(alonzo (Z (fn [f a b]
((zero? b)
(fn [_] a)
(fn [_] (f (succ a) (pred b)))
'dummy)))))
(is (= True (zero? ((add zero) zero))))
(is (= one ((add one) zero)))
(is (= True (zero? (pred (pred ((add one) one))))))
;; it's still bloated with thunks but that's better
;; in fact, I could thunk every expression in the macro and that would look
;; very nice, but that's a horrible solution
)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment