139 Frame Construction and Closure

Source environments

Every type T determines a carrier set carrier(T) whose members are the values of that type. The construction of these carrier sets is described for structural types, value types, and entity types.

A source environment σ supplies the source-level bindings used when interpreting a frame. These include program variables, root variables, and contextual bindings such as this. If a program variable x has element type T, its current extension in σ is a subset of carrier(T) satisfying the variable's declared cardinality constraint:

σ(x) ⊆ carrier(T)

For a cardinality-one variable, this extension contains exactly one value, and the source term x denotes that value. Optional and multivalued variables instead have extensions containing the number of values permitted by their cardinality constraints. A contextual binding such as this supplies a single value in the carrier of its type.

A logic-variable assignment ρ is distinct from the source environment. It maps each generated logic variable declared in the free variables F of a frame to a value in the carrier of its declared type:

(V:T from a) ∈ F  ⇒  ρ(V) ∈ carrier(T)

Frame extension and materialisation

A frame is a logical denotation, not its materialised extension. From a frame and a source environment σ, one can derive an extension: the set of results obtained from assignments ρ for which Ψ holds, by evaluating the terms in R:

Extσ(⟨R for F where Ψ⟩) =
    { evalσ(R, ρ) | ρ assigns vars(F) and σ,ρ ⊨ Ψ }

Thus Extσ(⟨R for F where Ψ⟩) is a set of result tuples. Each tuple is keyed by attribute rather than by position. For every binding (a,E,T) in R, the tuple maps a to the single value obtained by evaluating E; that value belongs to the carrier of T.

The extension is derived from the frame; it is not the frame itself. It forgets the formula, free-variable provenance, and the result terms after they have been evaluated. Distinct frames may therefore have the same extension.

Materialising Extσ(γ) is an execution strategy, not part of the denotational definition. Negation, implication, constraints, folds, and normative systems may all be interpreted as formulas without enumerating the full extension.

Domain

For a frame γ, the domain operation removes the result while preserving the condition and free variables:

domain(γ) = ⟨∅ for free(γ) where formula(γ)⟩

This is useful when a scalar expression is evaluated inside a current frame. The current frame's condition still constrains the expression, even if the current frame's result is not retained.

The operation domain(γ) is distinct from the current frame itself. Operations such as this, splat, and attribute navigation need the result term from the current frame and therefore use the frame itself. Operations that only need the current frame's condition and free variables use domain(γ).

Closure

For a frame γ and a set Q of logic variables, close∃(γ,Q) existentially binds the selected variables, while close∀(γ,Q) universally binds them. Both operations have the preconditions:

Q ⊆ vars(free(γ))
Q ⊆ FV(formula(γ)) \ FV(result(γ))

Thus every variable in Q has a typed declaration in the frame, occurs free in the formula, and does not occur in the result. The operations recover the declarations and their types from free(γ):

close∃(γ, Q)
{
    let K = decls(free(γ), Q)
    return ⟨result(γ) for free(γ) \ K where ∃(K) formula(γ)⟩
}

close∀(γ, Q)
{
    let K = decls(free(γ), Q)
    return ⟨result(γ) for free(γ) \ K where ∀(K) formula(γ)⟩
}

Example of closure

Continuing the supplier example from 137 Frames, translating s.supplier.name produces the following frame before closure, with both the supplier variable S and the result variable N free:

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

The ordinary composition rule closes the supplier variable that is not needed by the result:

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

Trying to close N would be an error, because N appears in the result { name = N:String }.