143 Frame Negation, Protected Comprehensions, and Unary Frames

Current-frame negation

pointNot(γ_current, γ)
{
    return ⟨
        result(γ)
        for
        free(γ_current) ∪ free(γ)
        where
        formula(γ_current) ∧ ¬formula(γ)
    ⟩
}

pathComplement(γ_current, γ, P)
{
    let F = free(γ)
    let Q_close =
        (vars(F) \ vars(free(γ_current)) \ P)
        ∩ FV(formula(γ))
    let Q_keep = vars(F) ∩ P ∩ FV(formula(γ))
    let K_close = decls(F, Q_close)
    let K_keep = decls(F, Q_keep)

    return ⟨
        result(γ_current)
        for
        free(γ_current) ∪ K_keep
        where
        formula(γ_current) ∧ ¬∃(K_close) formula(γ)
    ⟩
}

Both operations are logical negations. Any limits on materialising complements are operational limits, not denotational restrictions. pathComplement retains free variables for protected variables from the negated frame when those variables remain free in the returned formula.

Since the frame γ is normally translated in an environment containing γ_current, formula(γ) may already contain conjuncts from formula(γ_current). Implementations may factor out those known conjuncts before placing formula(γ) under negation; the denotation is unchanged in the returned frame because formula(γ_current) is conjoined outside the negation.

Protected comprehensions

Folds and cardinality expressions turn a unary frame into a set comprehension. In a current frame, some variables remain free in the comprehension term rather than being bound inside it. The protected set P records variables that the caller has already decided to retain; the current frame may also contribute protected variables when the folded value does not itself bind the current result.

comprehension(Γ, P, γ)
{
    let γ₀ = currentFrame(Γ)
    let (a,C,T) = unary(γ)
    let bindsCurrent =
        result(γ) = result(γ₀)
        or FV(C) ∩ vars(free(γ₀)) ≠ ∅

    let Ψ = formula(γ)
    for each γ_known in Γ
    {
        if γ_known = γ₀ and bindsCurrent
            continue
        if γ_known = γ₀ and vars(free(γ_known)) ∩ vars(P) = ∅
            continue
        if vars(free(γ_known)) ∩ vars(P) ≠ ∅
            Ψ = Ψ with formula(γ_known) factored out
    }

    let P' = vars(P)
    if bindsCurrent
        P' = P' \ vars(free(γ₀))
    else
        P' = P' ∪ vars(free(γ₀))

    let Q = vars(free(γ)) \ P'
    let D = { V:T | (V,T,a) ∈ free(γ) and V ∈ Q }
    let K = { d ∈ free(γ) | var(d) ∈ P' ∩ (FV(Ψ) ∪ FV(C)) }

    return (
        { C:T for D where Ψ },
        K
    )
}

The returned set K is retained by the caller, because those protected variables remain free in the comprehension term. As with negation, conjuncts that are already known outside the fold may be factored out of formula(γ) as a normalization step. Cardinality expressions protect the current frame before calling comprehension, so receiver predicates such as s.supplier(S) are not counted inside the per-receiver set.

Unary frames

Many rules require a unary frame:

unary(γ)
{
    if result(γ) does not contain exactly one term
        raise error

    return the unique (a,C,T) ∈ result(γ)
}

A unary frame may still have a non-trivial formula and free variables.

Examples

10

{
  _anon_ = 10:Integer
}

∅

true

s.supplier

{
  supplier = S:Supplier
}

{
  S:Supplier from supplier
}

s.supplier(S)

s.supplier.name

{
  name = N:String
}

{
  N:String from name
}

∃S:Supplier (
  s.supplier(S)
  ∧ S.name(N)
)

s.supplier.(status*rating)

{
  _anon_ = T*Q:Real
}

{
  T:Integer from status,
  Q:Real from rating
}

∃S:Supplier (
  s.supplier(S)
  ∧ S.status(T)
  ∧ S.rating(Q)
)

s.supplier.(status*rating).Σsum

{
  _anon_ = X:Real
}

{
  X:Real from _anon_
}

X = Σsum({
  T*Q : Real
  for(T:Integer, Q:Real)
  where ∃S:Supplier (
    s.supplier(S)
    ∧ S.status(T)
    ∧ S.rating(Q)
  )
})