Lambda Calculus: Functional Programming Basics

Introduction to Lambda Calculus

• Lambda calculus serves as an introduction to functional programming.
• Lambda calculus has features like functions.
• Lambda calculus allows you to define a function and call a function.

Describing a Programming Language

• Syntax describes what programs look like.
• Semantics describes what programs mean.
• Operational semantics are how programs execute step-by-step.

Syntax of Lambda Calculus

• Expressions can be variables (x, y, z), function definitions (λx -> e), or function calls (e1 e2).
• A function definition (abstraction) is written as \x -> e, where x is the formal parameter and e is the body.
• A function call (application) is written as e1 e2, where e1 is the function and e2 is the argument.

Examples of Lambda Calculus Expressions

• \x -> x represents the identity function.
• \x -> (\y -> y) represents a function that returns the identity function.
• \f -> f (\x -> x) represents a function that applies its argument to the identity function.

Semantics: Scope of a Variable

• The scope of a variable is the part of a program where the variable is visible.
• In the expression \x -> e, x is the introduced variable, and e is the scope of x.
• An occurrence of x in \x -> e is “bound” by the binder \x

Free and Bound Variables

• An occurrence of x in e is free if it is not bound by an enclosing abstraction.
• x is bound in expressions like \x -> x and \x -> (\y -> x)
• x is free in expressions like x y, \y -> x y, and (\x -> \y -> y) x.

Free Variables

• A variable x is free in e if there exists a free occurrence of x in e.
• FV(x) = {x}
• FV(\x -> e) = FV(e) - {x}
• FV(e1 e2) = FV(e1) U FV(e2)

Closed Expressions

• If e has no free variables, it is said to be closed.
• Closed expressions are also called combinators.
• The shortest closed expression is \x -> x.

Semantics

• Execute = rewrite step-by-step following simple rules until no more rules apply
• The rewrite rules of Lambda Calculus are:
• α-step (aka renaming formals)
• B-step (aka function call)

Semantics: B-Reduction

• (\x -> e1) e2 reduces to e1[x := e2], where e1[x := e2] means "e1 with all free occurrences of x replaced with e2".
• Computation in beta-reduction is performed by search-and-replace.
• In beta-reduction, the body of the abstraction is taken and all free occurrences of the formal are replaced by the argument.
• (\x -> e1) e2 B-steps to e1 [x := e2]

Capture-Avoiding Substitution

• You have to fix the definition of B-reduction:
• (\x -> e1) e2 =b> e1[x := e2]
• Where e1[x := e2] means “e1 with all free occurrences of x replaced with e2”
• e1 with all free occurrences of x replaced with e2, as long as no free variables of e2 get captured
• undefined otherwise

Semantics: α-Reduction

• \x -> e =a> \y -> e[x := y], where y is not in FV(e).
• In alpha-reduction, we can rename a formal parameter and replace all its occurrences in the body.
• (\x -> e) a-steps to (\y -> e[x := y])

Normal Forms

• A 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>.
• e' is in normal form.

Elsa Shortcuts

• let ID = \x -> x is an abbreviation for \x -> x.
• a =d> step: to substitute a name with its definition

Evaluation Shortcuts

• 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

Non-Terminating Evaluation

• The combinator (\x -> x x) (\x -> x x) is called Ω and can be used to write programs that loop back to themselves.
• Code using Ω never reduces to normal form.

Multi-Argument Functions

• You can define a function that takes two arguments and returns the second one with \x -> (\y -> y).
• You can apply \x -> (\y -> y) to apple and banana, first applying to apple, then applying the result to banana (((\x -> (\y -> y)) apple) banana)

Syntactic Sugar

• Syntactic Sugar is convenient notation used as a shorthand for valid syntax.
• Lambda calculus notation used as syntactic sugar shorthand:
• \x -> (\y -> (\z -> e)) can be written as \x -> \y -> \z -> e
• \x -> \y -> \z -> e can be written as \x y z -> e
• (((e1 e2) e3) e4) can be written as e1 e2 e3 e4
• \x y -> y is the function that takes two arguments and returns the second one.
• (\x y -> y) apple banana is a function applied to two arguments.

Booleans

• Boolean values (TRUE and FALSE) can be encoded as functions.
• To encode boolean values, you need to make a binary choice, if b then e1 else e2.

Boolean Implementation

• define three functions with Lambda expressions
  • let TRUE = \x y -> x
  • let FALSE = \x y -> y
  • let ITE = \b x y -> b x y

Boolean Operators

• With ITE, other Boolean operators can be defined.
• Example Boolean operators include:
• let NOT = \b -> λITE b FALSE TRUE
• let AND = \b1 b2 -> ITE b1 b2 FALSE
• let OR = \b1 b2 -> ITE b1 TRUE b2

Records

• start with records with two fields (aka pairs)
• Pack two items into a pair, then
• Get first item, or
• Get second item.

Pairs Implementation

• PAIR = \x y -> (\b -> ITE b x y) makes a pair with x and y, similar to { fst : x, snd : y }
• FST = \p -> p TRUE returns the first element, similar to p.fst
• SND = \p -> p FALSE returns the second element, similar to p.snd.

Exercise: Triples

• You can implement a record that contains three values by constructing Lambda expressions with the existing boolean expressions.
• Example implementation:
• TRIPLE = \x y z -> PAIR x (PAIR y z)
• FST3 = \t -> FST t
• SND3 = \t -> FST (SND t)
• TRD3 = \t -> SND (SND t)

Numbers in Lambda Calculus

• Natural numbers (0, 1, 2, ...) can be created.
• Count: 0, inc
• Arithmetic: dec, +, -, *
• Comparisons: ==, <=, etc

Natural Numbers API

• You need to define:
• A family of numerals: ZERO, ONE, TWO, THREE, ...
• Arithmetic functions: INC, DEC, ADD, SUB, MULT
• Comparisons: IS_ZERO, EQ
• Such that they respect all regular laws of arithmetic, e.g.
• IS_ZERO ZERO =~> TRUE
• IS_ZERO (INC ZERO) =~> FALSE
• INC ONE =~> TWO

Pairs: Church Numerals

• Church numerals encode a number called N that is encoded as a combinator that calls a function on an argument N times
• Example implementation:
• ONE = \f x -> f x
• TWO = \f x -> f (f x)
• THREE = \f x -> f (f (f x))
• FOUR = \f x -> f (f (f (f x))))
• FIVE = \f x -> f (f (f (f (f x)))))
• SIX = \f x -> f (f (f (f (f (f x))))))

Increment

• Call f on x one more time thann does
• INC = \n -> (\f x -> f (n f x))
• Example function call eval inc_zero : INC ZERO =d> ONE

Lambda Calculus Addition

• Start with m, and increment it n times
• ADD = \n m -> n INC m
• Example function call: eval add_one_zero : ADD ONE ZERO =~> ONE

Multipication

• There is a function that takes a 2nd arg z and computes (ADD m z)
• Start with 0, and add m to it n times.
• MULT = nm -> n (ADD m)
• Example eval two_times_one : MULT TWO ONE

Exponentials

• Start with 1, and multiply it by m, n times.
• Let Exponentials = \n m ->

Implementing Recursion

• Recursion requires being able to refer to functions by name, but in λ-calculus functions are anonymous.
• Step 1: You pass in the function to call “recursively”
• The function passed in to STEP
• is the same function as
• the result of STEP!
• Example implementation:
• STEP = \rec \n -> ITE (ISZ n) ZERO (ADD n (rec (DEC n)))

Lambda Calculus: Fixpoint Combinator

• A combinator FIX such that FIX STEP calls STEP with itself as the first argument
• Such that FIX STEP =*> STEP (FIX STEP)
• a fixpoint of a function f(x) is a point x, such that f(x) = x

Lambda Calculus: The Y Combinator

• Discoverd by Haskell Curry has the following implementation:
• let FIX = \stp -> (\x -> stp (xx)) (\x -> stp (xx))
• Example evaluation eval step: FIX STEP =b> STEP (FIX STEP)