96 Implementation Notes

This chapter collects implementation-facing consequences of the relation view. It is informative. The semantic authority remains the logic-frame denotation of path expressions. Relations, s-tuples, m-tuples, and m-relations are useful ways to explain, materialise, index, and optimise corresponding extensions of those frames.

Implementation Freedom

An implementation is not required to materialise relation extensions. For a query result it may:

• keep the logic frame symbolic;
• compile the frame into an iterator or query plan;
• materialise the s-relation extension;
• store indexes over the underlying unary predicate extensions;
• use m-relations or another factorised representation;
• use finite active domains for specific materialised operations.

These choices are physical choices. The obligation is that externally visible results agree with the logic-frame semantics and, when a relation view is exposed, with the relevant s-relation extension under its heading.

Expansion Is the Trust Boundary

An m-relation is a valid implementation representation only relative to a heading and domain context. The representation is correct when heading-relative expansion gives the intended s-relation extension:

M represents S under H  iff  M!_H = S

Equality of m-relation data structures is therefore not the important equality. Two different m-relations may be equally valid when they have the same heading-relative expansion:

M ≡_H N  iff  M!_H = N!_H

This is the same boundary used for accessors. If a materialised accessor is implemented directly on an m-relation, it must be defined exactly when the accessor on the expanded s-relation is defined, and it must return the same result.

Operation Obligations

An m-relation operation is valid when it commutes with the corresponding s-relation operation under heading-relative expansion:

op_m(M1, ..., Mn)!_H = op_s(M1!_H, ..., Mn!_H)

This form is the test for proposed implementation operations. The operations may be chosen for performance, compactness, streaming, or index use, but their externally visible result is judged by expansion.

(M ∪ N)!_H = M!_H ∪ N!_H

(M ∧ N)!_H = M!_H ⋈ N!_H

(not M)!_H = universe(H) \ M!_H

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

π_A^m(M)!_A = π_A(M!_H)

normalize(M,H)!_H = M!_H

Normalisation

Normalisation is an implementation freedom. It may remove redundancy, simplify rectangles, and improve later operations. A normalisation pass may, for example:

• discard m-tuples whose expansion under the heading is empty;
• drop attributes whose value set is the whole heading domain;
• remove an m-tuple whose expansion is contained in another m-tuple's expansion.

The implementation does not need a unique normal form. It only needs preservation of the extension under the chosen heading. If two normalisers produce different m-relation structures with the same expansion, they are equivalent for this purpose.

Important Pitfalls

The finite checker and the examples in this part highlight several pitfalls.

• Projection must account for unsatisfiable m-tuples before dropping attributes. Otherwise it can invent rows by removing the attribute whose empty value set made the rectangle empty.
• Complement is heading-relative and domain-relative. It cannot be computed from the relation body alone.
• Attribute-wise negation is not semantic complement. Complement requires an s-tuple to escape on at least one constrained attribute, not every constrained attribute.
• Attribute-wise union of m-tuples is not ordinary relation union. It forms one larger rectangle, while disjunction of rectangles is usually a set of rectangles.
• Partial expansion is not a substitute for heading-relative expansion. Losing the heading can invalidate algebraic laws that hold under a fixed heading.

Finite Law Checker

The development harness:

implementation/predica/python/m-relation/test.py

checks candidate laws over small finite universes. It is not a proof system and is not the specification. Its purpose is to expose bad candidate operations quickly and to build confidence before committing a law to prose or proof.

The checker has three modes:

• fast: a small random sample intended for development.
• deep: a larger random sample intended for higher confidence.
• exhaustive: enumeration of finite cases up to a chosen m-relation size.

For example:

python3 implementation/predica/python/m-relation/test.py --mode fast
python3 implementation/predica/python/m-relation/test.py --mode deep
python3 implementation/predica/python/m-relation/test.py --mode exhaustive --max-relation-size 2

The useful tested ideas include:

• m-lift preserves expansion;
• m-relation union and pairwise meet commute with heading-relative expansion;
• normalisation preserves heading-relative expansion and is idempotent in the tested finite model;
• compact complement and compact difference match exact multiply-out definitions;
• fixed-heading complement, difference, double complement, excluded middle, non-contradiction, and De Morgan laws hold modulo heading-relative expansion;
• extensional projection commutes with heading-relative expansion;
• naive projection works only under its precondition.

The checker also records expected counterexamples for tempting definitions, including attribute-wise negation as complement, pairwise generalised union as relation union, and algebraic reasoning over partial expansion where a fixed heading is required.

Specification Status

This chapter should be read as guidance for preserving the relation view efficiently. It does not require a particular storage structure, query engine, normal form, or finite-domain strategy. It does require that any externally visible relation result, relation accessor, or implementation-facing m-relation operation agree with the logic-frame semantics through the appropriate heading-relative extension.