153 Denotation of Absence, This, Splat, Let, and Constraints

12. Absence

The expression none is a curtailed no-result expression. It is not a value term and is not translated by the scalar/function-application rule. It may appear only in source contexts that explicitly permit absence, such as optional-result conditionals, presence tests, and optional location clearing. It is never a member of any value domain.

ℒ(Γ, P, none) =
    ⟨∅ for ∅ where false⟩

Source comparisons with none are desugared before denotation: E = none means E.Σempty, and E ≠ none means E.Σexists. After this rewrite, none is not passed to the scalar comparison rule as an operand.

13. this and splat

ℒ(Γ, P, this)
{
    if Γ = []
        raise error

    return currentFrame(Γ)
}

ℒ(Γ, P, *)
{
    if Γ = []
        raise error

    let γ = currentFrame(Γ)
    let (x,C,Tₓ) = unary(γ)
    let A = { a | (a,Tₐ) ∈ attributes(Tₓ) }

    return ⟨
        { _anon_ = A:Set<Attribute> }
        for
        free(γ)
        where
        formula(γ)
    ⟩
}

14. Let

ℒ(Γ, P, let a = E₁ in E₂)
{
    let γ₁ = ℒ(Γ, P, E₁)
    let (b,C,T) = unary(γ₁)

    let γₐ = ⟨{ a = C:T } for free(γ₁) where formula(γ₁)⟩
    let γ₂ = ℒ(push(Γ, γₐ), P, E₂)

    return bind∃(γ₁, γ₂, P)
}

The binding is structural: the name points to the bound value's result term while keeping the bound formula and free variables attached to it.

15. Constraints

For a constraint expression C declared on type T, start with a frame for the constrained value:

γ_this = ⟨{ this = this:T } for ∅ where true⟩
γ_C = ℒ([γ_this], ∅, C)

this is a source-level value supplied by the surrounding constraint, not a generated logic variable. Fresh variables introduced while translating the constraint are added to free(γ_C).

if result(γ_C) = { a = B:Boolean }
    constraint formula = ∀vars(free(γ_C)) ( formula(γ_C) → B )
else
    reject the constraint

Design consequences

The frame calculus has the following consequences:

• F is the set of free variables of the frame, not a result. Its attribute labels are informational and do not replace the derivation given by R and Ψ.
• The current frame and current domain are distinct views of the same top frame. Rules that need the current result value are based on the current frame rather than domain.
• Universal composition can be factored through bind∀, which selects variables satisfying the precondition of close∀.
• Filter, complement, fold, and cardinality rules show why protected variables are more than a control flag. A protected variable that remains free in the returned formula or term is retained in the returned frame's free variables.
• Tuple construction uses a stricter result merge than path-level meet and union. Duplicate result attributes and duplicate implicit result terms are rejected after attribute-set expansion, while deliberate aliases may expose the same variable under two explicit names.
• Path difference is written with source syntax --, distinct from scalar and set difference. Scalar and set difference use the canonical set-minus character described in the lexical grammar, with keyboard backslash accepted as an input alias.
• The right-hand frame in composition already contains the left-hand conditions that were available while the right-hand expression was translated.