140 Frame Relabelling and Merge

Relabelling

Relabelling changes the result attribute name of a unary frame. It does not change free(γ); the attribute labels in free(γ) describe where variables were introduced, not the current result attribute name.

relabel(γ, b)
{
    if result(γ) does not contain exactly one term
        raise error

    let (a,C,T) be the unique element of result(γ)

    return ⟨{ b = C:T } for free(γ) where formula(γ)⟩
}

Alignment and result merge

When two frames are combined horizontally, matching result attributes denote the same result attribute. Alignment unifies their terms and types; incompatibility is an error for meet and difference.

align(γ₁, γ₂)
{
    for every attribute a in attrib(result(γ₁)) ∩ attrib(result(γ₂))
    {
        let (a,C₁,T₁) ∈ result(γ₁)
        let (a,C₂,T₂) ∈ result(γ₂)

        unify T₁ with T₂
        unify C₁ with C₂

        if unification fails
            raise error
    }

    apply the resulting substitution to both frames
    return (γ₁', γ₂')
}

Union has one additional alignment case. If two matching result attributes have the same type but their terms cannot be unified, union may introduce a fresh variable V for that attribute, replace the result term in both branches by V, conjoin V = C₁ to the left branch and V = C₂ to the right branch, and declare V in the free variables of the aligned frame.

Fresh variables introduced by one translation run are globally fresh, except where frames are reused from the environment or matching attributes are explicitly unified. Therefore sibling frames do not need alpha-renaming before alignment. Implementations that compose independently translated frames may alpha-rename first.