Lambda Calculus 2

GOALS

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

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.

GRAPHIC GUIDE TO LAMDA CALCULUS 2/5

GRAPHIC GUIDE TO LAMDA CALCULUS 3/5

GRAPHIC GUIDE TO LAMDA CALCULUS 4/5

GRAPHIC GUIDE TO LAMDA CALCULUS 5/5

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.

< 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

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