Lambda Calculus Live Tutorial with Klipse: Boolean Algebra
source link: https://blog.klipse.tech/lambda/2016/07/24/lambda-calculus-2.html
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.
Lambda Calculus Live Tutorial with Klipse: Boolean Algebra
Jul 24, 2016 • Yehonathan Sharvit
In our previous article, we showed how the numbers are represented in lambda calculus.
The purpose of this article is to show how we represent boolean values in lambda calculus. And to show the code of the basic boolean operations: negation, conjunction and disjunction a.k.a not, and and or.
We are using clojure for the code snippets - as it belongs to the LISP family, and LISP is founded on top of lambda calculus.
Setup
All the code snippets on this article are live and interactive: feel free to modify the code and it will evaluate instantaneously!
The code snippets are powered by the Klipse plugin.
First, let’s create a namespace for our journey, and refer the disp macro, from the gadjett repository on github:
xxxxxxxxxx
(ns lambda.boolean-algebra
(:require-macros [gadjett.macros :refer [disp]]))
the evaluation will appear here (soon)...
More about the disp macro in this article…
In order to load code from a github repository, we use data-external-libs attribute on the code snippet as explained here.
Definition of true and false
Here is how we define T (true) and F (false) in lambda calculus:
xxxxxxxxxx
(defn T [x]
(fn [y] x))
(defn F [x]
(fn [y] y))
xxxxxxxxxx
the evaluation will appear here (soon)...
You can see T as a 2-arity function that returns the first argument and F as a 2-arity function that returns the second argument.
As we did with numerals, we can view a lambda boolean by passing to it T and F. Like this
xxxxxxxxxx
(defn view-bool [bool]
((bool "T") "F"))
xxxxxxxxxx
the evaluation will appear here (soon)...
And it works as expected: T returns "T"
xxxxxxxxxx
(view-bool T)
xxxxxxxxxx
the evaluation will appear here (soon)...
and F returns "F":
xxxxxxxxxx
(view-bool F)
xxxxxxxxxx
the evaluation will appear here (soon)...
As we did in Numbers and Arithmetics with functions only: lambda calculus live tutorial., we are going to define the Lambda type to make the visualisation and comparison of the lambda booleans more convenient.
xxxxxxxxxx
(deftype Lambda [f]
Object
(toString [_] (str (view-bool f)))
IPrintWithWriter
(-pr-writer [this writer _] (-write writer (str (view-bool f))))
IEquiv
(-equiv [this other]
(= (view-bool this) (view-bool other)))
IFn
(-invoke [this g]
(f g)))
xxxxxxxxxx
the evaluation will appear here (soon)...
(Check here for an explanation about the code of the Lambda type.)
Now, let’s redefine T and F using Lambda type:
xxxxxxxxxx
(def T (Lambda.
(fn [x]
(fn [y] x))))
(def F (Lambda.
(fn [x]
(fn [y] y))))
xxxxxxxxxx
the evaluation will appear here (soon)...
Now, the lambda booleans are viewed properly:
xxxxxxxxxx
[T F T T F T]
xxxxxxxxxx
the evaluation will appear here (soon)...
They are invokable as functions:
xxxxxxxxxx
((T T) F)
xxxxxxxxxx
the evaluation will appear here (soon)...
and they are comparable:
xxxxxxxxxx
(= ((T T) F) F)
xxxxxxxxxx
the evaluation will appear here (soon)...
Now, we are going to build the basic boolean operations, using the definition of T and F: In a nutshell, T returns the first argument and F returns the second argument.
Keep in mind that in boolean algebra, the operations are defined by their truth tables:
x y negation(x) conjunction(x, y) disjunction(x, y) T T F T T T F T F T F F F F F T F T
Negation
xxxxxxxxxx
(defn negation [x]
(Lambda.
((x F) T)))
xxxxxxxxxx
the evaluation will appear here (soon)...
Basically, what this code says is: if x is T then return the first argument - which is F. And if x is F then return the second argument - which is T. This is exactly what the negation is supposed to do.
Let’s check that negation respects the truth table:
xxxxxxxxxx
(disp
(negation T)
(negation F))
xxxxxxxxxx
the evaluation will appear here (soon)...
Interlude about names
In real lambda calculus, we cannot name things, so the real implementation of negation is:
xxxxxxxxxx
(defn negation-lambda [x]
(Lambda.
((x (fn [x]
(fn [y] y))) (fn [x]
(fn [y] x)))))
xxxxxxxxxx
the evaluation will appear here (soon)...
It works exactly the same as negation:
xxxxxxxxxx
(disp
(negation-lambda T)
(negation-lambda F))
xxxxxxxxxx
the evaluation will appear here (soon)...
But it is is much less readable.
From now on, we will use names to make our code readable and we will keep in the back on our mind that in real lambda calculus there are no names.
You might wondering how we are going to implement recursions in a language with no names?
We will answer that in another article, when we present the Y-combinator.
Back to our boolean operations…
Conjunction
xxxxxxxxxx
(defn conjunction [x]
(Lambda.
(fn [y]
(Lambda. ((x y) F)))))
xxxxxxxxxx
the evaluation will appear here (soon)...
Basically, this code says: if x is T return y else return F. This is exactly the definition of the conjunction in logic.
Let’s check that conjunction respects the truth table:
xxxxxxxxxx
(disp ((conjunction T) T)
((conjunction T) F)
((conjunction F) F)
((conjunction F) T))
xxxxxxxxxx
the evaluation will appear here (soon)...
Disjunction
xxxxxxxxxx
(defn disjunction [x]
(Lambda.
(fn [y]
(Lambda. ((x T) y)))))
xxxxxxxxxx
the evaluation will appear here (soon)...
Basically, this code says: if x is T return T else return y. This is exactly the definition of the disjunction in logic.
Let’s check that conjunction respects the truth table:
xxxxxxxxxx
(disp ((disjunction T) T)
((disjunction T) F)
((disjunction F) F)
((disjunction F) T))
xxxxxxxxxx
the evaluation will appear here (soon)...
Let us know what you think about this lambda-calculus tutorial in the comments below….
Now you are ready to move forward to the most beautiful idea of the lambda-calculus: the Y combinator…
to stay up-to-date with the coolest interactive articles around the world.
Discover more cool interactive articles about javascript, clojure[script], python, ruby, scheme, c++ and even brainfuck!
Give Klipse a Github star to express how much you appreciate Code Interactivity.
Subscribe to the Klipse newsletter:Feel free to email me [email protected] for getting practical tips and tricks in writing your first interactive blog post.
Recommend
-
47
Note: This article assumes some introductory Haskell knowledge. Introduction Just as algebra is fundamental to the whole of mathematics, algebraic data types (ADTs) are fundamental to many common func...
-
51
I found this awesome paper “ A tutorial implementation of a dependently typed lambda calculus “, by Löh, A., C. McBride, W....
-
49
How do you condense a 30 minute talk in 5 minutes? Should you even try? These are the questions I struggled with when someone nudged me to register for the lightning talks. My talk was 30 minute long because I was to jum...
-
11
Our exploration of type systems starts quite simple, with the simply typed lambda calculus (STLC). This type system is the foundation of more complex type systems such as Haskell’s. The simply typed lambda calcu...
-
20
In the previous post, we have explored the simply typed lambda calculus (STLC), an extension of the untyped lambda calculus with simple types. In this post, we’ll take a look at the polymorphic lambda calculus ,...
-
7
Numbers and Arithmetics with functions only: lambda calculus live tutorial Jul 24, 2016 • Yehonathan Sharvit The mathematical theory behind LISP is the
-
8
Multi language live snippets with the klipse plugin by @viebel Jun 28, 2016 • Yehonathan Sharvit What is Klipse? The klipse plugin is a javascript tag that transforms...
-
9
-
10
Python for Beginners, Part 17: Boolean Algebra Jiu-JitsuApril 12th 2022 new story4Up until now in the...
-
6
Boolean Algebra in a nutshell for JS/TS programmers There are a lot of strategies that you will hear about in the Javascript community for keeping your conditionals from becoming a tangled mess. This isn't like them. This is someting diff...
About Joyk
Aggregate valuable and interesting links.
Joyk means Joy of geeK