Lambda Calculus | Alpha renaming | Exercise 1

A formal system used to study functions, variables & how they interact through application & abstraction. It's a foundational mathematical framework that models computation in its purest form.

Key concepts:

1. Variables represents data or values
2. Functions: Defined using abstraction
3. \x.t , is function that takes x and returns t.
4. Application: Applying a function to an argument.

Sytax:

t:: = v | t t | \x.t

t: represents a term in lamda calculus. A term is any valid lambda expression. 

v: Represents a varibale, variables are the basic building blocks & are typically symbols like x, y, z

t t: Represents function application, where one term is applied to another. For example (f x) means applying the function t to the argument x. 

\x.t: Represents a lambda abstraction or function definition. It defines a function that takes a variable x as input & returns the term t as output. 




(\x.x) 3 -> applying identical function \x.x to 3

Breaking down the syntax:

1. Variables (V):
2. Represents atomic terms which cannot be broken down further.
3. Example x, y, z
4. Functions (\x.x):
5. Is a function that takes x as an input and returns x as output.
6. Applications (\x. x) 3: applying one term to another.
7. Applying the function \x. x to 3
8. result is 3
9. Nested functions: \x. \y. x
10. A function that takes x and return another function that takes y and always return x.

Why this syntax is important?

This simple grammer is Turing complete. With just variables, application & abstractions you can represent:

1. Functions: Mapping inputs to outputs.
2. Logic: True, False, conditions.
3. Data Structures: Numbers, lists & more.
4. Recursion: Using self-referencing functions.

Lambda calculus is Turing complete, meaning it can compute anything that any computer program can compute. Using just:

What is Alpha-renaming in lamda calculus? Why is it important?

Alpha renaming refers to the process of changing the names of bound variables in lambda expression without altering its meaning or functionality. This is essential to:

1. Avoid conflicts during substitution.
2. Distinguish between free & bound variables explicitly.
3. Maintain clarity when working with nested bindings or complex expressions.

Well, how do you distinguish between bound and free variables in lambda expression?

1. Bound variables are those declared in lambda abstraction and used within it's scope. For example x in \x. x is bound
2. Free variables are not bound within the lambda abstraction where they appear. For instance: \y. x , x is free variable.

What is the difference between free and bound variables?

• Free: Not declared within the lambda expression, e.g., x in \y.x.
• Bound: Declared within the lambda expression, e.g., y in \y.x.

Application of Alpha-renaming:

Can you explain with examples how to rename bound variables without changing the meaning of an expression?

1. Example 1 : Simple renaming:
2. \x. x is equivalent to \y. y
3. Rename x to y because x is bound, y does not conflict with any free variables.
4. Example 2: Nested Bindings:

\x. \y. x y  
here x and y both are binded. 
x -> a , y -> b
\a. \b . a b

What is Variable Capture?

Variable capture occurs when a free variable in an expression becomes bound during substitution, altering the meaning of the expression.

Example of risk of variable capture:

\x. \y . x y
x is bound by the outer \x
y is bound by inner \y

but if we zoom in on: \y . x. y
here x is a free variable and y is bound variable.

Substituting y for x:

1. x abstraction is no longer relevant it has been consumed by substitution.

2. We don't keep an unused \x in the final expression

\x.\y.xy

But after substitution of y for x, the full expression simplifies to just the inner lambda:

\y.y y

This happens because the outer parameter x has been completely replaced, so the result is now just the inner function. There's no longer a need for the outer lambda.

After substitution, the full expression simplifies to:
\y.y y

Here, the substitution causes variable capture because:

•  The original expression, x in x y was free (not bound to any lambda).
• After substitution, y in y y is bound by the \y.

How does alpha-renaming avoid this?

1. Each bound variable must be unique within its scope
2. \y . \y. y y , the 2nd \y shadows the 1st \y, which is completely overridden and no longer be accessed, this causes confusion and violates scoping rules.
3. Substitution respects scope:
4. When substitution a variable ( y for x), substitution only replaces free occurrences of x within its scope.
5. Here in our case these are bound variables.
6. We can rename our y for z;
7. \x . \z. x. y
8. Then we can substitute x for y:
9. \y. \z. y. z
10. Alpha-renaming avoids these conflicts:

Few more practice questions:

How do i partition lamda expression into groups based on alpha renaming equivalence?

• Group expressions that are identical except for the names of their bound variables. Example: Expressions:
• Alpha equivalent and belong to the same group.:
• \x . x
• \y. y
• \z. z
• Not equivalent so these are different group:

1. \x. y
2. \y. z

If it is alpha equivalent then it's the same group!

Alpha-equivalence: Two expressions are equivalent if one can be transformed into the other by renaming bound variables.

Same group: Expressions that are alpha-equivalent are grouped together.

Common mistakes in alpha-renaming problems:

1. Renaming free variables
2. Failing to check for conflicts with existing variables.
3. Misunderstanding nested scoping.

Example Practice Problems

Partition the following lambda expressions into groups such that within each group, any expression can be converted to another through alpha-renaming.

Expressions:

1. \x.x
2. \y.y
3. \z.z
4. \x.y
5. \y.x
6. \x.\y.x y
7. \a.\b.a b
8. \z.\w.z w

Group 1:

1. \x. x
2. \y. y
3. \z. z

Group 2:

1. \x . \y . x. y
2. \z. \w . z w
3. \a. \b. a. b

Group3 :

1. \x. y

Group 4:

1. \y. x

Validation of Groups

1. Group 1: { \x.x, \y.y, \z.z }

• These expressions are alpha-equivalent because they all represent the identity function (return the input directly) with bound variables.

1. Group 2: { \x.\y.x y, \z.\w.z w, \a.\b.a b }

• These expressions are alpha-equivalent because they share the same structure of applying the first bound variable to the second.
• The bound variable names differ, but the function's logic remains the same.

1. Group 3: { \x.y }

• This expression is unique as it introduces a free variable y. It cannot be alpha-renamed to match any other expressions.

1. Group 4: { \y.x }

• Similar to Group 3, this expression introduces a free variable x and cannot be alpha-renamed to match any other expressions.

More practice question:

Expressions:

1. \x.x x
2. \y.y y
3. \z.z z
4. \x.\y.x y
5. \a.\b.a b
6. \z.\w.z w
7. \x.y
8. \y.x
9. \x.\z.z x
10. \a.\y.y a

Group 1:

1. \x . x x
2. \y . y y
3. \z. z z

Group 2:

1. \x . \y. x y
2. \a . \b. a b
3. \z. \w. z w

Group 3:

1. \x. y

Group 4:

1. \y. x

Group 5:

1. \x.\z.z x
2. \a.\y.y a

Group 1: { \x.x x, \y.y y, \z.z z }

• These expressions are alpha-equivalent.
• Reason: They share the same structure, where the bound variable is applied to itself.

Group 2: { \x.\y.x y, \a.\b.a b, \z.\w.z w }

• These are alpha-equivalent.
• Reason: They all represent two nested abstractions where the first variable is applied to the second.

Group 3: { \x.y }

• This is a unique group.
• Reason: It contains a free variable y, so it is not alpha-equivalent to any other expression.

Group 4: { \y.x }

• This is another unique group.
• Reason: It introduces a free variable x, making it distinct from other expressions.

Group 5: { \x.\z.z x, \a.\y.y a }

• These are alpha-equivalent.
• Reason: Both represent nested abstractions where the second variable is applied to the first in reverse order compared to Group 2.

Exam Tips for Similar Problems

1. Check Bound Variables: Identify which variables are bound and rename systematically to test equivalence.
2. /abcd -> a,b,c,d are bound variables
3. \a.\b.\c.\d. a b (c d): All variables (a, b, c, d) are still bound.
4. Highlight Free Variables: Free variables cannot be renamed, which can isolate expressions into separate groups.
5. \x.\y.x z, z is free variables
6. (\x.x) y, y is free
7. \x.(x y z), y and z are free
8. Focus on Structure: Ignore specific variable names and compare the overall function structure and application order.
9. Alpha-equivalence depends only on the order of application and the function logic:
10. Example: \x.\y.x y is structurally equivalent to \a.\b.a b or \z.\w.z w.
11. Example: \x.x y is not equivalent to \y.y x because the application order differs.

Final exam: Practice question:

first step: categorize based on the outer variable

1. e1 = w (\xy. y w y )
2. e6 = w (\yz. y w y)

1. e2 = z ( \xy . y z y)
2. e3 = z ( \xz . w z w)
3. e4 = z ( \wy .w z w)
4. e5 = z ( \yz. y z y)

2nd step:

1. If we see free variable, it goes into it's own group
2. If we see bound variables, let's rename them and see if we can get alpha-equivalent.

let's work on these first:

1. e1 = w (\xy. y w y )
2. e6 = w (\yz. y w y)

Group 1:

1. e1 = w (\xy. y w y )
2. if we rename \x to y, -> w (\yy, y w y)?
3. so it can be categroized in the same bucket as w (\yz. y w y) ??
4. z ( \xy . y z y)

Group 2:

1. e6 = w (\yz. y w y)

Why two separate group?

1. if we rename x -> y, w (\xy. y w y ). here it won't be similar to w (\yz. y w y)

now let's focus on :

1. e2 = z ( \xy . y z y)
2. if we rename z to w -> w ( \xy . y w y)
3. thus goes to group 1
4. e3 = z ( \xz . w z w)
5. if we rename z to w -> w ( \xz . w w w)
6. here we renamed a free variable so it is on it's own
7. Group 3
8. e4 = z ( \wy .w z w)
9. if we rename z to w -> w ( \wy .w w w)
10. 
    
11. 
    
12. e5 = z ( \yz. y z y)
13.