148 Denotation Environment

The denotational rules define the frame denoted by each path expression. Most of the work is delegated to frame operations such as domain, relabel, close∃, close∀, ⊓, ⊔, --, tupleMerge, bind∃, and bind∀.

The rough mental model is that a rule translates an expression relative to the current frame and returns a new frame. The environment stack is bookkeeping for the cases where more information is available: structural lookup through enclosing frames, let-bound names, and tuple components already constructed.

Examples use the display notation introduced in the frame calculus section:

result(γ) = { attr = Term:Type, ... }
free(γ) = { Var:Type from attr, ... }

The formal triples are still present: Attr = Term:Type is (Attr,Term,Type) in the result, and Var:Type from Attr is (Var,Type,Attr) in the free variables. Lowercase names such as s are Predica source-code variables supplied by the program; uppercase names such as S, P, SP, N, and C are generated logic variables.

Environment and denotation function

An environment stack is a stack of frames. The top frame is the current frame; lower frames are available for structural lookup, let-bound names, and tuple-local names.

Γ = [γ₀, γ₁, ..., γₙ]
top(Γ) = γₙ
init(Γ) = [γ₀, γ₁, ..., γₙ₋₁]

ℒ(Γ, P, E) = γ

The protected set P contains variables protected from closure introduced while translating E.

emptyFrame = ⟨∅ for ∅ where true⟩

topOrEmpty(Γ)
{
    if Γ = []
        return emptyFrame
    else
        return top(Γ)
}

currentFrame(Γ) = topOrEmpty(Γ)

currentDomain(Γ) = domain(currentFrame(Γ))

push(Γ, γ) = Γ with γ appended on top

Some helper rules use the following meta-level sentinels. They are not Predica expressions, not values, and not frames in the semantic domain:

noFrame  = absence of a receiver frame
noResult = absence of a produced result term

currentFrame is the top frame, including its result. currentDomain is the same frame viewed only through its free variables and formula. Scalar terms use currentDomain; operations such as this, splat, and attribute navigation use frames with their results from the environment.

Tuple construction needs a way to make earlier tuple components available to later tuple components without replacing the current frame:

insertBeforeTop(Γ, γ)
{
    if result(γ) = ∅
        return Γ
    elif Γ = []
        return [γ]
    else
        return init(Γ) ⊕ [γ] ⊕ [top(Γ)]
}