138 Frame Display Forms

The full frame notation is the precise display form because it shows the result, the free variables, and the formula. For denotation output aimed at people reading examples or debugging ordinary path translations, a shorter display form may be used: 

R where Ψ

In this short form, R is written as a comma-separated list of result bindings such as supplier=S:Supplier, and the free-variable set F is not printed. The omitted F is still part of the frame being denoted. Short form is appropriate when the renderer is not trying to communicate the exact free-variable set or provenance, or when that information is already clear from context.

Four additional rules keep short frame displays compact and unambiguous:

  • If R contains a single anonymous binding _anon_=X:T, the short form prints just X:T.
  • If Ψ is true, the short form omits where true and prints only the result.
  • If R is empty, the short form prints only Ψ. This is a zero-result frame, not an anonymous Boolean result, so no :Boolean suffix is printed.
  • If R is empty and Ψ is true, the short form prints true.

For example, the frame for s.supplier may be displayed in full as: 

⟨ {supplier=S:Supplier} for {S:Supplier from supplier} where s.supplier(S) ⟩

or in short form as: 

supplier=S:Supplier where s.supplier(S)

For a tuple-valued path such as s.supplier.(name,status), the short form is: 

name=N:String,
status=S1:Integer
where
  ∃S:Supplier (
    s.supplier(S)
    ∧ S.name(N)
    ∧ S.status(S1)
  )

An anonymous unary frame such as: 

⟨ {_anon_=X:Set<String> } for ∅ where X = { C:String for ... } ⟩

has the short form: 

X:Set<String> where X = { C:String for ... }

Likewise, a frame whose formula is true displays just its result in short form.

For a path whose result set is empty, such as s.supplier.(), the full form: 

⟨ ∅ for ∅ where ∃S:Supplier (s.supplier(S)) ⟩

has the short form: 

∃S:Supplier (s.supplier(S))

Use the full frame form whenever the exact free-variable set, variable provenance, protected variables, or frame invariants matter. Short form is only a rendering convention; it does not change the denotation.