150 Denotation of Tuples, Filtering, and Composition

3. Renaming

ℒ(Γ, P, E as b)
{
    return relabel(ℒ(Γ, P, E), b)
}

4. Tuple construction

Tuple construction evaluates every component relative to the same current frame. Later components may also see attributes from earlier component results.

ℒ(Γ, P, (E₁, ..., Eₙ))
{
    let γ_base = currentDomain(Γ)

    if n = 0
        return γ_base

    let γ_acc = emptyFrame

    for each i
    {
        let Γᵢ = insertBeforeTop(Γ, γ_acc)
        let Pᵢ = P ∪ vars(free(γ_base)) ∪ vars(free(γ_acc))
        let γᵢ = ℒ(Γᵢ, Pᵢ, Eᵢ)

        // Attribute-set expansion.
        if result(γᵢ) = { a = A:Set<Attribute> }
        {
            let {a₁, ..., aₖ} = value(A)
            let γᵢ = ℒ(Γᵢ, Pᵢ, (a₁, ..., aₖ))
        }

        γ_acc = tupleMerge(γ_acc, γᵢ)
    }

    return γ_acc
}

The accumulated frame starts empty for non-empty tuples. Each component is still translated in the original frame environment, so the current frame's condition is carried by the component frames. The current frame and earlier tuple fields are protected while later components are translated; this matters for folds, cardinality expressions, and complements inside tuple components. The empty tuple is simply the current domain:

ℒ(Γ, P, ()) = currentDomain(Γ)

5. Filtering

A filter strengthens the current frame and preserves its result.

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

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

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

    if T ≠ Boolean
        raise error

    let Θ = formula(γ₁) ∧ C
    let F = free(γ₁)
    let Q_close =
        (vars(F) \ vars(free(γ₀)) \ P)
        ∩ FV(Θ)
    let Q_keep = vars(F) ∩ P ∩ FV(Θ)
    let K_close = decls(F, Q_close)
    let K_keep = decls(F, Q_keep)

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

This is the strict boolean-filter rule. A non-strict existence-filter mode can replace Θ with formula(γ₁), but the strict rule keeps existence tests explicit.

Because the condition expression is translated with γ₀ in the environment, formula(γ₁) may include conjuncts already present in formula(γ₀). Implementations may factor those known conjuncts out of Θ before existential closure; the displayed examples below use this normalized form.

Putting filtering and composition together, the supplier query from the foundations section:

s.supplier.[city = "London"].name

has, after the obvious formula simplifications, the frame:

⟨
  { name = N:String }
for
  { N:String from name }
where
  ∃S:Supplier ∃C:String (
    s.supplier(S)
    ∧ S.city(C)
    ∧ C = "London"
    ∧ S.name(N)
  )
⟩

The formula contains qualified unary predicates. In s.supplier(S), S.city(C), and S.name(N), the type of the value before the dot determines which attribute is meant.

6. Composition

Ordinary composition translates the right-hand expression with the left-hand frame as the current frame, then closes left-hand variables not needed by the result.

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

    return bind∃(γ₁, γ₂, P)
}

For s.supplier.name, the right-hand translation has only name = N:String in its result. Therefore bind∃ closes the supplier variable S, which is not needed by the result, and produces:

⟨
  { name = N:String }
for
  { N:String from name }
where
  ∃S:Supplier (
    s.supplier(S)
    ∧ S.name(N)
  )
⟩

Universal composition translates the right-hand expression with the left-hand variables protected, then universally closes left-hand variables not needed by the result.

ℒ(Γ, P, E₁⇒E₂)
{
    let γ₁ = ℒ(Γ, P, E₁)
    let γ₂ = ℒ(push(Γ, γ₁), P ∪ vars(free(γ₁)), E₂)

    return bind∀(γ₁, γ₂, P)
}

Because γ₂ is translated with γ₁ as the current frame, its formula may syntactically include formula(γ₁). Implementations may factor those known conjuncts out of the consequent before rendering the implication.