89 Notation and Surface Syntax

The Relations part uses several kinds of notation. Some examples are Predica source syntax, some are logic-frame display notation, and some are mathematical notation for relation views or implementation structures. This chapter fixes how to read those notations.

Three Layers of Notation

s.supplier.name
s.shipment.(supplier.name as sname, qty)
s.supplier -- s.shipment.supplier

name=N:String
where ∃S:Supplier (
    s.supplier(S)
    ∧ S.name(N)
)

{ id: 17 }
M!_H
M ≡_H N
π_A(M!_H)

A code block marked language-predica is intended as Predica source syntax. A code block marked language-predicalogic is usually a display of the logic-frame view; it may also be used for relation-view laws when the same symbolic highlighting improves readability. The surrounding text, not the highlighting class alone, determines which layer the notation belongs to. Unmarked code blocks in this part are usually mathematical or explanatory notation for relations, tuples, headings, and m-relations.

Relation-View Notation

The following notation is used to describe relation views and does not by itself introduce Predica surface syntax:

• s-tuples such as { id: 17, city: "London" };
• relation bodies such as { { id: 17 }, { id: 23 } };
• headings such as { id: Integer, city: String };
• projection notation such as π_A(R);
• universe notation such as universe(H);
• m-tuples such as < id: {17}, city: {"London", "Athens"} >;
• heading-relative expansion such as M!_H;
• m-relation equivalence such as M ≡_H N;
• m-relation algebra displays such as M ∧ N, M ∪ N, not M, and M -- N.

These notations are part of the explanatory and implementation-facing relation view. They are useful for specifying what an implementation must preserve, especially through heading-relative expansion, but they should not be read as a promise that Predica has relation literals or first-class relation algebra in surface syntax.

Overlapping Symbols

Some symbols also occur in Predica source expressions. For example:

s.supplier -- s.shipment.supplier

is a Predica path expression using path difference. By contrast:

(M -- N)!_H = M!_H \ N!_H

is relation-view notation saying that an m-relation difference operation must expand to ordinary s-relation difference under heading H.

The same caution applies to union, meet, complement, and projection notation. When the notation appears in a Predica source block, it is source syntax. When it appears in a relation law, it is mathematical notation for the relation view unless the surrounding chapter explicitly says otherwise.

Accessor Conventions

The notations $set, $tup, and $val are treated specially in this part. They name checked, lossy accessors from materialised relation-shaped results:

• R.$set extracts a set from a unary materialised relation;
• R.$tup extracts the single tuple from a singleton materialised relation;
• R.$val extracts the single value from a singleton unary materialised relation.

This chapter does not decide whether these exact spellings are mandatory Predica surface syntax, library operations, debugger conveniences, or implementation API names. It specifies the relation view behaviour that any such accessor must have if exposed.

M-Relation Notation

M-relation notation is implementation-facing. An implementation may store an m-relation-like structure, or it may use another factorised representation. The notation:

M!_H
M ≡_H N
normalize(M,H)

is used to state correctness obligations. It is not user-facing query syntax unless a later language chapter explicitly adopts it.

Relation Literals

Examples in this part sometimes display relation bodies directly:

{
    { id: 17, city: "London" },
    { id: 23, city: "Paris" }
}

These displays are examples of relation extensions. They do not establish relation literals as Predica source syntax. If Predica later adopts relation literals, their syntax and typing rules should be specified in the Syntax and Query parts, not inferred from these explanatory displays.