UCSD CSE 230 Midterm Review Note
01lambda
Programs are expressions e (also called λterms) of one of three kinds:
 Variable
 x, y, z
 Abstraction (aka nameless function definition)
 (\x > e)
 x is the formal parameter, e is the body
 “for any x compute e”
 Application (aka function call)
 (e1 e2)
 e1 is the function, e2 is the argument
 in your favorite language: e1(e2)
Execute = rewrite stepbystep
 Following simple rules
 until no more rules apply
An variable x is free in e if there exists a free occurrence of x in e.
If e has no free variables it is said to be closed.
Closed expressions are also called combinators
What is the shortest closed expression? \x>x
Rewrite Rules of Lambda Calculus
βstep (aka function call) αstep (aka renaming formals)
Semantics: Redex A redex is a term of the form
(\x > e1) e2
A function (\x > e1)
 x is the parameter
 e1 is the returned expression Applied to an argument e2
 e2 is the argument
Semantics: βReduction
A redex bsteps to another term …
(\x > e1) e2 =b> e1[x := e2]
where e1[x := e2] means
“e1 with all free occurrences of x replaced with e2” and as long as no free variables of e2 get captured
Computation by searchandreplace:

If you see an abstraction applied to an argument, take the body of the abstraction and replace all free occurrences of the formal by that argument

We say that (\x > e1) e2 βsteps to e1[x := e2]
Semantics: αRenaming
\x > e =a> \y > e[x := y] where not (y in FV(e))
 We rename a formal parameter x to y
 By replace all occurrences of x in the body with y
 We say that \x > e αsteps to \y > e[x := y]
Recall redex is a λterm of the form
(\x > e1) e2
A λterm is in normal form if it contains no redexes.
Semantics: Evaluation A λterm e evaluates to e’ if

There is a sequence of steps e =?> e_1 =?> … =?> e_N =?> e' where each =?> is either =a> or =b> and N >= 0

e’ is in normal form
So the result of a evaluation must be a normal form!!!
ELSA
Named λterms:
let ID = \x > x – abbreviation for \x > x
To substitute name with its definition, use a =d> step:
ID apple =d> (\x > x) apple – expand definition =b> apple – betareduce
Evaluation:
 e1 =*> e2: e1 reduces to e2 in 0 or more steps
 where each step is =a>, =b>, or =d>
 e1 =~> e2: e1 evaluates to e2 and e2 is in normal form