151 Denotation of Path Operations and Alternatives

7. Path meet, union, and difference

The path-level logical connectives are direct calls to the horizontal frame operations:

ℒ(Γ, P, E₁ ⊓ E₂)
{
    return ℒ(Γ, P, E₁) ⊓ ℒ(Γ, P, E₂)
}

ℒ(Γ, P, E₁ ⊔ E₂)
{
    return ℒ(Γ, P, E₁) ⊔ ℒ(Γ, P, E₂)
}

ℒ(Γ, P, E₁ -- E₂)
{
    return ℒ(Γ, P, E₁) -- ℒ(Γ, P, E₂)
}

The difference rule is unrestricted logical negation. Union-compatible results are not required. Source-level path difference is written --. Scalar and set difference use the canonical set-minus character described in the lexical grammar, with keyboard backslash accepted as an input alias.

For example, s.(supplier.city ⊔ part.city) is a genuine query-level union. Both operands have result attribute city = C:String, so alignment unifies the result city term and combines the two formulas with ∨.

8. Alternative operator

The operator | is the expression-level alternative operator. It combines branches with exactly one result term by logical disjunction. The branch result names do not need to align: matching names are preserved, while differing names produce an anonymous result. Each branch contributes possible values for one shared result, which is useful for expressions such as variant-derived definitions:

sphere.(4/3*pi*radius^3) | cube.(side^3) | cone.(pi*radius^2*height/3)

Each operand must denote exactly one result. The operand result types must have a common result type. The alternative expression introduces one fresh output variable and each branch states that this output variable equals the value produced by that branch.

branchAlt(γ, C, O, γ_receiver, P)
{
    let Ψ = formula(γ) ∧ O = C
    let F = free(γ)
    let Q = vars(F)

    if γ_receiver ≠ noFrame
        Q = Q \ vars(free(γ_receiver))

    Q = Q \ P
    Q = Q ∩ FV(Ψ)

    let K = decls(F, Q)
    return ∃(K) Ψ
}

ℒ(Γ, P, E₁ | E₂)
{
    let γ₁ = ℒ(Γ, P, E₁)
    let γ₂ = ℒ(Γ, P, E₂)

    let (a₁,C₁,T₁) = unary(γ₁)
    let (a₂,C₂,T₂) = unary(γ₂)

    require T₁ and T₂ have common type T

    let a = if a₁ = a₂ then a₁ else _anon_
    let O:T be fresh
    let γ_receiver = if Γ = [] then noFrame else currentFrame(Γ)

    let Ψ =
        branchAlt(γ₁, C₁, O, γ_receiver, P)
        ∨ branchAlt(γ₂, C₂, O, γ_receiver, P)

    let F =
        { O:T from a }
        ∪ { d ∈ free(γ₁) ∪ free(γ₂) | var(d) ∈ FV(Ψ) }

    return ⟨
        { a = O:T }
        for
        F
        where
        Ψ
    ⟩
}

This rule explains why a derived attribute over variant attributes naturally renders as a disjunction. For a Shape.volume definition, the sphere, cube, and cone branch formulas are inclusive alternatives for the same output volume variable. The | operator exposes one shared result whose possible values are constrained by the disjunction of the branch formulas; if the branch result names differ, that shared result is anonymous.

The raw alternative denotation is independent of schema cardinality constraints. A later schema-aware formula simplifier may use cardinality facts for display. For example, if a branch contains two structural equalities for the same single-valued record fields, the simplifier may infer the corresponding field-term equalities and remove redundant witnesses. That is a simplification of the rendered formula, not a side condition of the | denotation rule.

Declaration-level either is intentionally outside these path-expression rules. It is not a composite expression and does not introduce a disjunction into the denotation of a path expression.