137 Frames

A frame is the logical denotation of a Predica path expression. Frames were informally described in 22 Navigation as the three components of a set builder notation of an n-ary relation. We will now give a more formal definition.

A frame records three things: the result of the expression, the generated logic variables that remain free, and the formula that constrains those variables. Every path expression denotes a frame:

⟨R for F where Ψ⟩

where:

R ⊆ AttrName × Term × Type

R = { supplier = S:Supplier, _anon_ = T+10:Integer }

F ⊆ Var × Type × AttrName

{ S:Supplier from supplier, C:String from city }

This notation is a mnemonic for the triple (R,F,Ψ):

result R, for free variables F, where formula Ψ holds.

The key of R is the attribute name:

(a,E₁,T₁) ∈ R ∧ (a,E₂,T₂) ∈ R  ⇒  E₁ = E₂ ∧ T₁ = T₂

The key of F is the variable:

(V,T₁,a₁) ∈ F ∧ (V,T₂,a₂) ∈ F  ⇒  T₁ = T₂ ∧ a₁ = a₂

Attribute navigation

The lowercase source variable s is a Predica source-code variable of type ShipmentsSystem. It denotes the shipments system supplied by the surrounding program.

The denotation introduces fresh logic variables to range over values reached by path navigation. The uppercase logic variable S is the fresh logic variable of type Supplier introduced by the path expression below.

The logical denotation of the path expression s.supplier is the frame ⟨R for F where Ψ⟩ where:

{
  supplier = S:Supplier
}

{
  S:Supplier from supplier
}

s.supplier(S)

In classical first order logic predicates are global. In this denotational semantics the logic formulas instead involve qualified unary predicates. For example, the attribute supplier is a unary predicate that must be qualified, as in s.supplier(S).

Computed result term

The special attribute _anon_ is used for unnamed results in unary frames. R may contain terms that are not variables, such as arithmetic expressions, boolean expressions, or set comprehensions.

Consider the logical denotation of the path expression s.supplier.(status*rating). This path first ranges over suppliers of s, then has the computed term T*Q as its anonymous result.

It has a frame ⟨R for F where Ψ⟩ where:

{
  _anon_ = T*Q:Real
}

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

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

Here R contains the term T*Q. The variables used by that term are recorded separately in F.

Similarity to set builder notation

The notation ⟨R for F where Ψ⟩ reads like a set-builder expression:

⟨ result for free variables where condition ⟩

but the brackets ⟨...⟩ are not curly braces {...}. It retains the components R,F,Ψ without building a set. It keeps the denotation symbolic as logic, so later path operations can compose, close, negate, or fold it without first materialising an extension.

Accessors

For a result binding r = (a,E,T):

attribute(r) = a
term(r)      = E
type(r)      = T

For a free-variable declaration d = (V,T,a):

var(d)        = V
type(d)       = T
provenance(d) = a

For a result R, a free-variable set F, and a set Q of logic variables:

attrib(R)  = { attribute(r) | r ∈ R }
vars(F)    = { var(d) | d ∈ F }
decls(F,Q) = { d ∈ F | var(d) ∈ Q }

For a frame γ = ⟨R for F where Ψ⟩:

result(γ)  = R
free(γ)    = F
formula(γ) = Ψ

Quantification over declarations

Quantification over a set of free-variable declarations retains their types while ignoring their provenance attributes. If:

K = {
    V₁:T₁ from a₁,
    ...,
    Vₙ:Tₙ from aₙ
}

then:

• ∃(K) Ψ abbreviates ∃V₁:T₁ ... ∃Vₙ:Tₙ Ψ.
• ∀(K) Ψ abbreviates ∀V₁:T₁ ... ∀Vₙ:Tₙ Ψ.
• ∃(∅) Ψ = Ψ.
• ∀(∅) Ψ = Ψ.

Provenance attributes

The provenance attribute a in a triple (V,T,a) in F is only informational. For example, the following records that S was introduced by the supplier attribute:

S:Supplier from supplier

When V is introduced by attribute navigation, a is the attribute whose extension produced V by ranging over that extension. When V is introduced by a calculation, fold, or cardinality expression, a may be _anon_ or the result attribute. The calculation itself is represented by the result term and formula, not by a.

Multiple different variables may have the same attribute label in F. This is intentional: F is not a result.

Well-formed frames

A frame γ = ⟨R for F where Ψ⟩ is well formed when:

• R is keyed by attribute name.
• F is keyed by logic variable.
• Every free logic variable in Ψ or in a result term is declared in F.
• Every variable declared in F occurs free in Ψ or in a result term.
• Bound variables do not appear in F.
• Types are consistent between free variables, result terms, predicates, and functions.

Equivalently:

vars(F) = FV(Ψ) ∪ FV(R)

where FV(R) means the free logic variables occurring in the terms of R. This equality is about logic variables, not source-level program terms.

Source-level values supplied by the surrounding program, such as a root variable or the this value supplied to a constraint, are terms rather than generated logic variables. They therefore require no entry in F merely because they occur in R or Ψ.