141 Horizontal Frame Operations

Horizontal frame operations

The three horizontal operations differ only in the formula combiner used after result alignment. All three produce the union of the aligned results and declare the union of the free variables, including any fresh variables introduced by union alignment.

combine(α, κ, γ₁, γ₂)
{
    let (γ₁', γ₂') = α(γ₁, γ₂)

    return ⟨
        result(γ₁') ∪ result(γ₂')
        for
        free(γ₁') ∪ free(γ₂')
        where
        κ(formula(γ₁'), formula(γ₂'))
    ⟩
}

γ₁ ⊓ γ₂ = combine(align, (Ψ₁,Ψ₂) ↦ Ψ₁ ∧ Ψ₂, γ₁, γ₂)
γ₁ ⊔ γ₂ = combine(alignUnion, (Ψ₁,Ψ₂) ↦ Ψ₁ ∨ Ψ₂, γ₁, γ₂)
γ₁ -- γ₂ = combine(align, (Ψ₁,Ψ₂) ↦ Ψ₁ ∧ ¬Ψ₂, γ₁, γ₂)

The difference operation is logical difference, not relational-algebra difference. It does not require union-compatible results. The abstract path-difference operator is written --, distinct from scalar and set difference. Scalar and set difference use the canonical set-minus character described in the lexical grammar, with keyboard backslash accepted as an input alias.

Because horizontal operations expose the union of the aligned results, some result variables may be unconstrained in some branches of the formula. This is intentional. A frame is a logical denotation over assignments, not a promise that the extension can be finitely materialised by enumeration. Materialising such a frame may require finite domains, active-domain evaluation, solvers, indexes, or other execution assumptions; those assumptions are operational and do not restrict the denotation.

Tuple construction uses a stricter result merge than path-level meet and union. Tuple components are constructing a result, and duplicate attribute names across sibling component frames make the tuple ill formed. If the same visible variable is exposed twice and one occurrence still has its provenance label, that is also ill formed; two explicit aliases of the same variable are allowed.

tupleMerge(γ₁, γ₂)
{
    if attrib(result(γ₁)) ∩ attrib(result(γ₂)) ≠ ∅
        raise error(duplicate result attribute)

    if result(γ₁) contains a = V:T
       and result(γ₂) contains b = V:T
       and a ≠ b
       and (V:T from a ∈ free(γ₁) or V:T from b ∈ free(γ₂))
        raise error(duplicate implicit result term)

    return ⟨
        result(γ₁) ∪ result(γ₂)
        for
        free(γ₁) ∪ free(γ₂)
        where
        formula(γ₁) ∧ formula(γ₂)
    ⟩
}

For example, merging a component frame with result { name = N₁:String } and another component frame with result { name = N₂:String } is an error. tupleMerge does not try to align N₁ and N₂; duplicate result attributes are rejected because a tuple cannot contain two result bindings for name. Likewise, merging { supplier = S:Supplier } with { x = S:Supplier } is an error: the tuple would expose the implicit supplier result again under another name. Merging { y = S:Supplier } with { w = S:Supplier } is allowed when both are explicit aliases.

A genuine query-level union illustrates result alignment. The expression s.(supplier.city ⊔ part.city) asks for cities reached either through suppliers or through parts. Both operands have result attribute city = C:String, so alignment unifies the result city term before the formulas are joined by ∨. The operand frames below are shown after result alignment has unified their fresh city variables:

γ_supplier_city =
  ⟨
    { city = C:String }
  for
    { C:String from city }
  where
    ∃S:Supplier (
      s.supplier(S)
      ∧ S.city(C)
    )
  ⟩

γ_part_city =
  ⟨
    { city = C:String }
  for
    { C:String from city }
  where
    ∃P:Part (
      s.part(P)
      ∧ P.city(C)
    )
  ⟩

γ_supplier_city ⊔ γ_part_city =
  ⟨
    { city = C:String }
  for
    { C:String from city }
  where
    (∃S:Supplier (s.supplier(S) ∧ S.city(C)))
    ∨
    (∃P:Part (s.part(P) ∧ P.city(C)))
  ⟩