Introduction

Now that we can represent some basic theorems using a computer, we need to be able manipulate those representations. We also will want to be able to tell if two types are equivalent. This is important in type checking operations.

For example, \(2 + 2\) and \(4\) are equivalent. \(4\) is a natural number. So \(2 + 2\) should typecheck as a natural number¹.

This post is a sequel to an earlier post on the calculus of constructions. I recommend reading that post first.

Note that I found a few subtle errors in the code as I was writing this up: caveat lector. There could be more.

Definitional Equality

What does it mean for two terms to be equal? The simplest version of this is for two terms to be definitionally equal. That is, their structures are identical, and all the names of the variables are the same. Let’s take a look at what this looks like:

def definitionally_equal(input1: Term, input2: Term) -> bool:

    match input1:
        case Constant(name1):
            return name1 == input2.name
        case Variable(name1):
            return isinstance(input2, Variable) and name1 == input2.name
        case ProductType(var1, term11, term12):
            var_equal = definitionally_equal(var1, input2.variable)
            first_equal = definitionally_equal(term11, input2.term1)
            second_equal = definitionally_equal(term12, input2.term2)
            return var_equal and first_equal and second_equal
        case FunctionType(var1, term11, term12):
            var_equal = definitionally_equal(var1, input2.variable)
            first_equal = definitionally_equal(term11, input2.term1)
            second_equal = definitionally_equal(term12, input2.term2)
            return var_equal and first_equal and second_equal
        case Application(first1, second1):
            first_equal = definitionally_equal(first1, input2.first) 
            second_equal = definitionally_equal(second1, input2.second)
            return first_equal and second_equal
        case Let(var1, term11, term12, term13):
            var_equal = definitionally_equal(var1, input2.variable) 
            first_equal = definitionally_equal(term11, input2.term1)
            second_equal = definitionally_equal(term12, input2.term2) 
            third_equal = definitionally_equal(term13, input2.term3)
            return var_equal and first_equal and second_equal and third_equal
        case Prop():
            return isinstance(input2, Prop) 
        case Set():
            return isinstance(input2, Set) 
        case Type(n):
            return (isinstance(input2, Type) and n == input2.n) 
        case str():
            return isinstance(input2, str) and input1 == input2
        case _:
            raise TypeError(f"Unexpected type: {type(input1)}")

First, we check what the structure for the first term is. If it’s a sort, or some type we can check directly (like a constant), we compare directly. Otherwise, we recurse on each argument.

Definitional equality will only return True if the two structures are exactly equivalent, and in the same form. Unfortunately for us, different terms might be the same, just written in different ways. For example, we might have two expressions:

\[ \begin{align} \lambda &x:Z.x \\ \lambda &y:Z.y \end{align} \]

In our Python classes this might look something like:

def test_function_types_with_variables(self):
    x = Variable("x")
    y = Variable("y")
        
    func1 = FunctionType(x, Type(), x)
    func2 = FunctionType(x, Type(), y)
        
    self.assertFalse(definitionally_equal(func1, func2))

Both terms are the identity function. However, definitional equality can’t tell that they are same. It doesn’t know how to rename the variables. We will need “convertibility checking”, where we convert the functions to the same form (for example, \(\alpha\)-conversion can rename variables).

Conversion Rules

Now we’ll start look at the actual conversion rules.

\(\alpha\)-Conversion

The first rule is \(\alpha\)-conversion. As we just said, this rule essentially renames variables. But before we look at \(\alpha\)-conversion directly, we need some functions to help manage variables names: tracking names and generating new names.

Variable Names

First, let’s make sure we can get a list of all the variables in an expression. Here’s collect_names. This function recurses through the structure, finding all the variables, and adds their names to a set.

def collect_names(t: Term):
    used_names = set()
    match t:
        case Constant(n):
            used_names.add(n)
        case Variable(n): 
            used_names.add(n)
        case ProductType(var, t1, t2):
            used_names.update(collect_names(var))
            used_names.update(collect_names(t1))
            used_names.update(collect_names(t2))
        case FunctionType(var, t1, t2):
            used_names.update(collect_names(var))
            used_names.update(collect_names(t1))
            used_names.update(collect_names(t2))
        case Application(t1, t2):
            used_names.update(collect_names(t1))
            used_names.update(collect_names(t2))
        case Let(var, t1, t2, t3):
            used_names.update(collect_names(var))
            used_names.update(collect_names(t1))
            used_names.update(collect_names(t2))
            used_names.update(collect_names(t3))
        case _:
            pass
    return used_names

Now that we have this, we can use this to generate unique, fresh variables, not used in a given term:

def fresh_var(term: Term, name: str = "x") -> Variable:
    """Generate a fresh variable name not used in the term"""
    used_names = collect_names(term)
    i = 0
    fresh_name = name
    while fresh_name in used_names:
        i += 1
        fresh_name = f"{name}{i}"
    return Variable(fresh_name)

Rule

Now let’s look at \(\alpha\)-conversion itself.

Given a term like \(\lambda x.x\), we should be able to convert it to \(\lambda y.y\) using \(\alpha\)-conversion. Note that, while not definitionally equal, the two expressions are “the same”.

Here’s the function:

def alpha_convert(term: Term, old_var: Variable, new_var: Variable) -> Term:
    if (not isinstance(old_var, Variable)) or (not isinstance(new_var, Variable)):
        raise Exception("Can only alpha-convert two variables") 
    if new_var.name in collect_names(term):
        raise Exception(f"Shadowing. Term:{term} Old:{old_var} New:{new_var}")
    if old_var.name == new_var.name:
        return term

    match term:
        case Variable(name):
            return new_var if name == old_var.name else term
        case ProductType(var, term1, term2):
            if var.name == old_var.name:
                var = new_var
            return ProductType(var, 
                             alpha_convert(term1, old_var, new_var),
                             alpha_convert(term2, old_var, new_var))
        case FunctionType(var, term1, term2):
            if var.name == old_var.name:
                var = new_var
            return FunctionType(var,
                              alpha_convert(term1, old_var, new_var),
                              alpha_convert(term2, old_var, new_var))
        case Application(t1, t2):
            return Application(alpha_convert(t1, old_var, new_var),
                            alpha_convert(t2, old_var, new_var))
        case Let(var, t1, t2, t3):
            if var.name == old_var.name:
                var = new_var
            return Let(var,
                      alpha_convert(t1, old_var, new_var),
                      alpha_convert(t2, old_var, new_var),
                      alpha_convert(t3, old_var, new_var))
        case _:
            return term

What’s happening here? \(\alpha\)-conversion’s implementation is pretty similar to definitionally_equal, or collect_names. We recurse down the structure of the term, finding any instances of old_var and changing them to new_var.

Equivalence

We can use \(\alpha\)-conversion to check if two terms are \(\alpha\)-equivalent - that is, equal up to a renaming of bound variables.

def alpha_equivalent(term1: Term, term2: Term) -> bool:
    """Check if two terms are equal up to renaming of bound variables"""
    match (term1, term2):
        case (Variable(name1), Variable(name2)):
            return name1 == name2  # Free variables must match exactly
        case (Constant(name1), Constant(name2)):
            return name1 == name2
        case (ProductType(var1, t11, t12), ProductType(var2, t21, t22)):
            if not alpha_equivalent(t11, t21):
                return False
            # Use fresh variable to check body
            fresh = fresh_var(term1)
            fresh_var2 = Variable(fresh.name)
            # Convert both bodies to use same fresh variable
            body1 = alpha_convert(t12, var1, fresh)
            body2 = alpha_convert(t22, var2, fresh_var2)
            return alpha_equivalent(body1, body2)
        case (FunctionType(var1, t11, t12), FunctionType(var2, t21, t22)):
            if not alpha_equivalent(t11, t21):
                return False
            fresh = fresh_var(term1)
            fresh_var2 = Variable(fresh.name)
            body1 = alpha_convert(t12, var1, fresh)
            body2 = alpha_convert(t22, var2, fresh_var2)
            return alpha_equivalent(body1, body2)
        case (Application(f1, a1), Application(f2, a2)):
            return alpha_equivalent(f1, f2) and alpha_equivalent(a1, a2)
        case (Let(var1, t11, t12, t13), Let(var2, t21, t22, t23)):
            if not (alpha_equivalent(t11, t21) and alpha_equivalent(t12, t22)):
                return False
            fresh = fresh_var(term1)
            fresh_var2 = Variable(fresh.name)
            body1 = alpha_convert(t13, var1, fresh)
            body2 = alpha_convert(t23, var2, fresh_var2)
            return alpha_equivalent(body1, body2)
        case (Prop(), Prop()) | (Set(), Set()) | (SProp(), SProp()):
            return True
        case (Type(n1), Type(n2)):
            return n1 == n2
        case _:
            return False

Here’s an example:

def test_alpha_equivalence(self):
    x = Variable("x")
    y = Variable("y")
    z = Variable("z")

    term_x = ProductType(x, Type(), x)
    term_y = alpha_convert(term_x, x, y)
    term_z = ProductType(z, Type(), z)

    self.assertFalse(definitionally_equal(term_x, term_y))
    self.assertFalse(definitionally_equal(term_x, term_z))
    self.assertTrue(alpha_equivalent(term_x, term_y))
    self.assertTrue(alpha_equivalent(term_x, term_z))

Pretty cool. Now let’s handle the other conversion rules.

\(\beta\)-Conversion

Next up is \(\beta\)-conversion. Essentially, this captures the idea of “function evaluation”.

Let’s say we have a term like:

\[ \lambda x:A.(\lambda y:B.x) \]

This is a function that takes as argument n term \(x\) of type \(A\) and returns a function type. We want to apply this function to some term \(c:A\). This might be written as

\[ ((\lambda x:A.(\lambda y:B.x))\text{ }c) \]

According to our mathematical intuition, this term (called a \(\beta\)-redex when it’s in this unevaluated form) should be the same as this expression:

\[ \lambda y:B.c \]

That’s what \(\beta\)-conversion does: it reduces each redex to the evaluated form.

Substitution

To implement \(\beta\)-conversion, it will be helpful to have a preliminary function, substitution.

substitution is going to do the actual work of taking input of the application and putting it into our expression².

def substitute(original_term: Term, term_to_sub_in: Term, replacement_target: Variable | Constant, default_var_name=None) -> Term:

    match original_term:

        case Constant(name):
            return term_to_sub_in if (
                isinstance(replacement_target, Constant) and 
                name == replacement_target.name
            ) else original_term
            
        case Variable(name):
            return term_to_sub_in if (
                isinstance(replacement_target, Variable) and 
                name == replacement_target.name
            ) else original_term

        case Constant(_):
            return original_term
        case Variable(name):
            return term_to_sub_in if name == replacement_target.name else original_term
        
        case ProductType(var, term1, term2):

            new_term1 = substitute(term1, term_to_sub_in, replacement_target)

            if var.name in collect_names(term_to_sub_in) and var.name != replacement_target.name:
                fresh = fresh_var(original_term, name=default_var_name)
                while fresh.name in collect_names(original_term) or fresh.name in collect_names(term_to_sub_in):
                    fresh = fresh_var(original_term, fresh.name)
                new_term = alpha_convert(original_term, var, fresh)
                return substitute(new_term, term_to_sub_in, replacement_target)

            new_term2 = substitute(term2, term_to_sub_in, replacement_target)
            return ProductType(var, new_term1, new_term2)

        case FunctionType(var, term1, term2):

            new_term1 = substitute(term1, term_to_sub_in, replacement_target)

            if var.name in collect_names(term_to_sub_in) and var.name != replacement_target.name:
                fresh = fresh_var(original_term)
                while fresh.name in collect_names(original_term) or fresh.name in collect_names(term_to_sub_in):
                    fresh = fresh_var(original_term, fresh.name)
                new_term = alpha_convert(original_term, var, fresh)
                return substitute(new_term, term_to_sub_in, replacement_target)

            new_term2 = substitute(term2, term_to_sub_in, replacement_target)
            return FunctionType(var, new_term1, new_term2)
        
        case Application(first, second):
            return Application(
                substitute(first, term_to_sub_in, replacement_target),
                substitute(second, term_to_sub_in, replacement_target)
            )
        
        case Let(var, term1, term2, term3):
            if var.name in collect_names(term_to_sub_in) and var.name != replacement_target.name:
                fresh = fresh_var(original_term, name=default_var_name)
                while fresh.name in collect_names(original_term) or fresh.name in collect_names(term_to_sub_in):
                    fresh = fresh_var(original_term, fresh.name)
                new_term = alpha_convert(original_term, var, fresh)
                return substitute(new_term, term_to_sub_in, replacement_target)

            new_term1 = substitute(term1, term_to_sub_in, replacement_target)
            new_term2 = substitute(term2, term_to_sub_in, replacement_target)
            new_term3 = substitute(term3, term_to_sub_in, replacement_target)
            return Let(var, new_term1, new_term2, new_term3)
        
        case Prop() | Set() | Type(_) | SProp():
            return original_term
            
        case _:
            raise TypeError(f"Unexpected term type: {type(original_term)}")

Notice that if our term contains a variable with the same name as a variable bound in the inside of our expression target (“shadowing”), we use \(\alpha\)-conversion to rename that variable and keep going.

Rule

Now we’re ready for \(\beta\)-reduction.

def beta_reduce(term: Term) -> Term:
    match term:
        case Application(FunctionType(var, _, body), arg):
            # (λx:T.M) N → M[x := N]
            return substitute(body, arg, var)
        case Application(t1, t2):
            new_t1 = beta_reduce(t1)
            new_t2 = beta_reduce(t2)
            if new_t1 != t1 or new_t2 != t2:
                return Application(new_t1, new_t2)
            return term
        case ProductType(var, t1, t2):
            new_t1 = beta_reduce(t1)
            new_t2 = beta_reduce(t2)
            if new_t1 != t1 or new_t2 != t2:
                return ProductType(var, new_t1, new_t2)
            return term
        case FunctionType(var, t1, t2):
            new_t1 = beta_reduce(t1)
            new_t2 = beta_reduce(t2)
            if new_t1 != t1 or new_t2 != t2:
                return FunctionType(var, new_t1, new_t2)
            return term
        case Let(var, t1, t2, t3):
            new_t1 = beta_reduce(t1)
            new_t2 = beta_reduce(t2)
            new_t3 = beta_reduce(t3)
            if new_t1 != t1 or new_t2 != t2 or new_t3 != t3:
                return Let(var, new_t1, new_t2, new_t3)
            return term
        case _:
            return term

Looking closely, we see that if we have the Application of a FunctionType on some argument, we substitute in that expression. Otherwise, we recurse down the term and try to \(\beta\)-reduce each subterm.

Let’s look at our example of \(\beta\)-reduction in practice.

def test_beta_reduction(self):
    x = Variable("x")
    y = Variable("y")
    A = Variable("A")
    B = Variable("B")
    c = Variable("c")
        
    inner_term = FunctionType(y, B, x)
    function_term = FunctionType(x, Variable("A"), inner_term)
    term = Application(function_term, c)
            
    expected_term = FunctionType(y, Variable("B"), c)

    reduced = beta_reduce(term)
    self.assertTrue(definitionally_equal(reduced, expected_term))

Works as expected.

\(\delta\)-Conversion

The next rule is \(\delta\)-conversion. There’s two variants: “global” and “local”. Local takes variables and replaces them with their definition in the local context; global takes constants and replaces them with their definition in the global environment³. This is called “unfolding”.

def delta_reduce_local(term: Term, env: Environment) -> Term:
    match term:
        case Variable(name):
            if name in env.localContext.defined_terms:
                definition = env.localContext.defined_terms[name]
                substituted = substitute(term, definition, Variable(name))
                return delta_reduce_local(substituted, env)
            return term
        case Application(t1, t2):
            new_t1 = delta_reduce_local(t1, env)
            new_t2 = delta_reduce_local(t2, env)
            if new_t1 != t1 or new_t2 != t2:
                return Application(new_t1, new_t2)
            return term
        case ProductType(var, t1, t2):
            new_t1 = delta_reduce_local(t1, env)
            new_t2 = delta_reduce_local(t2, env)
            if new_t1 != t1 or new_t2 != t2:
                return ProductType(var, new_t1, new_t2)
            return term
        case FunctionType(var, t1, t2):
            new_t1 = delta_reduce_local(t1, env)
            new_t2 = delta_reduce_local(t2, env)
            if new_t1 != t1 or new_t2 != t2:
                return FunctionType(var, new_t1, new_t2)
            return term
        case Let(var, t1, t2, t3):
            new_t1 = delta_reduce_local(t1, env)
            new_t2 = delta_reduce_local(t2, env)
            new_t3 = delta_reduce_local(t3, env)
            if new_t1 != t1 or new_t2 != t2 or new_t3 != t3:
                return Let(var, new_t1, new_t2, new_t3)
            return term
        case _:
            return term

def delta_reduce_global(term: Term, env: Environment) -> Term:
    match term:
        case Constant(name):
            if name in env.globalEnvironment.defined_terms:
                definition = env.globalEnvironment.defined_terms[name]
                substituted = substitute(term, definition, Variable(name))
                return delta_reduce_global(substituted, env)
            return term
        case Application(t1, t2):
            new_t1 = delta_reduce_global(t1, env)
            new_t2 = delta_reduce_global(t2, env)
            if new_t1 != t1 or new_t2 != t2:
                return Application(new_t1, new_t2)
            return term
        case ProductType(var, t1, t2):
            new_t1 = delta_reduce_global(t1, env)
            new_t2 = delta_reduce_global(t2, env)
            if new_t1 != t1 or new_t2 != t2:
                return ProductType(var, new_t1, new_t2)
            return term
        case FunctionType(var, t1, t2):
            new_t1 = delta_reduce_global(t1, env)
            new_t2 = delta_reduce_global(t2, env)
            if new_t1 != t1 or new_t2 != t2:
                return FunctionType(var, new_t1, new_t2)
            return term
        case Let(var, t1, t2, t3):
            new_t1 = delta_reduce_global(t1, env)
            new_t2 = delta_reduce_global(t2, env)
            new_t3 = delta_reduce_global(t3, env)
            if new_t1 != t1 or new_t2 != t2 or new_t3 != t3:
                return Let(var, new_t1, new_t2, new_t3)
            return term
        case _:
            return term

Let’s look at a simple example:

    def test_delta_local_reduction(self):
        x = Variable("x")
        y = Variable("y")
        z = Variable("z")

        # Define x = y locally
        local_context = LocalContext(
            "TestLocal",
            {},
            {x.name: y},
            {}
        )
        env = Environment(self.global_env, local_context)
    
        # Test variable reduction
        test_term = x 
        reduced = delta_reduce_local(test_term, env)
        self.assertTrue(definitionally_equal(reduced, y))
    
        # Test reduction in nested term
        nested_term = FunctionType(z, Type(), x)
        reduced_nested = delta_reduce_local(nested_term, env)
        expected = FunctionType(z, Type(), y)
        self.assertTrue(definitionally_equal(reduced_nested, expected))

We set \(x := y\) in our local environment. delta_reduce_localreplaced \(x\) with \(y\). Global conversion works similarly.

\(\zeta\)-Conversion

\(\zeta\)-conversion is similar to \(\delta\)-conversion, but for let definitions. If you have a term like \(\text{let }x = t:T \text{ in } u\), then \(\zeta\)-conversion actually replaces all \(x\) terms in \(u\) with \(t\). After using the let definition, we don’t need it anymore, so we discard it.

Notice that substitution runs in the code below, this time for the let case:

def zeta_reduce(term: Term, env: Environment) -> Term:
    match term:
        case Let(var, t1, t2, t3):
            reduced_term1 = zeta_reduce(t1, env)
            reduced_body = zeta_reduce(substitute(t3, reduced_term1, var), env)
            return reduced_body
        case Application(t1, t2):
            new_t1 = zeta_reduce(t1, env)
            new_t2 = zeta_reduce(t2, env)
            if new_t1 != t1 or new_t2 != t2:
                return Application(new_t1, new_t2)
            return term
        case ProductType(var, t1, t2):
            new_t1 = zeta_reduce(t1, env)
            new_t2 = zeta_reduce(t2, env)
            if new_t1 != t1 or new_t2 != t2:
                return ProductType(var, new_t1, new_t2)
            return term
        case FunctionType(var, t1, t2):
            new_t1 = zeta_reduce(t1, env)
            new_t2 = zeta_reduce(t2, env)
            if new_t1 != t1 or new_t2 != t2:
                return FunctionType(var, new_t1, new_t2)
            return term
        case _:
            return term

\(\eta\)-Conversion⁴

The last type of conversion we’ll discuss in this post is \(\eta\)-expansion.

\(\eta\)-expansion says that if you have a term \(f\) of type \(A \to B\), then you can replace it with a term of type \(\lambda x:A.(f\text{ }x)\). Intuitively, taking a function and giving it an anonymous argument.

def eta_expand(term: Term, expected_type = None) -> Term:
    
    if expected_type is None:
        return term
        
    match expected_type:
        case ProductType(var, t1, t2) | FunctionType(var, t1, t2):
            fresh = fresh_var(term)
            return FunctionType(
                fresh,
                t1,
                eta_expand(
                    Application(term, Variable(fresh.name)),
                    substitute(t2, Variable(fresh.name), var)
                )
            )
        case _:
            return term

Normalization

Now that we have all the rules, we can put them together to fully normalize a term. What does normal form look like? Normal form means that the term is “as reduced as possible”: we cannot reduce the term any more.

Strong Normalization

CoC (and CiC) has a property called “strong normalization”. That means (roughly) that we’re guaranteed to reach the (unique) normal form if we just keep reducing until we can’t any more⁵.

def strong_normalize(term: Term, env: Environment) -> Term:
    current = term
    while True:
        # Try each reduction and normalize result if changed
        reduced = beta_reduce(current)
        if reduced != current:
            current = reduced
            continue
            
        reduced = delta_reduce_local(current, env)
        if reduced != current:
            current = reduced
            continue

        reduced = delta_reduce_global(current, env)
        if reduced != current:
            current = reduced
            continue
            
        reduced = zeta_reduce(current, env)
        if reduced != current:
            current = reduced
            continue
            
        # No reductions possible
        return current

Not very elegant or efficient. That being said, it may be good enough for now. We can add better normalization methods if/when we need them.

Other Normalizations

Strong normalization always puts the term in normal form. For performance reasons, this might not always be ideal.

For example, there are other normalization schemes on might use, that improve performance by only partially normalizing each term. If the partially normalized terms don’t match, you can stop because the terms aren’t the same. One such scheme is “weak-head normalization.”

I’m not going to implement anything like this yet. This post is too long already. If we need it, we can come back to it.

Term Equality

Now that we can normalize, we can check if two terms are equal:

def terms_equal(env: Environment, term1: Term, term2: Term) -> bool:
    term1_norm = strong_normalize(term1, env)
    term2_norm = strong_normalize(term2, env)
    return alpha_equivalent(term1_norm, term2_norm)

Changelog

11-30-2024: Added term equality section, modified some code to match the typing rules post.

Next Steps

We’ve skipped \(\iota\)-conversion (really it’s multiple reduction rules rolled into one). \(\iota\)-conversion is related to induction so we’ll handle that when we implement induction.

I also skipped a bunch of stuff in the documentation about subtyping relations. If these become of practical importance we will return to them.

Steps 1 and 2 of our game plan are complete. Now, we can represent terms and determine if they are equivalent. But how can we determine if a term is well-formed? For that we’ll need the typing rules, which will be the subject of the next post.

Footnotes

We won’t get to “+” or Nat in this post, as they require inductive types, but the point still stands.↩︎
Strictly speaking, substitution is a “meta-operator”. It exists outside the language. The \(\beta\)-redex is a definitionally different term than it’s evaluated form, according to our language. The substituted term, on the other hand, is definitionally equal. This StackExchange post was helpful in understanding the difference.↩︎
Coq only does this if the variables/constants are “transparent.” I’m ignoring this for now.↩︎
Only \(\eta\)-expansion is permitted. See the Coq documentation.↩︎
Coq links to this thesis by Thierry Coquand, which is in French. Sadly, I’m guessing, as I don’t speak French. Luckily, secondary sources seem to agree. C’est la vie.↩︎

Introduction

Definitional Equality

Conversion Rules

\(\alpha\)-Conversion

Variable Names

Rule

Equivalence

\(\beta\)-Conversion

Substitution

Rule

\(\delta\)-Conversion

\(\zeta\)-Conversion

\(\eta\)-Conversion4

Normalization

Strong Normalization

Other Normalizations

Term Equality

Changelog

Next Steps

Footnotes

\(\eta\)-Conversion⁴