# Lambda Calculus Notes

The following are my brief notes on the basic of Lambda Calculus. They are primarily just a public posting of my personal notes, and are not meant to be a tutorial per-se. Though it is my hope that someone else besides me would find them to be of use. All of the sources I used to compile these notes are including in the bottom of the page.

### Lambda Syntax

Expression (Mention) E ::= X Function (Application) | 𝜆x.E -- 𝜆 and . are the only keywords in the lambda calculus Application (Application) | E E

An expression can be surrounded with parenthesis for clarity.

(E) ::= E

### Function Application (Left Association)

E1E2E3...En => (...((E1E2)E3)...En) ^ n-4 more close parens, hence the use of ...

### Functions (or Lambda Abstractions)

An function (or abstraction) is another name for an anonymous function. In the lambda calculus an abstraction has two parts, a **head** that contains a single parameter and ends before a period, and a **body** that contains an expression.

𝜆𝑥 . 𝑥 𝜆𝑥 . 𝑥 𝜆𝑥 . 𝑥 ^^ ^ ^ Is the head Bound the head Is the body (tail)

### Function Argument

A function argument is declared in the header, and must be immediately preceded by a 𝜆 .

𝜆𝑥.𝑥 ^ Is a function argument.

### Bound Variables

A bound variable is a variable in the function body that has the same identifier as the function argument.

𝜆𝑥.𝑥 ^ Is a bound variable

A variable x (x can have any name y, z, etc.) is bound if one of the two following cases holds:

- If the x = x
_{1}or x is bound to E, then x is bound in λ x_{1}.E - If x is bound to E1 or E2, then x is bound in E
_{1}E_{2}- In this case “x is bound” means “there is an x bound”.

### Free Variables

𝜆𝑥.𝑥a ^ Is a free variable (𝜆𝑥.𝑥)(𝜆y.yx) ^ ^ Bound Free -- Note: The x in the first expression isn't the same as the x in the second.

A variable x (x can have an name y, z, etc.) is free in an expression (E) if one of the three following cases holds:

- If the free variables of x is x, then x is free
- x !=x
_{1}and x is free in E then x is free in (λ x_{1}.E) - If x is free in E
_{1}or E_{2}in_{,}then x is free- In this case “x is free” means “there is an x free”.

### Function Application

(𝜆x.x)y -- The identity function applied to y. The parenthesis avoid ambiguity. y

### Substitution Shorthand

The two common notations used to express the substitution process that occurs during function application.this is [y/x] and [x:=y] which

__The First Notation__

[y/x]E

The above can be read as, y will replace all occurrences of x in the expression E.

(𝜆x.xa)y = [y/x]xa = ya

__The Second Notation__

[x:= E]

The above can be read as, all occurrences of x will be replaced with E.

(𝜆x.xa)y [x:=y] ya

### Applying Substitutions

_{1}is applied to E

_{2}, then we substitute all free occurrences of x in E

_{1}with E

_{2}.

(𝜆𝑥.E1)E2

__Example 1__

(𝜆𝑥.(𝜆t.xt))y ^ ^ (𝜆𝑥.(E1)) E2 -- x in E1 is free, but bound by 𝜆𝑥 in the function head, so it will be replaced with y. 𝜆t.yt

In order to perform this substitution it is important to remember that the variables in function bodies can only be substitutes during application if they are bound only to that function. That is, if a function contains a function in its body, and the body function has a variable bound to it with the same name as the outer function, then an outer substitution must not change the inner functions variable.

__Example 2__

(𝜆x.x)(𝜆y.y)z -- The second function is applied to the first (𝜆y.y)z -- z is applied to the function z

Example 3

(𝜆𝑥𝑦𝑧.𝑥𝑧(𝑦𝑧))(𝜆𝑚𝑛.𝑚)(𝜆𝑝.𝑝) (𝜆𝑥.𝜆𝑦.𝜆𝑧.𝑥𝑧(𝑦𝑧))(𝜆m.𝜆n.m)(𝜆p.p) -- Function arguments are expanded to include the lambdas that bind them ^ ^ E1 E2 -- E1 = (𝜆𝑥.𝜆𝑦.𝜆𝑧.𝑥𝑧(𝑦𝑧)) is then applied to E2 = (𝜆m.𝜆n.m) -- [𝜆m.𝜆n.m / x] 𝜆𝑦.𝜆𝑧.𝑥𝑧(𝑦𝑧) = 𝜆𝑦.𝜆𝑧.(𝜆m.𝜆n.m)𝑧(𝑦𝑧) (𝜆𝑦.𝜆𝑧.(𝜆m.𝜆n.m)𝑧(𝑦𝑧))(𝜆p.p) ^ ^ E1 E2 -- E1 = (𝜆m.𝜆n.m) is then applied to E2 = z. -- [z / m] 𝜆n.m = 𝜆n.z = z (𝜆𝑦.𝜆𝑧.𝑧)(𝜆p.p) ^ ^ E1 E2 -- E1 = (𝜆𝑦.𝜆𝑧.𝑧) is then applied to E2 = (𝜆p.p) -- [𝜆p.p / y] 𝜆𝑧.𝑧 = 𝜆𝑧.𝑧 𝜆𝑧.𝑧

### Sources

- A Tutorial Introduction to the Lambda Calculus
- Haskell Programming from First Principles
- Haskell Wiki