Lecture 6: Meta-Theory of Lambda Calculus

Understanding Equality and Program Termination

1. Conversion (=): When are two programs "equal"?

A =r B (Reflexive, Symmetric, Transitive) [cite: 926-928]
In Lecture 5, we learned about reduction (→), which is like a one-way street. Conversion (=) is a two-way street. If Program A can eventually become Program B, or if they both come from the same source, we say they are convertible.

Analogy: The Many Names of Water

Think of "Ice," "Steam," and "Liquid Water." They look different, but they are all H2O. In Lambda Calculus, two programs might look totally different, but if they produce the same result, they are "Equal" (=).
# Two different ways to write a 'Double' function
f = lambda x: x + x
g = lambda x: x * 2

# These are 'convertible' because for any input, they behave identically.
print(f(5) == g(5)) # True

2. Normal Forms: The "Final Answer"

A is in r-normal form iff there is no B such that A →r B [cite: 960]
A term is in Normal Form when there are no more "Redexes" (reducible expressions) left. Think of this as the simplest possible version of a math problem. The expression 5 + 2 is NOT in normal form, but 7 is.
# (λx.x) 5  -> This has a redex. It can be simplified.
expression = (lambda x: x)(5)

# 5 -> This is in Normal Form. You can't simplify '5' any further.
final_answer = 5

3. Weak vs. Strong Normalization

Strongly Normalizing = Every path ends
This is a critical exam topic.
1. Weakly Normalizing: There is at least one way to finish the program[cite: 977].
2. Strongly Normalizing: Every possible way you try to solve it will eventually finish.

Analogy: The Infinite Toy Box

Imagine a toy box that automatically refills itself if you pull toys out from the left side, but empties if you pull from the right side. If you only pull from the right, the box empties (Weakly Normalizing). If the box emptied no matter where you pulled from, it would be Strongly Normalizing.
# A term that NEVER finishes (Omega): (λx.xx)(λx.xx)
# This is NOT normalizing. It's an infinite loop! [cite: 971]

def omega():
    return (lambda x: x(x))(lambda x: x(x))

# try: omega() 
# result: RecursionError (The computer's way of saying it won't stop)

4. The Power of Strategy

The order of reduction matters. Sometimes, a program has a final answer, but if you take the "wrong path," you might loop forever. The "Leftmost-Outermost" strategy is the golden rule that will find the answer if one exists.

Example from Exercise :

Term: (λz.y)((λx.xx)(λx.xx))

Pure Python Representation


# This is y
y = "y"

# λz. y
def outer(z):
    return y

# λx. x x
def inner(x):
    return x(x)

# Apply the full expression
result = outer(inner(inner))

print(result)

Note: Running this code in Python will cause infinite recursion because inner(inner) never terminates.