The Last Infinity

Arithmetical theorems with λ Calculus

Shubham Jain — Thu, 09 Feb 2017 00:00:00 GMT

In this post, I will introduce basic arithmetic with the lens of Lambda Calculus and try to derive some theorems about natural numbers.

We know what it means when a function applies to a number, but what happens when numbers themselves start behaving like functions? Let's start with this. Suppose there is some function $f$. If this function $f$ is applied $n$ number of times to $x$, then we can notate it by

$$\underset{\text{n times}}{\underbrace{f(f(..f}}(x))) \equiv f^n(x)$$ where $n$ is a natural number.

So we can say
$$\begin{align}
f^1(x) &= f(x), \\
f^2(x) &= f(f(x)), \\
f^3(x) &= f(f(f(x)))
\end{align}$$ and so on..

What if $n$ is $0$? $f$ is applied $0$ number of times to $x$. Hence

$$f^0(x) = x$$

Before moving ahead, Let me tell you how a function application is written as lambda term.
And the rule is simple, we omit the parenthesis around "$x$" in "$f(x)$" and write it as just "$f\ x$".

Let's now write $f^n(x)$ in lambda notation, i.e.
$$\begin{align}
f^n(x) &\equiv \overline{n}\ f\ x \\
&or \\
\overline{n}\ f\ x &\equiv \underset{\text{n times}}{\underbrace{(f(f..(f}}\ x))) \label{n1} \tag{n1}
\end{align}$$

What is $\overline{n}$ here? And how to read the expression $\overline{n}\ f\ x$?

$\overline{n}$ (which is $n$ with bar on top) is Church numeral function associated with the natural number $n$.
$\overline{n}\ f\ x$ should be read as $(\overline{n}\ f)\ x$ because application in lambda notations is left-associative. Here $\overline{n}$ is being applied to $f$, which after application returns a function that gets applied to $x$. So $\overline{n}$ is behaving like a higher order function or operator. See examples below:

$$\begin{align}
\overline{0}\ f\ x &= x, \\
\overline{1}\ f\ x &= (f\ x), \\
\overline{2}\ f\ x &= (f\ (f\ x))
\end{align}$$
and so on..

We can constructively create these numerals by Peano's axioms which states:

0 is a natural number.
If $n$ is a natural number, then $n^{+1}$ or $Succ(n)$ is also a natural number.
So these axioms states then we can construct all natural numbers using $0$ and $Succ$.

Let's write functional definitions for lambda terms associated with $0$ and $Succ$ (which are isomorphic to Peano's first two axioms).
$$\begin{align}
\overline{0}\ f\ x &:= x \label{1} \tag{1} \\
Succ\ \overline{n}\ f\ x &:= f\ (\overline{n}\ f\ x) \label{2} \tag{2} \\
\end{align}$$

You can simply understand the above definition of $Succ$ from following:

Since
$$\underset{\text{n+1 times}}{\underbrace{f(f(..f}}(x))) \equiv f(\underset{\text{n times}}{\underbrace{f(f(..f}}(x))))$$
hence
$$(Succ\ \overline{n})\ f\ x = f\ (\overline{n}\ f\ x)$$
and if we just omit the parenthesis, we obtain \eqref{2}
$$Succ\ \overline{n}\ f\ x = f\ (\overline{n}\ f\ x)$$

Using these constructive terms we can obtain numerals for all natural numbers:
$$\begin{align}
\overline{1} \equiv Succ\ \overline{0} \\
\overline{2} \equiv Succ\ \overline{1} \\
\overline{3} \equiv Succ\ \overline{2} \\
\overline{4} \equiv Succ\ \overline{3}
\end{align}$$

and so on..

I'll omit the bar on top of Church numeral terms from now on. So you should consider all numbers to be church numerals by default in expressions below.

Let's check what $2\ f\ x$ comes out to be?

$$\begin{align}
2\ f\ x & = Succ\ 1\ f\ x &&\text{(using definition of 2)} \\
& = f\ (1\ f\ x) &&\text{(using definition of Succ)} \\
& = f\ (Succ\ 0\ f\ x) &&\text{(using definition of 1)} \\
& = f\ (f\ ( 0\ f\ x)) &&\text{(using definition of Succ)} \\
& = f\ (f\ x) &&\text{(using definition of 0)} \\
\end{align}$$

which is it ought to be.

Addition

Can we define addition function over these numerals?

We know that
$$Succ\ m = m+1$$
and
$$m+n = (((m\ \underset{\text{n times}}{\underbrace{+1) +1)\ .. +1)}}$$
So
$$Plus\ m\ n = \underset{\text{n times}}{\underbrace{(Succ\ (Succ\ ..(Succ\ }}m)))$$
Hence by \eqref{n1}
$$Plus\ m\ n := n\ Succ\ m \tag{3}$$

Some proofs

$$\begin{align}
Plus\ m\ 0 = 0\ Succ\ m = m \implies m + 0 = m \label{4} \tag{4}
\end{align}$$

$$Succ\ m\ Succ\ n = Succ\ (m\ Succ\ n) \implies n + (m^{+1}) = (n + m)^{+1} \tag{5}$$

We have seen "$m + 0 = m$".
Let's try to prove "$0 + m = m$" by induction
Hypothesis: $m\ Succ\ 0 = m$
Case: $m = 0$
$$\begin{align}
Plus\ 0\ 0 = 0 &&\text{(using \eqref{4})}
\end{align}$$
Case: $m = Succ\ n$
$$\begin{align}
Plus\ 0\ (Succ\ n) & = (Succ\ n)\ Succ\ 0 && \text{(using definition of Plus)} \\
& = Succ\ n\ Succ\ 0 && \text{(omitting parenthesis)} \\
& = Succ\ (n\ Succ\ 0) && \text{(using definition of Succ)} \\
& = Succ\ n && \text{(using induction hypothesis)}
\end{align}$$
Hence
$$\begin{align}
\begin{split}
Plus\ 0\ m & = m \\
or & \\
m\ Succ\ 0 & = m
\end{split} \label{6} \tag{6}
\end{align}$$

Composition function

The composition function "$\circ$" is an infix operator and is defined by

$$Compose\ f\ g\ x \equiv (f\ \circ\ g)\ x := f\ (g\ x) \label{7} \tag{7}$$

Multiplication

Let's define function for multiplication over numerals
We know that
$$m\ \times\ n = 0\ \underset{\text{n times}}{\underbrace{+\ m\ +m\ +\ ..\ +m}}$$
So
$$\begin{align}
Mult\ m\ n & = \underset{\text{n times}}{\underbrace{((m\ Succ)\ ((m\ Succ)..((m\ Succ)}}\ 0))) \\
& = n\ (m\ Succ)\ 0 && \text{(by notation \eqref{n1})}\\
& = (n\ \circ\ m)\ Succ\ 0 && \text{(using \eqref{7} Composition operator def.)} \\
& = (n\ \circ\ m) && \text{(using \eqref{6} ‘m Succ 0 = m')}
\end{align}$$

Hence

$$\begin{align}
Mult\ m\ n &= n\ \circ\ m \label{8} \tag{8}
\end{align}$$

Multiplication of two numerals is just the composition of them.

Power

Let's define power (exponentiation) function for numerals

We know that if $n$ is a numeral then
$$\begin{align}
\overline{n}\ f\ x &\equiv \underset{\text{n times}}{\underbrace{(f\ (f\ (..(f}}\ x))) \\
&= \underset{\text{n times}}{\underbrace{(f\ \circ f\ \circ\ ..\ \circ\ f)}}\ x && \text{(using \eqref{7} definition of Composition operator)}
\end{align}$$

hence we can say, (by omitting the $x$ in above equation)
$$\begin{align}
\overline{n}\ f \equiv \underset{\text{n times}}{\underbrace{(f\ \circ f\ \circ\ ..\ \circ\ f)}} \label{9} \tag{9}
\end{align}$$

Again, by definition of power
$$m^n = \underset{\text{n times}}{\underbrace{m\ \times\ m\ \times\ ..\ \times\ m}}$$

Hence we can define $Power$ function as
$$\begin{align}
Power\ m\ n &= \underset{\text{n times}}{\underbrace{m\ \circ\ m\ \circ\ ..\ \circ\ m}} && \text{(using \eqref{8} definiion of Multiplication)} \\
&= (n\ m) && \text{(using \eqref{9})}
\end{align}$$

Hence
$$\begin{align}
Power\ m\ n = n\ m \label{10} \tag{10}
\end{align}$$

Power operation for two numerals is just the application between them.

Insights

Let's define identity function
$$I\ x = x \tag{11}$$

We know that
$$\begin{align}
0\ n\ x = x && \text{(by definition of 0)}
\end{align}$$
hence, $(0\ n)$ must be equal to Identity function $I$ so that appying $x$ to it returns $x$. So
$$0\ n = I \label{12} \tag{12}$$

Again, we know that
$$\begin{align}
&& 1\ f\ x &= f\ x && \text{(by definition of 1)} \\
or && 1\ f &= f && \text{(omitting x both side)}
\end{align}$$
hence $1$ is nothing but Identity function $I$
$$1 = I \label{13} \tag{13}$$

\eqref{12} & \eqref{13} implies
$$0\ n = 1 \tag{14}$$
If we see above equation in context of \eqref{10} then it states $Power\ n\ 0 = 1$ or arithmetically

$$\bbox[10px,border:1px solid #777]
{n^0 = 1}
$$

What a classical result!

More theorems?

By composition operator definition \eqref{7},

$$(l\ (m\ n)) \equiv (l\ \circ\ m)\ n$$

If $l$, $m$ and $n$ are numerals then (by \eqref{8} and \eqref{10}) above equation is equivalent to

$$\begin{align}
Power\ (Power\ n\ m)\ l \equiv Power\ n\ (Mult\ m\ l) \label{15} \tag{15}
\end{align}$$

or arithmetically,

$$\bbox[10px,border:1px solid #777]
{(n^m)^l = n^{m\ \times\ l}}
$$

Everything is making sense!! :D

Let's do same in Haskell interactive shell

Launch ghci

Here in shell, we'll define arithmetical operations given by above definitions and do computations using them.

let zero f x = x
let succ n f x = f (n f x)

let one = succ zero
let two = succ one
let three = succ two
let four = succ three

let plus m n = n succ m
let mult m n = n . m
let power m n = n m

let convert n = n (+ 1) 0

We've defined convert function to convert church numeral (which is a function) to number so that we can confirm our computation.

Let's do some computations using defined functions. (in ghci shell)

Prelude> convert (plus two three)   -- 2 + 3
5
Prelude> convert (mult two three)   -- 2 x 3
6
Prelude> convert (power two three)  -- 2 ^ 3
8

Prelude> convert (four . three)     -- 3 x 4
12
Prelude> convert (two three)        -- 3 ^ 2
9
Prelude> convert (three two two)    -- 2 ^ (2 ^ 3)
256

So we saw that, arithmetic operations can be defined in untyped Lambda Calculus without using any prior definition if natural numbers are treated as Church numerals.

An introduction to functional programming

Shubham Jain — Sun, 16 Aug 2015 00:00:00 GMT

There are plenty of other tutorials and posts on functional programming. This post takes an approach to give the underlying theory behind it. I hope you find it enlightening!

There are two major sets of programming languages which call themselves to be following functional paradigm. One is LISP-style and another is ML-style. There are many similarities but still quite differences between these two sets of languages. In this post, I'll be talking about the later one. The programming languages which come under ML-style are ML, OCaml, Haskell, Scala, Rust etc. I'll be using Haskell for demonstration because of it's style of purity.

Let's start!

What is Term?

Informally saying a term can be anything like

12                -- integer
'a'               -- char
3 + 8             -- sum of two integers
[1, 2, 3, 4]      -- list of integers
Int               -- a type
"Hello World!"    -- string
String            -- another type

It can be Data or Type. I just gave these examples so that you can relate the known entities to this thing that I am introducing. But before a formal introduction of Term you need to understand what Application is. There is application between f and x when you write f(x) in any imperative language e.g. c++, Java etc. Yes, you see it right, it's Function application, but here Application is not limited to function application only, It's more fundamental than this as you will see. The syntax for Application in Haskell is

f x

Yes, no parenthesis at all! You can argue why such syntax is used, just wait and you will see a lot of generality is achieved by using such syntax. Now let me introduce one rule for construction of Term that is if a is a term and b is a term then a b is also a term (* conditions apply). I'll tell you about those conditions later in this post. For now, I can give you only this information about terms till we get to the end of Computation section.

What is Arity?

Arity is the number of arguments or operands a function takes e.g. the addition function add has arity 2 which can be defined in Python by

def add(x, y):
    return x + y

In functional programming, not only functions but all terms have arity (zero or greater) since all functions are terms too. When constructing a term with Application the former term must have a non-zero arity i.e. in term f x, term f must have a non-zero arity.

In Haskell, all terms have arity of either zero or one and so all functions. Now you must be asking how functions with arity greater then one will be applied to its operands e.g. the add function defined above in python. Here comes the concept of Currying. Functions are "first class values" so functions may be used as the inputs, or be returned as output from other functions. Functions taking or returning functions are called "Higher order functions". Function calling in imperative languages e.g. add(x, y) can be written as add x y in Haskell and since application is left-assosiative, the term add x y should be taken as (add x) y. That means the add function applies to first argument x which returns another function which again takes the argument y and then returns the addition x + y. This is called Currying. The same add function can be defined in Python using currying style by

def add(x):
    def add_inner(y):
        return x + y
    return add_inner

The currying version of calling add function in Python would be add(3)(4) which is equivalent to add 3 4 in Haskell.

Computation

In start of section What is Term? I gave you some examples of term. Which examples do you find to be reducible to another term (able to change into a term with simpler form) ?

Only one example, 3 + 8, which is reducible to term 11. And reduction is the key to computation.

You just give computer a term and it reduces that term to the level where it can not be reduced further. This is the ideal philosophy of computation in functional programming. So there can be terms which can't be reduced further (all other terms in the example). Different kind of models can be made to specify the rules of reductions into a language. The ML-style functional programming languages follow a constructive model containing following rules:

A term is reducible or non-reducible. If it's non-reducible then it is said to be in its normal form.
A term can be either in application form or not. Recall that the term a b is in application form. Reducibility of a term in application form a b, depends only on first term a. And the term a can be either a function or a constructor.
If a is a function of non-zero arity, then a b is reducible, hence term a b is not in normal form. (Functions having zero arity i.e. functions which take no argument are used for computations with side effects only. A function having no side effect is called a pure function and I'll talk about them only in this article.)
Else if a is a constructor of non-zero arity, then a b is not reducible. And a b is in its normal form.
A constructor of zero arity is non-reducible hence in normal form. It's also called a nullary constructor or constant.

Constructor

Constructors in functional programming is totally a different concept than what constructors are in any imperative language like C++ or Python. From the last section, we can fetch the definition of Constructor. A constructor is a term that is always in its normal form and it can never be reduced further. Either it has zero arity that means it's a constant term and no other term can be applied to it, or it has arity greater than zero and new terms can be made by the application of itself and other terms. The new term made through the application of a constructor and another term is also in its normal form.

Data and Types

The term is leveled into many categories called Data, Type, Type of types (a.k.a. Kind in Haskell) and so on. In some programming languages, there are only two levels, data and type e.g. 4 is data and int is its type in C programming language. In Haskell, there are three levels of terms upto Kinds. In some programming languages, the levels are collapsed into single level e.g. in Python everything (data or type) is an object and treated equally. In functional programming, "every term has type" and the term representing the type of a term belong to the next level w.r.t. the level of that term. As of now in Haskell, you can deal with only type of data and type of types (which are kinds) not further. Constructors and functions also belong to these levels since they are terms. If a constructor is used to construct some data then it's called Data constructor otherwise if it is used to construct a type then it's called Type constructor. Haskell has full support for data level functions and some recent support for type level functions. There is one rule regarding levels while constructing a term using application that is term a b can be constructed from terms a and b only if a & b both belong to same level. Then the term a b belongs to same level too.

Algebraic data types

A program in Haskell, contains all the declarations or definitions of constructors and functions. Since all terms have types, a particular type term can belong to some data terms which can be constructed with some data constructors only. It is done using Data declaration in which the programmer specifies the type constructor and all the data constructors which can be used to construct a data for that type. The type and data constructors may have zero or more arguments. Data declaration starts with keyword data. Here's an example of data declaration of Bool type which is defined in the standard library

data Bool = True | False

In data declaration, the part which comes after data and before = specifies the type constructor and parts which come after = and are separated by | symbol, specifies the data constructors which can be used to construct the data terms of that type. The | should be read as "or". In this example, the type constructor Bool is a nullary type constructor with two nullary data constructors True and False which behave like constants. A variable having Bool value can be declared with following syntax.

x :: Bool   -- It tells the compiler that x has type `Bool`
x = True    -- Here the data `True` of type `Bool` has been bound to x

There's no need of first statement in above example that is type declaration of variable x. Haskell can infer it's type by seeing second statement of assignment. I wrote it just to keep things clarified.

Here is another example to define Color type whose data has information of values of all three color components Red, Green and Blue.

data Color = RGBColor Int Int Int     -- declaring the Color type

gray :: Color
gray = RGBColor 128 128 128

In this example, the type Color has only one data constructor RGBColor and RGBColor Int Int Int in data declaration means it can have 3 integer arguments to carry values of red, green and blue.

These types are called Algebraic data types because these types follow similar operations to algebraic operations sums and products while defining their data constructors. The Bool type's data constructors True, False were written in sum form (sum means "or" here) while the Color's data constructor RGBColor was written in product form in which it takes 3 integer values which can be perceived as product of 3 integers (product means "combination" here). Here's an example of data type which has both sum and product form in its data constructors.

data Shape = Circle Float Float Float | Rectangle Float Float Float Float

And different shapes can be defined by

circle :: Shape
rect :: Shape

circle = Circle 1 1 0.5    -- Circle centered at (1,1) with radius 0.5
rect = Rectangle 4 5 3 2   -- Rectangle centered at (4,5) with width = 3 and height = 2

You can see here how variables of type Shape can have value in either of two forms or variants with data constructors 'Circle' and 'Rectangle'. In this way, algebraic data types provide a more general model of relation between type and data than the model given by object oriented languages through relation between class and instances.

Let's define data type for natural numbers. A natural number is one of the values in {0,1,2,3...} . If we recall the Peano axioms then its two axioms state following:

0 is a natural number.
For every natural number n, successor of n i.e. (S n) is a natural number.

So we use above axioms to construct natural number.

data Nat = Zero | Succ Nat

It's a recursive definition as the second data constructor Succ (read as "successor of") takes an argument of same type Nat. A data type defined in recursive way is called Recursive or Inductive data type. Here's how you define some initial natural numbers using this scheme.

one :: Nat
one = Succ Zero

two :: Nat
two = Succ (Succ Zero)

three :: Nat
three :: Succ (Succ (Succ Zero))

-- And so on...

Functions

A function takes an argument and returns a result. Let's define a function that takes an integer and returns the square of it.

square :: Int -> Int   -- the type declaration of square function
square x = x * x       -- the function definition of square

y = square 5           -- function square is being called/reduced here. `y` stores 25

We have a new syntax in the type of function square. The type Int -> Int tells that any term having this type takes an integer and returns an integer. Before going ahead, let me tell you the most important rule of application that is

Term a can be applied to term b of type B if and only if a has type B -> C where C can be any other arbitrary type. Then the type of term a b would be C. (The term a can be a function or a constructor as well)

Lets define the currying version of add function in Haskell that I defined earlier in Python.

add :: Int -> Int -> Int
add x y = x + y

w = add 7 8  -- w stores 15

f = add 3    -- f is a partial function having type `Int -> Int`
z = f 5      -- z stores 8

Now you must be asking how terms like x * x or x + y get reduced further. It's because the operators * and + are infix operators hence any term in form a + b is taken as (+) a b by compiler. And (+) and (*) are actual functions which with 2 arguments get reduced to a number. In fact -> is an infix operator too which is actually a type constructor. Hence type A -> B can be taken as (->) A B.

The operator -> is right associative hence the type of function add should be taken as Int -> (Int -> Int) in infix notation. Now it should be clear why the type of term f is Int -> Int. And since the term add 7 8 is taken as (add 7) 8, the same partial function is made while evaluating add 7 and then it gets applied to 8 and returns 15. This is how currying works.

Constructor terms also have types just like functions. The type of constructors can be infered from the data declaration. Hence in declaring Nat type by data declaration

data Nat = Zero | succ Nat

The constructors Zero and Succ are understood as

Zero takes no other term for application and already of type Nat. That is to say Zero :: Nat.
Succ takes a term of type Nat and returns a Nat. Hence its type should be Nat -> Nat.

Pattern matching

Pattern matching is a concept which can't be avoided when a programming language has the feature of algebraic data types. This concept is used with function definitions. A function is a term that takes data of particular type and returns data of another type but if the input data can have multiple variant forms due to different data constructors given in data declaration of that input type then that function has to deal will each variant of that type separately while defining its own definition.

The rule of pattern matching is simple one that any argument to a function should be a variable or one of the variant forms for the input type. And each definition of that function is checked for pattern matching from top to bottom until one matches.

For example, the not boolean operator can be defined by pattern matching in following way

not :: Bool -> Bool

not True  = False
not False = True

x = not False    -- `not False` matches with the second definition
                 -- of `not` and hence reduces to `True`

Let's define the add function for Nat data type that we defined earlier using pattern matching.

add_nat :: Nat -> Nat -> Nat

add_nat Zero y      = y
add_nat (Succ x) y  = add_nat x (Succ y)    -- it's a recursive definition 

-- lets's add 2 and 1 and store it in x
x = add_nat (Succ (Succ Zero)) (Succ Zero)  

-- add_nat (Succ (Succ Zero)) (Succ Zero) reduces in following steps

-- add_nat (Succ (Succ Zero)) (Succ Zero)
-- add_nat (Succ Zero) (Succ (Succ Zero))    -- using second definition
-- add_nat Zero (Succ (Succ (Succ Zero)))    -- using second definition
-- (Succ (Succ (Succ Zero)))                 -- using first definition

-- which is nothing but 3

Generics

Till now, the above examples introduced data declarations of nullary type constructors only e.g. Bool, Color, Shape and Nat. These nullary types are also called concrete types. Since every term has type, what is the type (or I should say kind) of all concrete types? Answer is *. What! a star? Yes, the * is the type (kind) of all concrete types and this term belongs to the Kind level.

What would be the type constructors with arity greater than zero? Let's define such a type

data List a = Nil | Cons a (List a)

Here's what you infer from this data declaration:

List a is a concrete type for some concrete type a. Hence type (kind) of term List would be * -> *. Here, the type constructor List is not a concrete type. The variable type term a can be replaced by any concrete type term in List a to construct a list type e.g. List Int, List Bool, List Nat or even List (List Int).
Nil :: List a
Cons :: a -> (List a) -> (List a)

Here's how you make a term of type List Int:

list_of_integers :: List Int
list_of_integers = Cons 1 (Cons 4 (Cons 5 Nil))

If you know C++, then you know about template classes and functions. Or in Java, you'll be familiar with generics in it. In C++ or Java, a similar declaration of a variable of type 'list of integers' would be

list list_of_integers;

Actually there is no such type list in C++ or Java. Instead there is a vector class. I used it just for analogy.

Here you can see that list in C++ or Java is nothing but a type level application between terms list and int, which is just list int in Haskell.

In Haskell, there is already a pre-defined list type with different symbols used for constructors List, Nil and Cons in our example. Those are

In type level, ([]) is type constructor. Hence [Int], [Bool] are concrete types. [a] is syntactic sugar for ([]) a. Hence [Int] is actually ([]) Int.
In data level, [] is Nil data constructor. Haskell can distinguish the role of [] because it knows where it is being used, in type level or data level.
The data constructor (:) is replacement for Cons. (:) is an infix operator and is right associative.

Hence a variable term of type [Int] can be defined in Haskell by

list_of_ints :: [Int]
list_of_ints = 1:4:5:[]

There's another syntactic sugar for a:b:c:d:[] in Haskell, that is [a, b, c, d]. So above list assignment can be written simply

list_of_ints :: [Int]
list_of_ints = [1, 4, 5]

So now you know what magics Haskell is doing when you write a list in notation [a, b, c, .. g, h].

There's a lot more to be told about functional programming but I am afraid that the post has already gone long, so here I conclude it. The functional programming has its roots in Lambda calculus which is a mathematical framework for computation and Type theory. I have borrowed many concepts from these theories into this post, still many things are left as they can not be covered in a single post. In future I'll be writing on them, so stay tuned!