149 Denotation of Scalar Terms and Attribute Navigation

1. Scalar terms and function application

Function application covers literals, arithmetic, comparisons, type tests, boolean connectives, ordinary function calls, symbolic constants, finite value-set literals, and references to program variables. Boolean expressions are scalar terms until a rule lifts them into the formula layer.

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

    for each i
    {
        let γᵢ = ℒ(Γ, P, Eᵢ)
        let (aᵢ,Cᵢ,Tᵢ) = unary(γᵢ)
    }

    let T = resulttype(f, T₁, ..., Tₙ)

    return ⟨
        { _anon_ = f(C₁,...,Cₙ):T }
        for
        free(γ₀) ∪ free(γ₁) ∪ ... ∪ free(γₙ)
        where
        formula(γ₀) ∧ formula(γ₁) ∧ ... ∧ formula(γₙ)
    ⟩
}

For a literal or nullary program symbol, this reduces to:

ℒ(Γ, P, c) =
    ⟨{ _anon_ = c:type(c) } for free(currentDomain(Γ)) where formula(currentDomain(Γ))⟩

2. Attribute lookup and navigation

An attribute name is resolved by searching frames from top to bottom. Within a frame, scalar result navigation is tried before structural lookup.

The set attributes(T) includes the attributes of entity, value, variant, and enum types. Variant and enum attributes therefore use the same navigation rule as ordinary entity and value attributes.

ℒ(Γ, P, a)
{
    for each γ in Γ, searching top first
    {
        // Nominal navigation: unary frame whose result type defines attribute a.
        if result(γ) = { x = C:Tₓ } and (a,T) ∈ attributes(Tₓ)
        {
            let V be fresh

            return ⟨
                { a = V:T }
                for
                free(γ) ∪ { V:T from a }
                where
                formula(γ) ∧ C.a(V)
            ⟩
        }

        // Structural lookup: the frame result already contains attribute a.
        if a = C:T ∈ result(γ)
        {
            return ⟨{ a = C:T } for free(γ) where formula(γ)⟩
        }
    }

    raise error(attribute a not found)
}

This rule carries the frame's formula into the resulting path frame. Later composition rules do not need a side condition saying that the left-hand frame was already used; it is already in formula(γ).

For example, with source variable s:ShipmentsSystem, nominal navigation of supplier introduces an uppercase logic variable S:

ℒ([], ∅, s.supplier)
  =
  ⟨
    { supplier = S:Supplier }
  for
    { S:Supplier from supplier }
  where
    s.supplier(S)
  ⟩