142 Vertical Frame Operations

Vertical frame operations

Vertical composition is current-frame-sensitive. The right-hand frame is translated in an environment where the left-hand frame is the current frame.

bind∃(γ_left, γ_right, P)
{
    let D = vars(free(γ_left)) \ FV(result(γ_right))

    if D ∩ FV(formula(γ_right)) = ∅
        return γ_right

    let γ =
        ⟨
          result(γ_right)
        for
          free(γ_left) ∪ free(γ_right)
        where
          formula(γ_left) ∧ formula(γ_right)
        ⟩

    let Q =
        (vars(free(γ_left)) \ P)
        ∩ FV(formula(γ))
        \ FV(result(γ))

    return close∃(γ, Q)
}

bind∃ is ordinary path composition. If the right-hand formula still depends on variables from the left-hand frame, the left-hand formula is carried forward before non-result, non-protected variables are closed. This includes protected variables: protection prevents capture, but it does not make the formula that introduced the protected variable optional.

bind∀(γ_left, γ_right, P)
{
    let γ =
        ⟨
            result(γ_right)
            for free(γ_left) ∪ free(γ_right)
            where formula(γ_left) → formula(γ_right)
        ⟩

    let Q =
        (vars(free(γ_left)) \ P)
        ∩ FV(formula(γ))
        \ FV(result(γ))

    return close∀(γ, Q)
}

bind∀ is universal path composition. The intermediate implication frame keeps free variables from both sides because the formula mentions both formula(γ_left) and formula(γ_right).