# Lambda Calculus 2

## GOALS

• 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''

## TRUTH VALUES, CONDITIONALS

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 absx to the absolute value of x we'd say absx = x<0?-x:x.

We can model a conditional expression with a version of make-pair:
def cond = λ e1. λ e2. λ c.((c e1) e2).

## TRUTH VALUES, CONDITIONALS CON'T

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

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.

## MORE NOT DETAILS

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. ```

## AND

``` 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).

## SIMPLIFY AND?

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 ```

## OR

``` 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.

## GRAPHIC GUIDE TO LAMDA CALCULUS 1/5

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.

## RECURSIVE DATA TYPES

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.

## NATURAL NUMBERS --- STRATEGY

Begin with recursive definition in terms of a "first" number zero, 0 and the successorfunction: 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).

## THE PLOT

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.

## NATURAL NUMBERS --- CHURCH'S ENCODING

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.

## CHURCH CONT'D -- ADDITION AND MULTIPLICATION

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.

## NATURAL NUMBERS --- MICHAELSON'S ENCODING

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) ```

## E.G. THREE

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

## WHY false AND identity ? ISZERO

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) .

## The Predecessor Function

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.

## NATURAL 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)) ```

## SCOTT'S ENCODING

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.

## ENCODING SUMMARY

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,zs in Scott and Michaelson!

## SCOTT Example

``` 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: ``` 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, all goes as above but since 0 is sel-2nd applying it to the two arguments ignores the identity and evaluates to 0, which is (for us) its own predecessor. ``` pred 0 == λz.z (λp.p) 0 0 => % copy 0 to front 0 (λp.p) 0 -> % 0 is sel-2nd, so 0 ```

## MORE NOTATION SIMPLIFICATION

---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 ```

## SUMMARY of Common Conventions

• 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

## YET MORE NOTATION SIMPLIFICATION

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!).

## STILL MORE NOTATION SIMPLIFICATION

``` 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 ```

## SUMMARY

• 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 > ```