# Introduction

So far, we have been able to build in
multi-argument
handling,
booleans, numerals, arithmetic,
equality and lists
all while staying in the Pure λ-Calculus. However, it is convenient to introduce
primitives like numbers and booleans when working on more complicated examples
in order to remove some extra cognitive steps. As an examples, which takes fewer
steps to recognize: `2`

or the return value of `scc(scc(0))`

?

In this post, I describe the means of converting some of the strictly pure
λ-calculus primitives to a more common numeric and boolean representations that
Pierce calls λNB - which is his name for the *enriched* λ-calculus. I will also
detail how to convert the other way from λNB→λ.

# Boolean

As a reminder, the Church boolean `tru`

and `fls`

are defined:

```
tru = λt. λf. t
fls = λt. λf. f
```

## Church boolean → Boolean

To convert from λ→λNB we simply apply the λ-expression to `true`

and `false`

:

```
realbool = λb. b true false
```

```
# realbool = λb. b true false
realbool = lambda b: (b)(True)(False)
>>> realbool(tru)
True
>>> realbool(fls)
False
```

## Boolean → Church boolean

In the other direction, λNB→λ, we use an `if`

expression:

```
churchbool = λb. if b then tru else fls
```

```
# churchbool = λb. if b then tru else fls
churchbool = lambda b: (tru) if b else (fls)
>>> realbool(churchbool(False))
False
>>> realbool(churchbool(True))
True
```

# Equality

Just like we were able to build higher level equality functions using Church booleans, we can do higher level conversions as well. As a reminder of the definition of equality:

```
equal = λm. λn. and (iszro (m prd n))(iszro (n prd m))
```

## Church equality → Equality

```
realeq = λm. λn. (equal m n) true false
```

```
# realeq = λm. λn. (equal m n) true false
realeq = lambda m: lambda n: (equal(m)(n))(True)(False)
>>> realeq(c1)(c1)
True
>>> realeq(c1)(c2)
False
```

## Equality → Church equality

```
churcheq = λm. λn. if equal m n then tru else fls
```

```
# churcheq = λm. λn. if equal m n then tru else fls
churcheq = lambda m: lambda n: (tru) if m == n else (fls)
>>> realbool(churcheq(3)(3))
True
>>> realbool(churcheq(3)(2))
False
```

# Numbers

I have already been converting Church numerals to numbers in my previous posts
using the `(lambda n: n+1)(0)`

function, here we will define it as a callable
function. Church numerals are defined as:

```
scc = λn. λs. λz. s (n s z)
c0 = λs. λz. z
c1 = scc c0
c2 = scc c1
c3 = scc c2
```

## Church numeral → Natural number

```
realnat = λm. m (λx. succ x) 0
```

```
# realnat = λm. m (λn. succ n) 0
realnat = lambda m: (m)(lambda n: n + 1)(0)
>>> realnat(c2)
2
>>> realnat(times(c2)(c3))
6
```

## Natural number → Church numeral

This is more complicated and possible conversions require methods that I have not covered yet. I will revisit this when I post about Recursion.