152 Denotation of Conditionals, Negation, Folds, and Cardinality

9. Conditional expression

The expression if A then B else C is not translated as ordinary function application. The condition and both branches are contextual expressions; a branch may carry path constraints, receiver variables, and an optional no-result denotation. The conditional introduces one shared output term, then guards the whole denotation of each producing branch.

branchIf(γ_cond, B, whenTrue, γ_branch, V, O, γ_receiver, P)
{
    let G = formula(γ_cond) ∧ (if whenTrue then B else ¬B)
    let Ψ = G ∧ formula(γ_branch) ∧ O = V
    let F = free(γ_cond) ∪ free(γ_branch)
    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, if A then E₁ else E₂)
{
    let γ₀ = ℒ(Γ, P, A)
    let (a₀,B,T₀) = unary(γ₀)
    require T₀ = Boolean

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

    let r₁ = if result(γ₁) = ∅ then noResult else unary(γ₁)
    let r₂ = if result(γ₂) = ∅ then noResult else unary(γ₂)

    if r₁ = noResult and r₂ = noResult
        return ⟨∅ for ∅ where false⟩

    require the producing branch result types have common type T

    let a be the producing branch attribute
        if all producing branches use the same one,
        otherwise _anon_
    let O:T be fresh
    let γ_receiver = if Γ = [] then noFrame else currentFrame(Γ)

    let branches = ∅
    if r₁ = (a₁,V₁,T₁)
        add branchIf(
            γ₀, B, true, γ₁, V₁, O, γ_receiver, P
        ) to branches
    if r₂ = (a₂,V₂,T₂)
        add branchIf(
            γ₀, B, false, γ₂, V₂, O, γ_receiver, P
        ) to branches

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

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

A branch with no result contributes no possible output values; it does not contribute a marker value. For example, in if email ≠ none then email else none, the then branch contributes the email values under the presence guard and the else branch contributes no values.

10. Complement and pointwise negation

ℒ(Γ, P, E!)
{
    let γ₀ = currentFrame(Γ)
    let γ = ℒ(Γ, P, E)

    return pointNot(γ₀, γ)
}

ℒ(Γ, P, E~)
{
    if Γ = []
        raise error

    let γ₀ = currentFrame(Γ)
    let γ = ℒ(Γ, P ∪ vars(free(γ₀)), E)

    return pathComplement(γ₀, γ, P)
}

11. Fold and cardinality

Folds turn a unary path frame into a set comprehension. Variables in the protected set remain free in the comprehension term; all other frame variables are bound by the comprehension. The comprehension helper is sensitive to currentFrame(Γ): if the folded value does not itself bind the current result, variables from the current frame are retained so the fold is evaluated per current receiver.

The fresh variables introduced by folds and cardinality are calculated variables. Their from component is an attribute label such as _anon_; the actual derivation is the defining equation X = Σop(comp) or N = Σcount(comp). _anon_ is the attribute name for unnamed results in unary frames.

ℒ(Γ, P, E.Σ)
{
    let γ = ℒ(Γ, P, E)
    let (comp,K) = comprehension(Γ, P, γ)
    let comp have type Set<T>
    let X be fresh of type Set<T>

    return ⟨
        { _anon_ = X:Set<T> }
        for
        { X:Set<T> from _anon_ } ∪ K
        where
        X = comp
    ⟩
}

ℒ(Γ, P, E.Σop)
{
    let γ = ℒ(Γ, P, E)
    let (comp,K) = comprehension(Γ, P, γ)
    let T_out = foldtype(op, type(comp))
    let X be fresh of type T_out

    return ⟨
        { _anon_ = X:T_out }
        for
        { X:T_out from _anon_ } ∪ K
        where
        X = Σop(comp)
    ⟩
}

Cardinality expressions are boolean scalar folds over the same comprehension:

Cardinality protects the current frame before building the comprehension. This keeps receiver predicates outside the counted set, so a path such as supplier.[city:+] counts cities per supplier rather than counting supplier-city pairs globally.

ℒ(Γ, P, E:k)
ℒ(Γ, P, E:k..m)
ℒ(Γ, P, E:?)
ℒ(Γ, P, E:+)
ℒ(Γ, P, E:k+)
{
    let γ = ℒ(Γ, P, E)
    let Pcard = P ∪ vars(free(currentFrame(Γ)))
    let (comp,K) = comprehension(Γ, Pcard, γ)
    let N be fresh of type Integer

    let Ccard =
        N = k              for E:k
        0 ≤ N ≤ 1          for E:?
        N ≥ 1              for E:+
        k ≤ N              for E:k+
        k ≤ N ≤ m          for E:k..m

    return ⟨
        { _anon_ = Ccard:Boolean }
        for
        { N:Integer from _anon_ } ∪ K
        where
        N = Σcount(comp)
    ⟩
}