Reduction Strategies For Lambda Calculus

Redex is a deducible expression. It is a lambda abstraction applied to an argument

Reduction replaces a redex with the result of applying the function.

Beta Reduction:

The process of applying the function to its argument. The process of replacing the bound variable in the function with the argument.

(\x.x) y 
a function that takes x as an input and returns x as output
y is the argument being applied to the function 

Reduction Process:

1. Identify the Redex:
2. The expression (\x.x) y is a redex because it is a function application where a lambda abstraction is applied to an argument
3. Apply the function: To reduce it, we need to substitute x in the body of the lambda abstraction with the argument y.
4. Perform the Substitution:
5. The body of the function is simply x. When we apply the function to y, we replace every occurrence of x in the body with y.
6. Before Substitution:
7. (\x. x), Body : x
8. After substitution:
9. repalce x with y
10. result y

Final result:

Therefore the reduction of (\x. x) y is y.

Think of it as a function that says: " Whatever you give me, i will give it back to you"

& you give it y, it will just return y.

Consider the expression (\x.x + 1) 3:

1. Identify redex: (\x .x + 1 ) 3 is a redex because it's function application where a lambda abstraction is applied to an argument
2. Substitute: Replace x with 3, in x + 1,
3. Result : 3 + 1 = 4, which simplifies to 4.

Reduction Strategies:

1. Call by Value (CBV):
2. Fully evaluate the argument before applying the function
3. Call by Name (CBN):
4. Substitute the argument into the function without evaluating it first.

Example 1:

Iteration 1:

 (\x.x x) ((\x y.y x) z (\x.x))
 --------- --------------------
function    applied to this arg
(\x . x x)  y = arg

1. Identify the Redex: (\x. x x) t1, where t1 =((\x y.y x) z (\x.x))
2. Apply the function: To reduce it, we need to substitute x in the body of the lambda abstraction with the

(\x.x x) t1, where argument t1 = ((\x y.y x) z (\x.x))
\x. x x, where body  x x
x x -> repaced with t1 = ((\x y.y x) z (\x.x))
((\x y.y x) z (\x.x))  ((\x y.y x) z (\x.x))

Iteration 2:

here again we follow the same step:

1. Identify Redex:

((\x y.y x) z (\x.x))  ((\x y.y x) z (\x.x))
----function---------   -----arguments--------

comaping to

(\x.x + 1)   3
-func-----  --arg--

so we look again in left part where the function exist ignoring the argument

• here we identify our redex again:

((\x y.y x) z (\x.x)) 
-funcn--  ---argument---
(\x y . y x) t1, where t1 = z (\x.x)

now substitute x with t1:

• Substitute: we again replace our \x with argument like previously
• when applying the fucntion (\xy. yx) to the argument z (\x.x) we replace x in the body yx with z and y

((\x y.y x) z (\x.x)) 
this function expects x & y, then applies it in the body, where x = z , y = (\x.x)
(\x.x) z

So, the resulting expression after applying the function is: (\x.x)z

Iteration 3:

• Again identifying the redex

(\x.x) z
comparing with (\x.x) t
x = x, t = z 

• Substituting x with t

z

Key Difference

• Call by value:
• CBV reduces arguments before substituting into the function.
• If we reduce the arguments first
• Call by Name
• CBN substitutes arguments without evaluating them, reducing only when needed.
• if we reduce the arguments later on after passed into the function

Practice question for final:





What's the key take away how to solve it?