157 Denotation of Predica Locations

The query-frame calculus defines the value denotation of Predica expressions. Location denotation is a second, partial denotation for expressions that can be used as update targets. Query denotation answers which values an expression produces. Location denotation answers which occurrences of those values the expression can update. It retains the provenance and entity witnesses needed for writes without making those witnesses visible in the value result.

A location is an addressable place in a Predica state, not the value currently stored there. Equal values may occur in independent variable locations. Conversely, schema constraints may make several paths reach one shared entity occurrence and therefore the same attribute location. Location denotation is interpreted relative to those constraints.

States, Occurrences, and Addresses

Let σ be the pre-state in which an expression is evaluated and let Τ be the applicable schema theory. A raw entity occurrence records a receiver value together with the provenance by which it was reached from a root location:

RawOccurrence ::= Occ(RootAddress, ReceiverTerm, Provenance)

RawAddress ::=
    VarLoc(Environment, VariableName)
  | RawAttrLoc(RawOccurrence, QualifiedAttributeName)

The provenance distinguishes equal values held independently. For example, equal Supplier values held by variables a and b have occurrences rooted at different VarLoc addresses. Updating a.status therefore does not update b.status merely because the values read from a and b are equal.

Entity occurrences can nevertheless be shared. The schema theory induces an equivalence relation ~Τ on raw occurrences. Two raw occurrences are equivalent when the sharing rules generated by the applicable constraints establish that they are occurrences of the same entity in the model. A concrete entity occurrence is an equivalence class [O]Τ, and concrete addresses are:

Address ::=
    VarLoc(Environment, VariableName)
  | AttrLoc([RawOccurrence]Τ, QualifiedAttributeName)

It follows directly that attributes reached through equivalent occurrences have equal addresses:

O₁ ~Τ O₂
    ⇒ AttrLoc([O₁]Τ, T.a) = AttrLoc([O₂]Τ, T.a)

Keys, attribute constraints, inverse definitions, derived definitions, and inclusion dependencies can establish sharing. They do not make all equal entity values shared: sharing depends on the occurrences being connected by the constraints of the model in which they occur.

TODO: Define the generators of ~Τ for every constraint form that establishes sharing. The rules must specify the extension within which a key is unique and how occurrence equivalence is carried through inverse paths, derived alternatives, and inclusion dependencies.

TODO: Define an effective construction of occurrence equivalence. Its implementation may use canonical occurrence handles, key indexes, references, or another representation, but mechanical evaluation must not require deciding unrestricted logical entailment.

Raw Location Frames

Raw location denotation is written RawLoc(Τ, Γ, P, E) and mirrors the shape of a query frame:

RawLoc(Τ, Γ, P, E) = ⟪ L for F where Ψ ⟫

where:

• L is an attribute-keyed set of typed raw-address bindings, written a = A:T;
• F is the set of free logic variables retained as witnesses; and
• Ψ is the formula selecting those witnesses.

The well-formedness invariant is:

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

Variables occurring only in addresses remain visible to raw location denotation. This is what keeps the receiver and its provenance available for an update after query projection would otherwise hide them.

Concrete location denotation quotients raw occurrences by the sharing equivalence and removes duplicate concrete addresses:

Loc(Τ, Γ, P, E) = RawLoc(Τ, Γ, P, E) / ~Τ

The shorter notation Loc(Γ, P, E) used elsewhere omits Τ. It always means the concrete location denotation relative to the applicable schema theory.

Reading Locations

There are two read operations. Read₀ preserves the address witnesses needed by an update. Readᵥ existentially closes address-only witnesses so the result agrees with ordinary query denotation. The central consistency law is:

Readᵥσ(Loc(Τ, Γ, P, E)) ≡ ℒσ(Γ, P, E)

The equivalence ≡ is equality of query frames up to ordinary frame normalisation and existential closure. The law applies whenever location denotation is defined.

For a program variable location, reading returns the value held in its environment slot:

Read₀σ(⟪ { _anon_ = VarLoc(env, s):T } for F where Ψ ⟫)
  =
⟨ { _anon_ = valueσ(env, s):T } for F where Ψ ⟩

For an attribute location whose occurrence has receiver term C, reading introduces the current attribute value as a fresh logic variable:

Read₀σ(⟪ { a = AttrLoc([O]Τ, T.a):U } for F where Ψ ⟫)
  =
⟨ { a = V:U } for F ∪ { V:U from a } where Ψ ∧ C.a(V) ⟩

where C = receiver(O)

This read must be independent of the representative O chosen from [O]Τ. Optional and set-valued attributes remain addressable when their current extensions are empty; absence of a value witness does not imply absence of the location.

TODO: Prove that reading and writing an attribute location are well-defined on occurrence equivalence classes: equivalent representatives must produce the same read and the same state transition.

Basic Raw Location Rules

Location denotation is partial. It is defined for mutable variables, mutable base attributes, and structured targets whose components have location denotations. It is undefined for literals, arithmetic expressions, function calls, comparisons, folds, and derived or read-only attributes unless an explicit inverse update rule supplies a location denotation.

Variables

RawLoc(Τ, [], ∅, s)
  =
⟪ { _anon_ = VarLoc(env, s):ShipmentsSystem }
  for ∅
  where true ⟫

Attribute locations

When the current receiver frame exposes C:T together with occurrence witness O, and T declares a mutable base attribute a:U, the raw location is:

RawLoc(Τ, Γ, P, a)
  =
⟪ { a = RawAttrLoc(O, T.a):U }
  for free(γ) ∪ occurrenceVars(O)
  where formula(γ) ⟫

where γ ∈ Γ, result(γ) = { x = C:T }, and receiver(O) = C

Unlike query navigation, this rule does not add C.a(V) to the formula. The attribute location exists even when its extension is empty. The value predicate is added only when the location is read.

Composition

For a composed target E₁.E₂, the left side selects receiver values using query denotation while raw location evaluation retains the root and path provenance of those receivers. The right side is then interpreted as a target relative to the resulting receiver occurrences:

RawLoc(Τ, Γ, P, E₁.E₂)
{
    let γ₁ = ℒ(Γ, P, E₁)
    let Ω₁ = receiverOccurrences(Τ, Γ, P, E₁, γ₁)
    return RawLoc(Τ, pushOccurrences(Γ, γ₁, Ω₁), P, E₂)
}

This is not an inversion of query semantics. Query denotation selects the receiver values; raw location evaluation additionally preserves how each selected occurrence was reached. Filters retain the provenance of the receivers that satisfy their conditions.

TODO: Define receiverOccurrences and pushOccurrences for every path-expression form. In particular, projection and existential closure in the value frame must not discard provenance needed by a later update target.

Structured targets

RawLoc(Τ, Γ, P, (E₁, ..., Eₙ))
{
    return rawLocationTupleMerge(
        RawLoc(Τ, Γ, P, E₁), ..., RawLoc(Τ, Γ, P, Eₙ))
}

Each component must have a location denotation. Result attributes must be unique, formulas are conjoined, and free and occurrence witnesses are unioned. A structured target is invalid if two of its fields reduce to the same concrete address and would supply competing replacements.

Assignability

assignable(Τ, Γ, P, E)
  ⇔ Loc(Τ, Γ, P, E) is defined and writable(Loc(Τ, Γ, P, E))

Failure to form a location denotation is an invalid update target. A valid location frame whose formula selects no occurrences is instead a zero-location update and performs no writes.

Every address has an element type and cardinality obtained from the variable environment or schema:

elem(VarLoc(env, x)) = element type of x
card(VarLoc(env, x)) = cardinality of x

elem(AttrLoc([O]Τ, T.a)) = declared element type of T.a
card(AttrLoc([O]Τ, T.a)) = declared cardinality of T.a

validWrite(A, X)
  ⇔ (∀v ∈ X. v isa elem(A)) ∧ |X| ∈ card(A)

For a required location, X contains exactly one value. For an optional location it contains zero or one value, and assigning none supplies the empty extension. For a set-valued location, X is the replacement extension. The same rule covers all other declared cardinality bounds.

Writing and State Transitions

Writing is a semantic state transformation:

Write(σ, A, X) = σ′

For a VarLoc, the transformation replaces the value in that variable slot. For an AttrLoc, it replaces the attribute extension of the shared entity occurrence. Every path that reaches the same occurrence class subsequently reads the replacement. This requirement is independent of whether an implementation mutates shared storage, updates indexes, or reconstructs enclosing values.

TODO: Complete the definition of Write for shared entity occurrences. It must state how a revised occurrence is reflected in every base extension containing it, preserve constraints on enclosing values, and cover changes to both key and non-key attributes.

Assignment and Compound Updates

For T := E, the target locations and right-hand query frame are evaluated in the same statement pre-state:

λ = Loc(Τ, Γ, P, T)
ρ = ℒ(Γ, P, E)

If λ and ρ each contain one binding, they align regardless of attribute name. Otherwise their attributes must match exactly. Each aligned right-hand result supplies the replacement extension for the corresponding target address.

The target must be assignable, right-hand element types must be assignable to the target element types, and static right-hand cardinalities must fit the target cardinalities. Runtime extensions are then checked with validWrite. All selected addresses and replacements are computed and validated before any write is applied. Failure leaves the statement state unchanged.

The selected concrete addresses form a set, not a bag. Several paths or witness assignments that reduce to the same address cause that address to be read and written once. Writes to distinct addresses are applied simultaneously to produce the statement post-state.

Numeric and string compound operators read each selected address in the pre-state, compute its replacement, and apply the same validation and simultaneous-write rules. For ordinary value-typed extensions, ∪=, ∩=, and ∖= compute set union, intersection, and difference respectively.

For an entity-typed extension, ∪= is a keyed extension update: it inserts a right-hand member whose key is absent and replaces the existing member whose key is present.

TODO: Complete keyed ∪= for set-valued right-hand operands and for the case where different candidate keys match different existing members. The Updates part records the available design choices and the provisional recommendation.

Supplier and Part Sharing Example

Consider a schema in which Supplier.shipment contains shipments constrained to name that supplier, Part.shipment contains shipments constrained to name that part, Shipment has key {supplier, part}, and ShipmentsSystem.shipment is derived as the alternative of the two shipment paths. Let s be a supplier, p a part, and h their shipment.

s.shipment.[part = p].qty
p.shipment.[supplier = s].qty

Raw location evaluation retains two path occurrences for h, one reached through the supplier and one through the part. The ownership constraints, derived alternative, and shipment key establish that those occurrences are shared:

O_supplier ~Τ O_part

Both targets therefore reduce to:

AttrLoc([O_supplier]Τ, Shipment.qty)
  = AttrLoc([O_part]Τ, Shipment.qty)

Assigning a quantity through either path changes this one location. Reading through the other path, or through the derived ShipmentsSystem.shipment path, observes the assigned quantity. This is a required semantic behaviour and is the principal worked test for the completed occurrence-equivalence and Write rules.