# Notes (TILC 03/05): Conditionals

# 3 Conditionals

```
true = \x y.x
false = \x y.y
```

Why these expressions? Probably because it’s convenient to have `false`

be the same expression as `0_`

:

`false => \x y. y => \s z. z => 0_`

This matches the common convention found in imperative programming languages. We could choose to make `true`

equal zero instead, and then change all the logic functions by negating their inputs, so `(and a b)`

in the usual way becomes

`(and (not a) (not b))`

But I’m not sure if there’s any tangible benefit to doing this other than being contrarian.

## 3.1 Logical operations

`and = \x y. x y (\x y. y) => \x y. x y false`

The first parameter of `and`

returns the second parameter, if it is `true`

and `false`

if it is `false`

. The only way `And`

returns `true`

is if both parameters are `true`

.

`or = \x y. x (\x y. x) y = \x y. x true y`

Same general idea as `And`

. The first parameter selects `true`

if `true`

and `y`

if `false`

.

`not = \x. x false true`

Straightforward, it’s just flipping the order of the parameter.

## 3.2 A conditional test

`isZero = \x. x false not false`

If x is `0_`

:

```
isZero 0_ => (\x. x false not false) 0_ =>
0_ false not false =>
not false =>
true
```

If x is `1_`

:

```
isZero 1_ => (\x. x false not false) 1_ =>
1_ false not false =>
(\x y. y) not false =>
(\y. y) false =>
false
```

If x is `2_`

:

```
isZero 2_ => (\x. x false not false) 2_ =>
2_ false not false =>
(\x y. y) ((\x y. y) not) false =>
(\y. y) false =>
false
```

It doesn’t matter how many times we apply `false`

to `not`

because `false`

applied to any expression is always the Identity function.

## 3.3 The predecessor function

The predecessor function `pred`

is like the opposite of the successor function `succ`

. Instead of adding one to a number, it subtracts one from a number (the words increment and decrement are sometimes used in other contexts to describe adding or subtracting one, respectively).

Since numbers are functions that take other functions (higher-order functions), and apply them a certain number of times, predecessor can be thought of as an “apply one less time than this number” function.

Recall that `succ`

is

`succ = \n f x. f (n f x)`

Naively, we might want something that looks like this

`pred n = \n f x. (invert f) (n f x)`

where `(invert f)`

is the inverse function of `f`

:

`(invert f) (f x) = x`

But we have a problem: Not every function is invertible.

Take `false`

for example:

`false x = (\x y. y) x = (\y. y) = id`

Since `false`

of any argument `x`

is the `identity`

function, and since a function can only have one ouput for any given input, there’s no way for us to build an expression for `(invert false).`

And that means that we can build an `invert`

function that is *total*, in that it is defined over all possible inputs.

But it turns out it is possible to build a total `pred`

function, but we have to try another method. Instead of starting from `n`

and working backwards, we’ll start from `0_`

and build forwards. If we apply `succ`

`n`

-times to `0_`

, we get `n`

. So if we apply `succ`

only `(n-1)`

-times to `0_`

., /e’ll get `n - 1`

which is `pred n.`

We’ll start by building an expression that holds a pair of numbers, `a_`

and `b_`

. Suppose we just put them next to each other:

`a_ b_`

This might look fine at first, but watch what happens if we give them concrete values:

```
0_ 0_ => (\s z. z) (\s z. z)
=> \z.z
```

The numbers evaluate against each other! Let’s add an abstraction to stop the application:

`\x. a_ b_`

Okay, that stops the application, but only temporarily. If we ever apply this expression to anything, it’ll just reduce back again and throw away the values in the pair.

What we want is some way to access the two individual values in the pair.

`\x. x a_ b_`

We already have functions which will return only their first or second arguments: `true`

and `false`

. We can use these to select which element of the pair we want:

```
(\x. x a_ b_) true = a_
(\x. x a_ b_) false = b_
```

Great, we’ve got a pair! Now we need a function which we’ll call `phi`

to turn a pair of numbers `(a, b)`

into `(a + 1, a)`

`phi = \p z. z (succ (p true)) (p true)`

For example,

```
(\p z. z (succ (p true)) (p true)) (\x. x 2_ 1_) =>
(\z. z (succ ((\x. x 2_ 1_) T)) ((\x. x 2_ 1_) T)) =>
(\z. z (succ ((\x. x 2_ 1_) T)) ((\x. x 2_ 1_) T)) =>
```

Now we just need to apply `phi`

to `\x. x 0_ 0_`

, `n`

-times, and the first element will be equal to `n`

and the second will be `n - 1`

:

`\n. n phi (\z. z 0_ 0_)`

But since this function is supposed to be the predecessor, we really just want the second element:

`pred n = \n. n phi (\z. z 0_ 0_) F`

## 3.4 Equality and inequalities

A number, `x`

is greater than or equal to a number `y`

if applying predecessor `x`

-times to `y`

is 0:

`gte x y = \x y. isZero (x pred y)`

The reason this function is “greater than or equal to” and not just “equals” is that the predecessor of `0`

is `0`

.

But we can get an equals function by simply doing:

`eq x y = \x y. and (gte x y) (gte y x)`

Then, not equal is:

`neq x y = \x y. not (eq x y)`

Greater than:

`gth x y = \x y. and (gte x y) (not x y)`

Less than or equal to:

`lte x y = \x y. not (gth x y)`

Less than:

`lth x y = \x y. not (gte x y)`