- Work toward higher-level primitive functional programming constructs.
- Pair functions to build conditionals.
- Use Conditionals to build Boolean operations
`and, or, not`. - Numbers! Pair functions and the successor function for 0,1,2,...
- New notation simplifying function definition and
`if-then-else`. - Chap3.pdf in BB content ``lambda calculus''

Spoiler: use
`select-first` to represent TRUE and

`select-second` to represent FALSE, and a
version of
`make-pair` to build the logical
operations. Everything's a function, we need to make pieces fit
together.

C-language conditional statement:

`< condition > ? < expression >
: < expression >`

selects first expression for evaluation if condition is true, second if it is false. So to set

We can model a conditional expression with a
version of `make-pair`:

`
def cond = λ e1. λ e2. λ c.((c e1) e2)`.

`
def cond = λ e1. λ e2. λ c. ((c e1) e2)`.

The condition is the third
argument. It takes two applications to go
from

`
((cond < exp1 > ) < exp2 > )
`

to
`
λ c. ((c < exp1 >) < exp2 >)
`

Claim: If this expression is applied to
`select-first` it evaluates to `< exp1 >` and
if it is applied to `select-second` it
evaluates to

`< exp2 >`. So...

```
def true = select-first
def false = select-second
```

As in:
` if_cond ? then-action : else-action`

NOT is a unary function that should look like

`
NOT < operand > ,
`
described by truth table:
```
X NOT X
------------------
FALSE TRUE
TRUE FALSE
```

*
Written as a C conditional,* (our primary translation technique
for logic operations -- we use a pair!),

NOT is: ` X? FALSE: TRUE`.

Thus:

`
def not= λ x.(((cond false) true) x)
`

Think of
```
(cond < value if true > < value if false >
< condition a>)
```

as
a ```then-else-if`'' statement.

`
def not= λ x. (((cond false) true) x)
`

Simplify inner body:
```
(((cond false) true) x) ==
((( λ e1. λ e2. λ c. ((c e1) e2) false)
true) x) =>
(( λ e2. λ c. ((c false) e2) true) x) =>
( λ c. ((c false) true ) x) =>
((x false) true)
```

Put that back into
definition of `not`:

`
def not = λ x.((x false) true)`

We'll use this form of simplfication again:
```
(((cond false) true) x) =>...=>
((x false) true)
```

Test: NOT TRUE:
```
(not true) ==
( λ x. ((x false) true) true) =>
((true false) true) ==
(( λ first. λ second. first false) true) =>
( λ second. false true) =>
false.
```

```
X Y X AND Y
-------------------
TRUE TRUE TRUE
TRUE FALSE FALSE
FALSE TRUE FALSE
FALSE FALSE FALSE
```

---Notice that for

`
< l-operand > AND < r-operand > `,

- If left operand is TRUE, then answer depends on (is) the right operand:
- If left operand is FALSE then the final value must also be FALSE.
- AND In C with conditional
(we
*know how to do*conditionals!):`X ? Y : FALSE`. - We also know about
selector functions, and in that vein
say that if left operand is TRUE then select the right
operand, and if the left operand is FALSE, then select FALSE. Thus
define the two-argument function AND as:

`def`

and = λ x. λ y.(((cond y) false) x)

recall (then, else, if).

`def and = λx.λy.(((cond y) false) x)`

Evaluate inner body:
```
(((cond y) false) x) ==
((( λ e1. λ e2. λ c. ((c e1) e2) y) false) x) =>
(( λ e2. λ c. ((c y) e2) false) x) =>
(λ c. ((c y) false) x) =>
((x y) false),
```

This is more elegant. It's just a conditional, saying "if x is true
evaluate to y, else false", so we'll use

`def and = λ x. λ y. ((x y) false)`

Does it work? Try
`TRUE AND FALSE`:

```
((and true) false) ==
((λ x. λ y. ((x y) false) true) false) =>
(λ y. ((true y) false) false) =>
((true false) false) ==
((λ first. λ second. first false) false)=>
( λ second. false false) =>
false
```

```
X Y X OR Y
-------------------
TRUE TRUE TRUE
TRUE FALSE TRUE
FALSE TRUE TRUE
FALSE FALSE FALSE
```

Similar to AND:
`< operand > OR < operand >`

Given what we know
(conditionals, selectors) we say:

if first operand is TRUE, so is final value of OR. Else the final value is the second operand.

In C:
conditional
`X ? TRUE : Y`

With selectors: if the first operand is true, select TRUE. If the
first operand is false, select the second operand.

`def or = λ x. λ y. (((cond true) y) x)`

Simplifying as with AND leaves:

`def or = λ x. λ y. ((x true) y))`

Practice on this: `FALSE OR TRUE`.

Perhaps twisted approach I made up to help me understand this stuff. Maybe only of interest as an example of trying to reformulate concepts in possibly (or not) helpful ways.

How do we implement datatypes with constructors (e.g. `cons, zero`) , tests
(e.g. `null`, ≤), and selectors (e.g. `car, cdr`)?

I'll not even describe the general solutions by Church and by Dana Scott, but will go immediately to the specialized case of natural numbers.

We'll see three closely-related solutions to this problem.

Begin with recursive definition in terms of a "first" number
`zero, 0` and the *successor*function: 1 is
the successor of 0; 2 is the successor of 1, or the
successor of the successor of 0, *etc. ad infinitum*.

Once we find constructor functions for
`zero`
and successor, `succ`, then:
```
def one = (succ zero)
def two = (succ one)
def three = (succ two)...
```

Thus

```
two = (succ (succ zero))
three = (succ (succ (succ zero)))
...
```

Then of course an issue is how to use such a "unary" number representation (say to do arithmetic).

Church's encoding: use depth of expression nesting to count.
Elegant but the Predecessor(N)
function (as in `pred(three) = two`) takes O(N) to compute.

Scott's encoding: use depth of function application nesting to count. Needs different approach to arithmetic and test algorithms.

Our text uses what I call "Michaelson's encoding",
which is like Scott except a number N is nested pairs, each
of which has, if you like, a `car` with the answer to
`iszero`, (i.e. ` false`) if N>0, and the
predecessor of N as the `cdr`--
thus `cdr` of `zero` ends the "list".

See: "A tutorial introduction to the lambda calculus", Raul Rojas, FU Berlin, WS-97/98.

"Directly Reflective Meta-Programming", Aaron Stump, Computer Science and Engineering, Washington University in St. Louis, St. Louis, Missouri, USA.

Generally,
constructors can have different arity (zero:0, succ:1, cons:2,...) --
Church implements the
recursive action (say of `cdr` or `succ`) in a way that acts like an
iterator.

We'll use natural numbers as a familiar, easy (and usual) example.
```
def zero = λs.(λz.z)
```

Now we notice that `zero` is good old `select-second`,
and that's because all the iterators of the data type are contained in
Church's encoding and we'll see that zero is the second one, formally,
and successor is the first. So the `s` and `z` in these
definitions can be thought of as "sucessor iterator (constructor)" and
"zero constructor". That's a mnemonic, not a semantics!

We can forget Church and iterators entirely (so let's do that), and think of these definitions as being entirely arbitrary.

We'll use this shorthand for functions of more than one variable:

`(λfa.(f a) p q) => (p q) `

Important: args are in same order
as their λ's, and the first one (here `f`) is substituted
first (by `p`) in evaluation, with `q` substituted
for `a` second.
```
def zero = λsz.z = λs.(λz.z)
def one = λsz.s(z)
def two = λsz.s(s(z))
...
```

So if the functions that compute successor and zero, AND the numbers
0,1,2, ... are given the two functions `succ` and
`zero`,
as parameters, then

` λsz.z` makes sense for zero and

` λsz. s(z)` literally looks like "successor of zero".

The vital successor function:
```
def succ = λw. λy. λx.(y ((w y) x))
```

Note that we can write this in shorthand (3 args; evaluate
concatenated functions left-associatively)
```
def succ = λwyx.y(wyx)
```

Let's check:
```
succ zero = (λwyx.y(wyx))(λsz.z) =>
λyx.y(λsz.z)yx) => % inner sel-2, lose y
λyx.y(λz.z)x) =>
λyx.y(x) = one
```

So far no O(1) implementation of `predecessor` has been found for this
encoding...they all involve a nested recurrence N deep to get back to
zero.

Recall
```
def one = λsz.s(z)
```

whose body `sz` is the application of the function `s`
to
`z`.

Adding two to three amounts to applying `succ` twice to three.
It turns out we can do that like this for 2+3, just concatenating
`two` with `succ` with `three`.
```
2S3 = (λsz.s(sz)) (λwyx.y(wyx))
(λuv.u(u(uv))) =>
(λwyx.y((wy)x)) ((λwyx.y((wy)x))
(λuv.u(u(uv)))) = SS3
```

Notice that addition here is done without recursive calls, but with
normal-order β-reduction, i.e. textual substitution.
There are only λs at the topmost level, so here the number of
`s`'s in the expression for 2 determined how many time the S
function is applied to 3.

Here's multiplication of `x, y`:
```
(λxyz.x(yz)) % so 2*2 is
(λxyz.x(yz))22 =>
(λz.2(2z))
```

which turns out to give four. I find it rather miraculous that these algorithms work! + I get, but * I haven't seen through yet.

As mentioned above, Church resorts to a nesting of pair functions to
allow
computation of `pred`. Here we abandon Church and go right
to the treatment in our text:
```
def zero = identity
def succ = λ n.λ s.((s false) n)
```

This choice models numbers as functions with selector arguments.
The pair function is at the bottom of it all
(definition of `succ`.)

When `succ` is applied to a number it builds a pair function
with `false` first and the original number second.
*E. g.*
```
one ==
(succ zero) ==
(λ n. λ s. ((s false) n) zero) =>
```

*1* λ s. ((s false) zero)

```
three ==
(succ two) ==
(λ n. λ s. ((s false) n) two) =>
```

So the number is represented by the level of nesting ---
sort of unary representation, in which (with *2* λ s. ((s false) two) ==
λ s. ((s false) λ s. ((s false) one)) ==
λ s. ((s false) λ s. ((s false)
λ s. ((s false) zero))).
`F` for
`FALSE`), the number 6 ``looks like'' a nested function

`F (F (F (F (F (F identity())))))`.

By the definition of `succ`, (illustrated in ONE and THREE defs),
any number looks like

`identity` (if zero) or

`λ s. ((s false) < number >)`
(if positive).

Let's try to implement unary function `iszero`.

Try sending `select-first` selector in as the argument
of a non-zero number:
```
( λ s. ((s false) < number >) select-first) =>
((select-first false) < number >) ==
(λ first. λ second. first false) < number >) =>
(λ second. false < number >) =>
false
```

If send `select-first` to `zero`:
```
zero select-first ==
(λ x. x select-first) =>
select-first ==
true
```

since true is defined as `select-first`.
So...

`def iszero = λ n. (n select-first)
`.

`pred` is the inverse of `succ`.
```
pred(one) => ... => zero
...
pred(three) => ... => two
...
```

In representation for positive numbers created by
`succ`:

*3* `λ s. ((s false) < number >)`,

`pred`
must strip off a layer of nesting and return the

`< number >`
found inside.

`select-second` applied to the rep. of line *3*
returns
the

`< number >`, (again, not unlike `cdr`).

BUT! `
def pred1 λ n. (n select-second)` isn't good enough: `zero`
has no predecessor with non-negative numbers.

Special-case hack to deal with natural (non-negative) integers and
`pred`.

- Declare zero to be its own predecessor, and thus
- add a special-purpose check to return zero as the predecessor of zero, using the equivalent of the following C conditional to implement predecessor.

```
< number > = zero ? zero :
predecessor of < number >
```

```
def pred = λ n. (((cond zero) (pred1 n))
(iszero n))
```

Simplifying the body is an exercise, giving

`(((iszero n) zero) (pred1 n))`

In this, substitute the definition of `pred1` and
make an application to produce (another exercise)

```
```

*4* def pred = λ n. (((iszero n) zero)
(n select-second))

We'll study Scott's encoding in the exercises, but it's
just Michaelson's *without* the "frozen-in" `false`
and `true` values in the pairs. That means rather than
just reading out the answer for `iszero` it must be computed by
a little test function.

Also we haven't mentioned it in this light, but Scott's (and thus
Michaelson's) encodings are naturally thought of in terms
of *continuations*, or "what happens next". Usually what happens
next in these number representations is we operate on the
predecessor or we find a base case, and these continuations are
just the functions that make up the nested-lambda number
representations
(Scott, Michaelson), not the outer-lambda-only representation of
Church.

Church:

Evaluation by β-reduction (!!).

```
def zero = λ.s λz.z
def succ = λw. λy. λx.(y ((w y) x))
2 = λs.λz.s(s(z))
```

Scott:

Evaluation by recursive function application.

```
zero = λs.λz.z
succ = λn.λs.λz.s n
2 = λs.λz.s(λs.λz.s(λs.λz.z))
```

Michaelson:

Evaluation by recursive function application.

```
def zero = identity = λx.x
def succ = λn.λs.((s false) n)
2 = λs.((s false) λs.((s false) zero))
```

Note limited scope of the `s,z`s in Scott and Michaelson!

```
zero = λxy.y %select-second
2 = λxy.x(λxy.x(λxy.y))
%sel-1st sel-1st sel-2nd
```

Important Applicative order semantics! Eval. Arguments First! (-> not =>)

Predecessor: show
```
pred = λz.z (λp.p) 0
```

Rationale: Assume N not 0. `pred N ` first copies N to front with first identity
function (λz.z). Now N is applied to the last two arguments: N's first
λ expression is `sel-1st`, which chooses arg1, (λp.p),
and ignores 0 (arg2). The identity function (λp.p) is substituted
in place of the first `sel-1st`'s
body (so the first `sel-1st` vanishes)
and applied to the rest of the original N, yielding N-1.
Let's try ```
pred 2 == λz.z (λp.p) 0 2 => % copy 2 to front
2 (λp.p) 0 -> % evaluate first sel-1st of 2,
% get id fn (1st arg) and lose 2nd arg
(λp.p λxy.xλxy.y) -->
(λp.p 1) ->
1
```

For ```
pred 0 == λz.z (λp.p) 0 0 => % copy 0 to front
0 (λp.p) 0 -> % 0 is sel-2nd, so
0
```

---Abandon some ()s: use

`< function > < arg1 > < arg2 > ... < argn >`

for

```
( ... ((< function > < arg1 >) < arg2 >) ... < argn >)
```

In the non-parenthesized form, a function is applied first to the
nearest argument on its right. If the argument is a function
application itself, its parens must stay, and we keep parens around
function body applications. So from above:
```
```

*4* def pred = λ n. (((iszero n) zero)
(n select-second))
⇒
def pred = λ n. ((iszero n) zero
(n select-second))

Rewrite
```
def < names > = λ < name >. < expression >
```

where
`names` is one or more `< name >`s, as
`def < names > < name > = < expression >`

That is, drop the `λ` and its `.` altogether
and bring the bound variable over to the left of the `=`.
E.g
```
def identity x = x
def self-apply s = s s
def apply func = λ arg. (func arg)
def apply func arg = func arg
def select-first first = λ second. first
```

- Outermost parentheses are dropped: M N instead of (M N)
- Applications are assumed to be left associative: M N P may be written instead of ((M N) P)
- The body of an abstraction extends as far right as possible: λx.M N means λx.(M N) and not (λx.M) N
- A sequence of abstractions is contracted: λx.λy.λz.N is abbreviated as λxyz.N

Continue with our new simplifying
tool:
```
def select-first first second = first
def select-second first = λ second. second
def select-second first second = second
def make-pair e1 = λ e2. λ c. (c e1 e2)
```

and the last line yields
```
def make-pair e1 e2 = λ c. (c e1 e2)
def make-pair e1 e2 c = c e1 e2
```

Last line transforms `cond`'s ```then-else-if`''
semantics to ```if-then-else`''. (Recall
`cond` and `make-pair` are the same!).

```
```

*5* def cond e1 e2 c = c e1 e2
def true first second = first
def false first second = second
def not x = x false true
*6* def and x y = x y false
*7* def or x y = x true y

Replace
```
cond < true choice > < false choice >
< condition >
```

with
```
if < condition >
then < true choice >
else < false choice >.
```

This form, along with line *5*
helps explain lines *6* and *7*:
```
def and x y =
if x
then y
else false
```

```
def or x y =
if x
then true
else y
```

- Conditional expressions with truth values may be represented by pair functions and used to develop boolean operations.
- Natural numbers may be represented recursively by zero and the successor function.
- We saw several ways to remove parentheses from expressions, which
simplifies function definitions, and we introduced the
`if-then-else`form of conditional expressions.- Removing Parens:
`(...(( < function > < arg1 >) < arg2 > ) ...< argN >) == < function > < arg1 > < arg2 > ... < argN >`

- Simplifying Function Definitions:

`def < names > = λ < name >. < expression > == def < names > < name > = < expression >`

- If ... then ... else :
`if < condition> then < true choice > else < false choice > == cond < true choice > < false choice > < condition >`

- Removing Parens: