1 Introduction to Predica

Predica is a formal language grounded in predicate logic, but unlike the Relational Model (RM), it does not begin with relations of arbitrary arity. Instead, Predica models the world as a collection of domains whose properties are expressed solely through unary predicates. This shift in foundation has many benefits, including direct cardinality control, precise handling of partial information, reduced reliance on surrogate identifiers, simple mappings to efficient implementations, modular schema evolution, and a powerful, navigation-oriented query language.

Like the RM, Predica is defined entirely at the level of logic and semantics. Nothing in the language assumes a particular storage model, indexing strategy, or execution engine. This physical independence means that a Predica specification can be executed on top of any suitable backend. A Predica compiler may for example target SQL, Cypher, Datalog, or a custom engine, while the Predica schema, constraints, and queries remain unchanged. This separation of logical meaning from physical representation allows Predica to serve as a portable semantic layer above diverse data systems.

Decomposition into domains with unary predicates

A domain is a subject of discourse: it is something about which predicates record information. A domain can be almost anything, for example a geometrical point in Euclidean space or an entire shipments system containing thousands of suppliers, parts, and shipments. A domain is simply whatever the predicates are about.

The term domain is often used differently in other literature, especially in the Relational Model and in Date & Darwen, where it refers to the set of values of an attribute type (for example, the set of integers or the set of all finite Unicode text strings). In this specification, we never use the term domain to refer to a type or to its carrier set. In particular, a Predica domain is not the mathematical set over which a logical variable ranges; that set is called the carrier of a type.

So to be clear, we use the first meaning of domain, not the second:

1. Predica: domain = subject
2. Other literature: domain = type or carrier

The world is modelled as a decomposition into domains, and all information about each domain is recorded using unary predicates.

In classical logic, unary, binary, and ternary predicates are sometimes called monadic, dyadic, and triadic. Predica uses the Latin-derived terms to avoid confusion with the unrelated notion of monads in programming and category theory.

In this specification, the word predicate refers to a symbol (or name). For this reason, we usually say predicate rather than predicate symbol. The semantic object associated with a predicate is its extension.

Example: Circle

A circle value can be regarded as a domain, having two unary predicates centre and radius.

The following relate an atomic formula for each predicate to an English gloss which we call a natural language predicate:

    centre(C) ⇔ The centre of the circle is C
    radius(R) ⇔ The radius of the circle is R

In the atomic formula centre(C), the symbol C is a logical variable ranging over points. In the atomic formula radius(R), the symbol R is a logical variable ranging over real numbers. For unary predicates, the variable name isn't important because there is only one argument position.

An instantiation of a unary predicate is an application of that predicate to one value. For example, radius(10) is a ground atomic formula obtained by instantiating radius(R) with the value 10.

The extension of a unary predicate is the set of values for which its instantiations are true. Thus, if radius(10) is true, then 10 is in the extension of radius.

The extension of centre is the set:

    { C ∈ ℝ2 | centre(C) }

A circle has exactly one centre so the cardinality of this extension is one. Similarly for the radius.

The modeling of a circle with unary predicates is associated with a value type Circle having attributes centre and radius:

value Circle
{
    Point centre;
    Real radius;
}

In this specification, the word attribute means the name. As with predicates, we usually say attribute rather than attribute name. Since we also use the word predicate for the name, we can say that an attribute is a unary predicate. That means we can speak of the extension of an attribute.

The centre of a circle is itself a domain, i.e. a subdomain, with unary predicates for its x and y coordinates, giving rise to another value type:

value Point
{
    Real x;
    Real y;
}

with unary predicates:

    x(X) ⇔ The x-coordinate of the point is X
    y(Y) ⇔ The y-coordinate of the point is Y

This is an example of domain decomposition.

Derived attributes

An attribute may be derived from other attributes rather than supplied as stored state. A derived attribute declaration begins with an arrow (→):

value Circle
{
    Point centre;
    Real radius;
    → Real perimeter = 2 * pi * radius;
    → Real area = pi * radius ^ 2;
}

The derived attributes perimeter and area are also unary predicates. Their extensions are determined by their defining expressions rather than recorded independently.

Cardinality constraints

Predica allows every attribute to declare its own cardinality constraint directly and locally. The following example illustrates the syntax:

value S
{
    Integer a;          // exactly 1
    Integer b?;         // 0 or 1
    Integer c*;         // any finite cardinality
    Integer d+;         // any nonzero finite cardinality
    Integer e[6];       // exactly 6
    Integer f[7..9];    // 7, 8 or 9
    Integer g[4..*];    // any finite cardinality of at least 4
    Integer h[0..∞];    // any cardinality, including infinite
    Integer i[1..∞];    // any nonzero cardinality, including infinite
}

All cardinality constraints are finite unless their upper bound is explicitly ∞. Thus *, + and an upper bound of * permit arbitrarily large finite extensions, but not infinite extensions. The ∞ upper bound permits finite, countably infinite or uncountable extensions, subject to the carrier of the attribute type.

For example:

value Triangle
{
    Point vertex[3];
}

This introduces the unary predicate:

    vertex(V) ⇔ V is a vertex of the triangle

The syntax [3] on the attribute vertex specifies a cardinality constraint on its extension:

    { V:Point | vertex(V) }

Here V:Point means the logical variable V ranges over values of type Point. More generally, the notation V:T means logical variable V ranges over values of type T. This notation is used in set-builder expressions and with existential and universal quantifiers, such as ∃V:T and ∀V:T.

Recursive decomposition

Predica supports two parallel forms of recursive decomposition:

1. Decomposition in the world, where domains decompose into subdomains; and
2. Decomposition in the model, where types decompose into attribute types.

In these examples both forms ultimately bottom out at the predefined simple types (Boolean, Integer, Real and String).

Predica allows self-recursive types, for example:

value List
{
    Integer head;
    List tail?;
}

A type's self-recursive structure describes how domains may reference one another, but domains themselves cannot be self-recursive. A domain may contain subdomains, but it cannot contain itself as a subdomain.

Domains that exist in time and space

The examples above use values, such as circles, as domains. An entity is a domain that is not a value, such as a person. Information about entities is likewise recorded through unary predicates. For example:

entity Person
{
    Integer id;
    String name;
    Email email*;
    PhoneNumber phone+;
    Person mother?;
    Person father?;
    → Person parent* = mother | father;
    → Person child* = inverse parent;
    → Person grandparent* = parent.parent;
    → Person sibling* = let p = this in parent.child.[this ≠ p];
    → Person cousin* = parent.sibling.child;
    → Boolean hasEmail = email.Σexists;
    key {id};
}

The derived attribute parent combines the extensions of mother and father, and child is its inverse. Further navigation derives grandparent, sibling, and cousin. The derived attribute hasEmail is true exactly when the extension of email is non-empty. Like base attributes, all of these derived attributes are unary predicates on each Person domain.

Note that we have consistently used singular names for attributes, regardless of whether their extensions may contain multiple values. For example, we used vertex in the singular, and here the email, phone, parent, child, grandparent, sibling, and cousin attributes are singular.

Typically an entity will declare key constraints, for example:

key {id};

Why distinguish entities from values?

It may initially seem simpler to declare Person as an ordinary value type. The reason for the entity distinction is that entity occurrences can be shared within a model. Schema constraints can establish that different paths reach the same person occurrence, and an update through any one of those paths then updates the location shared by all of them. A key must be unique within each applicable entity-typed attribute extension and helps the constraints identify the occurrence being reached.

For example, the same person might be reached directly from a collection of people, as the mother of one person, and as the mother of another. Where the schema constraints establish that these paths reach the same person occurrence, an update to that person's email through one path is observed through the others. Equal values held independently do not have this sharing merely because they are equal.

This does not put physical people into the formal semantics and it does not require hidden object identity. A Predica entity type still has a mathematically defined carrier of values. The entity declaration allows those values to participate in constraint-induced shared occurrences whose locations can be reached and updated through multiple paths. Later chapters define carriers, keys, constraints, and location denotation precisely.

It's like applying the RM to many domains

This is like independently applying the RM to each domain, because each domain has its own set of named relations that record the extensions of its predicates.

Note however:

• In the RM, the relvar name is the predicate.
• In Predica, the attribute is the predicate.

Consider the following schema:

entity City
{
    String name;
    key {name};
}

entity Supplier
{
    String id;
    City city*;
    key {id};
}

entity ShipmentsSystem
{
    Supplier supplier*;
}

Applying the RM recursively through nested domains means that Predica attributes can have a dual role:

• city is a predicate, and from the RM viewpoint resembles a relvar recording cities.
• city is an attribute, and from the RM viewpoint resembles an attribute of a relvar recording suppliers.

What the RM separates into relvars and attributes, Predica unifies as named attributes/predicates within domains.

Correspondence between query expressions and logic formulas

Predica query expressions correspond to logic formulas over the attributes, which are unary predicates.

For example, given a variable C of type Person the path expression C.mother.father.email has the following logic denotation:

email=E:Email
where
  ∃M:Person ∃F:Person
    C.mother(M)
  ∧ M.father(F)
  ∧ F.email(E)

Here the attributes mother, father, and email appear in the formula as unary predicates. The logical variables are M, F, and E. The result binding exposes the logical variable E under the output attribute email.

Qualified predicate names

This is not classical first-order-logic syntax, because we have qualified predicates such as C.mother. Predica needs qualified predicates because the world is decomposed into many domains, each with its own predicates, whereas classical FOL assumes a single global predicate namespace.

A formula with a qualified predicate, such as C.mother(M), is not a well-formed formula in classical first-order logic.

It can be mapped to a global binary predicate in classical first-order logic, such as mother(C,M):

Predica can be understood as reinterpreting such global binary predicates as families of unary predicates, each scoped to a particular domain instance. This preserves the familiar shape of unary predicate instantiation while avoiding global predicate names and enabling compositional path expressions.

This avoids global namespace pollution and solves a practical naming problem. Multiple types of domains may each have an attribute named city, for example Supplier.city, Warehouse.city, and Person.city. In classical FOL, these would require distinct global predicates such as Supplier_city, Warehouse_city, and Person_city, and they could not be unary predicates because they would need to identify which supplier, warehouse, or person is involved. Predica’s qualified naming is cleaner, more modular, and more readable.

2 Entity Types as Logical Sorts

Predica's approach to modelling the world gives rise to entity types such as: Supplier, Part, and Shipment. Each of these becomes a sort for variables in logic. You can constrain variables by these sorts and quantify over them. For example, in the following formula the variable P ranges over parts:

∃P:Part s.part(P)

This formula can be read in two ways:

1. Informally, P ranges over parts, and s.part(P) says that P belongs to the naive set of parts in the shipments system s. The formula says that this set contains at least one part.
2. Formally, P ranges over the carrier of the entity type Part. This carrier is a mathematical set of Part values defined by the language semantics, which are themselves defined entirely in terms of mathematical logic and set theory. The formula says that at least one of those values is in the extension of s.part. Consequently, a conforming Predica implementation can evaluate the formula in a given program state: it is true exactly when the extension of s.part contains at least one Part value.

This distinction applies throughout the specification: informal entities and naive sets belong to the subject matter being modelled, whereas entity values, carriers, and predicate extensions belong to the formal language semantics.

The RM has no direct analogue of this. It has relations and simple value types, but it does not have entity types such as Part and cannot express "a part" as a logical sort.

This absence of entity types makes the RM more cumbersome where composite keys are involved. A change to a key can require updates to many relvars with foreign keys, and can affect all applications built on top of the database. For this reason, many RM practitioners introduce surrogate identifiers to simplify foreign keys and reduce the impact of key changes.

In Predica, composite keys are used exactly when they are appropriate because the choice of key is localised to a type. For example, a Part may have a natural composite key with three attributes:

entity Part
{
    String manufacturer;
    String catalogueNumber;
    Integer revision;

    key {manufacturer,catalogueNumber,revision};
}

Changing a key affects only that type and does not propagate changes to other parts of the schema, so applications built on top of the database are largely unaffected by key changes. For example, the ShipmentSystem contains a set of parts but does not need to repeat the three key attributes, and it does not need to change if Part later changes its key:

entity ShipmentSystem
{
    Part part*;
}

Queries are independent of the chosen key as well. An application can ask for the red parts shipped by suppliers located in London:

s.supplier.[city = "London"].shipment.part.[color = Color.red]

This query navigates to Part values and filters them by colour. It does not mention the attributes that currently form the key of Part, so it does not need to be rewritten if the key of Part changes.

Its frame denotation has Part as the result sort:

part=P:Part
where
  ∃S:Supplier ∃H:Shipment
    s.supplier(S)
  ∧ S.city("London")
  ∧ S.shipment(H)
  ∧ H.part(P)
  ∧ P.color(Color.red)

Having Part available as a logical sort allows logic expressions to range over parts directly, without mentioning the attributes that currently form the key of Part.

In the RM, a relvar that refers to parts normally carries foreign-key attributes for the current key of the part relvar. If that key changes, those foreign-key attributes, joins, views, constraints, and application queries can all need corresponding changes.

3 Cardinality Constraints and 1NF

In conventional languages (SQL, OO, functional languages, JSON, UML), type and cardinality are tightly linked. If something may occur zero times, one time, or many times, the type must change: T, Optional<T>, List<T>, Set<T>, typed tuples, arrays, and so on.

Predica separates these two concepts entirely. For a given attribute the type describes what kind of value may occur in its extension and the cardinality constraint describes how many values may occur in its extension. This follows naturally from interpreting attributes as unary predicates.

For this reason the cardinality constraint is written on the attribute, not inside its type:

Email email*;

The attribute email is singular, and its declared type Email is singular too. Even so, the * cardinality constraint allows the email predicate to hold for zero or more email address values.

Attaching cardinality to attributes rather than to types looks unconventional, yet it cleanly separates “what” from “how many”, enabling flexible modelling without proliferating container types.

The natural-language predicate is likewise phrased in the singular:

    email(E) ⇔ The person has an email address E

In the formula email(E), the parameter E ranges over individual values of type Email. The extension of the email predicate may contain many such values, but each value is still a single Email value.

The 1NF distinction in Predica

In this specification the following definition of 1NF is used:

This has nothing to do with whether attribute types are simple, and it has nothing to do with the declared cardinality constraints.

Under this definition this satisfies 1NF:

entity Person
{
    String name;
    Email email*;
    key {name};
}

whereas this is a violation of 1NF:

entity Person
{
    String name;
    Set<Email> emails;
    key {name};
}

Ironically, cardinality constraints that allow multiplicity might appear to violate 1NF and they indeed allow for multiple values in attribute extensions, yet the whole point is to preserve 1NF. They allow a predicate to hold for zero, one, or many values while keeping each value singular.

4 Supplier-and-Parts Database

The following example appears in Chris Date's book An introduction to Database Systems. There are three relvars in the schema, used to represent suppliers, parts and shipments. It is a conventional normalised relational database schema.

Schema in Tutorial D versus Predica

Chris Date and Hugh Darwen defined a language named Tutorial D which is faithful to the Relational Model.

Here is a side by side comparison of the schema for the Supplier-and-parts database expressed in Tutorial D and Predica:

VAR S BASE RELATION
{
    S#     CHAR,
    SNAME  CHAR,
    STATUS INTEGER,
    CITY   CHAR
}
KEY { S# };


VAR P BASE RELATION
{
    P#     CHAR,
    PNAME  CHAR,
    COLOR  CHAR,
    WEIGHT RATIONAL,
    CITY   CHAR
}
KEY { P# };


VAR SP BASE RELATION
{
    S#   CHAR,
    P#   CHAR,
    QTY  INTEGER
}
KEY { S#, P# };


CONSTRAINT SP_S_FK
    SP { S# } ⊆ S { S# };

CONSTRAINT SP_P_FK
    SP { P# } ⊆ P { P# };

entity Supplier
{
    String id;
    String name;
    Integer status;
    String city;
    Shipment shipment* where shipment.supplier = this;
    key {id};
}

entity Part
{
    String id;
    String name;
    Color color;
    Real weight;
    String city;
    Shipment shipment* where shipment.part = this;
    key {id};
}

entity Shipment
{
    Supplier supplier;
    Part part;
    Integer qty;
    key {supplier,part};
}


entity ShipmentsSystem
{
    Supplier supplier*;
    Part part*;
    → Shipment shipment* = either
        supplier.shipment, part.shipment;
}

// Database variable of type ShipmentsSystem
var s = openDatabase<ShipmentsSystem>("/path/to/database");

The two schemas organise the same subject matter in different ways. The following table compares their database variables, nominal types, attributes, predicates, and constraints.

Example queries

The following examples express the same queries in Tutorial D and Predica, and show the logical frame denoted by each Predica path expression. These frames are obtained by the formally specified, compositional mapping defined in Part XIV: Semantics, and in particular in 150 Denotation of Tuples, Filtering, and Composition.

Suppliers located in London

S WHERE CITY = 'London' { SNAME }

s.supplier.[city = "London"].name

name=N:String
where
  ∃S:Supplier ∃C:String
    s.supplier(S)
  ∧ S.city(C)
  ∧ C = "London"
  ∧ S.name(N)

Parts supplied by supplier S1

( ( S WHERE S# = 'S1' ) JOIN SP JOIN P ) { PNAME }

s.supplier.[id = "S1"].shipment.part.name

name=N:String
where
  ∃S:Supplier ∃I:String ∃SP:Shipment ∃P:Part
    s.supplier(S)
  ∧ S.id(I)
  ∧ I = "S1"
  ∧ S.shipment(SP)
  ∧ SP.part(P)
  ∧ P.name(N)

Shipments with a quantity greater than 300

( SP WHERE QTY > 300 ) { S#, P#, QTY }

s.shipment.[qty > 300].
    (supplier.id as sid, part.id as pid, qty)

sid=SI:String, pid=PI:String, qty=Q:Integer
where
  ∃SP:Shipment ∃S:Supplier ∃P:Part
    s.shipment(SP)
  ∧ SP.qty(Q)
  ∧ Q > 300
  ∧ SP.supplier(S)
  ∧ S.id(SI)
  ∧ SP.part(P)
  ∧ P.id(PI)

Suppliers of part P2

( ( P WHERE P# = 'P2' ) JOIN SP JOIN S ) { SNAME }

s.part.[id = "P2"].shipment.supplier.name

name=N:String
where
  ∃P:Part ∃I:String ∃SP:Shipment ∃S:Supplier
    s.part(P)
  ∧ P.id(I)
  ∧ I = "P2"
  ∧ P.shipment(SP)
  ∧ SP.supplier(S)
  ∧ S.name(N)

Suppliers who supply all red parts

S WHERE NOT EXISTS (
    (P WHERE COLOR = 'Red')
    WHERE NOT EXISTS (
        SP WHERE SP.S# = S.S#
           AND SP.P# = P.P#
    )
)

s.part.[color = Color.red]⇒(shipment.supplier)

supplier=S:Supplier
where
  ∀P:Part
    (s.part(P) ∧ P.color(Color.red))
    → ∃SP:Shipment
      P.shipment(SP)
      ∧ SP.supplier(S)

Suppliers for which all shipped parts are red

S WHERE NOT EXISTS (
    (SP JOIN (P WHERE COLOR <> 'Red'))
    WHERE SP.S# = S.S#
)

s.supplier.[shipment.part.color.Σ ⊆ {Color.red}]

supplier=S:Supplier
where
  s.supplier(S)
  ∧ { C:Color | ∃SP:Shipment ∃P:Part
      S.shipment(SP)
      ∧ SP.part(P)
      ∧ P.color(C) } ⊆ {Color.red}

Supplier city, part city, and shipment quantity

( SP JOIN S JOIN P ) { SCITY := S.CITY, PCITY := P.CITY, QTY }

s.shipment.(supplier.city as scity, part.city as pcity, qty)

scity=SC:String, pcity=PC:String, qty=Q:Integer
where
  ∃SP:Shipment ∃S:Supplier ∃P:Part
    s.shipment(SP)
  ∧ SP.supplier(S)
  ∧ S.city(SC)
  ∧ SP.part(P)
  ∧ P.city(PC)
  ∧ SP.qty(Q)

Queries with unary predicates

The mapping into logic is independent of attribute cardinality constraints.

Each predicate in the formula of this denotation is unary, and yet the conjunction expresses exactly the same result as the relational algebra expression using n-ary predicates.

A conjunction of unary predicates over shared existential variables behaves as a relation with arbitrary:

• arity
• join structure
• constraints
• projections
• renamings
• navigation paths
• multiplicities
• optionalities
• cardinality patterns

The “n-ary-ness” is not in the predicates. It is in the pattern of shared variables. Unary predicates are local and simple. But when you conjoin them, you recover the full expressive power of n-ary predicates in a way that is:

• compositional
• navigational
• readable
• type-safe
• aligned with domain decomposition
• aligned with first-order logic semantics

This is one of the key conceptual advantages of Predica: it exposes the underlying logical structure directly, without requiring n-ary predicates to express n-ary relationships.

Decomposing a domain into unary predicates removes the rigid arity-coupling that binds attributes together in n-ary tuple structures. Each attribute becomes an independent predicate whose optionality, multiplicity, and evolution can be expressed without reshaping the surrounding domain. This aligns with Predica’s broader principle that domains decompose recursively into subdomains, producing models that are modular, deeply structured, and easier to extend.

Relationship to graph queries

The logical denotations above are reminiscent of graph-database pattern matching. Graph query languages (Cypher, SPARQL, Gremlin, GQL) are all, at their core, syntactic sugar over first-order logic with existential quantification and conjunction.

Each existential variable corresponds to a node, each attribute corresponds to an edge or property, and the conjunction of unary predicates forms a graph pattern. Predica achieves this expressiveness without requiring graph-database storage structures or pointer semantics.

Graph databases internally bind nodes, follow edges, constrain properties and return a projection. Predica expresses the same logical structure using unary predicates and attribute navigation.

5 Nesting the Relational Model

This chapter explains the shift from the unnested n-ary relations of the conventional Relational Model to Predica's nested domains with unary predicate extensions.

The conventional RM is unnested

When Codd introduced the RM he described First Normal Form (1NF), where there are no repeating groups, attribute types are "atomic" or simple, there are no nested relations and no hierarchical structure inside tuples.

The conventional RM is unnested in exactly this sense: hierarchical structure is not permitted inside tuples. This absence of nesting is core to the use of the RM as envisaged by Codd.

A conventional relational database has relation variables (relvars) which record n-ary relations which are the extensions of n-ary predicates about the world.

For example, for the relvar for suppliers:

Predica : nesting the RM

There is an important change in thinking required to understand Predica for those familiar with the RM.

Predica does not reject hierarchical structure; it embraces it. This decomposes the n-ary predicates/relations into unary predicates/relations. Predicates are simpler, but there are more of them, allowing for recording the same information as the unnested RM.

The restriction to unary predicates and relations sounds severely limiting. One might surely think this is fatal for representing the kind of information that can be recorded in the RM. Although each Predica predicate is unary, their composition preserves the information represented by n-ary relations while allowing that information to be organised through nested domain structure.

The following ideas explain how Predica recovers the expressive power of the RM while adopting a radically different structure:

• A domain may be recursively split into smaller domains ("subdomains"). This decomposition is mirrored by nested types. Predica does not require every attribute type to be simple, but it does keep multiplicity in attribute extensions rather than in collection-valued attribute values.
• The decomposition from domains to subdomains and smaller subdomains and so on is mirrored in the use of nested types.
• The unnested RM makes a distinction between relvars (which hold relations), and tuple attributes (which hold atomic values). There is no such distinction in Predica. There are just attributes, and an attribute records its extension.
• The information recorded about a domain is represented by the extensions of its attributes.
• Every attribute of a domain is a unary predicate on that domain.
• The restriction to unary predicates forces decomposition.

Predica decomposition of Supplier

The decomposition is easiest to see in stages. Start with a single supplier domain and one of its attributes. For that supplier, the attribute S# is a unary predicate whose extension contains one value:

Now add the other attributes for the same supplier. This gives four unary predicate extensions:

At first glance, restricting all predicates to be unary seems to lose the correlations that ordinary n-ary relations record. If all we kept were separate global projections for S#, SNAME, STATUS, and CITY, the original supplier relation would not be recoverable. The nesting is doing important work here: these are not four independent global projections. They are correlated because they belong to the same supplier element.

Now regard each supplier itself as an entity in the extension of the outer unary predicate Supplier:

Expanding each supplier gives a picture that deliberately resembles the ordinary supplier relation. But structurally it has been turned into nesting: the outer unary predicate Supplier has five elements, and inside each element the former columns appear as extensions of unary predicates:

In this decomposition, each attribute of Supplier records its extension. This is exactly the same information as the corresponding column in the unnested 4-ary relation. Nothing is lost: the supplier number, name, status, and city are all represented as facts of unary predicates. What changes is the structural organisation of those facts. Instead of being bundled together into a single n-ary tuple, they are distributed across simpler predicates that can be composed through the domain structure.

This illustrates the central idea of Predica's approach to nesting: the expressive power of the relational model does not come from n-ary tuples, but from the logical relationships among predicates. By decomposing domains into subdomains and representing attributes as unary predicates, Predica preserves the same information while allowing domains and their types to be recursively composed—structure that the unnested RM deliberately excludes. The absence of nesting in the conventional RM is not a logical necessity but a design choice; Predica shows how to recover the same semantics in a compositional form.

6 Cardinality

Attribute cardinality

Suppose that for the supplier-parts database we make small, natural cardinality adjustments to the supplier model: a supplier may have one or two names, the status is optional, and a supplier may be located in one or more cities. In Predica, these changes are expressed locally:

entity Supplier
{
    Integer id;
    String name[1..2];
    Integer status?;
    String city+;
    key {id};
}

The nested picture has the same shape; only the permitted sizes of the unary extensions have changed:

These cardinality changes affect the constraints on the attribute extensions, but not how queries are written, nor their denotations into logic.

To express the same simple cardinality changes that Predica handles locally, The RM is forced into a 6NF explosion. Tutorial D must:

• split the S relvar into four relvars (S, S_NAME, S_STATUS, S_CITY)
• introduce three new keys for (S_NAME, S_STATUS, S_CITY)
• introduce three new foreign-key constraints (one for each of the new relvars)
• change every query that touches names, cities or status
• change every constraint that refers to SNAME, CITY, or STATUS
• change every view or derived relvar that depends on S or any of the attributes that were factored out

This illustrates the structural fragility that Predica avoids. In Predica, cardinality is a declarative property of each attribute. In the RM, the same information must be encoded by restructuring the schema, introducing new relvars, new keys, new foreign keys, and rewriting every query and constraint that touches the affected attributes.

VAR S BASE RELATION
{ 
    S#     CHAR,
    SNAME  CHAR,
    STATUS INTEGER,
    CITY   CHAR 
}
KEY { S# };

-- Supplier S# exists
VAR S BASE RELATION
{
    S#  CHAR
}
KEY { S# };

-- Supplier S# has NAME
VAR S_NAME BASE RELATION
{
    S#   CHAR,
    NAME CHAR
}
KEY { S#, NAME };

CONSTRAINT S_NAME_FK
    S_NAME { S# } ⊆ S { S# };

CONSTRAINT S_NAME_CARDINALITY
    IS_EMPTY (
        S
        MINUS
        ( ( S_NAME GROUP ( NAME AS NAMES ) )
            WHERE COUNT(NAMES) BETWEEN 1 AND 2 ) { S# }
    );

-- Supplier S# has status STATUS
VAR S_STATUS BASE RELATION
{
    S#     CHAR,
    STATUS INTEGER
}
KEY { S# };

CONSTRAINT S_STATUS_FK
    S_STATUS { S# } ⊆ S { S# };

-- Supplier S# is located in CITY
VAR S_CITY BASE RELATION
{
    S#   CHAR,
    CITY CHAR
}
KEY { S#, CITY };

CONSTRAINT S_CITY_FK
    S_CITY { S# } ⊆ S { S# };

CONSTRAINT S_CITY_MIN_1
    IS_EMPTY (
        S
        MINUS
        S_CITY { S# }
    );    

Partial information

Predica provides a native, principled, and compositional way to model partial information. The key idea is simple: optional information is represented by empty attribute extensions, not by a special marker value inside a tuple.

An unnested, single-relvar representation becomes structurally unstable under partial information. The pure relational answer is usually to decompose optional or repeating attributes into separate relvars. SQL practice often takes more convenient shortcuts. If an entity has dozens of attributes, any of which may be unknown, practitioners typically reach for some mixture of:

• nullable columns, with SQL's special NULL behaviour
• separate child tables for optional or repeating attributes
• outer joins and CASE expressions in queries
• EAV-style designs for highly sparse data
• JSON/document columns when the relational shape becomes too cumbersome
• application-level validation to recover constraints no longer expressed cleanly in the schema

Some of these approaches are principled in isolation, especially decomposition into separate relvars. But they are not local: changing the optionality or cardinality of an attribute changes the surrounding schema shape and forces queries, views, and constraints to be rewritten. The common SQL shortcuts are more convenient, but they introduce their own semantic complications around NULLs, outer joins, constraint checking, and type information.

Predica’s “attributes as unary predicates” implicitly handles partial information, because each attribute has its own extension, which can be empty independently of other attributes. In Predica:

• each attribute is a unary predicate
• ? means “0 or 1”. Partial information is first-class
• unions of populations are always well-formed
• projection can be defined to skip entities lacking the attribute
• derived attributes can be typed and constrained
• the type system can infer union types automatically

The important point is locality. In Predica, optionality is stated directly on the attribute:

Email email?;

The attribute remains part of the conceptual type, while its denotation remains relational: email is a predicate that may hold for zero or one email values.

This yields a modelling space where every subset of attributes corresponds to a well-typed, well-formed predicate.

Example

Consider using the ? cardinality qualifier on dozens of attributes of a Person entity type:

entity Person
{
    String name?;
    Address address?;
    Phone phone?;
    Email email?;
    Date birthdate?;
    ...
}

entity Company
{
    Person person*;
}

// Database variable of type Company
var c = openDatabase<Company>("/path/to/database");

For any subset of attributes, say {name, email}, you can simply write: c.person.(name, email). Its logical denotation is:

name=N:String, email=E:Email
where
  ∃P:Person
    c.person(P)
  ∧ P.name(N)
  ∧ P.email(E)

This yields a clean, well-typed population of:

• exactly those people who have both attributes
• with both attributes guaranteed to be present
• with no NULLs
• with no schema gymnastics
• with no loss of type information

Adding another projected attribute, as in c.person.(name, address, email), adds P.address(A) to the conjunction, so the result contains exactly those people for whom all three attributes are present.

This is much cleaner than the usual SQL alternatives: no NULL tests, no outer joins, no JSON unpacking, and no separate modelling pattern just because an attribute is optional.

Zaniolo’s interpretation of partial information

Predica is sympathetic to the “no-information” interpretation of NULL associated with Carlo Zaniolo, but implements the idea differently. Zaniolo interprets NULLs inside relations. Predica avoids null markers altogether: optional attributes are predicates whose extensions may be empty for a given entity.

Projection over a set of attributes then restricts to those entities for which all projected attributes are present, producing a clean, total representation with no NULLs and no special cases. Missing information is represented by empty attribute extensions, not by special marker values.

In this way, Predica captures much of the motivation behind the no-information interpretation while remaining within classical two-valued logic and preserving strong typing, compositionality, and clean set-theoretic semantics.

The none expression

The expression none denotes an empty result, not a value. It is valid only where the surrounding expression form explicitly permits absence, especially for optional attributes and conditional branches whose result cardinality permits absence.

entity Person
{
    Email email?;
    → Boolean hasEmail = email ≠ none;
    → Email primaryEmail? = if hasEmail then email else none;
}

none is not a marker value stored inside the attribute, is not a member of any value domain, and must not be passed to ordinary functions as an argument. For an optional path or attribute expression E, the expression E = none tests that the extension of E is empty, while E ≠ none tests that it is non-empty. Equivalently, E = none means E.Σempty, and E ≠ none means E.Σexists. In an update to an optional location, assigning none clears the corresponding attribute extension.

Difference from SQL NULL

Although none is used where an application might otherwise use SQL NULL, it has a different semantic role. SQL NULL is a marker that can appear in a column position and then affects ordinary expressions through special three-valued logic. Predica none is not a value at all: it denotes the absence of a result in a context that permits absence.

This avoids the usual NULL pathologies. Equality remains ordinary two-valued equality over actual values; none is never an extra inhabitant of every type; arithmetic and ordinary functions do not need null-propagation rules; and stored predicates do not contain a hidden marker. Presence tests are explicit extension tests, written with none only as source shorthand for Σempty or Σexists.

7 Identity

Example where the RM needs artificial surrogate keys

Predica’s structural identity eliminates the need for surrogate keys in situations where the RM is forced to introduce them.

Consider a box of objects that are uniquely identified by their shape and colors. There are no other identifying attributes. The following Predica schema represents the required information and models the constraints:

variant Shape
{
    { Real radius } sphere;
    { Real side } cube;
    { Real radius, Real height } cone;
}
enum Color
{
    red, green, blue 
}
entity Object
{
    Shape shape;
    Color color+;
}
entity Box
{
    Object object*;
}

This can be mapped to Tutorial D as follows:

variant Shape
{
    { Real radius } sphere;
    { Real side } cube;
    { Real radius, Real height } cone;
}
        

TYPE Sphere POSSREP { radius RATIONAL };
TYPE Cube   POSSREP { side   RATIONAL };
TYPE Cone   POSSREP { radius RATIONAL, height RATIONAL };

TYPE Shape UNION { Sphere, Cube, Cone };
        

enum Color
{
    red, green, blue
}
        

TYPE Color POSSREP { tag CHAR }
CONSTRAINT ColorConstraint
    tag IN { 'red', 'green', 'blue' };
        

entity Object
{
    Shape shape;
    Color color+;
}
        

TYPE ObjectId POSSREP { id INTEGER };

VAR Object :
    RELATION {
        ObjectId : ObjectId,
        Shape    : Shape
    }
KEY { ObjectId };

VAR ObjectColors :
    RELATION {
        ObjectId : ObjectId,
        Color   : Color
    }
KEY { ObjectId, Color };

-- Inclusion dependencies
CONSTRAINT ColorRefersToObject
    ObjectColors.ObjectId ⊆ Object.ObjectId;

CONSTRAINT EveryObjectHasColor
    Object.ObjectId ⊆ ObjectColors.ObjectId;
        

entity Box
{
    Object object*;
}
        

-- No two objects may have the same
-- shape and the same set of colors
CONSTRAINT NoDuplicateObjects
    IS_EMPTY (
        (Object JOIN Object AS O2)
        WHERE
            Object.ObjectId <> O2.ObjectId
        AND Object.Shape = O2.Shape
        AND
            (ObjectColors WHERE ObjectId = Object.ObjectId)
            =
            (ObjectColors WHERE ObjectId = O2.ObjectId)
    );
        

1NF forbids representing the multivalued color+ attribute as a value, so the RM must split it into a separate relvar. That split destroys the natural identity of an object, forcing the introduction of a surrogate key to maintain identity across relvars.

8 Boolean-valued Attributes

In predicate logic, a 0‑ary predicate is a proposition. Predica deliberately avoids 0‑ary predicates for attributes: every attribute corresponds to a unary predicate, even when the attribute’s type is Boolean. This keeps the semantics uniform and avoids special‑case rules for Boolean attributes.

entity Supplier
{
    Integer id;
    Boolean certified;
}

The query s.supplier.certified is equivalent to:

certified=C:Boolean
where
  ∃S:Supplier
    s.supplier(S)
  ∧ S.certified(C)

When certified is used in a filter in the query s.supplier.[certified], the Boolean-valued variable C appears as a conjunct:

supplier=S:Supplier
where
  ∃C:Boolean
    s.supplier(S)
  ∧ S.certified(C)
  ∧ C

Boolean attribute with relaxed cardinality constraint

In the following example there is no cardinality constraint on respondedThatlikesIcecream. Therefore its extension can be {}, {false}, {true}, or {false,true}. This is an example where a relaxed cardinality constraint allows for recording partial information or conflicting information.

entity Person
{
    String name;
    Boolean respondedThatlikesIcecream*;
}

9 Types

Predica largely accepts Date and Darwen’s value, type and variable semantics, logical interpretation, explicit identity and rejection of OO machinery. It departs from them by applying those principles to entity types and to the database as a whole. Where D&D retain relvars as variables outside the type system, Predica treats the database as a variable of a nominal type and obtains relvar-like pseudovariables through its attributes.

A type classifies mathematical values. It defines a carrier set of values and the operations that can be performed on those values.

A type has a set of attributes (i.e. names) which are available to be used in queries, and sometimes can be the target for update operations.

Structural types

A structural type is described by a type expression such as:

{ Integer a; Real b*; String c?; }

A value of a structural type is a tuple that records an extension for each attribute. For example:

(
    a = {-4},  
    b = {2.5, 3.7, 10.0},  
    c = {"hello"}
)

The extension of an attribute is a set of values of the attribute's declared type, regardless of its cardinality constraint.

Value types

An example of a value type is:

value Circle
{
    Point centre;
    Real radius where radius ≥ 0;
}

A value type is a nominal type. Its carrier is isomorphic to the carrier of the corresponding structural type using its non-derived attributes, after imposing the constraints.

Entity types

An example of an entity type is:

entity Supplier
{
    String id;
    String name;
    Integer status;
    key {id};
}

As for value types, entity types have a carrier which is a set of abstract mathematical values, and that set is defined in exactly the same way as for value types. In the formal language semantics entity types are treated like value types. At the level of the semantic model, however, a value in an entity type's carrier records the extensions of attribute predicates about an entity.

Entity types may declare keys, but these are irrelevant to how the carrier set and equality of the entity type are defined. Key constraints conveniently impose constraints on attributes that use the entity type. For example, the key constraint defined on Supplier is imposed on attribute supplier of ShipmentsSystem:

entity ShipmentsSystem
{
    Supplier supplier*;
}

At the level of the semantic model, the main purpose of distinguishing entity types from value types is to express a metaphysical distinction. Attributes express predicates about the things classified by those types, and all changing database state resides in their extensions.

In most cases, the intended modelling role makes it clear whether a type should be an entity type or a value type. This can readily be seen by considering the examples in the table.

The metaphysical distinction is only informal. It is useful in practise to think of entities as things that exist in time and space and can be referred to, albeit taking this very liberally. An entity need not be a physical object; it may also be an organisation, event, action, or relationship. A birth, a marriage, a shipment, or an ownership are all entities in this sense. Predica therefore has no separate category of relationship types.

The Entity–Relationship Model (ERM) distinguishes entity boxes from relationship diamonds. Predica has no corresponding category of relationship types.

Computer representations are not the values they denote or the entities they identify, and the same value or entity may have many representations. Predica permits types to classify both mathematical values and modelled entities while keeping them distinct. This allows a schema to express the kinds of things in its model directly.

Semantic distinction: entity occurrences can be shared

Values have no identity beyond their structure, so two locations may independently hold equal values. Entities can instead have shared occurrences in a model: several paths may reach the same occurrence, and an update through any one of those paths updates the location shared by all of them. This sharing is established by the schema constraints; an entity type by itself does not make arbitrary occurrences shared. Location denotation is interpreted under those constraints and retains the entity witnesses needed to identify shared attribute locations. Sharing is therefore observable language behaviour, not merely a choice of physical representation. An implementation may realise shared locations using references and key-indexed collections, but it must preserve the behaviour defined by the constrained location semantics.

For example, consider a supplier-and-parts schema in which shipments are recorded under both their supplier and their part:

entity Supplier
{
    Integer id;
    Shipment shipment* where shipment.supplier = this;
    key {id};
}

entity Part
{
    Integer id;
    Shipment shipment* where shipment.part = this;
    key {id};
}

entity Shipment
{
    Supplier supplier;
    Part part;
    Integer qty;
    key {supplier, part};
}

entity ShipmentsSystem
{
    Supplier supplier*;
    Part part*;
    → Shipment shipment* = either supplier.shipment, part.shipment;
}

The where constraints require a shipment under a supplier to name that supplier and a shipment under a part to name that part. Together with the key on Shipment and the definition of ShipmentsSystem.shipment, these constraints determine when the two paths reach the same shipment occurrence. Thus a shipment h for supplier s and part p is visible through both s.shipment and p.shipment as one shared occurrence, not as independent copies. The following targets therefore denote the same Shipment.qty location:

s.shipment.[part = p].qty
p.shipment.[supplier = s].qty

After an assignment through either target, a query through the other path observes the assigned quantity. The derived ShipmentsSystem.shipment attribute observes that same updated shipment as well. A conforming implementation must exhibit this behaviour whether it represents the shipment once and shares a reference, maintains indexes over it, or uses another physical representation.

TODO: Complete the location semantics by defining location denotation relative to the schema constraints and stating when those constraints entail that entity witnesses reached through different paths denote the same occurrence. In particular, the rules must derive from the schema above that the two targets produce the same concrete address.

TODO: Define how a write to an attribute of a shared entity occurrence updates every base extension that contains that occurrence while preserving the constraints on the enclosing values. This definition must cover an update to a key attribute as well as an update to a non-key attribute such as qty.

TODO: Reconcile the general location-semantics rule that ∪= computes set union with the keyed replacement semantics of ∪= on entity-typed extensions, including the unresolved case where different candidate keys match different existing members.

Another possible distinction when value types have keys

If value types can declare keys, a further formal distinction arises between value and entity types.

Note: The formal semantics distinction is deontic:

• Value types must satisfy the determinacy condition.
• Entity types are not required to satisfy it.

The following value type satisfies the determinacy condition, but only because its constraints establish the internal isomorphism between its Cartesian and polar coordinates:

value Point
{
    Real x;
    Real y;
    Real r;
    Real θ;

    key {x,y};
    key {r,θ};

    constraints
    {
        r = sqrt(x^2 + y^2);
        θ = atan2(y,x);
        x = r * cos θ;
        y = r * sin θ;
    }
}

Without these constraints, Point would violate the determinacy requirement for a value type.

Attributes

Attributes are part of the type system, but they are also logical predicates. An attribute does not store a collection inside a value. It denotes a unary predicate from an instance of the containing type to an extension of values of the attribute type.

The cardinality marker constrains that extension:

entity Supplier
{
    Integer id;
    String name;
    City city*;

    key {id};
}

Here city* does not mean that the attribute type is “set of cities”. The attribute type is City. The * says that the extension of the city predicate may contain zero or more city values for a supplier. The same pattern covers single-valued, optional, non-empty, and bounded attributes.

Type expressions

A type expression is syntax that denotes a type. It may refer to a nominal type by name, write a structural type directly, or form a type from existing types:

String
Set<String>
subtype Real where this > 0
union { EmailContact, PhoneContact }
intersection { Shape, Visible }
{ String name; Point point; }

For example, union { A, B } denotes the union of the carrier sets of A and B, while intersection { A, B } denotes values that inhabit both. Union and intersection of two types are only permitted when equality is defined across them.

Type expressions are recursive, so they can be nested inside each other:

Set<(subtype (union { EmailContact, PhoneContact }) where verified)>

Type aliases

A type declaration gives a name to a type expression. The name can then be used in place of that type expression to mean the same thing; it does not declare a new type:

type Names = Set<String>;
type PositiveReal = subtype Real where this > 0;

Subtyping

Subtyping is subset inclusion:

A is a subtype of B iff A ⊆ B

The subtype relation gives rise to a type graph.

Abstract types and nominal subtyping

An abstract type introduces a carrier set without providing constructors for all of its values. Concrete nominal types can select subsets of that carrier. Abstract types are useful when the model needs a common domain, but no single concrete representation covers every possible value.

abstract value Shape
{
    Real area;  // Abstract types can declare attributes.
}

value Circle isa Shape
{
    Point centre;
    Real radius;
    → area = pi * radius * radius;  // Can implement inherited attributes.
}

Circle isa Shape declares Circle as a nominal subtype of Shape. The area attribute declared by the abstract type is given a derived definition by Circle.

Refinement types

A refinement type denotes the subset of an existing type whose values satisfy a predicate.

type Adult = subtype Person where age ≥ 18;

Adult is a type alias for the subset of Person values whose age satisfies the refinement predicate. It does not declare a new nominal type.

Equality and comparability

Equality is not automatically available between every pair of types. An equality expression is well-typed only when equality is defined for the relevant static types. Values of the same concrete value type usually have intrinsic equality. Structural, enum, and quotient types define equality by their own rules. Subtypes use equality from their base type.

value BadComparison
{
    Point p;
    Supplier s;

    constraints
    {
        // Static type error.
        // Equality is undefined between Point and Supplier.
        p = s; 
    }
}

Two different types can also become comparable through a concrete common supertype with defined equality, through an explicit equality function, or through a disjointness declaration that makes cross-type equality always false. This is why type expressions and equality evidence are separate concerns.

Static typing and cardinality

Predica is statically typed by default. A variable, attribute, parameter, or expression has an element type known to the checker. Locations and path expressions also have cardinality information. These are separate checks:

• The element type says what kind of value may appear.
• The cardinality says how many such values may appear.

For example, Integer id* has element type Integer and cardinality zero or more. It is not an attribute of type Set<Integer>. Flow-sensitive checks may refine cardinality or type inside a guarded scope, such as after testing that an optional path is not none, or after a positive isa type test.

10 Database Values and Consistency

A Predica schema defines the type of a database. A database state is a value of that type, and a database is a variable whose successive values are database states. For example:

entity ShipmentsSystem
{
    Supplier supplier*;
    Part part*;
    Shipment shipment*;
}

var db = openDatabase<ShipmentsSystem>("/path/to/database");

Here ShipmentsSystem is a nominal entity type, db is a database variable of that type, and the current value of db is a complete database state. Expressions such as db.supplier designate pseudovariables within that state.

Consistency as type membership

A constraint is part of a nominal type and restricts the values belonging to that type. If S is the unconstrained structural carrier of a database type and K is the conjunction of its applicable constraints, then the carrier of the constrained database type is:

carrier(S with K) =
{
    d ∈ carrier(S)
    |
    K(d)
}

A database state is consistent if and only if it belongs to this constrained carrier. Consistency is therefore type membership at the level of the complete database value. The applicable constraints include attribute types, attribute cardinalities, keys, derived definitions, where clauses, subtype structure, and explicit constraint blocks.

This account does not require consistency to be checked one relvar at a time. A constraint may relate several predicate extensions in the same database value. The database type defines which combinations of extensions constitute valid states.

Consistency and correctness

Consistency is not the same as correctness. A database can satisfy every declared constraint while containing a false statement about the modelled world. For example, a database might consistently record that a supplier is located in Paris even though the supplier is actually located in London. The constraints determine which database values are admissible; they do not establish that the base facts supplied to the database are true.

In Predica's descriptive interpretation, constraints classify admissible models. In its normative interpretation, they classify compliant worlds. In either interpretation, consistency means satisfaction of the specification. Whether the specification itself accurately expresses the intended domain is a separate question.

Consistency and satisfiability

Checking a database value is also different from checking the specification itself. For a particular structural database value d, consistency asks whether K(d) holds. Satisfiability asks whether any such value exists:

∃d ∈ carrier(S). K(d)

If this formula is false, the constrained carrier is empty. The type definition is meaningful, but no database state can inhabit it. A consistency check can reject one proposed state; a satisfiability check detects that every proposed state must be rejected.

Transactions preserve consistency

An update transaction begins with a consistent database state and constructs a proposed successor state. Individual update statements may pass through intermediate transaction states that violate constraints. The transaction boundary is the point at which the complete proposed state is required to satisfy the applicable constraints.

committed update : ShipmentsSystem -> ShipmentsSystem

The notation above states the semantic contract rather than the implementation strategy. A legal successful commit replaces one value of the database type with another. A program that attempts to commit a proposed final state outside the constrained carrier is illegal; the language does not prescribe the runtime behaviour of that attempt. See Constraint-Violating Updates.

This leaves implementations free to use mutation, logs, snapshots, copy-on-write pages, or other physical techniques. Those techniques do not change the logical account: the externally committed states are values of the declared database type.

Local and global constraints

Good schema design makes many consistency conditions follow compositionally from type definitions, keys, cardinalities, and correctly placed attributes. A constraint that initially appears global may indicate that a domain is missing or that a fact has been attached to the wrong subject. Normalisation uses dependencies as diagnostics for finding such designs.

Some business rules genuinely relate several independently meaningful predicate extensions. Such a rule remains an explicit constraint on the database type. It still contributes to the definition of the constrained carrier, but it is not thereby local to an individual attribute or entity type. The distinction between local structure and explicit global constraints remains important even though both participate in determining consistency.

11 Closed World Assumption

As in the Relational Model, Predica adopts the closed world assumption (CWA). In Predica this follows directly from its treatment of predicates and from the fact that every attribute stores the extension of a unary predicate. Under the CWA, the extension of a predicate is taken to be complete: every fact that holds is recorded, and every fact not recorded is taken to not hold.

For a value type such as:

value Circle
{
    Point centre;
    Real radius;
}

the attribute centre is the unary predicate whose extension contains all and only the centres of the circle. Likewise, radius records all and only the radii of the circle. If a value does not appear in the extension of an attribute, Predica interprets this as meaning that the value is not a centre (or radius) of the circle.

This behaviour is fundamental to Predica’s logical operators. Negation, difference, and constraint subtraction all rely on the assumption that the recorded extensions are complete. Without the CWA, these operators would not have a well-defined meaning.

The closed world assumption does not restrict the kinds of predicates that may be defined. A predicate’s extension may record facts about the actual world, or it may record what is known, believed, permitted, required, possible, or otherwise modal in character. The closed world assumption applies only to the chosen extension: whatever belongs to that extension is taken to be completely recorded for the purpose of logical inference, regardless of the interpretation of the predicate itself.

12 Relvar versus attribute predicates

In the Relational Model (RM), each relvar has an associated predicate. For the supplier-and-parts database, there is a relvar recording suppliers:

VAR S BASE RELATION
{
    S#     CHAR,
    SNAME  CHAR,
    STATUS INTEGER,
    CITY   CHAR
}
KEY { S# };

and its predicate is:

In Predica this relvar is represented by entity Supplier together with a reference from entity ShipmentsSystem:

entity Supplier
{
    String id;
    String name;
    Integer status;
    String city;
    key {id};
}

entity ShipmentsSystem
{
    Supplier supplier*;
    ...
}

The Supplier attributes are predicates, simpler and more atomic than the relvar predicate of the RM:

and in the ShipmentsSystem there is a predicate for existence of a supplier:

13 Metadata annotations

Metadata is a sequence of source annotations attached to a schema declaration or member. Each metadata item is written as @name or @name(arguments...). The arguments are ordinary Predica expressions. The leading @ attaches the item to the declaration that follows; it is not part of the metadata name.

Metadata may be attached where the grammar admits MetaData, including nominal type declarations, type aliases, constants, functions, folds, procedures, generic parameters, attributes, derived attributes, variant attributes, subtype embeddings, dropped attributes, and external function declarations.

Unless a metadata form is given a meaning by the spec, metadata is preserved annotation data. It does not add declarations, constraints, predicates, or denotations by itself.

The Predica schema can be annotated with domain and predicate definitions in natural language. For example:

@domain("A supplier in the shipments system")
entity Supplier
{
    @predicate("id(I) ⇔ The supplier has id I")
    Integer id;

    @predicate("name(N) ⇔ The supplier has name N")
    String name;

    @predicate("status(S) ⇔ The supplier has status S")
    Integer status;

    @predicate("city(C) ⇔ The supplier is located in city C")
    String city;

    key {id};
}

Notice that the domain definition uses "a supplier" whereas the predicates use "the supplier".

The predicates use the definite article because the domain is the subject of the predicates.

14 Pushing relationships down into the entities

Schema which aligns closely with the RM

Predica can also express the supplier-and-parts database in a form that closely mirrors the classical RM structure:

entity Supplier
{
    Integer id;
    String name;
    Integer status;
    String city;
    key {id};
    → shipment* = inverse shipment.supplier;
}

entity Part
{
    Integer id;
    String name;
    Color color;
    Real weight;
    String city;
    key {id};
    → shipment* = inverse shipment.part;
}

entity Shipment
{
    Supplier supplier;
    Part part;
    Integer qty;
    key {supplier,part};
}

entity ShipmentsSystem
{
    Supplier supplier*;
    Part part*;
    Shipment shipment*;
    constraints 
    {
        shipment.supplier.Σ ⊆ supplier.Σ;
        shipment.part.Σ ⊆ part.Σ;
    }
}

This mirrors the classical RM structure. The base attribute ShipmentsSystem.shipment resembles a global shipments relvar with two foreign keys supplier and part. The foreign keys are expressed as inclusion dependencies:

constraints 
{
    shipment.supplier.Σ ⊆ supplier.Σ;
    shipment.part.Σ ⊆ part.Σ;
}

There are two derived attributes Supplier.shipment and Part.shipment declared using inverse:

entity Supplier
{
    ...
    → shipment* = inverse shipment.supplier;
}
entity Part
{
    ...
    → shipment* = inverse shipment.part;
}

These enable path-based navigation from suppliers to shipments and from parts to shipments. For example, the following expression returns the parts shipped by London suppliers:

system.supplier.[city = "London"].shipment.part;

This is a faithful RM-style design, and it works perfectly in Predica. But it carries the same structural implications as the RM:

• ShipmentsSystem.shipment behaves like a global relationship base relvar.
• Navigation from suppliers/parts to shipments depends on inverse.
• A physical implementation would likely materialise a join table.

Predica supports this, but it does not require it.

Pushing relationships down into the entities

The schema used in the introduction pushes the relationship down into the entities that participate in it. This gives a logically equivalent schema that maps directly to a more efficient physical implementation, avoiding the need for inverse entirely:

entity Supplier
{
    Integer id;
    String name;
    Integer status;
    String city;
    Shipment shipment* where shipment.supplier = this;
    key {id};
}

entity Part
{
    Integer id;
    String name;
    Color color;
    Real weight;
    String city;
    Shipment shipment* where shipment.part = this;
    key {id};
}

entity Shipment
{
    Supplier supplier;
    Part part;
    Integer qty;
    key {supplier,part};
}

entity ShipmentsSystem
{
    Supplier supplier*;
    Part part*;
    → Shipment shipment* = either supplier.shipment, part.shipment;
}

This version is:

• logically equivalent to the RM-style schema
• physically more efficient
• free of inverse declarations
• free of global relationship relvars

The key idea is simple: A relationship belongs with the entities that participate in it. In Predica, this is not just a stylistic preference, it is a semantic advantage.

Why this works so well

A shipment is naturally “owned” by its supplier and its part. Predica lets you express this directly:

entity Supplier
{
    ...
    Shipment shipment* where shipment.supplier = this;
}

entity Part
{
    ...
    Shipment shipment* where shipment.part = this;
}

These are declarative constraints, not physical pointers. For the supplier it means: The shipments belonging to this supplier are exactly those whose supplier attribute equals this supplier. This expresses the same information as a foreign key, but in a way that:

• supports downward navigation
• avoids global join tables
• avoids inverse declarations
• avoids surrogate identifiers

Shared ownership emerges naturally

Because both Supplier and Part define their shipments, the system exhibits logical shared ownership:

• each supplier records the shipments for which it is the supplier
• each part records the shipments that ship that part

This is shared ownership without:

• object identity
• reference semantics
• object identifiers
• aliasing problems

It is a purely logical notion of sharing, not an OO one.

The global relationship becomes derived, not stored

→ Shipment shipment* = either supplier.shipment, part.shipment;

This is a derived attribute, not a stored one. It declares two equivalent definitions, and the compiler may use whichever one is cheaper in a given query. This is the Predica analogue of:

• a view
• a derived relvar
• a logical relationship

but without the RM’s suggestion for a physical join table.

Emphasising local relationships in queries

Consider the following query in Tutorial D which finds the parts shipped by London suppliers:

(SP JOIN S WHERE CITY='London'){PNO} JOIN P

The most direct counterpart in Predica uses the global shipment predicate:

s.shipment.[supplier.city = "London"].part

However, we can take advantage of the local navigation from supplier to shipment and instead write:

s.supplier.[city = "London"].shipment.part

The second is preferred because it follows the structure of the schema, avoids filtering a global relationship, and is suggestive of an efficient implementation using local navigation.

15 The Information Principle

Chris Date’s “Information Principle”, originating in the work of E.F. Codd, states that all information in a relational database must be represented in exactly one way: as explicit data values within tuples in relations. The intent is to ensure a single, uniform representational mechanism for information, free of ad-hoc devices such as pointers, flags, or hidden structures.

However, the principle becomes less constraining once complex data values are permitted within tuples. Date and Darwen explicitly allow tuple-valued attributes, relation-valued attributes, and user-defined types with possreps. Under such a permissive notion of “value”, it becomes formally possible to embed an entire object-oriented database as the value of a single attribute in a single tuple of a single relvar, while still claiming to adhere to the Information Principle. This is clearly not what they intended, and they would certainly reject such a design as contrary to the spirit of the relational model.

Indeed, their aim was to rule out representational mechanisms such as:

• pointers
• arrays
• nested documents
• object graphs
• NULLs
• hidden metadata
• physical ordering

For good reasons, Date and Darwen argue that the relational model should play a central role in any information system. But in practice, the strength of the Information Principle depends on how “simple” the permitted data values are. Once values may be arbitrarily complex, the principle relies on the informal and historically vague notions of First Normal Form and “atomicity” that Codd originally invoked. There seems to be no way around this: the Information Principle only has real force if the allowed values are sufficiently simple.

Predica's information principle

It is not immediately obvious whether Predica should be regarded as adhering to the Information Principle. Predica does not expose relations or tuples in its surface syntax, and so one might think it violates the principle by abandoning the tuple-based representation of information.

Predica retains the intent of the Information Principle but states it in terms of unary predicates:

The information principle: Every materialised value in a Predica database is used to instantiate a unary predicate, down to the level of simple values such as integers, strings, and values of enumerated types, yielding a true proposition about the modelled world.

Each attribute introduces a unary predicate, and the extension of the attribute is the set of values for which that predicate holds. Information is therefore represented as facts of unary predicates, without alternative representational mechanisms. In this sense, Predica preserves the original intent of the Information Principle at least as faithfully as the classical relational model, and arguably more so.

Several corollaries follow.

• Predicates as the foundation. Attributes are unary predicates. Their extensions are true predicate instances.
• Separation of schema from values. Relation values do not carry headings or types. The schema defines attribute names, domains, and constraints; relation values are pure sets of tuples. This keeps the algebra simple and avoids artificial distinctions between relations that differ only in annotations.
• No primitive n-ary relvars. N-ary relational structure is recovered by composing unary predicates.
• Full decomposition. Multi-attribute structure is decomposed into predicate instances and recovered by composition.

No hidden identifiers

Another corollary of the information principle is that Predica does not use memory addresses, object identifiers, or other hidden handles as logical identity. Hidden identifiers are not values used to instantiate predicates about the modelled world; they are representational machinery.

Several consequences follow.

• Entities have keys. Entity identity is stated by declared keys and constraints, not by physical or hidden object identity.
• Entity and value types. Entity types represent identified things that exist in time and space. Value types represent pure values with no independent identity. This distinction localises identifiers, avoids foreign-key proliferation, and supports clean modelling of real-world domains.
• Object orientation is rejected. Predica does not model values as objects with hidden identity that receive messages through object handles. Dynamic dispatch through object identifiers is not part of the logical model.

Predica entity types are not OO objects

Predica’s entity types resemble OO classes in surface syntax, but they do not behave like OO object types. Their instances have explicit logical identity defined by keys, never hidden object identity.

This distinction matters. In OO, there are two very different notions of “class”:

• Reference classes: objects with identity, pointer semantics, and mutability (Java, C#, Python, Smalltalk).
• Value classes: immutable records with no hidden identity (Rust structs, Swift structs, Haskell records, ML records, C++ POD types).

Predica entity types are closer to the second category. They have explicit keys and:

• no hidden identity
• no pointer semantics
• no aliasing
• no mutability
• no object-identity behaviour

The correct analogy is therefore:

Predica entity types are like immutable record types
with explicit logical keys, not like OO objects.

Predica resembles OO only in notation, not in semantics. It embraces the clarity of class-like syntax while avoiding hidden identity, pointer semantics, and mutable object state.

16 The Atomicity Paradox

Predica appears, at first glance, to violate every classical intuition about First Normal Form and atomicity. It promotes rich, structured types such as Point, Circle, and Polygon; it has entity types like Supplier with internal attributes; and it permits cardinality constraints at any level. Superficially, this looks like a wholesale abandonment of Codd's requirement that attribute types be "atomic".

The irony is that Predica is more faithful to 1NF than many conventional relational systems, because it requires:

1. information inside structured values to be recursively decomposed through attributes down to simple types such as Boolean, Integer, Real, and String
2. multiplicity to be represented by attribute extensions, not by collection-valued attribute values
3. every value that appears in the database to be a value of some attribute
4. every attribute to be a unary predicate
5. attributes to record their extensions

Together these imply that primitive values such as 5 or "Alice" that appear in the database participate in the logical model through predicates, even when they occur inside structured values.

Circles, points, suppliers, and shipments are all values that represent facts, but they are not simple or primitive. Predica does not require them to be. For the values that appear in a database, Predica rejects:

    value of attribute ⇒ value is primitive

and mandates only the converse:

    value is primitive ⇒ value of attribute

In practice many relational systems violate 1NF. For example, it is common to store arrays, lists, tuples, JSON, XML, and spatial geometry types in a single column in PostgreSQL, MySQL, Oracle, and SQL Server.

In Predica, attributes with multivalued extensions do not violate 1NF: multiplicity is represented as multiple facts of a unary predicate, while the declared attribute type remains singular. Predica’s surface syntax resembles nested structures, but its semantics remain fully relational.

The conventional RM appears “atomic” but routinely violates 1NF in practice; Predica appears “non-atomic” but adheres to it in principle.

17 The First Great Blunder

According to Date and Darwen, the first great blunder is the relvar = class equation: treating a relation variable as the counterpart of an object class, and treating each tuple in its current value as an object instance. This mistake, they argue, leads directly to a host of conceptual and practical problems:

• hidden object identity
• pointer-based semantics
• update anomalies
• confusion between value and identity
• non-logical equality
• mixing logical and physical models
• OO-style thinking infecting the relational model

This is why they attack systems that treat tuples as mutable objects:

• OIDs
• object databases
• ORMs
• SQL’s row identifiers
• any model in which a tuple has hidden identity or reference semantics

The essence of the blunder is confusing the logical notion of a relation with the object-oriented notion of a class. In the relational model, tuples are values, not objects; they have no identity beyond their value. In OO, objects have identity independent of their state. Conflating these two worlds leads to the pathologies Date and Darwen warn against.

Does Predica commit the first great blunder?

At its most literal, the equation relvar = class is already a category error: a relvar is a variable, whereas a class is a type. Predica does not make that identification. Indeed, Predica has no independently declared relvars. It has types and attributes, while a database is a variable whose declared type is an entity type.

Predica allows entity (and relationship) types in semantic modelling to be genuine types in the type system. For example:

entity Supplier
{
    Integer id;
    String name;
    Integer status;
    String city;
    key {id};
}

In An Introduction to Database Systems, 8th edition, Chapter 14, C. J. Date says:

... the entity type concept as used in (e.g.) the E/R model is not at all the same thing as the type concept discussed in Chapter 5. To be more specific, such entity types will probably map to relvars in a relational design, so they certainly do not correspond to relational attribute types (domains).

Predica deliberately rejects that boundary. Supplier is simultaneously:

• a semantic-modelling entity type; and
• a genuine type in Predica’s type system.

As a genuine type in the type system, Supplier is expected to occur as an attribute type:

entity ShipmentsSystem
{
    Supplier supplier*;
    Part part*;
    Shipment shipment*;
}

This is not committing the first great blunder, i.e. the category error.

Let db be a database variable of type ShipmentsSystem:

// Database variable of type ShipmentsSystem
var db = openDatabase<ShipmentsSystem>("/path/to/database/on/file/system");

The attribute name supplier, when applied to db, gives the pseudovariable db.supplier. This pseudovariable is a location whose current value is the extension of the supplier predicate and can therefore correspond to a relvar:

// db.supplier is a pseudovariable recording extensions of type Supplier
assert( db.supplier isa Supplier );
print(db.supplier);

But Supplier is the type used in the declaration of that attribute; it is neither the attribute supplier nor the pseudovariable db.supplier. Predica therefore does not make the relvar = class identification.

Predica distinguishes between attributes, value types and entity types. The identifiers appearing in these examples can be partitioned into those three groups as follows:

• attributes: id, name, status, city, supplier, part, shipment. These are unary predicates. They have extensions, and in this respect correspond to relvars, understood as predicate names.
• value types: Integer, String.
• entity types: Supplier, Part, Shipment, ShipmentsSystem. These are kinds of domains. They have domain definitions, not predicate definitions.

Going back to C. J. Date’s quotation above, there remains a substantive difference from Date’s conception, and this highlights a distinction between Predica and the standard and expected application of the Relational Model.

Allowing semantic entity types to be genuine types is a major advantage of Predica. It lets a Predica schema directly perform the semantic modelling that a schema is supposed to perform. Supplier remains the type of supplier entities throughout the model, rather than being translated into a relvar whose tuples stand for suppliers.

18 Design Principles and Features

This chapter summarises some of the design principles behind Predica and the language features that follow from them.

Design Principles

Predica is shaped by several design principles. The principles listed here are central examples: they keep the model logical, compositional, and independent of physical representation choices.

Logical denotation

Logic defines the semantics of Predica constructs. This specifies what they mean, not how they operate or are implemented. The main example is the denotation of path expressions into logic frames.

This gives another corollary.

• Physical independence. Storage layout, indexing, chunking, and physical identifiers do not determine the meaning of a Predica model.

Additional principles

• Schema supplies the context. The schema declares attribute names, types, cardinalities, and constraints. Query denotations are checked and interpreted against that context.
• Cardinality is local to attributes. Optionality and multiplicity are properties of individual predicates. Changing the cardinality of one attribute is a local schema change; it does not by itself turn the surrounding domain into a different n-ary relation.
• Recursive decomposition and atomic domains. Types decompose into simpler types until reaching atomic domains. This provides a principled interpretation of Codd’s atomicity and naturally leads to schemas equivalent to 6NF.
• Subtyping is subset. Subtypes represent subsets of a domain. This gives constrained types, classifications, variant refinements, and comparable types a common set-theoretic interpretation.
• Path-based navigation. Path expressions provide a concise, readable way to traverse relationships without exposing physical implementation details. They replace foreign-key navigation with a logical, compositional mechanism.
• Isomorphisms and updatable views. Bijections between types are first-class constructs. They allow alternative representations of the same information and support principled, updatable views.

Together, these principles explain why Predica's type, query, and constraint constructs share the same predicate-based interpretation.

Features

Predica offers:

• A foundation in predicate logic, giving clear semantics for information representation, integrity constraints, and query behaviour.
• Modelling capabilities that subsume the Relational Model, including the use of Relational Algebra for integrity constraints and queries.
• Greater decomposition than the RM, down to unary predicates.
• Strong modularity: complex domains are recursively decomposed into subdomains.
• Uniform application of predicate logic to both physical and mathematical domains.
• A logical level of discourse designed to achieve physical independence.
• Independence from foreign-key choices. When multiple candidate keys exist, the logical layer remains unaffected; the choice is purely physical.
• Avoidance of surrogate keys in cases where the RM would normally require them.
• Attribute cardinality defined independently for each attribute, making changes trivial. In the RM, such changes often require structural alterations to relvars.
• Natural support for large, wide-scope databases through compositional modelling.
• A principled treatment of atomicity, addressing Codd’s concerns.
• A modelling discipline that naturally avoids denormalised designs. Practitioners tend to produce schemas equivalent to 6NF.
• Excellent support for schema evolution, far beyond what the RM offers.
• A rich type system, including:
  • quotient types defined via equivalence relations
  • value types for mathematical structures
  • powerful constraint mechanisms
  • subtyping interpreted as subset
  • closed and open variant types
  • enumerated types
  • entity types for modelling things that exist in time and space
  • precise control over cardinality
  • isomorphisms between types, enabling updatable views

19 Benefits of a Decomposition into Domains with Unary Predicates

Predica has a minimal mechanism:

• uniformity
• no relation-valued attributes
• no tuple-valued attributes
• no possreps
• no need for relvars
• no need for n-ary relations in the underlying semantics

The RM works directly with n-ary predicates whereas Predica uses unary predicates. This finer-grained approach has a wide range of significant benefits, including:

• Improved modularity. Complex domains are decomposed into smaller ones. Key definitions are local to the types they belong to and can be changed without affecting all references, as discussed for composite keys in entity types as logical sorts.
• Direct cardinality control. Cardinality constraints attach directly to attributes, making them easy to express and modify. In the RM, such changes require structural modifications to relvars, as discussed in the chapter on cardinality.
• Avoidance of artificial surrogate keys. Some domains that require surrogate keys in the RM do not require them in Predica. The chapter on identity gives an example where a simple change to Predica cardinality constraints becomes a substantial Tutorial D redesign.
• Natural support for partial information. Decomposition into unary predicates is a game changer for handling incomplete data. The RM becomes cumbersome when pushed toward 6NF, often leading practitioners to introduce NULLs, special marker values, subtype tables, EAV encodings, or other representational workarounds that compromise typing, inference, and constraint checking. Predica naturally supports partial information because attributes have independent unary predicates. Optional information is modelled using cardinality constraints, as discussed in the chapter on cardinality, and queries that reconstruct n-ary relations account for partial information by the way queries work.
• Clearer semantics for derived information. Because each attribute is a unary predicate, derived attributes and constraints are expressed uniformly as logical definitions. This cleanly separates stored and derived information without procedural machinery, as illustrated by the Person example in event sourcing.
• Smoother schema evolution. Adding, removing, or changing an attribute affects only one predicate. Structural changes that require table redesign in the RM become local and incremental in Predica; see schema evolution.
• Alignment with programming models. The decomposition of value domains mirrors object composition and algebraic data types, making Predica a natural bridge between logical modelling and programming languages.
• Reduced join complexity. Navigation between domains is expressed directly through attributes, avoiding the need for explicit joins for simple traversal. Reconstructing n-ary relations is done only when needed; see navigation.
• Alignment with high-performance implementations. The logical model allows emphasis of bidirectional navigation between domains, resembling navigation along edges in graph databases, as discussed in pushing relationships down into the entities.
• Intuitive query formulation. The attributes of domains give rise to navigation paths that are natural to follow when expressing queries; see navigation.
• High-performance ingestion and flexible constraint layering. Because each attribute is an independent unary predicate, constraints can be relaxed in the base representation to allow very fast ingestion, higher concurrency, and independent updates. Different predicates can even be stored in separate physical databases. More complex constraints are then imposed in derived attributes, which provide a pristine, fully-checked view of the data. This separation avoids the view-update problem and enables both high performance and strong semantics.
• No view-update problem. In the RM, n-ary relations are stored directly, and views that reconstruct information introduce ambiguity about how updates should be propagated back to base tables. Predica stores only unary predicates, and n-ary relations are reconstructed on demand. As a result, updates always apply to the underlying unary predicates, and the classical view-update problem does not arise.
• Support for Operational Transformation. Because each attribute is an independent unary predicate, updates are fine-grained and commute naturally. Constraints can be relaxed in the base representation to allow concurrent, distributed updates, while derived attributes impose stricter semantics in the pristine view. This separation provides exactly the conditions required for Operational Transformation: independent updates, conflict-free merging, and convergence without the view-update problem.
• Zero-latency editing, local replicas, and branching/merging. Because each attribute is an independent unary predicate, updates are fine-grained and commute naturally. This enables Operational Transformation and local replicas that can be edited with zero latency, without pessimistic or optimistic concurrency control. The relaxed base representation allows independent updates and high ingestion rates, while derived attributes impose stricter constraints in the pristine view. The same structure also supports branching and merging of databases in the style of version-control systems such as Git.
• Ability to record conflicting information. Because cardinality constraints are legality conditions rather than storage restrictions, Predica can record multiple conflicting facts about the same attribute. This is invaluable for high-throughput ingestion, distributed updates, Operational Transformation, and branching/merging workflows. Conflicts are preserved as data and resolved in derived, constraint-rich views rather than being rejected at ingestion time; see Boolean-valued attributes for a simple example.

20 Related Work

Full decomposition with unary predicates

Predica’s treatment of all attributes as unary predicates over decomposed domains resonates with several strands of prior work, but the specific combination of ideas does not appear in the literature as a unified modelling foundation.

In classical first-order logic, it is well known that n-ary predicates can be simulated using unary predicates together with additional structure, and that monadic fragments of first-order logic enjoy strong decidability properties. However, these results are typically presented as technical encodings or proof techniques rather than as a basis for data modelling or schema design.

In knowledge representation, especially in frame systems, semantic networks, and description logics, one finds the notion of roles that behave much like unary predicates on individuals. Binary and higher-arity relations are still treated as primitive, and n-ary relations are often handled via reification, but there is no systematic commitment to representing all information as unary predicates over a recursively decomposed domain.

In the relational model and its successors, attributes are sometimes informally described as roles, and domains are allowed to be arbitrarily complex. Nonetheless, n-ary relations remain the primary semantic unit, and there is no move to reconstruct them compositionally from families of unary predicates. Attribute-centric perspectives have been explored, but not to the extent of eliminating n-ary relations as primitives.

Categorical and type-theoretic semantics introduce another closely related perspective: predicates can be viewed as families of sets indexed by a domain, and unary predicates correspond to fibres in a fibration or objects in a comprehension category. This aligns well with Predica’s view of attributes as unary predicates whose extensions vary over domain instances, but these constructions are typically used to model existing logics and type systems, not to drive a reorganisation of data modelling around unary predicates.

Finally, in programming languages and type theory, higher-arity functions and tuples are routinely encoded using unary functions and nested pairs (via currying and Church encodings). These encodings demonstrate that higher-arity structure can be reduced to iterated unary structure, but they are employed as representational devices rather than as a semantic stance on how information should be modelled.

Predica differs from these lines of work by taking the unary perspective as foundational: all attributes are unary predicates; domains are recursively decomposed; and n-ary relations are reconstructed from the cross-product of unary predicate facts. This yields a uniform representation of information that removes the need for tuple-valued attributes, relation-valued attributes, and possreps, while keeping natural language predicates as the primary semantic anchor.

21 Example Schema

This part uses a small university schema as its running example. The schema is deliberately light on constraints. Its purpose is to provide a familiar world for reading path expressions, not to model every rule of a university.

The main objects are students, courses, departments, enrolments, teaching sessions and assessments. An enrolment records that a student is taking a course. A department offers courses. A course may have prerequisites, scheduled sessions and assessments.

enum Day
{
    monday,
    tuesday,
    wednesday,
    thursday,
    friday
}

value TimeSlot
{
    Day day;
    Integer startMinute;
    Integer endMinute;
}

value Exam
{
    Day day;
    Integer durationMinutes;
    Integer weight;
    Integer maxMark;
}

value Assignment
{
    Day dueDay;
    Integer wordLimit;
    Integer weight;
    Integer maxMark;
}

value Project
{
    Day dueDay;
    Boolean groupWork;
    Integer estimatedHours;
    Integer weight;
    Integer maxMark;
}

variant Assessment
{
    Exam exam;
    Assignment assignment;
    Project project;
}

entity Department
{
    String name;

    Course course* where course.department = this;

    key { name };
}

entity Course
{
    String code;
    String title;
    Boolean advanced;
    Department department;

    Course prerequisite*;
    Session session* where session.course = this;
    Assessment assessment*;
    Enrolment enrolment* where enrolment.course = this;

    key { code };
}

entity Session
{
    Course course;
    TimeSlot time;
    String room;
}

entity Student
{
    String name;
    Course completed*;

    Enrolment enrolment* where enrolment.student = this;
    → Course enrolled* = enrolment.course;

    key { name };
}

entity Enrolment
{
    Student student;
    Course course;
    Boolean current;
    Integer mark?;
}

entity University
{
    Department department*;
    Course course*;
    Student student*;
    Enrolment enrolment*;
}

Some relationships are stored directly. For example, an Enrolment stores its student and course, and a Course stores its department. Other relationships are derived for convenient navigation. For example, Student.enrolled is calculated from the student's enrolments, and Department.course is the reverse direction of Course.department.

Assessment is a variant type: an assessment is an exam, an assignment or a project. Assessment attributes include numeric fields such as weight and maxMark so later chapters can use them for calculations and folds. Later examples also use Assessment to show that path expressions work over sum-shaped values as well as ordinary product-shaped values.

The following chapters use this schema to build up path expressions step by step: simple navigation first, then filters, naming, reshaping, summaries and the common places where the wrong mental model leads to mistakes.

22 Navigation

The University database

Let u be a program variable of type University. It can be thought of as the database being queried.

University u;

The aim for the chapters in this part is to explain how to write read-only queries on u. The emphasis will be on using examples to illustrate how it works, without delving into the formal denotational semantics.

Path expressions

A path expression is an expression which can appear in Predica programs and in queries:

u.student.name
u.course.[advanced].code
u.course.(code, title)
u.student.name as studentName
u.course.session.time.(day, startMinute)
u.course.let c = this in c.prerequisite.code
u.course.assessment.exam.durationMinutes.Σsum
u.course.[advanced]⇒session.time.day

Path expressions are analogous to relational algebra expressions used to express queries on a relational database.

In our examples path expressions start at u then typically follow attributes through the schema.

Frames

Here we give an informal description of frames and explain the notation used to write them. They underpin the semantics of Predica.

Consider the following set builder notation for the points on the unit circle:

{ (X,Y) ∈ ℝ² | X² + Y² = 1 }

In an analogous way we can use a set builder notation to denote a relation with two attributes code and title which represents a query on the university database:

{ { (code=X:String), (title=T:String) } 
  where ∃C:Course 
        u.course(C) ∧ C.code(X) ∧ C.title(T) }

This is an expression of the form {R where Ψ}.

In this case we are ranging over the variables in R. That is not always the case, the more general form is written {R for F where Ψ}. The following illustrates use of for in a set builder notation:

{ r(X,Y) for X:A,Y:B where p(X,Y) }

In the formal denotational semantics a path expression denotes a frame (R,F,Ψ), i.e. the three components of a set builder notation of an n-ary relation.

It is convenient to write a frame using the notation R for F where Ψ or sometimes just R where Ψ.

For example, the path expression u.student denotes the frame:

student=S:Student where u.student(S)

Navigation

The simplest paths select one kind of object from the university.

u.student
u.course
u.department
u.enrolment

A path is read from left to right. The expression u.student.name starts with the university, reaches its students, and then reaches each student's name.

u.student.name

The same idea works for longer paths. The following expression starts at the university, reaches students, reaches their enrolments, reaches the courses for those enrolments, and finally reaches the course codes.

u.student.enrolment.course.code

This is relational-join-like traversal: the path crosses from students to enrolments to courses by following declared relationships instead of writing the relational joins explicitly.

Paths can move through derived attributes in the same way as stored attributes. Student.enrolled is calculated from Student.enrolment.course, so these two expressions reach the same courses. Path expressions do not need to distinguish between base attributes and derived attributes.

u.student.enrolment.course
u.student.enrolled

A path may reach many values. The expression u.course.session.room reaches the rooms used by course sessions; it is not a single room unless the data and the schema make it single-valued.

u.course.session.room

Navigation can also follow relationships that were written in the reverse direction for convenience. Department.course is derived from Course.department, but it still reads as ordinary navigation from a department to the courses it offers.

u.department.course.code

The important habit is to keep track of the current kind of value at each step. In u.student.enrolment.course.department.name, the path passes through a university, students, enrolments, courses, departments, and finally department names.

u.student.enrolment.course.department.name

For example, the path u.student.enrolment.course.code corresponds to a chain of relationships in logic:

code=X:String
where
  ∃S:Student ∃E:Enrolment ∃C:Course
    u.student(S)
  ∧ S.enrolment(E)
  ∧ E.course(C)
  ∧ C.code(X)

The result attribute is code, bound to X. The variables S, E and C are the intermediate values reached by the path. Each dotted step contributes another predicate, and the intermediate values are existentially quantified. This is why a dotted path should be read as relational navigation, not as ordinary object property access.

Navigation is uniform across type kinds

This is an important unification in Predica, and may be surprising at first. Base and derived attributes of value types, entity types and quotient types, fields of structural types, and attributes of enum types and variant types are all navigated in the same way. Enum and variant attributes are regarded as always present as unary predicates, which is why they can be used in path expressions without conditionals. Their denotations into logic work identically as well.

For example:

u.course.session.time.startMinute
u.course.session.time.day.monday
u.course.assessment.exam.durationMinutes
u.student.enrolled.code

The first path uses attributes of entity and value types. The second uses an enum attribute. The third uses a variant attribute. The fourth uses the derived attribute Student.enrolled. All of these are ordinary path expressions, and their denotations as frames have the same form.

23 Path Tails

A path tail is any expression that can appear to the right of a dot in a Predica path expression. Path tails include attribute access, filters, tuple constructions, scalar expressions, and nested combinations of these.

We use the term path tail to highlight that such an expression has meaning in the context of a full path expression in which it appears.

For example, if there is no program variable named course, then an expression like course.session is a path tail rather than a complete path expression by itself. It is meaningful as the tail of a larger path expression such as:

u.course.session

Given a variable s of type ShipmentsSystem, consider the path expression:

s.supplier.[city = "London"].(name,status)

This expression contains the following path tails:

    •  supplier
    •  city
    •  name
    •  status
    •  (name,status)
    •  [city = "London"]
    •  supplier.[city = "London"]
    •  supplier.[city = "London"].(name,status)
    •  [city = "London"].(name,status)

Path tails can also include:

• renamed tails (e.g., name as n)
• universal tails (e.g., supplier⇒order)
• logical combinations (e.g., named ⊓ status)
• scalar expressions (e.g., qty * price)
• constants (e.g., 42, "London" )
• nested tuples (e.g., (name,(status,city)) )
• deeper chains (e.g., shipment.part.name )

Square brackets are the filter form. A round tail constructs a tuple or scalar projection even when the projected item is Boolean, so document.(kind = DocumentKind.customsEntry) is not the same path as document.[kind = DocumentKind.customsEntry].

To catch this common mistake, a single predicate-shaped round projection followed directly by Σexists is rejected by the source language. Predicate-shaped projections include comparisons, logical connectives, cardinality tests, type tests, and logical negation. Write:

document.[kind = DocumentKind.customsEntry].Σexists

rather than:

document.(kind = DocumentKind.customsEntry).Σexists

24 Filters

A filter keeps the current values for which a condition is true. In relational-model terms, filtering is the restriction operation inside a path expression.

The following path reaches the advanced courses in the university:

u.course.[advanced]

The filter is applied to the current courses. After the filter, the path still contains courses, just fewer of them.

The path tail advanced is evaluated as C.advanced(A), and the filter condition itself becomes the conjunct A in the frame:

course=C:Course
where
  ∃A:Boolean
    u.course(C)
  ∧ C.advanced(A)
  ∧ A

Navigation can continue from the filtered courses in the usual way.

u.course.[advanced].code
u.course.[advanced].department.name

Filters can use ordinary comparisons. This expression reaches the enrolments whose mark is at least 50:

u.enrolment.[mark ≥ 50]

A filter can appear after navigation. In the next expression, the path first reaches each student's enrolments, then keeps only current enrolments, then reaches the corresponding course codes.

u.student.enrolment.[current].course.code

The position of the filter matters. A filter applies to the values reached at that point in the path. Here [advanced] applies to courses:

u.student.enrolment.course.[advanced].code

Here [current] applies to enrolments:

u.student.enrolment.[current].course.code

Path tails inside filters

In general, filter conditions are logic formulas whose terms are path tails. This is powerful because filtering composes with navigation, folds and the other forms of path expression.

For example, this path reaches courses offered by the mathematics department:

u.course.[department.name = "Mathematics"].code

Attributes are reached one value at a time

An attribute is used as a value of its declared type. Its cardinality says how many values may be reached; it does not turn each reached value into a set.

For example, name has type String, so this is a type error:

u.department.[name ⊆ {"Mathematics", "Physics"}]

The operator ⊆ compares sets. The path tail name reaches strings, so membership is the right test:

u.department.[name ∈ {"Mathematics", "Physics"}]

The same rule would apply if an entity could have several names. Each reached name would still be a String, so the filter would still use ∈, not ⊆. This mistake often appears with ⊂, ⊃, ⊆, ⊇, ⊄ and ⊅ in filters and constraints.

Using richer logic formulas in filters

A filter condition can be more substantial. This expression reaches current enrolments in advanced mathematics courses where the student has not already completed the course and either has a passing mark or no mark has been recorded:

u.enrolment.[
    current
    ∧ course.advanced
    ∧ course.department.name = "Mathematics"
    ∧ course ∉ student.completed.Σ
    ∧ (mark ≥ 50 ∨ mark = none)
]

The condition inside a filter is a Boolean-valued path expression evaluated in the current path context. It may itself contain path tails, such as course.department.name and student.completed.Σ above. Existing knowledge about writing Boolean expressions still applies. For example:

25 Tuple Construction

Tuple construction picks several things and combines them to give the set of attributes output by the frame. The following expression selects course and department from the university as outputs:

u.(course, department)

Here course and department are both evaluated from the same university u.

Its denotation as a frame is:

course=C:Course, department=D:Department
where
    u.course(C)
  ∧ u.department(D)

The same idea works after navigation. The following expression selects code and title from each course as outputs:

u.course.(code, title)

The path tails inside the parentheses are evaluated from the same current value. In this case, both code and title are evaluated from the same course.

The empty tuple () projects away all attributes. The following expression reaches each course and then returns the empty tuple for each one:

u.course.()

This is the zero-attribute projection. It is useful when only the existence of a matching value matters, rather than any attributes of that value.

Nested tuple expressions

Tuple expressions can be nested:

u.course.((code, title), department.name)

Nesting does not create nested structure in the output frame. The output attributes are flattened:

code=C:String, title=T:String, name=N:String
where
  ∃K:Course ∃D:Department
    u.course(K)
  ∧ K.code(C)
  ∧ K.title(T)
  ∧ K.department(D)
  ∧ D.name(N)

Empty tuple expressions also disappear when flattened. For example, a.(b,(),(()).()) is equivalent to a.b.

Analogies with unwrapping, projection and Cartesian products

These examples have several relational-model analogies:

• u.(course, department) is relational-product-like because course and department are independent tails evaluated from the same university.
• u.course.(code, title) is relational-projection-like because it selects code and title as outputs.
• u.course.(code, title) is also unwrapping-like because it selects parts of each current course.

Later chapters use the same parentheses with renaming, calculations, folds and nested path expressions.

Path tails inside tuple construction

In general, tuple construction contains path tails. This is powerful because tuple construction composes with navigation, filters, folds and the other forms of path expression.

For example, this expression selects the student's name and the course code from each enrolment as outputs:

u.enrolment.(student.name, course.code)

Both path tails are evaluated from the same enrolment. That is why the student name and course code remain associated with each other.

The path tails can use filters too:

u.course.(code, [advanced].title)

Here code and [advanced].title are both evaluated from the same course. The second path tail begins with a filter before selecting the course title.

A theta-join-like expression

Tuple construction and filters can be combined in a way that resembles a theta join:

u.(enrolment, session).[enrolment.course = session.course]

The tuple construction forms enrolment-session combinations from the university. The filter keeps the combinations where the enrolment and the session refer to the same course.

26 Renaming with as

The as operator changes the output attribute name of a path tail.

For example:

u.student.name as studentName

The path still reaches student names, but the output attribute is named studentName instead of name.

Its denotation as a frame is:

studentName=N:String
where
  ∃S:Student
    u.student(S)
  ∧ S.name(N)

Restrictions on where as can be used

The as operator can be used wherever there is a single output attribute to rename. This limits how it can be used after tuple construction:

a.() as x       // wrong
a.(b) as x      // allowed
a.(b, c) as x   // wrong

Renaming inside tuple construction

Renaming is often used inside tuple construction, because path tails such as student.name and course.code would otherwise have output names taken from their final attributes.

u.enrolment.(student.name as studentName, course.code as courseCode)

The path tails are still evaluated from the same enrolment. The as clauses only choose the output attribute names.

Avoiding name clashes

Renaming is also useful when two outputs would otherwise have the same name:

u.enrolment.(student.name as studentName, course.department.name as departmentName)

Both path tails would otherwise output an attribute named name. The as clauses give them distinct output names.

27 This

The path tail this refers to the current value in the path. It is useful when the current value itself is needed, rather than one of its attributes.

For example, the following expression outputs each session together with the code of the course it belongs to:

u.course.session.(course.code as courseCode, this)

Inside session.(...), the current value is a session, so this outputs that session. The path tail this does not navigate anywhere; it uses the value already reached at that point in the path.

A path is read from left to right, and this means the current value at the point where it is written.

The output can give an explicit name to this. This expression reaches the advanced courses and outputs the course value itself, together with some of its attributes:

u.course.[advanced].(this as advancedCourse, code, title)

Inside [advanced].(...), the current value is still a course. The output named advancedCourse is therefore the reached course value, while code and title are attributes of the same course.

The same pattern is useful when a path has reached a value but the result should also show where it came from:

u.course.session.(this as scheduledSession, room, course)

Here this is the session reached by u.course.session, exposed under the result name scheduledSession. The course attribute is the course attached to that session.

28 Calculated Attributes

A path tail can calculate an output attribute from values reached in the current path context. The following expression calculates the duration of each session:

u.course.session.time.(endMinute-startMinute as durationMinutes)

The calculation uses two path tails, endMinute and startMinute, both evaluated from the same time slot. The as clause names the calculated output.

Calculations are path tails, so they can appear beside ordinary navigation in tuple construction:

u.course.session.(room, time.(day, endMinute-startMinute as durationMinutes))

This selects the room, the day, and the calculated duration for each session.

Calculations over assessment fields

The assessment variant attributes have numeric fields that can be used in calculations. This expression calculates how many minutes of exam time are assigned to each mark:

u.course.assessment.exam.(durationMinutes/maxMark as minutesPerMark)

The same idea works for assignments:

u.course.assessment.assignment.(wordLimit/maxMark as wordsPerMark)

Products are ordinary calculations too:

u.course.assessment.project.(estimatedHours*weight as weightedHours)

Calculated path tails inside filters

Calculated path tails can also appear inside filters. The following expression reaches long sessions:

u.course.session.time.[endMinute-startMinute > 120]

The filter condition calculates the duration from the current time slot, then compares it with 120.

Gotcha: Cartesian products with repeated use of attributes

Consider the following schema:

value X
{
    Real v*;
}

Multiple occurrences of an attribute in a path expression can lead to Cartesian products, which can be unexpected. For example, given a program variable x of type X the path expression:

x.(v*v as product)

is equivalent to:

x.(v as v1, v as v2).(v1*v2 as product)

Each occurrence of v is a distinct path tail, so the two occurrences are evaluated independently. The calculation therefore gives all combinations of V1*V2 where x.v(V1) and x.v(V2). This follows from the uniform rule that each path tail contributes its own frame; treating two identical-looking tails as the same reached value would be an extra special case.

One way to ask for all values of V*V where x.v(V) is to navigate to v first and then use this:

x.v.(this*this as product)

Another approach is to give the calculation a name by defining a function:

func Real square(Real x) = x*x;

The path expression can then call the function on the current reached value:

x.(square(v) as product)

For larger calculations, named functions make path expressions easier to read and avoid repeating the same multivalued path tail inside the calculation.

When several path tails need values below the same prefix, navigate to the shared prefix first. Repeating a multivalued prefix in separate tails can create Cartesian products between independently reached values.

29 Let Bindings

A let binding gives a name to a path tail so the named result can be used in the expression that follows.

The previous chapter showed that this expression forms products of independently reached values:

x.(v*v as product)

If the intention is to square each value reached by v, bind the reached value once:

x.(let a = v in a*a as product)

The name a refers to the value reached by the binding. The calculation uses that same named value twice.

Naming an intermediate calculation

let can also name an intermediate calculation:

u.course.session.time.(
  let duration = endMinute-startMinute in duration as durationMinutes)

This is deliberately a small example. The calculation is simple enough to write without let, but the shape becomes useful when the intermediate value is used more than once.

Keeping an outer value available

The chapter on this showed that let can preserve an outer value before navigation changes the current value. In the following expression, c names the current course before the path enters its sessions:

u.course.(let c = this in session.(c.code as courseCode, room))

Inside session.(...), the current value is a session. The name c still refers to the outer course.

Gotcha: this changes inside path tails

This expression tries to compare each session with the other sessions for the same course:

u.course.session.(let s=this in
    session.[this ≠ s])

The unqualified inner session is evaluated from the current session, not from the course. Save the course first, then navigate back through the saved course:

u.course.(let c=this in
    session.(let s=this in
        c.session.[this ≠ s]))

Use let outer=this in ... before entering a path tail when the nested expression still needs the outer object.

Let bindings inside filters

A let binding can appear inside a filter condition:

u.course.session.time.[let duration = endMinute-startMinute in duration > 120]

The filter keeps the time slots whose calculated duration is greater than 120.

30 Splat

The splat expression * denotes the set of attributes of the current value.

For example, the following expression unwraps each course:

u.course.(*)

The output frame has the attributes of Course, rather than a single output attribute named course.

Its denotation as a frame has the same result attributes as the Course type:

code=Code:String,
title=Title:String,
advanced=Advanced:Boolean,
department=D:Department,
prerequisite=P:Course,
session=S:Session,
assessment=A:Assessment,
enrolment=E:Enrolment
where
    u.course(C)
  ∧ C.code(Code)
  ∧ C.title(Title)
  ∧ C.advanced(Advanced)
  ∧ C.department(D)
  ∧ C.prerequisite(P)
  ∧ C.session(S)
  ∧ C.assessment(A)
  ∧ C.enrolment(E)

Attribute sets

Attribute names are first-class values. The expression @title denotes the attribute name title, and expressions such as {@code, @title} denote sets of attribute names.

The splat expression * also evaluates to a set of attributes. Tuple construction allows sets of attributes to be provided, so set operations can be used to manipulate the output attributes.

The set operators ∩, ∪ and ∖, and the set tests ⊂, ⊃, ⊆, ⊇, ⊄, ⊅, ∈ and ∉, work as expected on sets of attributes.

Removing attributes

Because * denotes a set of attributes, set operations can be used to shape the output attributes. This expression unwraps each course except for title:

u.course.(* \ {@title})

The output has every Course attribute except title.

Adding selected attributes

Splat can be combined with ordinary path tails in tuple construction:

u.course.(* \ {@department}, department.name as departmentName)

This unwraps each course, removes the department attribute, and adds the department name under the output attribute departmentName.

Name clashes

Unwrapping can introduce name clashes. If two splatted values have attributes with the same name, rename or remove attributes before combining them:

u.enrolment.(* \ {@student}, student.name as studentName)

The splat exposes the enrolment attributes except student; the renamed path tail adds the student's name.

31 Folds

A fold takes the values reached by a path and collapses them to one value. The following expression counts the sessions for each course:

u.course.(code, session.Σcount as sessionCount)

Without the fold, session reaches the sessions of a course one at a time. With Σcount, those reached sessions are counted and the count is output as sessionCount.

The same idea works for numeric values. The following expression sums the maximum marks available from a course's exams:

u.course.(code, assessment.exam.maxMark.Σsum as examMarks)

The path before the fold reaches the exam maximum marks for the current course. The fold turns those marks into one number.

Common folds

These standard folds cover many common cases:

Collecting reached values

The fold .Σ collects the reached values as a set. The following expression gives each course with the set of codes for its prerequisites:

u.course.(code, prerequisite.code.Σ as prerequisiteCodes)

This is useful when the path should remain attached to the current course as one set-valued output, rather than producing one output for each prerequisite code.

Folds after filters

Because filters are path tails, a fold can summarise the values that remain after filtering. The following expression counts long teaching sessions for each course:

u.course.(
  code, 
  session.time.[endMinute-startMinute > 60].Σcount 
    as longSessionCount)

The filter reaches only the time slots whose duration is greater than sixty minutes. The fold counts those filtered time slots.

Inline folds

Named folds such as Σsum are ordinary fold definitions. An inline fold writes the reduction directly:

u.course.(
  code, 
  assessment.exam.durationMinutes.Σ{ 0 ; total d ↦ total + d } 
    as examMinutes)

The first part, 0, is the initial accumulator. The step total d ↦ total + d says how to update the accumulator for each reached duration. This example is equivalent to using Σsum, but inline folds are useful when the reduction is specific to the query.

An inline fold can also use the first reached value as its seed:

u.course.(
  code, 
  session.time.startMinute.Σ{ 
      first m ↦ m ; 
      earliest m ↦ if m < earliest then m else earliest } 
    as firstStart)

This is the shape used by folds such as Σmin and Σmax.

Empty inputs

Some folds have a value even when no values are reached. For example, Σcount gives 0, Σexists gives false, and Σempty gives true.

Other folds need at least one reached value. For example, Σmean, Σmin and Σmax are not defined on an empty input. When that matters, use a filter or a separate test such as Σexists to say when the folded value is required.

Composability

Folds compose with the path tails from earlier chapters. Navigation chooses what values can be reached, filters remove unwanted values, calculations can produce values to fold, and as names the folded output.

u.course.(
  code, 
  assessment.project.[groupWork].estimatedHours.Σsum 
    as groupProjectHours)

Here the path reaches each course, enters its project assessments, keeps only the group projects, reaches their estimated hours, sums those hours, and names the result.

32 Universal Navigation

Ordinary navigation reaches values that can be reached from at least one current value. Universal navigation reaches values that can be reached from every current value.

For example, the following expression reaches the teaching days used by every advanced course:

u.course.[advanced]⇒session.time.day

A day is output only if each advanced course has some session on that day. The left side, u.course.[advanced], supplies the courses being tested. The right side, session.time.day, is tested from each of those courses.

The logical shape is:

day=D:Day
where
  ∀C:Course ∀A:Boolean
    (u.course(C) ∧ C.advanced(A) ∧ A)
  → ∃S:Session ∃T:TimeSlot
      C.session(S)
    ∧ S.time(T)
    ∧ T.day(D)

For every advanced course C, the right-hand path must be able to reach the output day D.

Ordinary navigation versus universal navigation

Changing ⇒ to . changes the meaning:

u.course.[advanced].session.time.day

This reaches days used by at least one advanced course. The universal version:

u.course.[advanced]⇒session.time.day

reaches only days used by all advanced courses. Ordinary navigation is like a union of what each current value can reach. Universal navigation is like an intersection of what each current value can reach.

Asking whether all values satisfy a condition

Often a universal requirement is easiest to write by looking for counterexamples. This expression reaches courses that have no assessment worth more than 60 percent:

u.course.[assessment.[weight > 60].Σempty]

The inner filter reaches the bad assessments. Σempty then says that there are none. This pattern is often the clearest way to say "all reached values satisfy the condition".

Using folds and subset tests

Another common pattern is to collect reached values with .Σ, then compare sets. For example, this expression reaches advanced courses whose prerequisites are all mathematics courses:

u.course.[advanced].[
    prerequisite.Σ ⊆ u.department.[name = "Mathematics"].course.Σ
]

Here the requirement is naturally a set inclusion. The left side is the set of prerequisites of the current course. The right side is the set of courses offered by the mathematics department.

Relation to relational division

Universal navigation is the path-expression form of division-style queries. A division query asks for the values related to all values in some divisor relation. In the first example, the divisor is the advanced courses, and the result contains days related to every one of those courses by the session.time.day path.

The classic supplier-parts query "suppliers who supply all parts" has exactly this shape:

In Tutorial D, it can be written using non-existence:

S WHERE NOT EXISTS (
    P WHERE NOT EXISTS (
        SP WHERE SP.S# = S.S#
           AND SP.P# = P.P#
    )
)

It can also be written using DIVIDEBY:

S MATCHING (
    SP { S#, P# }
    DIVIDEBY P { P# }
    PER ( S { S# } )
)

In Predica, universal navigation gives the same query directly:

s.part⇒(shipment.supplier)

The left side supplies the required parts. The right side reaches the suppliers for each part. The output suppliers are those reached from every part.

Adding a filter gives the usual "suppliers who supply all red parts" query:

In Tutorial D, the non-existence form is:

S WHERE NOT EXISTS (
    (P WHERE COLOR = 'Red')
    WHERE NOT EXISTS (
        SP WHERE SP.S# = S.S#
           AND SP.P# = P.P#
    )
)

The corresponding DIVIDEBY form is:

S MATCHING (
    SP { S#, P# }
    DIVIDEBY (P WHERE COLOR = 'Red') { P# }
    PER ( S { S# } )
)

In Predica, the filter is part of the left side of the universal navigation:

s.part.[color = Color.red]⇒(shipment.supplier)

The DIVIDEBY versions make the relation to relational division explicit. In practice, Tutorial D users will often prefer the non-existence form: choose the candidate values for which there does not exist a required value with no matching relationship. Universal navigation packages that double-negation pattern into a path operator.

Choosing the universal pattern

There are three common ways to express universal requirements. The best choice usually depends on the sentence you are trying to write.

prerequisite.Σ ⊆
  u.department.[name="Mathematics"].course.Σ

u.course.[
    assessment → assessment.weight ≤ 60
]

The difference is that Σempty tests for absence, a.Σ ⊆ b.Σ compares two collected sets, ⇒ produces common reachable values, and → states a conditional requirement.

Using → inside a filter often makes universal quantification appear when the frame condition is written out. The implication itself is the condition, but the witnesses used by its antecedent are usually universally closed when the filter is rendered. This is why:

u.course.[assessment → assessment.weight ≤ 60]

reads like "courses for which every assessment has weight at most 60". The same idea can also be written by looking for no counterexamples:

u.course.[assessment.[weight > 60].Σempty]

The two expressions approach the universal requirement from different directions. The first says what must follow from each reached assessment. The second says there are no reached assessments that break the rule.

Do not reach for it too soon

Universal navigation is powerful, but it is not the only way to write universal requirements. Use ⇒ when the result should be values reachable from every left-side value. Use Σempty when the clearest thought is "there are no bad cases". Use .Σ with subset testing when the clearest thought is "this set is contained in that set".

33 Path Operations

Path operations combine whole path expressions. They are useful when the question is easier to write as two paths that are then combined.

For example, this expression reaches courses that are both advanced and offered by the mathematics department:

u.course.[advanced]
  ⊓ u.department.[name = "Mathematics"].course

Both sides output courses. The ⊓ operation keeps the course values that satisfy both sides.

Meet

Use ⊓ when the thought is "both paths must hold".

u.course.[advanced]
  ⊓ u.course.[assessment.exam.Σexists]

This reaches courses that are advanced and have at least one exam assessment. The two sides are ordinary path expressions; ⊓ combines their frame conditions with logical conjunction.

In relational-model terms, ⊓ is relational-join-like. When both sides expose the same output, it looks like intersection, as in the examples above. When the sides expose different outputs while sharing some surrounding condition, it looks more like a relational join.

u.course.(enrolment.student ⊓ session.room)

This combines students and rooms for each course. If a course has several enrolled students and several rooms, the expression can form combinations of those reached values, just as a join can.

This is the path-expression counterpart of relational natural join ⨝, but at a different level. The relational operator joins relations. The path operator ⊓ combines path denotations by aligning common result attributes and conjoining their frame conditions. When the path results have relation-shaped tuples, that frame meet behaves like natural join.

(E₁ ⊓ E₂).Σ = E₁.Σ ⨝ E₂.Σ

This law holds when E₁ and E₂ are evaluated in the same context and their result attributes are join-compatible. The left side performs the meet at the path/frame level and then collects the resulting tuples; the right side collects each path result first and then joins those tuple sets.

Union

Use ⊔ when the thought is "either path may hold".

u.course.[advanced]
  ⊔ u.department.[name = "Mathematics"].course

This reaches courses that are advanced, courses offered by the mathematics department, or both. When the two sides output the same attribute, the result is the ordinary union-like case.

(E₁ ⊔ E₂).Σ = E₁.Σ ∪ E₂.Σ

This ordinary set-union law holds when E₁ and E₂ are evaluated in the same context and have the same result shape. More generally, path union is frame-level disjunction: it aligns compatible result attributes and combines the branch conditions with ∨.

The operation can also combine paths that reach the same kind of output by different routes:

u.(student.name ⊔ department.name)

This exposes names reached through students or departments. That is a genuine path-level disjunction. It is not tuple construction; tuple construction would try to combine outputs side by side.

Difference

Use -- when the thought is "the left path, except where the right path also holds".

u.course -- u.student.completed

This reaches courses that are not among the completed courses of any student. The left side supplies the result shape. The right side removes assignments that also satisfy its path.

(E₁ -- E₂).Σ = E₁.Σ ∖ E₂.Σ

This ordinary set-difference law holds when E₁ and E₂ are evaluated in the same context and have the same result shape. In the general path case, -- is logical difference over frames: it keeps the left condition and conjoins the negation of the right condition.

Path difference is written --. Set difference is written with the set-minus operator, as in expressions over sets of attributes or values. Keeping those two spellings separate helps distinguish path difference from set difference.

Pointwise negation

The postfix operator ! negates a path while preserving the path's output. It is most intuitive on Boolean-valued paths:

u.course.(code, advanced! as notAdvanced)

Here advanced reaches the Boolean values recorded for the course. advanced! reaches the Boolean values not reached by advanced. Since advanced is a single-valued Boolean attribute in the example schema, this reads as the opposite Boolean value.

This is different from filtering courses that are not advanced:

u.course.[¬advanced]

The filter keeps courses. The expression advanced! still outputs Boolean values.

Path complement

The postfix operator ~ negates the existence of a path and returns to the current receiver. For example, this reaches courses with no prerequisites:

u.course.prerequisite~

The prerequisite path is tested from each course. If no prerequisite can be reached, the course itself is retained.

The same idea can be written with a fold:

u.course.[prerequisite.Σempty]

The fold version is often easier to read when the thought is simply "there are no values". The ~ form is useful when the expression is already being written as a path and the desired result is the current receiver.

The current receiver is kept when the following path has no match. In relational-model terms this resembles semidifference or anti-join, but in Predica it is defined as path complement relative to the current receiver.

Composability

Path operations compose with the earlier path tails. Each side of an operation can use navigation, filters, tuple construction, renaming, folds and universal navigation.

(
    u.course.[assessment.exam.Σexists]
    ⊔ u.course.[assessment.project.Σexists]
)
.[prerequisite.Σempty]
.(code, title)

This reaches courses that have an exam or a project, have no prerequisites, and then outputs the course code and title. The important habit is to read each operation as combining path expressions, not as changing what dots mean.

34 Alternatives

The alternative operator | combines result-producing expressions. It is most useful when the same idea can be reached through several shapes.

For example, a variant type can define a calculated attribute by giving one expression for each case:

variant Shape
{
    { Real radius } sphere;
    { Real side } cube;
    { Real radius, Real height } cone;

    → Real volume =
        sphere.(4/3*pi*radius^3)
      | cube.(side^3)
      | cone.(pi*radius^2*height/3);
}

For each shape, exactly one effective current variant base attribute applies, so the corresponding branch contributes the volume. The result is a single Real value.

Similarly, an assessment may be an exam, an assignment or a project. Each kind of assessment has a maximum mark, but the path to the maximum mark depends on the variant attribute:

u.course.assessment.(
    exam.maxMark
  | assignment.maxMark
  | project.maxMark
)

For each assessment, whichever branch applies contributes the maximum mark. The three branches all produce one result of the same type, so the alternative expression exposes one result.

Naming the result

The result can be named with as, just like any other single output:

u.course.assessment.(
    (exam.maxMark | assignment.maxMark | project.maxMark)
      as maxMark
)

The name belongs to the result of the whole alternative, not to only the final branch.

Alternatives are not union

The operator | is different from ⊔. The ⊔ operator combines path frames. The | operator combines single-result expressions and exposes one result.

u.course.assessment.(
    exam.maxMark
  | assignment.maxMark
  | project.maxMark
)

This should be read as an expression-level choice of result. It is not asking for a tuple with three attributes, and it is not joining three paths side by side.

Using alternatives in calculations

Alternatives can appear inside calculations. The following expression calculates the weighted maximum mark for each assessment:

u.course.assessment.(
    (exam.maxMark | assignment.maxMark | project.maxMark)
  * (exam.weight | assignment.weight | project.weight)
  / 100
    as weightedMaxMark
)

The example schema makes this easy because every assessment variant attribute has maxMark and weight. The path expression does not need a special case statement; each branch is an ordinary expression component.

When the branches differ

Branches do not have to keep the same output name. If branch names differ, the alternative still exposes one result, but the result is anonymous unless it is renamed:

u.course.assessment.(
    (exam.durationMinutes | assignment.wordLimit | project.estimatedHours)
      as size
)

This can be useful when the alternatives are deliberately being normalised into one common measure. The name size is supplied by the outer as.

A gotcha about repeated alternatives

Separate alternatives are separate path tails. In the weighted mark example, the disjoint variant attributes make the intended pairing clear: an exam mark is paired with an exam weight, an assignment mark with an assignment weight, and a project mark with a project weight.

Do not generalise that into a rule that repeated alternatives always share the same witness. As with calculations, repeated multivalued path tails can create combinations. When several values must come from the same place, navigate to the shared prefix first, then pick the values below it.

Composability

Alternatives compose with filters, tuple construction and folds. The following expression sums the maximum marks available from all assessments in each course:

u.course.(
    code,
    assessment.(
        exam.maxMark
      | assignment.maxMark
      | project.maxMark
    ).Σsum as totalMaxMark
)

The path reaches each course, reaches its assessments, chooses the appropriate maximum-mark path for each assessment, sums those marks, and names the result.

35 Conditionals

A conditional chooses between two result-producing expressions using a Boolean condition.

For example, this expression labels each course as advanced or introductory:

u.course.(
    code,
    (if advanced then "advanced" else "introductory") as level
)

The condition is advanced. If it is true for the current course, the result is "advanced". Otherwise the result is "introductory".

Conditions can use path tails

The condition is an ordinary Boolean-valued expression, so it can use navigation, filters and folds:

u.course.(
    code,
    (if assessment.exam.Σexists then "exam" else "coursework")
      as assessmentStyle
)

This labels a course as "exam" when it has at least one exam assessment, and as "coursework" otherwise.

Branches can use path tails too

The then-branch and else-branch are also path expressions. The following expression uses a fold in the then-branch:

u.course.(
    code,
    (if advanced
     then assessment.project.estimatedHours.Σsum
     else 0)
      as advancedProjectHours
)

For advanced courses, the result is the total estimated project hours. For other courses, the result is 0.

Both branches produce one result

The producing branches must have a common result type. This works because both branches produce strings:

u.course.(
    code,
    (if session.time.day.Σcount > 2
     then "spread out"
     else "compact")
      as timetableShape
)

A conditional exposes one result. The result name can be supplied with as on the whole conditional expression.

Conditionals are not alternatives

Conditionals and alternatives are both expression-level branching constructs, but they answer different questions. Use if then else when there is an explicit Boolean condition. Use | when several branches may produce the same kind of result.

u.course.assessment.(
    (if exam.Σexists
     then exam.maxMark
     else (assignment.maxMark | project.maxMark))
      as maxMark
)

This is legal, but it is not the clearest expression of the idea. The variant case is better written with alternatives:

u.course.assessment.(
    (exam.maxMark | assignment.maxMark | project.maxMark)
      as maxMark
)

The first version asks a Boolean question and then chooses a branch. The second version simply says which paths can produce the maximum mark.

Composability

Conditionals compose with the earlier path tails. The condition can filter, count or navigate. The branches can calculate, fold, use alternatives, or return constants.

u.course.(
    code,
    (if advanced ∧ assessment.project.Σexists
     then assessment.project.estimatedHours.Σsum
     else 0)
      as projectHoursForAdvancedCourses
)

The expression reaches each course, checks a Boolean condition about that course, and then chooses the value to output. Each part is still a path expression.

36 Lists

The fold .Σ collects reached values as a set. The list form Σlist collects reached values as an ordered list.

For example, this expression gives the course codes in code order:

u.course.Σlist(code order by code)

The path u.course reaches courses. For each course, code produces the list item, and the order by code clause says how to order the list.

List items can be tuples

The list item can be a tuple expression. The following expression gives a list of course summaries:

u.course.Σlist((code, title) order by code)

The tuple expression controls the shape of each list item. The order by clause controls the order of the list items.

Ordering keys

The ordering key does not have to be part of the list item:

u.course.Σlist(title order by code)

This lists course titles but orders them by course code.

A simple ordering key is enough when that key determines the intended order:

u.student.Σlist(name order by name)

Ordering direction can be written with ↑ for ascending and ↓ for descending. If no direction is written, ascending order is assumed. Several ordering keys may be supplied; they are compared from left to right:

u.course.Σlist((code, title) order by advanced↓, code↑)

Filtering list items

A list expression can include an if clause. Only reached values satisfying the condition contribute list items:

u.course.Σlist(code order by code if advanced)

This gives an ordered list of advanced course codes.

The filter condition can use path tails, just like an ordinary filter:

u.course.Σlist(
    (code, title)
    order by code
    if assessment.exam.Σexists
)

This lists the courses that have at least one exam assessment.

Lists and sets

Use .Σ when the result should be a set. Use Σlist when order is part of the result.

u.course.code.Σ
u.course.Σlist(code order by code)

The first expression produces a set of course codes. The second produces a list of course codes ordered by code. Set operations such as ⊆, ∈ and ∩ are for sets; list operations are for ordered values.

List items can use earlier ideas

The list item is a path expression evaluated for each reached value, so it can use tuple construction, calculations, alternatives and conditionals.

u.course.Σlist(
    (
        code,
        (if advanced then "advanced" else "introductory") as level,
        assessment.(exam.maxMark | assignment.maxMark | project.maxMark).Σsum
            as totalMaxMark
    )
    order by code
)

This produces an ordered list of course summaries. Each summary contains the course code, a calculated level, and the total maximum mark across assessments.

Composability

Because Σlist is path-based, it can be used inside tuple construction to attach an ordered list to each current value.

u.department.(
    name,
    course.Σlist((code, title) order by code) as courses
)

This reaches each department and attaches an ordered list of the courses offered by that department.

37 Groups

Many useful summaries do not need explicit grouping. When a fold appears inside tuple construction, it is evaluated relative to the current receiver.

For example, this expression counts enrolments for each course:

u.course.(
    code,
    enrolment.Σcount as enrolmentCount
)

There is no separate group by course clause. The current course already gives the group: enrolment.Σcount counts the enrolments reached from that course.

Explicit grouping

Use explicit grouping when the groups are not already the current receiver. The following expression groups enrolments by course code:

u.enrolment.groupby(course.code)

This does not compute an aggregate. It groups the observed enrolments by the key course.code. Aggregates are then written as folds over the group.

u.enrolment.groupby(course.code).(
    code,
    group.Σcount as enrolmentCount
)

The key course.code supplies the output code. The name group refers to the enrolments in that group.

Naming the group

An explicit group label can make later path tails easier to read:

u.enrolment.group(e)by(course.code).(
    code,
    e.Σcount as enrolmentCount,
    e.[current].Σcount as currentEnrolmentCount
)

Here e names the enrolments in each group. The second count counts all enrolments for the course; the third count counts only the current enrolments.

Grouping by another key

The grouping key can navigate. This expression groups enrolments by department name:

u.enrolment.group(e)by(course.department.name).(
    name as departmentName,
    e.Σcount as enrolmentCount
)

Each group contains the enrolments whose courses are offered by the same department.

Grouping by several values

The key can be a tuple expression. This groups enrolments by department and by whether the enrolment is current:

u.enrolment.group(e)by(
    (
        course.department.name as departmentName,
        current
    )
).(
    departmentName,
    current,
    e.Σcount as enrolmentCount
)

The tuple key gives one group for each department/current combination that is observed.

Relation to relational grouping

Explicit grouping is the path-expression counterpart of grouping before aggregation. In Tutorial D, a summary query uses SUMMARIZE ... PER ... ADD .... In Predica, grouping and aggregation remain separate path-expression steps:

u.enrolment.group(e)by(course.code).(
    code,
    e.Σcount as enrolmentCount
)

The group(e)by(course.code) part forms the groups. The e.Σcount part is the aggregate over each group.

Groups and lists

Groups compose with Σlist. The following expression gives each department with an ordered list of its course enrolment counts:

u.enrolment.group(e)by(course.department.name).(
    name as departmentName,
    e.groupby(course.code).Σlist(
        (
            code,
            group.Σcount as enrolmentCount
        )
        order by code
    ) as courseEnrolments
)

The outer grouping forms department groups. Inside each department group, the enrolments are grouped again by course code and collected into an ordered list.

Composability

Grouping does not replace the other path-expression tools. It gives a new current group, and then the usual operations can be used inside that group: filters, tuple construction, folds, lists, alternatives and conditionals.

u.enrolment.group(e)by(course.code).(
    code,
    e.[current].Σcount as currentCount,
    e.[¬current].Σcount as pastCount,
    (if e.[current].Σexists then "active" else "inactive")
        as status
)

The expression groups enrolments by course, computes two filtered counts, and then uses a conditional to label the course group.

38 Type Checking Path Expressions

This chapter gives an informal way to think about type checking path expressions. The full definition is recursive: each path tail is checked in the context produced by the tails before it. Part XIV: Semantics formalises the propagation of type information recorded in frames, and therefore formalises the static typing of path expressions. Here the aim is only to make the typing intuition clear.

Attributes are generally named with singular nouns, such as course or name, and have singular types like Course or String. Predica path expressions have the singular type of each reached value. A path may reach many values through such an attribute, but each reached value still has the attribute's singular type. Set-valued expressions are available when the set itself is needed, for example by writing course.Σ.

Current type

While reading a path from left to right, the type checker keeps track of the current type. A navigation step may be used when the current type has the named attribute. After the step, the current type is the declared type of that attribute.

For example, if course has type Course and code has type String, then:

u.course.code

is checked by first reaching courses from u, then checking code from each reached course. The code step reaches String values.

Cardinality is not part of the type

An attribute's cardinality says how many values may be reached. It is not part of the type itself. A plural attribute of type Real still reaches Real values, one at a time.

For example:

value X
{
    Real v*;
}

The attribute v can reach many values, but each reached value has type Real. This is why the following expression type checks:

func Real square(Real x) = x*x;

x.(square(v) as product)

The function square takes one Real. The path tail v reaches Real values, so square(v) applies the function to each reached value. The result may have many product values, but each individual function call is still a call on a Real value.

This is the same rule described earlier for filters: do not mistake a plural attribute for a set-valued expression. If name has type String, then each reached name is a String, even when many names can be reached.

u.department.[name ∈ {"Mathematics", "Physics"}]

The condition uses ∈ because each reached name is a String. It does not use ⊆, because name is not a set-valued expression.

Tuple construction

In tuple construction, each component is checked from the same current type. The current value denoted by this does not change between components.

u.course.(code, title)

Both code and title are checked from Course, because both are inside the tuple construction following u.course.

Filters

A filter condition is checked from the current type, and the filter keeps current values for which the condition holds. The condition must be a Boolean-valued expression. The filter does not change the type of the current value.

u.course.[advanced].code

The filter [advanced] is checked from Course and keeps courses. The following .code is still checked from Course, not from Boolean.

A Boolean condition may be false for every current value. This is still a well-typed path expression:

u.[false]

The result has the same current type as u, namely University, but reaches no values.

Calculated outputs

A calculated output is checked as an ordinary expression in the current path context. The expression must be well typed. Its result type becomes the type of the output attribute named by the as clause.

u.course.assessment.exam.(durationMinutes/maxMark as minutesPerMark)

Inside the parentheses, durationMinutes and maxMark are both checked from the current exam assessment value. The output attribute minutesPerMark has the result type of the / expression.

Σ gives a Set<T>

When a calculation really needs the set of all values reached by a plural path, use a fold to make that set explicit. In the following example, v.Σ has type Set<Real>, so it can be compared with a set:

x.((if v.Σ ⊆ {1, 2, 3} then 1 else 2) as a)

The condition in the if expression is Boolean-valued because ⊆ compares two sets. This differs from using v directly: v reaches Real values one at a time, while v.Σ collects the reached values into a set.

39 Constraint Forms

Predica supports several forms of constraints, each governing different aspects of the values and relationships in a model.

• Attribute type constraints:
  These restrict the possible values of an attribute.

  
          X x;            // Each value of x must be of type X
          

• Attribute cardinality constraints:
  These constrain the cardinality of an attribute's extension.

  
          X x[1..3];      // Cardinality of extension of x must be between 1 and 3
          

• Key constraints:
  Keys identify when two instances of a nominal type represent the same entity.

  
          entity X
          {
              Name name;
              Integer value;
              key { name };       // Instances of X with the same name are the same
          }
          

• Derived attribute constraints:
  A derived attribute is constrained by the expression that defines it.

  
          value Rectangle
          {
              Real width;
              Real height;
              → Real area = width*height;       // constrained by expression
          }
          

• Where‑constraints on attributes:
  A where‑clause restricts the value of an attribute.

  
          entity Supplier
          {
              String name;
              Shipment shipment* 
                  where shipment.supplier = this;   // where constraint on shipment
              key {name};
          }
          

• Constraint blocks:
  A nominal type may include a constraints block containing Boolean expressions, each terminated with ;.

  
          entity Person
          {
              String name;
              Boolean registered_to_vote;
              Integer age;
  
              constraints
              {
                  ¬name.empty();
                  registered_to_vote → age ≥ 18;
              }
          }
          

Constraint expressions

A constraint expression may appear in a where clause or a constraints block.

A constraint expression must be Boolean-valued. It may use:

• logical connectives ¬, ∧, ∨ and →
• Parentheses
• Truth constants: true and false
• Boolean-valued path expressions (including sentences such as path.())
• Comparison operations <, ≤, >, ≥, = and ≠.

Predica uses a single expression grammar for both path expressions and logic expressions. This allows a single expression to freely mix logic connectives (¬ ∧ ∨ →) with path constructs (. ⇒ ⊓ ⊔ | \ [] () ! ~). The result is interpreted as a logical formula parameterised by the terms introduced by path expressions. The overall expression may itself be a path expression, allowing shared path prefixes and compositional navigation.

For example:

entity A
{
    Boolean x;
    Boolean y;
}

entity B
{
    A z*;
    constraints
    {
        // ∀Z:A ∀X:Boolean ∀Y:Boolean (this.z(Z) ∧ Z.x(X) ∧ Z.y(Y)) → (X ∨ Y)
        z.(x ∨ y);
    }
}

Cardinality constraints in path expressions

Predica allows : for writing cardinality constraints on path expressions. In the following example b:2 expresses the condition that the cardinality of the extension of b is exactly 2:

entity X
{
    Boolean a;
    Integer b*;
    constraints
    {
        // Shorthand for a → b.Σcount=2
        // ∀A:Boolean this.a(A) → (A → |{B:Integer|this.b(B)}| = 2)
        a → b:2;
    }
}

A cardinality constraint on a path expression uses the syntax:

path : k        // exactly k
path : k..m     // between k and m inclusive
path : ?        // 0 or 1
path : +        // 1 or more
path : k+       // k or more

where k and m are integer literals.

Cardinality binds looser than path composition, so it constrains the complete path expression to its left. For example, licence.[valid]:1 is parsed as (licence.[valid]):1, not as licence.([valid]:1).

This syntax mirrors attribute cardinality (x?, x+, x[k], x[k..m]).

40 Firearm Purchase Example

A person may purchase a firearm only if they hold a valid licence. This example shows how Predica expresses such legality conditions directly as constraints on the FirearmPurchase entity. The constraints are declarative: they state what must be true in any world where a firearm purchase is legally permitted.

entity Person
{
    String name;
    Integer age;
}

entity FirearmLicence
{
    Person holder;
    Boolean valid;
}

entity FirearmPurchase
{
    Person buyer;
    FirearmLicence licence where licence.holder = buyer;

    constraints
    {
        buyer.age ≥ 18;
        licence.valid;
    }
}

When mapped into logic, these constraints become:

// buyer.age ≥ 18
∀B:Person ∀A:Integer
    (this.buyer(B) ∧ B.age(A)) → (A ≥ 18)

// licence.valid
∀L:FirearmLicence ∀V:Boolean
    (this.licence(L) ∧ L.valid(V)) → V

// licence.holder = buyer (from the where constraint)
∀L:FirearmLicence ∀H:Person ∀B:Person
    (this.licence(L) ∧ L.holder(H) ∧ this.buyer(B)) → (H=B)

41 Construction Project Example

This example shows how legality conditions can be expressed directly as constraints across a small network of related entities:

• Multi-entity legality: legality depends on the builder, licence, zoning rule, environmental clearance, project site and recorded violations.
• Temporal constraints: the licence and environmental clearance must be valid at the project start date.
• Identity and backlink constraints: licences, clearances and violations must refer to the same builder, site or project being certified.
• Cross-value constraints: project height and intended use must be compatible with the zoning rule.
• Declarative legality: there is no procedural validation code, only constraints that describe compliant worlds.

entity Person
{
    String name;
    Integer age;
}

entity BuilderLicence
{
    Person holder;
    Date validFrom;
    Date validTo;
    Boolean suspended;

    constraints
    {
        // ∀A:Integer ∀H:Person
        //     (this.holder(H) ∧ H.age(A) → A ≥ 18)
        holder.age ≥ 18;

        // ∀V:Date ∀V1:Date
        //     (this.validFrom(V) ∧ this.validTo(V1) → V ≤ V1)
        validFrom ≤ validTo;
    }
}

entity ZoningRule
{
    String zone;
    Integer maxHeight;
    Boolean residential;
    Boolean commercial;
}

entity EnvironmentalClearance
{
    String siteId;
    Boolean approved;
    Date expiry;
}

entity ConstructionProject
{
    String id;
    String siteId;
    Person builder;
    BuilderLicence licence;
    ZoningRule zone;
    Boolean residential;
    Boolean commercial;
    Integer height;
    EnvironmentalClearance clearance;
    Date startDate;

    constraints
    {
        // 1. Builder must match the licence holder
        // ∀H:Person ∀B:Person ∀L:BuilderLicence
        //     (this.licence(L) ∧ L.holder(H) ∧ this.builder(B) → H = B)
        licence.holder = builder;

        // 2. Licence must be valid at the start date
        // ∀V:Date ∀S:Date ∀L:BuilderLicence
        //     (this.licence(L) ∧ L.validFrom(V) ∧ this.startDate(S) → V ≤ S)
        licence.validFrom ≤ startDate;

        // ∀S:Date ∀V:Date ∀L:BuilderLicence
        //     (this.startDate(S) ∧ this.licence(L) ∧ L.validTo(V) → S ≤ V)
        startDate ≤ licence.validTo;

        // 3. Licence must not be suspended
        // ∀S:Boolean ∀L:BuilderLicence
        //     (this.licence(L) ∧ L.suspended(S) → ¬S)
        ¬licence.suspended;

        // 4. Height must comply with zoning
        // ∀H:Integer ∀M:Integer ∀Z:ZoningRule
        //     (this.height(H) ∧ this.zone(Z) ∧ Z.maxHeight(M) → H ≤ M)
        height ≤ zone.maxHeight;

        // 5. Environmental clearance must be approved and valid
        // ∀A:Boolean ∀C:EnvironmentalClearance
        //     (this.clearance(C) ∧ C.approved(A) → A)
        clearance.approved;

        // ∀S:Date ∀E:Date ∀C:EnvironmentalClearance
        //     (this.startDate(S) ∧ this.clearance(C) ∧ C.expiry(E) → S ≤ E)
        startDate ≤ clearance.expiry;

        // 6. The clearance must be for this project site
        // ∀S:String ∀S1:String ∀C:EnvironmentalClearance
        //     (this.clearance(C) ∧ C.siteId(S) ∧ this.siteId(S1) → S = S1)
        clearance.siteId = siteId;

        // 7. Residential/commercial compatibility
        //    (example: a commercial project cannot be built in a residential-only zone)
        // ∀R:Boolean ∀R1:Boolean ∀Z:ZoningRule
        //     (this.residential(R) ∧ this.zone(Z) ∧ Z.residential(R1) ∧ R → R1)
        residential → zone.residential;

        // ∀C:Boolean ∀C1:Boolean ∀Z:ZoningRule
        //     (this.commercial(C) ∧ this.zone(Z) ∧ Z.commercial(C1) ∧ C → C1)
        commercial → zone.commercial;

        // ∀R:Boolean ∀C:Boolean
        //     (this.residential(R) ∧ this.commercial(C) → ¬(R ∧ C))
        ¬(residential ∧ commercial);
    }
}

entity Violation
{
    ConstructionProject project;
    String code;
    Boolean resolved;
}

entity LegalProject
{
    ConstructionProject project;
    Violation violation*;

    constraints
    {
        // All violations must be resolved
        // ∀R:Boolean ∀V:Violation
        //     (this.violation(V) ∧ V.resolved(R) → R)
        violation.resolved;

        // Every listed violation must belong to this legal project
        // ∀P:ConstructionProject ∀P1:ConstructionProject ∀V:Violation
        //     (this.violation(V) ∧ V.project(P) ∧ this.project(P1) → P = P1)
        violation.project = project;
    }
}

42 Cardinality Constraint Patterns

Exactly one requirements

• a person must have exactly one primary residence
• a project must have exactly one responsible officer

entity Person
{
    Address primaryResidence;
}

At least one requirements

• a company must have at least one director
• a contract must have at least one signatory

entity Company
{
    Person director+;
}

At most one

A person may have at most one active passport.

entity Person
{
    Passport passport?;
}

Optional-but-constrained fields

Sometimes a field is optional, but if present, it must satisfy further constraints. Example: A building project may have an environmental clearance, but if it does, it must be valid.

entity Project
{
    EnvironmentalClearance clearance?;

    constraints
    {
        // ∀C:EnvironmentalClearance ∀V:Boolean
        //     (this.clearance(C) ∧ C.valid(V)) → V
        clearance.valid;
    }
}

Collections that must be non-empty when another condition holds

Example: A project with “commercial = true” must have at least one safety audit.

entity Project
{
    Boolean commercial;
    Audit audit*;

    constraints
    {
        // if commercial, then there is at least 1 audit
        // Shorthand for commercial → audit.Σexists;
        // ∀C:Boolean (this.commercial(C) → ∃A:Audit this.audit(A))
        commercial → audit:+;
    }
}

Cardinality constraints on joins

A builder must hold exactly one valid licence at the time of a project.

entity BuilderLicence
{
    ...
    Boolean valid;
}

entity Builder
{
    BuilderLicence licence*;

    constraints
    {
        // exactly one valid licence
        // This is shorthand for licence.[valid].Σcount = 1
        // |{ L:BuilderLicence | ∃V:Boolean this.licence(L) ∧ L.valid(V) ∧ V }| = 1
        licence.[valid]:1;
    }
}

43 Student Enrolment Courses Example

This example keeps the model deliberately small. The main design choices are:

• Enrolment is the source of truth for which student is taking which course.
• Student.enrolled is derived from the student's enrolments.
• Course.prerequisite is the source of truth for course ordering.
• There is no separate dependent attribute, so the model cannot drift into two inconsistent views of the same prerequisite relationship.

enum Day
{
    monday,
    tuesday,
    wednesday,
    thursday,
    friday,
    saturday,
    sunday
}

value TimeSlot
{
    Day day;
    Integer startMinute;
    Integer endMinute;
}

func Boolean overlaps(TimeSlot a, TimeSlot b) =
    a.day = b.day
    ∧ a.startMinute < b.endMinute
    ∧ b.startMinute < a.endMinute;

entity Course
{
    String code;
    Boolean advanced;
    TimeSlot timeslot;

    Course prerequisite*;

    // Navigation back to enrolments is derived from Enrolment.course.
    Enrolment enrolment* where enrolment.course = this;

    key { code };
}

entity Student
{
    String name;
    Course completed*;

    // Navigation to enrolments is derived from Enrolment.student.
    Enrolment enrolment* where enrolment.student = this;

    // A student's current courses come from the enrolment records.
    → Course enrolled* = enrolment.course;

    key { name };

    constraints
    {
        // A course cannot be both completed and currently enrolled.
        [completed = enrolled].Σempty;

        // If an enrolled course is advanced, all its prerequisites
        // must already be completed by this student.
        let s=this in
            enrolled.(advanced → prerequisite.Σ ⊆ s.completed.Σ);

        // No two currently enrolled courses may overlap in time.
        let s=this in
            enrolled.(let c=this in
                s.enrolled.[this ≠ c].(¬overlaps(timeslot, c.timeslot)).Σall);

        // Do not enrol in a prerequisite after completing a course
        // that already depends on it.
        let s=this in
            enrolled.(let c=this in
                s.completed.[c ∈ prerequisite.Σ].Σempty);
    }
}

entity Enrolment
{
    Student student;
    Course course;
}

entity University
{
    Student student*;
    Course course*;
}

Reading the constraints

The first constraint uses an intensional filter as a relation. It says there is no course value that is both in completed and in enrolled.

[completed = enrolled].Σempty

The second constraint keeps the current student in s before entering enrolled.(...). Inside that path tail, this is the enrolled course, so prerequisite.Σ is the set of prerequisites of that course, while s.completed.Σ is the set of courses completed by the original student.

let s=this in
    enrolled.(advanced → prerequisite.Σ ⊆ s.completed.Σ)

The third constraint compares each enrolled course c with the other enrolled courses for the same student. The filter .[this ≠ c] removes the course from its own comparison set.

let s=this in
    enrolled.(let c=this in
        s.enrolled.[this ≠ c].(¬overlaps(timeslot, c.timeslot)).Σall)

The final constraint checks the opposite direction of the prerequisite relationship without storing a separate dependent attribute. For each currently enrolled course c, it rejects any completed course whose prerequisite set contains c.

let s=this in
    enrolled.(let c=this in
        s.completed.[c ∈ prerequisite.Σ].Σempty)

The student constraints above translate to the following logic:

// A course cannot be both completed and currently enrolled.
∀C:Course
    this.completed(C) → ¬this.enrolled(C)

// Advanced enrolled courses require completed prerequisites.
∀A:Boolean ∀E:Course ∀P:Course
    (this.enrolled(E) ∧ E.advanced(A) ∧ A ∧ E.prerequisite(P))
  → this.completed(P)

// Currently enrolled courses must not overlap.
∀T:TimeSlot ∀T1:TimeSlot ∀E1:Course ∀E:Course
    (this.enrolled(E1)
     ∧ this.enrolled(E)
     ∧ E1 ≠ E
     ∧ E1.timeslot(T)
     ∧ E.timeslot(T1))
  → ¬overlaps(T, T1)

// Do not enrol in a prerequisite after completing a dependent course.
∀C:Course ∀E:Course
    (this.completed(C) ∧ this.enrolled(E))
  → ¬(E ∈ { P:Course | C.prerequisite(P) })

Common wrong turns

The following examples are deliberately concrete. Each one shows a tempting expression, what it actually denotes, and the form that matches the intended constraint.

1. Comparing scalar paths as if they were sets

A common first attempt is to write the prerequisite rule without folds:

enrolled.(advanced → prerequisite ⊆ completed)

This has no logic denotation, because it is not well typed. Inside enrolled.(...), both prerequisite and completed denote individual Course values in the current path context. The operator ⊆ expects sets, so the type checker rejects the expression:

ERROR: No overload of ⊆ matches operand types ['Course', 'Course']

The correct expression explicitly folds both sides to sets. It also saves the original student in s, because inside enrolled.(...) the receiver this is the enrolled course.

let s=this in
    enrolled.(advanced → prerequisite.Σ ⊆ s.completed.Σ)

∀A:Boolean ∀E:Course ∀P:Course
    (this.enrolled(E) ∧ E.advanced(A) ∧ A ∧ E.prerequisite(P))
  → this.completed(P)

Principle: use .Σ when the constraint is about a set of values. Use let before a path composition when the inner expression still needs the outer receiver.

2. Forgetting that this changes inside a path tail

This schedule rule looks plausible, but it accidentally compares each enrolled course only with itself:

enrolled.(let c=this in
    enrolled.[this ≠ c].(¬overlaps(timeslot, c.timeslot)).Σall)

Its denotation exposes the problem. The antecedent contains E ≠ E, which is impossible:

∀T:TimeSlot ∀T1:TimeSlot ∀E:Course
    (this.enrolled(E) ∧ E ≠ E ∧ E.timeslot(T) ∧ E.timeslot(T1))
  → ¬overlaps(T, T1)

The issue is that the unqualified inner enrolled is evaluated relative to the current enrolled course, not relative to the student. Save the student first, then navigate back through s.enrolled.

let s=this in
    enrolled.(let c=this in
        s.enrolled.[this ≠ c].(¬overlaps(timeslot, c.timeslot)).Σall)

∀T:TimeSlot ∀T1:TimeSlot ∀E1:Course ∀E:Course
    (this.enrolled(E1)
     ∧ this.enrolled(E)
     ∧ E1 ≠ E
     ∧ E1.timeslot(T)
     ∧ E.timeslot(T1))
  → ¬overlaps(T, T1)

Principle: after x.(...), unqualified paths in the parentheses are evaluated from each value of x. Use let outer=this in ... when a nested path still needs the outer object.

3. Using value inequality when the domain has a richer predicate

If TimeSlot is an interval, this rule is too weak:

let s=this in
    enrolled.(let c=this in
        s.enrolled.[this ≠ c].timeslot ≠ c.timeslot)

It only says the two enrolled courses cannot have exactly equal TimeSlot values:

∀T:TimeSlot ∀T1:TimeSlot ∀E1:Course ∀E:Course
    (this.enrolled(E1)
     ∧ this.enrolled(E)
     ∧ E1 ≠ E
     ∧ E1.timeslot(T)
     ∧ E.timeslot(T1))
  → T ≠ T1

For interval times, equality is not the important domain concept. Use the domain predicate:

let s=this in
    enrolled.(let c=this in
        s.enrolled.[this ≠ c].(¬overlaps(timeslot, c.timeslot)).Σall)

∀T:TimeSlot ∀T1:TimeSlot ∀E1:Course ∀E:Course
    (this.enrolled(E1)
     ∧ this.enrolled(E)
     ∧ E1 ≠ E
     ∧ E1.timeslot(T)
     ∧ E.timeslot(T1))
  → ¬overlaps(T, T1)

Principle: write constraints in the vocabulary of the domain. If the domain concept is overlap, encode overlap directly instead of relying on value inequality.

4. Misusing universal navigation for a universal condition

This example refers to a variant of the model that stores a reverse navigation Course dependent*. The tempting expression is:

course.(dependent ⇒ advanced)

It does not mean "all dependent courses are advanced". Universal navigation returns values that all dependents agree on. Used as a Boolean constraint, it says that if every dependent agrees on some advanced value A, then A must be true:

∀A:Boolean ∀C:Course
    (this.course(C) ∧ (∀D:Course (C.dependent(D) → D.advanced(A))))
  → A

The direct constraint is to look for counterexamples: dependent courses that are not advanced. Then require that set to be empty.

course.dependent.[¬advanced].Σempty

∀D:Course ∀C:Course ∀A:Boolean
    (this.course(C) ∧ C.dependent(D) ∧ D.advanced(A))
  → A

Principle: to say "all X satisfy P", filter X by the negation of P and require .Σempty. This is often clearer than reaching for ⇒.

5. Traversing the relationship in the wrong direction

Again suppose the model stores dependent. This expression is easy to write backwards:

student.completed.dependent ≠ course

Its denotation says that the enrolment course must not be a dependent of any completed course:

∀D:Course ∀C1:Course ∀C:Course ∀S:Student
    (this.student(S) ∧ S.completed(C) ∧ C.dependent(D) ∧ this.course(C1))
  → D ≠ C1

That is the reverse of "do not enrol in a prerequisite after completing a course that depends on it". With a stored dependent navigation, the direction should be:

course.dependent ≠ student.completed

∀D:Course ∀C1:Course ∀C:Course ∀S:Student
    (this.course(C) ∧ C.dependent(D) ∧ this.student(S) ∧ S.completed(C1))
  → D ≠ C1

The revised model avoids storing dependent at all. It asks whether the currently enrolled course c appears in the prerequisite set of any completed course:

let s=this in
    enrolled.(let c=this in
        s.completed.[c ∈ prerequisite.Σ].Σempty)

∀C:Course ∀E:Course
    (this.completed(C) ∧ this.enrolled(E))
  → ¬(E ∈ { P:Course | C.prerequisite(P) })

Principle: read a path left to right and name the relationship direction. If the prose says "completed courses that depend on the enrolled course", either navigate from the enrolled course to its dependents, or test whether the enrolled course appears in a completed course's prerequisite set.

Constraint-writing principles

• Decide which entity should own the constraint. If a rule is naturally about one student's courses, put it on Student.
• Keep one source of truth for each relationship. Prefer deriving reverse navigation instead of storing both directions independently.
• Use .Σ when comparing sets of path values; otherwise a path usually denotes individual values.
• Use let to preserve an outer receiver before entering a path composition that changes this.
• For universal requirements, look for bad cases and require .Σempty.
• Use domain predicates such as overlaps when equality or inequality does not capture the real business rule.

44 Using Predica to define legality

Predica can support traditional database applications, but its scope is broader. Its logical foundation provides a principled basis for expressing legality in laws, contracts, and other normative systems where clarity and unambiguous semantics are essential.

The preceding chapters developed the ordinary constraint reading first. The constraint forms and the examples on firearm purchases, construction projects, cardinality constraints and student enrolment can all be read as database invariants. They can also be read normatively, as conditions that a situation must satisfy in order to be compliant.

Predica supports two semantic modes:

• Descriptive (model‑theoretic): constraints classify models.
• Normative (contract‑theoretic): constraints classify worlds.

In the normative mode, constraints are not merely descriptions of admissible models. Instead, they are interpreted as contractual conditions that classify possible worlds. A world that satisfies all constraints is compliant; a world that fails any constraint is in violation.

Predica uses a global normative interpretation. A legal specification is written as a collection of ordinary descriptive constraints, and the normative force is applied to the specification as a whole: the relevant world ought to satisfy the conjunction of its active constraints.

This avoids requiring every clause to carry its own normative language. Drafting each condition with words such as “shall”, “must”, “may”, “must not”, “is prohibited”, or “is required” is cumbersome, and small differences in wording can introduce ambiguity or accidental differences in legal effect. Predica instead lets the author state the condition directly using ordinary logical structure.

This makes the formal part of legal drafting more accessible to people trained in ordinary logic, mathematics, engineering, science, and software, without requiring them to work directly in deontic or modal logic. Normativity is supplied by the legal interpretation of the specification, not by special operators inside each constraint.

Why no modal operators are needed

Predica does not require an explicit modal operator to express legality. In the normative (contract‑theoretic) mode, the shift from describing models to classifying worlds is achieved entirely by changing the interpretation of constraints, not by extending the language.

A constraint has the same logical form in both modes. What changes is what the formula is about:

• In descriptive mode, it states a property that admissible models must satisfy.
• In normative mode, it states a property that admissible worlds must satisfy.

Predica’s normative semantics is not modal in either syntax or semantics. It introduces no accessibility relation, modal frame, or deontic operators.

Because the syntax already expresses a precise condition, no additional modal operator is needed to say “this must hold in the world.” The normative force comes from the semantic stance: the constraint is taken as a requirement on reality rather than a filter on models. Predica’s existing logical constructs are sufficient; only the target of evaluation changes.

45 Types

Up to now we have used the word ‘type’ informally to refer to the kinds of values introduced by nominal type declarations. We now give the semantic definition of a type and explain how types relate.

A type is a semantic classification of values. Each type has a carrier set: the set of values classified by that type. Predica types are introduced or described in the following ways:

• It is a predefined type.
• It is a structural type.
• It is a nominal type introduced by a nominal type declaration.
• It is a type expression formed from existing types, such as Set<T>, a subtype T where p refinement, a union, or an intersection.
• It is the intersection of two or more comparable types, where comparability ensures a unique least common supertype with defined equality

Any type may have multiple names.

In the semantic model, type equality is equality of carrier sets. Consequently, two types are equal exactly when they have the same carrier set.

A type expression denotes a type, and therefore determines a carrier set drawn from a fixed background universe of sets. Type expressions provide the syntax for referring to types.

Some declarations, such as value and entity, introduce new nominal type identity. Other declarations, such as type aliases, bind a name to a type expression without creating a new carrier set. A subtype T where p type expression denotes a subset of an existing type.

Type test expressions

The expression L isa T tests the relationship of its left operand L to the type denoted by its right operand T. Its result type is Boolean. The left operand may be either a value expression or a type expression.

When L is a value expression, L isa T tests whether the value denoted by L is a member of T. The test is about the value of L, not the syntactic form of the expression that produced it. When L is a type expression, L isa T tests whether the type denoted by L is a subtype of T.

abstract entity Animal {}

entity Dog isa Animal
{
    String bark;
}

entity Owner
{
    Animal pet;

    → Boolean petIsDog = pet isa Dog;
    → String sound? = if pet isa Dog then pet.bark else none;
}

For a value left operand, a type test is invalid when the static type known for the value is necessarily disjoint from T, because such a test cannot be satisfied. For a type left operand, the test is false when the left type is not a subtype of T.

A positive type test narrows the static type known for the tested expression in the guarded scope. For example, in if pet isa Dog then pet.bark else none, the then-branch may use members of Dog through pet. In pet isa Dog ∧ pet.bark = "woof", the right-hand side of the conjunction is checked with the same positive narrowing. The test does not introduce a general negative narrowing rule for else-branches or disjunctions.

Int8
Int16
Int32
Int64
Uint8
Uint16
Uint32
Uint64

{ Real x; Real y; }
{ Point centre; Real radius; }
{ Supplier supplier*; Part part*; Shipment shipment*; }

S = ((A1, T1, C1), ..., (An, Tn, Cn))

carrier(S) =
{
    ((A1, E1), ..., (An, En))
    |
    Ei ⊆ carrier(Ti)
    ∧ Ci(|Ei|)
    for each i ∈ {1, ..., n}
}

{
    Integer a;
    Real b*;
}

{
    ((a, A), (b, B))
    |
    A ⊆ Integer
    ∧ |A| = 1
    ∧ B ⊆ Real
}

((a, {3}), (b, ∅))
((a, {4}), (b, ∅))

type Point2D = { Real x; Real y; };
type AlsoPoint2D = { Real x; Real y; };
type SwappedPoint2D = { Real y; Real x; };

variant Option<T>
{
    T some;
    {} absent;
}

{
    {
        Integer id;
        String name;
        Integer status;
        String city;
    } supplier*;
    {
        Integer id;
        String name;
        Color color;
        Real weight;
        String city;
    } part*;
    {
        Integer supplier_id;
        Integer part_id;
        Integer qty;
    } shipment*
}

{ Real x; Real y; } point = { x = 1, y = 3 };

type PositiveRealSet = Set<(subtype Real where this > 0)>;
type VisibleRenderableShape = subtype (intersection { Shape, Renderable }) where visible;
type Contact = subtype (union { EmailContact, PhoneContact }) where verified;

value Point 
{
    Real x;
    Real y;
}

type Name = TypeExpression;

type Length = Real;
type Mass = Real;
type PointTuple = { Real x; Real y; };
type CircleTuple = { PointTuple centre; Real radius; };
type Names = Set<String>;
type PositiveReal = subtype Real where this > 0;
type ContactMethod = union { EmailContact, PhoneContact };
type ShapeTexture = intersection { Shape, Texture };

value B { Integer x; };
value C { Integer x; };

var b = B { x = 1 };
var c = C { x = 1 };

print b = c;        // type error unless equality between B and C is defined

value B { Integer x; };
value C { Integer x; };

func Boolean =(B b, C c) = b.x = c.x;

type Contact = union { EmailContact, PhoneContact, PostalContact };

disjoint EmailContact, PhoneContact, PostalContact;
type Contact = union { EmailContact, PhoneContact, PostalContact };

Boolean b = true;
Int32 n = 1;
Float32 x = 1.5;
String s = "London";

Set<Integer> numbers = ∅;
names ∩ ∅;
"London" ∈ ∅;

{1, 2, 3}
{1, 2.5}
{Color.red, Color.green}

1..4        // {1, 2, 3, 4}
3 ∈ 1..4    // true

{ Real x; Real y; } point = { x = 1, y = 3 };

value Point
{
    Real x;
    Real y;
}

Point { x = 1, y = 3 }
Box<Integer> { value = 1 }

var Point point;
point.x := 1;
point.y := 3;

Point(1, 3)
Box<Integer>(1)

// Introduces a statically typed variable named x. Its static type is Integer.
var x = 10;

// Gives an empty multi-valued variable an explicit element type.
var Integer id* = {};

// Static type check failure: String is not assignable to Integer.
x := "hello";

value List
{
    Integer head;
    List tail?;
}

func Boolean memberOf(List list, Integer value)
{
    if list.head = value {
        return true;
    }

    if list.tail = none {
        return false;
    }

    return list.tail.memberOf(value);
}

@dynamic = true;

// First assignment introduces a dynamic variable named y.
y := 10;

// y can be freely reassigned a value of any type.
y := "hello";

@dynamic = false;

// Static error: dynamic variables are disabled.
y := 10;

value A
{
    T v?;
}

variant B
{
    T v;
    Boolean unknown;
}

A a ← B b
{
    a.v = if b.unknown then none else b.v;
}

B b ← A a
{
    b = if a.v = none then unknown(true) else v(a.v);
}

namespace A
{
    @domain("employee with known name")
    entity R1 
    {
        Integer id;
        String name;
        key {id};
    }

    @domain("employee with known address")
    entity R2 
    {
        Integer id;
        String address;
        key {id};
    }

    entity System
    {
        R1 r1*;
        R2 r2*;
        → all* = r1 ∪ r2;
    }
}

namespace B
{
    @domain("employee with known name and unknown address")
    entity S1 
    {
        Integer id;
        String name;
        key {id};
    }

    @domain("employee with known address and unknown name")
    entity S2 
    {
        Integer id;
        String address;
        key {id};
    }

    @domain("employee with known name and known address")
    entity S3 
    {
        Integer id;
        String name;
        String address;
        key {id};
    }

    entity System
    {
        S1 s1*;
        S2 s2*;
        S3 s3*;
        → all* = s1 ∪ s2 ∪ s3;
        constraints
        {
            disjoint { s1, s2, s3 };
        }
        theorems
        {
            // Employees with both name and address known
            s3 = (s1 ∪ s3) ∩ (s2 ∪ s3);

            // These follow from the disjointness axiom
            s1 ∩ s2 = ∅;
            s1 ∩ s3 = ∅;
            s2 ∩ s3 = ∅;
        }
    }
}

isomorphism employeeInfoRefinement
{
    // {R1, R2} → {S1, S2, S3}
    a:A.System → B.System   
    {
        s3 = a.r1 ⨝ a.r2;
        s1 = a.r1 ∖ s3.{id, name};
        s2 = a.r2 ∖ s3.{id, address};
    }

    // {S1, S2, S3} → {R1, R2}
    b:B.System → A.System
    {
        r1 = b.s1 ∪ b.s3.{id, name};
        r2 = b.s2 ∪ b.s3.{id, address};
    }
}

entity System
{
    S1 s1*;
    S2 s2*;
    S3 s3*;
    → all* = s1 ∪ s2 ∪ s3;
}

value Point
{
    // cartesian representation
    Real x;
    Real y;

    // polar representation
    Real r where r ≥ 0;
    Real θ where 0 ≤ θ < 2*pi;

    constraints
    {
        r=0 → θ=0;
    }

    isomorphism {x,y} ↔ {r,θ}
    {
        r = sqrt(x^2 + y^2);
        θ = atan2(y,x);
        x = r * cos θ;
        y = r * sin θ;
    }
}

object T

// Encoding of an image using JPEG format
type JpegBytes = Vector<Byte>;

value RGB
{
    Uint8 r;
    Uint8 g;
    Uint8 b;
}

value Image<Type T>
{
    Vector<T> values;
    Int32 width;
    Int32 height;
}

value Point<Type T>
{
    T x;
    T y;
}

func Point<T> componentWiseProduct<Type T>(Point<T> a, Point<T> b) =
    Point<T> { x = a.x * b.x, y = a.y * b.y };

// Pure function that decodes JPEG into an RGB image in memory
extern "C++:predica"
{
    Image<RGB> decodeJpeg(JpegBytes jpeg);
}

// Single image with synchronous decoding
value Jpeg
{
    JpegBytes bytes;
    → Image<RGB> image = decodeJpeg(bytes);
}

value TiledImage
{
    const Point<Int32> numTiles;
    const Point<Int32> tilePixelSize;

    constraints
    {
        isPowerOfTwo(numTiles.x);
        isPowerOfTwo(numTiles.y);
    }

    → Int64 countTiles =
        Int64(numTiles.x) * Int64(numTiles.y);

    → imageSize =
        componentWiseProduct(numTiles, tilePixelSize);

    MortonArray<object Jpeg?, numTiles.x, numTiles.y> tiles;
}

MortonArray<object Jpeg?, numTiles.x, numTiles.y> tiles;

tileOid(x,y) = tilesBaseOid + morton2D(x,y)

morton2D(x,y) =
    Σᵢ ((((x >> i) & 1) << (2i))
      + (((y >> i) & 1) << (2i + 1)))

tiles[x,y]          // Jpeg, cardinality 0..1
tiles[x,y].image    // Image<RGB>, cardinality 0..1

tiles[x,y]

s.supplier.[city = "London"].shipment.part.[color = Color.red]

value Point
{
    Real x;
    Real y;
}

value Circle
{
    Point centre;
    Real radius where radius ≥ 0;
}

value Circle
{
    Point centre;
    Real radius where radius ≥ 0;
}

{
    Point centre;
    Real radius;
}

carrier(V) ≅ { v ∈ carrier(S) | K(v) }

entity Supplier
{
    Integer id;
    String name;
    Integer status;
    String city;
    key {id};
}

entity Part
{
    Integer id;
    String name;
    Color color;
    Real weight;
    String city;
    key {id};
}

entity Shipment
{
    Supplier supplier;
    Part part;
    Integer qty;
    key {supplier,part};
}

entity ShipmentsSystem
{
    Supplier supplier*;
    Part part*;
    Shipment shipment*;
    constraints 
    {
        shipment.supplier.Σ ⊆ supplier.Σ;
        shipment.part.Σ ⊆ part.Σ;
    }
}

entity Supplier
{
    Integer id;
    String name;
    Integer status where status ≥ 0;

    key {id};
}

{
    Integer id;
    String name;
    Integer status;
}

carrier(E) ≅ { v ∈ carrier(S) | K(v) }

entity Supplier
{
    Integer id;
    key {id};
}

entity ShipmentsSystem
{
    Supplier supplier*;
}

key {name, date};       // valid
key {missing};          // Error: unknown attribute
key {name, name};       // Error: repeated attribute

key {customer.id};          // Error: paths are not permitted
key {normalize(email)};     // Error: expressions are not permitted

→ String normalizedEmail = normalize(email);
key {normalizedEmail};      // valid

abstract value AbstractValue
{
    String description;
}

entity Observation
{
    AbstractValue subject;

    key {subject};  // valid: equality is defined on AbstractValue
}

entity Person
{
    String name;
    String email+;

    key {name, email};
}

∀a ∈ K, a(x) = a(y)

a(x) = a(y)  iff  ∀v:T (v ∈ a(x) ↔ v ∈ a(y))

entity Person
{
    String givenName;
    String familyName;
    → String normalizedName = normalizeName(givenName, familyName);

    key {normalizedName};
}

abstract entity Identified
{
    String identifier;

    key {identifier};
}

entity Customer isa Identified
{
    String identifier;
    String name;
}

entity Catalogue
{
    Integer id;
    Identified item*;

    key {id};
}

entity Book
{
    Integer id;
    Person author;
    String title;
    String description;

    key {id};
    key {author, title};
}

entity Ownership
{
    Person owner;
    Vehicle vehicle;
}

enum PrimaryColor
{
    red,
    green,
    blue
}

enum HttpStatus
{
    ok = 200,
    notFound = 404,
    unavailable = 503
}

enum Offset<Integer N>
{
    first = N,
    second,
    last = N + 10
}

carrier(PrimaryColor) = { red, green, blue }

variant PrimaryColor
{
    {} red;
    {} green;
    {} blue;
}

enum Color
{
    red,
    green,
    blue,
    magenta,
    cyan,
    yellow
}

enum PrimaryColor isa Color
{
    red,
    green,
    blue
}

enum HttpStatus : Uint16
{
    ok = 200,
    notFound = 404,
    unavailable = 503
}

variant Shape
{
    Circle circle;
    Triangle triangle;
    Rectangle rectangle;
}

variant Shape
{
    @predicate("The shape is a circle value equal to [circle]")
    Circle circle;

    @predicate("The shape is a triangle value equal to [triangle]")
    Triangle triangle;

    @predicate("The shape is a rectangle value equal to [rectangle]")
    Rectangle rectangle;
}

variant Shape
{
    { Real radius; } sphere;
    { Real side; } cube;
    { Real radius; Real height; } cone;

    → Real volume = sphere.(4.0/3.0*pi*radius^3)
                  | cube.(side^3)
                  | cone.(pi*radius^2*height/3);
}

variant Shape
{
    Circle circle;
    Rectangle rectangle;
}

carrier(Shape) =
    ({circle} × carrier(Circle))
    ∪ ({rectangle} × carrier(Rectangle))

W = variant { T1 A1; ...; Tn An; }

carrier(W) =
    ⋃i=1n ({Ai} × carrier(Ti))

abstract value Solid
{
    { Real radius; } sphere?;
    { Real side; } cube?;

    constraints
    {
        // ∀S:{ Real radius; } ∀R:Real
        //     (this.sphere(S) ∧ S.radius(R)) → R > 0
        sphere.(radius > 0);

        // ∀C:{ Real side; } ∀L:Real
        //     (this.cube(C) ∧ C.side(L)) → L > 0
        cube.(side > 0);
    }
}

variant BasicSolid isa Solid
{
    { Float64 radius; } sphere where sphere.radius > 1;
    { Float64 side; } cube;
}

variant PaymentResult
{
    completed;
    cancelled;
    String declined;
    { String provider; String reference; } pending;
}

variant PaymentResult
{
    {} completed;
    {} cancelled;
    String declined;
    { String provider; String reference; } pending;
}

variant Shape
{
    Circle circle;
    Point point+;
}

variant Shape
{
    Circle circle;
    PointSet pointSet;
}

@domain("A finite binary tree with integers at a subset of the leaf nodes")
variant BinaryTree
{
    @predicate("The binary tree is an empty node")
    {} empty;

    @predicate("The binary tree is a leaf node holding the integer value [leaf]")
    Integer leaf;

    @predicate("The binary tree is a binary node equal to [node]")
    { BinaryTree left; BinaryTree right; } node;
}

quotient Rational
{
    // Base attributes for the representation
    Integer numerator;
    Integer denominator where denominator > 0;

    // Derived attribute
    → Boolean zero = numerator = 0;

    equivalence
    {
        x ~ y where x.numerator * y.denominator = y.numerator * x.denominator;
    }
}

Rep(T) = { r ∈ carrier(S) | K(r) }

carrier(T) = Rep(T) / ~T

func B f(A x);

x ~ y ⇒ f(x) = f(y)

func Boolean ≤(Rational x, Rational y) =
    x.numerator * y.denominator ≤ y.numerator * x.denominator;

equivalence
{
    x ~ y where x.numerator * y.denominator = y.numerator * x.denominator;

    canonical x:
        gcd(abs(x.numerator), x.denominator) = 1;
}

entity Supplier
{
    Integer id;

    @predicate("The supplier is located in [city]")
    City city*;
}

value S
{
    T a;
    T b?;
    T c*;
    T d+;
    T e[2];
    T f[4..10];
}

entity Document
{
    const Integer id;
    String title;
}

var document1 = Document { id = 1, title = "First" };
var document2 = Document { id = 2, title = "Second" };

entity Document
{
    // Error: cannot give const attribute a value in its declaration
    const Integer id = 1;
}

value Image<Type T>
{
    const Uint32 width;
    const Uint32 height;

    Array<T, width, height> pixels;
}

value ScalarField
{
    Real val(Real x, Real y);
}

entity Supplier
{
    City city(Country country)*;
}

enum Material
{
    wood,
    plastic,
    metal
}

entity Object
{
    Real mass(Material material);
}

value TemperatureGrid
{
    Real celsius(Integer x, Integer y);

    → Real fahrenheit(Integer x, Integer y) =
        celsius(x, y) * 1.8 + 32;
}

s.supplier.(name, city)    // tuple construction
a.f(x, y)                  // parameterised attribute application

// Objects whose mass of wood is greater than 10.
object.[mass(Material.wood) > 10]

// Objects having more than 10 units of some material.
object.[∃ material:Material (mass(material) > 10)]

object.mass(Material.wood) := 12;

value SampledImage<Type T>
{
    T val(Integer x, Integer y);
}

value ConstImage
{
    Real sample;
}

embed ConstImage image isa SampledImage<Real> =
    SampledImage<Real> {
        val(x, y) = image.sample
    };

value Circle
{
    Real radius where radius ≥ 0;
    → Real diameter = 2 * radius;
}

entity Person
{
    String email*;
    → Boolean hasEmail = email.Σexists;
}

enum TrafficLight
{
    red,
    amber,
    green,

    → Boolean stop = red ∨ amber;
}

variant Payment
{
    Cash cash;
    Card card;

    → Boolean electronic = card.Σexists;
}

quotient Rational
{
    Integer numerator;
    Integer denominator where denominator > 0;

    → Boolean zero = numerator = 0;

    equivalence
    {
        x ~ y where x.numerator * y.denominator = y.numerator * x.denominator;
    }
}

value Point
{
    Real x;
    Real y;
}

value Circle
{
    Point centre;
    Real radius;
    → Real area = 3.14159 * radius * radius;
}

entity Wheel
{
    embed Circle;
    Real mass;
}

entity Wheel
{
    embed Circle as circle;
    Real mass;
}

value RationalRepresentation
{
    Integer numerator;
    Integer denominator;
}

quotient Rational
{
    embed RationalRepresentation;

    equivalence
    {
        x ~ y where
            x.numerator * y.denominator = y.numerator * x.denominator;
    }

    constraints
    {
        denominator > 0;
    }
}

enum Gender
{
    male,
    female
}

entity Person
{
    String name;
    embed Gender;
}

value Point<Type T, Integer N>
{
    T coordinate[N];
}

value Holder
{
    Point<Real, 3> position;
}

value Vector<@role("coordinate") Type T = Float64,
             @count Integer N = 3>
    where T isa Real, N ∈ 1..4
{
    T coordinate[N];
}

value Array2d<Type T, Integer N, Integer M>
    where T isa Real, N > 0, M > 1, N + M < 10, isOdd(N)
{
}

enum Axis
{
    x,
    y,
    z
}

value AxisTag<Axis A>
{
    Integer id;
}

Point<Real, 3>
Vector<Integer>
Vector<Float64, 2+1>
AxisTag<Axis.x>
AxisTag<x>

value Box<Type T>
{
    T value;
}

variant Maybe<Type T>
{
    T some;
    absent;
}

entity Node<Type T>
{
    Integer id;
    T value;

    key { id };
}

enum Offset<Integer N>
{
    first = N,
    second,
    last = N + 10
}

const plus<Integer N = 2> = N + 1;

func T identity<Type T>(T value) = value;

extern "C++:math"
{
    T clamp<Type T, Integer N = 3>(T value)
        where T isa Real, N ∈ 1..4;
}

identity<Integer>(1)
plus<2+1>

using acme.Library { Box, identity };
using acme.Library as lib;

value Holder
{
    Box<Integer> localName;
    lib.Box<Real> qualifiedName;
    Integer copied = identity<Integer>(1);
}

enum Month
{
    jan, feb, mar, apr, may, jun, jul, aug, sep, oct, nov, dec
}

value Time
{
    Integer hour where hour ∈ [0..23];
    Integer minute where minute ∈ [0..59];
    Integer second where second ∈ [0..59];
}

value unordered DebugTime
{
    Integer hour where hour ∈ [0..23];
    Integer minute where minute ∈ [0..59];
    Integer second where second ∈ [0..59];
}

value Date
{
    Integer year;
    Month month;
    Integer day;

    order [year↓, month, day];
}

value Point
{
    Real x;
    Real y;

    order [x*x + y*y, x, y];
}

enum Color
{
    red,
    green,
    blue
}

// Explicit order: blue < green < red.
func Boolean ≤(Color x, Color y) =
    if x = y then
        true
    else if x = blue then
        true
    else if y = blue then
        false
    else if x = green then
        true
    else
        false;

quotient Rational
{
    Integer numerator;
    Integer denominator where denominator > 0;

    equivalence
    {
        x ~ y where x.numerator * y.denominator = y.numerator * x.denominator;
    }
}

embed Rational r isa Real =
    r.numerator / r.denominator;

func Boolean ≤(Rational x, Rational y) =
    x.numerator * y.denominator ≤ y.numerator * x.denominator;

value Point
{
    Real x where x > 0;
    Real y;

    constraints
    {
        x < y;
    }
}

value Point
{
    Real x;
    Real y;

    constraints
    {
        x > 0;
        x < y;
    }
}

Real percentage where percentage ≥ 0, percentage ≤ 100;

value Rectangle
{
    Real width where width ≥ 0;
    Real height where height ≥ 0;
    → Real area = width * height;

    constraints
    {
        area ≤ 100;
    }
}

carrier(S with K) =
{
    v ∈ carrier(S)
    |
    K(v)
}

value P
{
    Real x*;
    Real y*;

    constraints
    {
        x < y;
    }
}

((x, X), (y, Y))

∀x ∈ X. ∀y ∈ Y. x < y

value Point
{
    Real x;
    Real y;

    constraints
    {
        x < y;
    }
}

value Q
{
    Point p*;
}

entity Assignment
{
    Person supplier*;
    Person customer*;

    constraints
    {
        disjoint { supplier, customer };
    }
}

supplier ∩ customer = ∅;

disjoint { supplier, customer, reviewer };

supplier ∩ customer = ∅;
supplier ∩ reviewer = ∅;
customer ∩ reviewer = ∅;

entity ShipmentsSystem
{
    Supplier supplier*;
    Part part*;
    Shipment shipment*;
    constraints 
    {
        shipment.supplier.Σ ⊆ supplier.Σ;
        shipment.part.Σ ⊆ part.Σ;
    }
}

value Account
{
    Real balance where balance ≥ 0;
    Real reserved where reserved ≥ 0;
    → Real available = balance - reserved;

    constraints
    {
        reserved ≤ balance;
    }

    theorems
    {
        available ≥ 0;
    }
}

enum TrafficLight
{
    red,
    amber,
    green,

    → Boolean stop = this = red;
    → Boolean proceed = this = amber ∨ this = green;

    theorems
    {
        stop ≠ proceed;
    }
}

value Rectangle
{
    Real width where width ≥ 0;
    Real height where height ≥ 0;
    → Real area = width * height;

    theorems
    {
        area ≥ 0;
    }
}

// 1) Declare concrete type A to be a subtype of an abstract type B as A is declared
value A isa B { ... };

// 2) Declare existing concrete type A to be a subtype of an existing abstract type B
A isa B;

// 3) Embed existing type A in existing type B, so that A ⊆ B
embed A a isa B = expressionOfTypeB;

// 4) Create new subtype A as an intersection of existing comparable types B and C
type A = intersection { B, C };

// 5) Define a supertype A of existing types B and C
type A = union { B, C };

// 6) Name the subtype of B satisfying a predicate
type A = subtype B where p(this);

type A = subtype B where p(this);

type A1 = subtype B where p1(x);
type A2 = subtype B where p2(x);

value A {Integer x};

type B = subtype A where p1(x);
type C = subtype A where p2(x);

void foo(b*:B) 
{ 
    print b;
}

var B b* = { A { x = 1 }, A { x = 2 } };
var C c* = { A { x = 2 }, A { x = 3 } };

foo(b ∩ c);     // type error if static type of b ∩ c is A

value Rectangle
{ 
    Real width;
    Real height;
}

value Rhombus
{ 
    Real side;
    Real θ;
}

// Error: Rectangle and Rhombus are incomparable
type Square = intersection { Rectangle, Rhombus };

var a* = SomeRectangles();
var b* = SomeRhombuses();

// Error: need unique least common supertype of Rectangle and Rhombus with defined equality
var c* = a.Σ ∩ b.Σ;

value Code
{
    Integer number;
}

{ Code{ number={N} } | N ∈ ℤ }

value RealPoint { Real x; Real y; };

{ RealPoint{ x={X}, y={Y} } | X ∈ ℝ and Y ∈ ℝ }

@domain("A shape is a locus of points in Euclidean 2d space")
abstract value Shape
{
    @predicate("The area of the shape is [area]")
    Real area;

    → Real equivalentRadius = sqrt(area / pi);
}

var s = Shape { area = 10.0 };      // Error: cannot instantiate abstract type

abstract value RectangleShape
{
    Real width;
    Real height;
    → Real area = width * height;
}

value ConcreteRectangle isa RectangleShape
{
    Real width;
    Real height;
}

abstract value Quadrilateral isa Shape
{
}

value IncompleteRectangle isa Quadrilateral
{
    Float64 width;
    Float64 height;
}

Concrete type IncompleteRectangle does not implement
attribute area defined in supertype Shape.

abstract value NonnegativeMeasure
{
    Real magnitude;

    constraints
    {
        magnitude ≥ 0;
    }
}

value Length isa NonnegativeMeasure
{
    Real magnitude;
}

var invalid = Length { magnitude = -1 };  // Error: inherited constraint is violated

abstract entity Identified
{
    String identifier;

    key {identifier};
}

entity Customer isa Identified
{
    String identifier;
    String name;
}

value Point
{
    Float64 x;
    Float64 y;
}

value Circle isa Shape
{
    Point centre;
    Float64 radius;
    → Float64 area = pi * radius * radius;
}

abstract value Shape
{
    Real area;
    → Real equivalentRadius = sqrt(area / pi);
}

type NonnegativeReal = subtype Real where this ≥ 0;

value Disk isa Shape
{
    NonnegativeReal radius;
    → Real area = pi * radius * radius;
    → NonnegativeReal equivalentRadius = radius;
}

func String describe(Shape shape) = "shape";
func String describe(Circle circle) = "circle";

Circle circle = ...;
Shape shape = circle;

describe(circle)  // selects describe(Circle)
describe(shape)   // selects describe(Shape)

abstract value Path
{
    Point point*;
}

value NonemptyPath isa Path
{
    Point point+;
}

value Circle isa Shape
{
    Point centre;
    Real radius;
    → perimeter = 2 * pi * radius;
    → area = pi * radius * radius;
}

// Component A
value Polygon
{
    Point vertex*;
}

// Component B
abstract value Shape {};

// Component C, with dependencies on A and B
using A { Polygon };
using B { Shape };

Polygon isa Shape;

value Rectangle
{
    Real width;
    Real height;
    → perimeter = 2 * (width + height);
    → area = width * height;
}

// illegal: cannot use isa with a concrete supertype
value Square isa Rectangle
{
    → height = width;
}

type Square = subtype Rectangle where width = height;

type Square = subtype Rectangle where width = height ∧ area > 0;

type Square = subtype Rectangle where this.width = this.height;

type PositiveReal = subtype Real where this > 0;

value Square
{
    Real side;
}

embed Square s isa Rectangle =
    Rectangle { width = s.side; height = s.side };

embed Rational r isa Real =
    r.numerator / r.denominator;

value Polygon
{
    List<Point> vertex;
    → Real area = polygonArea(this);

    constraints
    {
        vertex.length ≥ 3;
    }
}

func Real polygonArea(Polygon polygon)
{
    var Integer count = polygon.vertex.length;
    var Real twiceSignedArea = 0;

    for Integer i in 0..count - 1 {
        var Integer next = if i + 1 = count then 0 else i + 1;
        var Point a = polygon.vertex[i];
        var Point b = polygon.vertex[next];

        twiceSignedArea += a.x * b.y - b.x * a.y;
    }

    return abs(twiceSignedArea) / 2;
}

value AxisAlignedRectangle
{
    Point origin;
    Float64 width;
    Float64 height;
    → List<Point> vertex = rectangleVertices(origin, width, height);
    → Float64 area = width * height;
}

embed AxisAlignedRectangle rectangle isa Polygon =
    Polygon { vertex = rectangle.vertex };

abstract value A {};
value B { Integer x; };
value C { Integer x; };
value D { Integer x; };
B,C isa A;
// D isa B,C;
B(D:d) { x = d.x; }
C(D:d) { x = d.x; }
var b = B { x=1 };
var c = C { x=1 };
print b = c;        // type error:  B and C are incomparable

value B { Integer x; };
value C { Integer x; };
disjoint B, C;
type A = union { B, C };
var b = B { x=1 };
var c = C { x=1 };
print b = c;        // prints false

value B { Integer x; };
value C { Integer x; };
disjoint B, C;
type A1 = union { B, C };
type A2 = union { B, C };
var b = B { x=1 };
var c = C { x=1 };
print b = c;        // prints false

type Contact = union { EmailContact, PhoneContact };
type VisibleContact = subtype (union { EmailContact, PhoneContact }) where visible;

type Contact = union { EmailContact, PhoneContact };
type ShapeTexture = intersection { Shape, Texture };

type A = union { B, C };

disjoint B, C;
type A = union { B, C };

value B { Integer x; };
value C { Integer x; };
value D { Integer x; };

B(D d) { x = d.x; }
C(D d) { x = d.x; }

disjoint B, C;        // Error: B and C have a common subtype.

type A1 = union { B, C };
type A2 = union { B, C };

type A1 = union { B, C };
type A2 = A1;

const pi = 3.141592653589793;
const Real one = 1;

const Integer next<Integer N> = N + 1;
const Set<T> emptySet<Type T> = ∅;

const Integer plus<Integer N = 2> = N + 1;

plus<3>
plus<>

func Boolean overlaps(TimeSlot a, TimeSlot b) =
    a.day = b.day
    ∧ a.startMinute < b.endMinute
    ∧ b.startMinute < a.endMinute;

func String appendGreeting(^String x)
{
    x += "hi";
    return x;
}

extern "C++:std"
{
    @domain("Sine")
    Float64 sin(Float64 x);

    Float64 atan2(Float64 y, Float64 x);
}

sin(angle)
Geometry.distance(a, b)
identity<Integer>(value)

func Boolean overlaps(TimeSlot a, TimeSlot b) =
    a.day = b.day
    ∧ a.startMinute < b.endMinute
    ∧ b.startMinute < a.endMinute;

overlaps(slot, other)
slot.overlaps(other)

value Square { Real side; }

value Rectangle
{
    Real width;
    Real height;
}

func Real area(Rectangle r) =
    r.width * r.height;

embed Square s isa Rectangle =
    Rectangle { width = s.side; height = s.side };

var square = Square { side = 5 };

area(square)
square.area()

value TimeSlot
{
    Boolean overlaps;
}

slot.overlaps
slot.overlaps(other)

value Rectangle
{
    Real width;
    Real height;
}

value Rhombus
{
    Real side;
    Real angle;
}

func Boolean =(Rectangle r, Rhombus h) =
    r.width = r.height ∧ r.width = h.side ∧ h.angle = 90;

func T identity<Type T>(T value) = value;

func Integer addN<Integer N = 2>(Integer value) = value + N;

extern "C++:math"
{
    T clamp<Type T, Integer N = 3>(T value)
        where T isa Real, N ∈ 1..4;
}

func String describe(Shape x) = "shape";
func String describe(Rectangle x) = "rectangle";

describe(rectangle)  // selects describe(Rectangle)

func Result combine(Rectangle a, Shape b) = ...;
func Result combine(Shape a, Rectangle b) = ...;

combine(r1, r2)  // ambiguous: each overload is narrower in one position

value List
{
    Integer head;
    List tail?;
}

var xs =
    List {
        head = 1,
        tail = List {
            head = 2,
            tail = List {
                head = 3,
                tail = none
            }
        }
    };

value List
{
    Integer head;
    List tail?;

    → Integer member* = head | tail.member;
}

func Boolean memberOf(List list, Integer value) =
    value ∈ list.member;

memberOf(xs, 2)
xs.memberOf(2)

func Boolean memberOf(List list, Integer value)
{
    if list.head = value {
        return true;
    }

    if list.tail = none {
        return false;
    }

    return list.tail.memberOf(value);
}

entity Supplier
{
    Integer id;
    String name;
    Integer status;
    String city;
    Shipment shipment* where shipment.supplier = this;
    key {id};
}

entity Part
{
    Integer id;
    String name;
    Color color;
    Real weight;
    String city;
    Shipment shipment* where shipment.part = this;
    key {id};
    //constraints { shipment.part ⊆ { this }; }
}

entity Shipment
{
    Supplier supplier;
    Part part;
    Integer qty;
    key {supplier,part};
}

entity ShipmentsSystem
{
    Supplier supplier*;
    Part part*;
    → Shipment shipment* = either supplier.shipment, part.shipment;
}

s.supplier

s.supplier.name

s.supplier.(name, city)

s.shipment.(
    supplier.name as supplier_name,
    part.name as part_name,
    qty)

s.supplier.[city = "London"]

s.supplier.[city = "London"].name

s.part.[weight > 15]

s.shipment.[part.color = Color.red]

s.supplier.shipment

s.supplier.(name, shipment.part.name as part_name)

s.supplier.[shipment.Σexists]

s.supplier.[shipment.Σempty]

s.supplier.(
    name,
    shipment.Σcount as shipment_count)

s.supplier.(
    name,
    shipment.qty.Σsum as total_qty)

s.part.[shipment.supplier.Σcount = 1]

var id1 = 0;
id1 := s.supplier.id;     // static cardinality constraint check failure

var Integer id2* = {};
id2 := s.supplier.id;     // ok

Shipment {
    supplier = ..supplier[id = 1],
    part = ..part[id = 2],
    qty = 200
}

s.supplier.[city = "London"].name

name=N:String
where ∃S:Supplier ∃C:String (
    s.supplier(S)
    ∧ S.city(C)
    ∧ C = "London"
    ∧ S.name(N)
)

path frame  --add filter condition-->  filtered path frame
filtered path frame  --observe under heading H-->  selected s-relation extension

entity Supplier
{
    Integer id;
    String name;
    Integer status;
    String city;
    key {id};
    → shipment* = inverse shipment.supplier;
}
  

entity Supplier
{
    Integer id;
    String name;
    Integer status;
    String city;
    key {id};
    → shipment* = inverse shipment.supplier;
}
entity Part
{
    Integer id;
    String name;
    Color color;
    Real weight;
    String city;
    key {id};
    → shipment* = inverse shipment.part;
}
entity Shipment
{
    Supplier supplier;
    Part part;
    Integer qty;
    key {supplier, part};
}
entity ShipmentsSystem
{
    Supplier supplier*;
    Part part*;
    Shipment shipment*;
    constraints
    {
        shipment.supplier.Σ ⊆ supplier.Σ;
        shipment.part.Σ ⊆ part.Σ;
    }
}
  

inverse p
  

supplier.shipment.part.color
  

namespace Internal
{
    entity Employee
    {
        Integer id;
        String name;
        String address;
        Money salary;
        key {id};
    }
    entity System
    {
        Employee employee*;
    }
}

namespace Public
{
    entity Employee
    {
        Integer id;
        String name;
        key {id};
    }
    entity System
    {
        Employee employee*;
    }
}

func Public.System directory(Internal.System i) =
    Public.System {
        employee = i.employee.(id, name)
    };

synchronous evaluation
    + demand-triggering access
    + asynchronously published information
    + later independent evaluations
    = responsive application

required inputs incomplete  → calculation is not runnable
last required input arrives → calculation becomes runnable
calculation runs            → result is published

MortonArray<object Jpeg?, numTiles.x, numTiles.y> tiles;

desired child tile available → render child tile
desired child tile pending   → render best available parent tile
desired child tile failed    → render failure indication or another fallback

displayₙ   = derive(snapshotₙ,   contextₙ)
displayₙ₊₁ = derive(snapshotₙ₊₁, contextₙ₊₁)

using vendor.Stats as stats;
using vendor.Stats { count as weightedCount };

items.Σcount          // std.count, even though vendor.Stats also declares count
items.Σstats.count    // vendor.Stats.count
items.ΣweightedCount  // vendor.Stats.count through an alias

using vendor.Stats { count, avg as mean };

using vendor.Stats as stats;
using vendor.Stats { count as statsCount, avg as statsMean };

items.Σcount       // std.count
items.Σmean        // std.mean
items.Σstats.count // vendor.Stats.count
items.Σstats.avg   // vendor.Stats.avg
items.ΣstatsCount  // vendor.Stats.count
items.ΣstatsMean   // vendor.Stats.avg

s.part.[shipment.supplier.Σcount = 1]

e.Σ{ z ; a v ↦ ⊕(a,v) }

e.Σ{ first v ↦ seed(v) ; a v ↦ ⊕(a,v) }

fold ResultType name<GenericParams> where constraints =
    Σ{ initial ; accumulator element ↦ step };

fold ResultType name<GenericParams>(ParameterType parameter, ...) where constraints =
    Σ{ initial ; accumulator element ↦ step };

E.Σname(argument, ...)
E.Σname<ExplicitGenericArgs>(argument, ...)

fold ResultType name<GenericParams>(params...) over input where constraints =
    expression;

fold Real shiftedMean<Type T>(Real offset) over input where T isa Real =
    input.Σmean + offset;

items.ΣshiftedMean(2.5)

fold Real mean<Type T> over input where T isa Real =
    input.Σsum / input.Σcount
    defined where input.Σcount > 0;

using vendor.Stats as stats;

items.Σmedian       // valid only if a visible declaration named median exists
items.Σstats.median // vendor.Stats.median, if that component declares it

// Cardinality folds
fold Integer count<Type T> =
    Σ{ 0 ; n v ↦ n + 1 };

fold Boolean exists<Type T> =
    Σ{ false ; found v ↦ true };

fold Boolean empty<Type T> =
    Σ{ true ; empty v ↦ false };

// Boolean folds
fold Boolean all =
    Σ{ true ; result v ↦ result ∧ v };

fold Boolean any =
    Σ{ false ; result v ↦ result ∨ v };

// Numeric folds
fold T sum<Type T> where T isa Real =
    Σ{ 0 ; total v ↦ total + v };

fold T product<Type T> where T isa Real =
    Σ{ 1 ; total v ↦ total * v };

fold Real mean<Type T> over input where T isa Real =
    input.Σsum / input.Σcount
    defined where input.Σcount > 0;

fold Real variance<Type T> over input where T isa Real =
    ((input - input.Σmean)^2).Σmean
    defined where input.Σcount > 0;

fold Real stddev<Type T> over input where T isa Real =
    sqrt(input.Σvariance)
    defined where input.Σcount > 0;

// Ordered folds
fold T min<Type T> where ordered(T) =
    Σ{ first v ↦ v ; best v ↦ if v < best then v else best };

fold T max<Type T> where ordered(T) =
    Σ{ first v ↦ v ; best v ↦ if best < v then v else best };

// Ordered-input folds
fold String concat =
    Σ{ "" ; text v ↦ text + v };

items.Σexists = (items.Σcount > 0)
items.Σempty  = (items.Σcount = 0)
items.Σexists = not items.Σempty

s.part.Σlist(name order by weight)

s.part.Σlist((name, weight) order by weight)

s.part.Σlist((name, weight * 1000) order by weight)

s.part.Σlist(name order by weight, name)

s.part.Σlist(name order by weight↓, name↑)

s.supplier.Σlist(name order by status if city = "London")

s.supplier.Σlist(
    (name, shipment.Σcount)
    order by shipment.Σcount↓, name
    if city = "London"
)

ListExpression =
    "Σlist", "(", ListItem, [ ListOrderClause ], [ ListFilterClause ], ")";

ListItem =
    Expression;

ListOrderClause =
    "order", "by", ListOrderKey, { ",", ListOrderKey };

ListOrderKey =
    Expression, [ ListOrderDirection ];

ListOrderDirection =
      "↑"
    | "↓";

ListFilterClause =
    "if", Expression;

s.supplier.(id, shipment.qty.Σsum)

{
    (id = 1, qty = 1300),
    (id = 2, qty = 700),
    (id = 3, qty = 200),
    (id = 4, qty = 900),
    (id = 5, qty = 0)
}

SUMMARIZE SP PER SP { S# } ADD COUNT(*) AS NUM_SHIPMENTS

s.supplier.(id, shipment.Σcount as num_shipments)

id=I:Integer, num_shipments=C:Integer
where
  ∃S:Supplier
    s.supplier(S)
  ∧ S.id(I)
  ∧ C = |{ SP:Shipment | S.shipment(SP) }|

s.supplier.[shipment.Σ ≠ ∅].(id, shipment.Σcount as num_shipments)

s.shipment.groupby(supplier.id)

s.shipment.groupby(supplier.id).(id, group.qty.Σsum as total_qty)

s.shipment.group(g)by(supplier.id).(id, g.qty.Σsum as total_qty)

SUMMARIZE SP PER SP { S# } ADD SUM(QTY) AS TOTAL_QTY

SUMMARIZE SP 
    PER SP { S# }
    ADD SUM(QTY) AS TOTAL_QTY

s.supplier.(
    id,
    shipment.qty.Σsum as total_qty)

SUMMARIZE SP 
    PER SP { P# }
    ADD SUM(QTY) AS TOTAL_QTY

s.part.(
    id,
    shipment.qty.Σsum as total_qty)

SUMMARIZE SP 
    PER SP { S# }
    ADD COUNT(*) AS NUM_SHIPMENTS

s.supplier.(
    id,
    shipment.Σcount as num_shipments)

SUMMARIZE SP 
    PER SP { S# }
    ADD COUNT(P#) AS NUM_PARTS

s.supplier.(
    id,
    shipment.part.Σcount as num_parts)

SUMMARIZE SP 
    PER SP { S# }
    ADD SUM(QTY) AS TOTAL_QTY,
        COUNT(*) AS NUM_SHIPMENTS

s.supplier.(
    id,
    shipment.qty.Σsum as total_qty,
    shipment.Σcount as num_shipments)

SUMMARIZE (SP JOIN S) 
    PER (SP JOIN S) { S#, CITY }
    ADD SUM(QTY) AS TOTAL_QTY

s.supplier.(
    id,
    city,
    shipment.qty.Σsum as total_qty)

SUMMARIZE SP 
    PER SP { P# }
    ADD SUM(QTY) AS TOTAL_QTY,
        COUNT(S#) AS NUM_SUPPLIERS

s.part.(
    id,
    shipment.qty.Σsum as total_qty,
    shipment.supplier.Σcount 
        as num_suppliers)

SUMMARIZE (SP JOIN P) 
    PER (SP JOIN P) { S# }
    ADD SUM(QTY * WEIGHT) 
        AS TOTAL_WEIGHT

s.supplier.(
    id,
    shipment.(qty * part.weight).Σsum 
        as total_weight)

SUMMARIZE SP 
    PER SP { S# }
    ADD { P#, PNAME } AS PARTS

s.supplier.(
    id,
    shipment.part.(id, name).Σ as parts)

SUMMARIZE (SP JOIN P 
        WHERE WEIGHT > 15) 
    PER (SP JOIN P) { S# }
    ADD COUNT(*) AS NUM_HEAVY

s.supplier.(
    id,
    shipment.[part.weight > 15].Σcount
        as num_heavy)

SUMMARIZE SP PER SP { S#, P# }
    ADD SUM(QTY) AS TOTAL_QTY

s.shipment.(
    supplier.id as s#,
    part.id as p#,
    qty.Σsum as total_qty)

(SUMMARIZE (SP RENAME S# AS OUTER_S#) PER (SP RENAME S# AS OUTER_S#) { OUTER_S# }
    ADD SUMMARIZE SP WHERE S# = OUTER_S#
        PER SP { P# }
        ADD SUM(QTY) AS TOTAL_QTY
        AS PART_SUMMARY
) RENAME OUTER_S# AS S#

s.supplier.(
    id,
    shipment.(
        part.id,
        qty.Σsum as total_qty
    ).Σ as part_summary)

SUMMARIZE (SP JOIN S) PER (SP JOIN S) { CITY }
    ADD SUM(QTY) AS TOTAL_QTY,
        COUNT(DISTINCT S#) AS NUM_SUPPLIERS

s.shipment.(
    supplier.city,
    qty.Σsum as total_qty,
    supplier.id.{ }.Σcount as num_suppliers)

(SUMMARIZE (SP RENAME P# AS OUTER_P#) PER (SP RENAME P# AS OUTER_P#) { OUTER_P# }
    ADD SUMMARIZE SP WHERE P# = OUTER_P#
        PER SP { S# }
        ADD SUM(QTY) AS TOTAL_QTY
        AS SUPPLIER_SUMMARY
) RENAME OUTER_P# AS P#

s.part.(
    id,
    shipment.(
        supplier.id,
        qty.Σsum as total_qty
    ).Σ as supplier_summary)

SUMMARIZE (SP JOIN P WHERE COLOR = 'Red') PER (SP JOIN P) { S# }
    ADD SUM(QTY) AS TOTAL_RED_QTY

s.shipment.[part.color = Color.red].(
    supplier.id,
    qty.Σsum as total_red_qty)

(SUMMARIZE ((SP JOIN P) RENAME S# AS OUTER_S#) PER ((SP JOIN P) RENAME S# AS OUTER_S#) { OUTER_S# }
    ADD SUMMARIZE (SP JOIN P WHERE S# = OUTER_S#)
        PER (SP JOIN P) { COLOR }
        ADD COUNT(*) AS NUM_PARTS
        AS COLOR_SUMMARY
) RENAME OUTER_S# AS S#

s.supplier.(
    id,
    shipment.part.(
        color,
        Σcount as num_parts
    ).Σ as color_summary)

(SUMMARIZE (S RENAME CITY AS OUTER_CITY) PER (S RENAME CITY AS OUTER_CITY) { OUTER_CITY }
    ADD SUMMARIZE (SP JOIN S WHERE CITY = OUTER_CITY)
        PER (SP JOIN S) { S# }
        ADD SUM(QTY) AS TOTAL_QTY
        AS SUPPLIER_SUMMARY
) RENAME OUTER_CITY AS CITY

s.supplier.(
    city,
    shipment.(
        supplier.id,
        qty.Σsum as total_qty
    ).Σ as supplier_summary)

SUMMARIZE (SP JOIN S WHERE CITY = 'London') PER (SP JOIN S) { P# }
    ADD SUM(QTY) AS TOTAL_QTY

s.shipment.(
    part.id,
    supplier.[city = "London"].qty.Σsum as total_qty)

(SUMMARIZE (SP RENAME S# AS OUTER_S#) PER (SP RENAME S# AS OUTER_S#) { OUTER_S# }
  ADD SUMMARIZE SP WHERE S# = OUTER_S#
      PER SP { P# }
      ADD SUM(QTY) AS TOTAL_QTY
      AS PART_SUMMARY
) RENAME OUTER_S# AS S#

s.supplier.(
    id,
    shipment.(
        part.id,
        qty.Σsum as total_qty
    ).Σ as part_summary)

(SUMMARIZE (S RENAME CITY AS OUTER_CITY) PER (S RENAME CITY AS OUTER_CITY) { OUTER_CITY }
  ADD SUMMARIZE (SP JOIN S WHERE CITY = OUTER_CITY)
      PER (SP JOIN S) { S# }
      ADD SUM(QTY) AS TOTAL_QTY
      AS SUPPLIER_SUMMARY
) RENAME OUTER_CITY AS CITY

s.supplier.(
    city,
    shipment.(
        supplier.id,
        qty.Σsum as total_qty
    ).Σ as supplier_summary)

(SUMMARIZE ((SP JOIN P) RENAME S# AS OUTER_S#) PER ((SP JOIN P) RENAME S# AS OUTER_S#) { OUTER_S# }
  ADD SUMMARIZE (SP JOIN P WHERE S# = OUTER_S#)
      PER (SP JOIN P) { COLOR }
      ADD SUM(QTY) AS TOTAL_QTY
      AS COLOR_SUMMARY
) RENAME OUTER_S# AS S#

s.supplier.(
    id,
    shipment.(
        part.color,
        qty.Σsum as total_qty
    ).Σ as color_summary)

SUMMARIZE (SP JOIN S) PER (SP JOIN S) { P#, CITY }
  ADD SUM(QTY) AS TOTAL_QTY

s.shipment.(
    part.id as p#,
    supplier.city,
    qty.Σsum as total_qty)

(SUMMARIZE (SP RENAME S# AS OUTER_S#) PER (SP RENAME S# AS OUTER_S#) { OUTER_S# }
  ADD AVG(
        SUMMARIZE SP WHERE S# = OUTER_S#
            PER SP { P# }
            ADD SUM(QTY)
      ) AS AVG_QTY
) RENAME OUTER_S# AS S#

s.supplier.(
    id,
    shipment.(
        part.id,
        qty.Σsum as total_qty
    ).total_qty.Σavg as avg_qty)

(SUMMARIZE (S RENAME CITY AS OUTER_CITY) PER (S RENAME CITY AS OUTER_CITY) { OUTER_CITY }
  ADD COUNT(*) AS NUM_SUPPLIERS,
      SUMMARIZE (SP JOIN S WHERE CITY = OUTER_CITY)
          PER (SP JOIN S) { CITY }
          ADD SUM(QTY) AS TOTAL_QTY
          AS SHIPMENT_SUMMARY
) RENAME OUTER_CITY AS CITY

s.supplier.(
    city,
    Σcount as num_suppliers,
    shipment.qty.Σsum as total_qty)

(SUMMARIZE (SP RENAME S# AS OUTER_S#) PER (SP RENAME S# AS OUTER_S#) { OUTER_S# }
  ADD SUMMARIZE (SP JOIN P WHERE S# = OUTER_S# AND WEIGHT > 15)
        PER (SP JOIN P) { S# }
        ADD SUM(QTY) AS HEAVY_QTY
        AS HEAVY,
      SUMMARIZE (SP JOIN P WHERE S# = OUTER_S# AND WEIGHT ≤ 15)
        PER (SP JOIN P) { S# }
        ADD SUM(QTY) AS LIGHT_QTY
        AS LIGHT
) RENAME OUTER_S# AS S#

s.supplier.(
    id,
    shipment.[part.weight > 15].qty.Σsum as heavy_qty,
    shipment.[part.weight ≤ 15].qty.Σsum as light_qty)

(SUMMARIZE ((SP JOIN S) RENAME P# AS OUTER_P#) PER ((SP JOIN S) RENAME P# AS OUTER_P#) { OUTER_P# }
  ADD SUMMARIZE (SP JOIN S WHERE P# = OUTER_P#)
        PER (SP JOIN S) { STATUS }
        ADD SUM(QTY) AS TOTAL_QTY
        AS STATUS_SUMMARY
) RENAME OUTER_P# AS P#

s.part.(
    id,
    shipment.(
        supplier.status,
        qty.Σsum as total_qty
    ).Σ as status_summary)

SUMMARIZE SP PER SP { S# }
  ADD SUM(QTY) AS TOTAL_QTY,
      AVG(QTY) AS AVG_QTY

s.shipment.(
    supplier.id,
    qty.Σsum as total_qty,
    qty.Σavg as avg_qty)

⟨R for F where Ψ⟩

extension(⟨R for F where Ψ⟩)
    = { evaluate(R, σ) | σ assigns F and σ satisfies Ψ }

{ id: 17, city: "London" }

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

< id: {17}, city: {"London", "Athens"} >

{
    { id: 17, city: "London" },
    { id: 17, city: "Athens" }
}

< id: {17}, city: {"London", "Athens"}, status: {} >

t↑a = t.a if a ∈ dom(t), otherwise the value domain of a

t!_H = { s | dom(s) = H and for every a ∈ H, s.a ∈ t↑a }

M!_H = ⋃ { t!_H | t ∈ M }

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

(op_m(M₁, ..., Mₙ))!_H = op_s(M₁!_H, ..., Mₙ!_H)

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

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

< a: {0}, b: {0} >!_{a,b}
    = { {a: 0, b: 0} }

not < a: {0}, b: {0} >
    expands to
    {
        {a: 0, b: 1},
        {a: 1, b: 0},
        {a: 1, b: 1}
    }

(not M)!_H = universe(H) \ M!_H
(M -- N)!_H = M!_H \ N!_H
M -- N ≡_H M ∧ (not N)

t subsumes u under H  iff  for every a ∈ H, t↑a ⊇ u↑a

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

(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
(M ∪ not M)!_H      = universe(H)
(M ∧ not M)!_H      = {}
(not not M)!_H      = M!_H
not (M ∪ N) ≡_H (not M) ∧ (not N)
not (M ∧ N) ≡_H (not M) ∪ (not N)

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)

s.supplier -- s.shipment.supplier

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

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

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

H = { id: Integer, city: String }

{ id: 17, city: "London" }

{} under { id: Integer }
{} under { id: Integer, city: String }

H = { id: Integer, city: String }

universe(H) =
{
    { id: i, city: c }
    | i ∈ Integer and c ∈ String
}

R under H  iff  R ⊆ universe(H)

not_H(R) = universe(H) \ R

D_id   = {17, 23}
D_city = {"London", "Paris"}
H      = { id: D_id, city: D_city }

R =
{
    { id: 17, city: "London" }
}

not_H(R) =
{
    { id: 17, city: "Paris" },
    { id: 23, city: "London" },
    { id: 23, city: "Paris" }
}

t↑a = t.a if a ∈ dom(t), otherwise domain_H(a)

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

< id: {17} >

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

⟨R for F where Ψ⟩

project_A(⟨R for F where Ψ⟩) = ⟨R|A for F where Ψ⟩

id=I:Integer, city=C:String
where ∃S:Supplier (s.supplier(S) ∧ S.id(I) ∧ S.city(C))

id=I:Integer
where ∃S:Supplier ∃C:String (s.supplier(S) ∧ S.id(I) ∧ S.city(C))

π_A(S) = { s|A | s ∈ S }

S =
{
    { id: 17, city: "London" },
    { id: 17, city: "Athens" },
    { id: 23, city: "Paris" }
}

π_{id}(S) =
{
    { id: 17 },
    { id: 23 }
}

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

π_A^naive(M) = { t|A | t ∈ M }

M = { < id: {17}, status: {} > }

M!_{id,status} = {}

π_{id}(M!_{id,status}) = {}

π_{id}^naive(M) = { < id: {17} > }

π_{id}^naive(M)!_{id} =
{
    { id: 17 }
}

π_A^m(M) = { t|A | t ∈ M and t!_H ≠ {} }

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

statuses=TS:Set<Integer>
where TS = { T:Integer | S.status(T) }

entity Supplier
{
    Integer id;
    String city*;
    Integer status?;
}

entity ShipmentsSystem
{
    Supplier supplier*;
}

{
    < id: {17}, city: {"London", "Athens"}, status: {} >,
    < id: {23}, city: {"Paris"}, status: {20} >
}

id=I:Integer, city=C:String
where ∃S:Supplier (s.supplier(S) ∧ S.id(I) ∧ S.city(C))

M =
{
    < id: {17}, city: {"London", "Athens"} >,
    < id: {23}, city: {"Paris"} >
}

M!_{id,city} =
{
    { id: 17, city: "London" },
    { id: 17, city: "Athens" },
    { id: 23, city: "Paris" }
}

id=I:Integer, city=C:String, status=T:Integer
where ∃S:Supplier (s.supplier(S) ∧ S.id(I) ∧ S.city(C) ∧ S.status(T))

N =
{
    < id: {17}, city: {"London", "Athens"}, status: {} >,
    < id: {23}, city: {"Paris"}, status: {20} >
}

N!_{id,city,status} =
{
    { id: 23, city: "Paris", status: 20 }
}

id=I:Integer, cities=CS:Set<String>, statuses=TS:Set<Integer>
where ∃S:Supplier (
    s.supplier(S)
    ∧ S.id(I)
    ∧ CS = { C:String | S.city(C) }
    ∧ TS = { T:Integer | S.status(T) }
)

{
    { id: 17, cities: {"London", "Athens"}, statuses: {} },
    { id: 23, cities: {"Paris"}, statuses: {20} }
}

logic frame  --heading H-->  s-relation extension under H

s.supplier.(id, name, status, city)

id=I:Integer, name=N:String, status=T:Integer, city=C:String
where ∃S:Supplier (
    s.supplier(S)
    ∧ S.id(I)
    ∧ S.name(N)
    ∧ S.status(T)
    ∧ S.city(C)
)

(S WHERE CITY = 'London'){SNAME}

s.supplier.[city = "London"].name

name=N:String
where ∃S:Supplier ∃C:String (
    s.supplier(S)
    ∧ S.city(C)
    ∧ C = "London"
    ∧ S.name(N)
)

(SP JOIN S JOIN P){SNAME, PNAME, QTY}

s.shipment.(
    supplier.name as sname,
    part.name as pname,
    qty)

sname=SN:String, pname=PN:String, qty=Q:Integer
where ∃X:Shipment ∃S:Supplier ∃P:Part (
    s.shipment(X)
    ∧ X.supplier(S)
    ∧ X.part(P)
    ∧ S.name(SN)
    ∧ P.name(PN)
    ∧ X.qty(Q)
)

( (S RENAME CITY AS SCITY) TIMES (P RENAME CITY AS PCITY) )
WHERE SCITY > PCITY

s.(supplier, part).[supplier.city > part.city]

s.(supplier, part).[supplier.city > part.city].(
    supplier.city as scity,
    part.city as pcity)

M is valid under H  iff  M!_H is the intended s-relation extension

Predica path expression  --logic frame-->  corresponding s-relation

s.supplier.(id as s_id, name as sname, status, city)

s_id=SI:Integer, sname=SN:String, status=ST:Integer, city=C:String
where ∃S:Supplier (
    s.supplier(S)
    ∧ S.id(SI)
    ∧ S.name(SN)
    ∧ S.status(ST)
    ∧ S.city(C)
)

s.part.(id as p_id, name as pname, color, weight, city)

s.shipment.(
    supplier.id as s_id,
    part.id as p_id,
    qty)

s_id=SI:Integer, p_id=PI:Integer, qty=Q:Integer
where ∃X:Shipment ∃S:Supplier ∃P:Part (
    s.shipment(X)
    ∧ X.supplier(S)
    ∧ X.part(P)
    ∧ S.id(SI)
    ∧ P.id(PI)
    ∧ X.qty(Q)
)

(S WHERE CITY = 'London'){SNAME}

s.supplier.[city = "London"].name

name=N:String
where ∃S:Supplier ∃C:String (
    s.supplier(S)
    ∧ S.city(C)
    ∧ C = "London"
    ∧ S.name(N)
)

(SP JOIN S JOIN P){SNAME, PNAME, QTY}

s.shipment.(
    supplier.name as sname,
    part.name as pname,
    qty)

sname=SN:String, pname=PN:String, qty=Q:Integer
where ∃X:Shipment ∃S:Supplier ∃P:Part (
    s.shipment(X)
    ∧ X.supplier(S)
    ∧ X.part(P)
    ∧ S.name(SN)
    ∧ P.name(PN)
    ∧ X.qty(Q)
)

S MINUS (SP {S#} JOIN S)

s.supplier -- s.shipment.supplier

{ supplier: Supplier }

(...).(id as s_id, name as sname, status, city)

S WHERE NOT EXISTS (
    (P WHERE COLOR = 'Red')
    WHERE NOT EXISTS (
        SP WHERE SP.S# = S.S#
           AND SP.P# = P.P#
    )
)

s.part.[
    color = Color.red
]⇒(shipment.supplier)

S WHERE STATUS >= ALL S{STATUS}

s.supplier.[
    status ≥ s.supplier⇒status
]

P WHERE WEIGHT > ANY (
    (SP WHERE S# = 'S1' JOIN P){WEIGHT}
)

s.part.[
    weight > s.shipment.[
        supplier.id = 1
    ].part.weight
]

{
    < id: {1}, city: {"London"}, status: {20} >,
    < id: {5}, city: {"Athens"}, status: {30} >
}

H = { city: String }
R =
{
    { city: "London" },
    { city: "Paris" },
    { city: "Athens" }
}

R.$set = { "London", "Paris", "Athens" }

R.$set = { s.a | s ∈ R }

H = { id: Integer, city: String }
R =
{
    { id: 17, city: "London" }
}

R.$tup = { id: 17, city: "London" }

H = { status: Integer }
R =
{
    { status: 20 }
}

R.$val = 20

R.$val = v

H = { statuses: Set<Integer> }
R =
{
    { statuses: {} }
}

R.$val = {}

H = { status: Integer }
R = {}

accessor(M under H) is defined iff accessor(M!_H) is defined
and then accessor(M under H) = accessor(M!_H)

M represents S under H  iff  M!_H = S

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

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

(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

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

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

component SalesMutable;

entity Customer
{
    Text email;
    Text name?;
}

entity Order
{
    Text customerEmail;
    Text orderNumber;
}

entity Sales
{
    Customer customer*;
    Order order*;
}

component SalesPristine;

using SalesMutable as mutable;

entity Sales
{
    snapshot mutable.Sales source;

    → Customer customer* = source.customer.[
        let c=this in source.customer.[email = c.email].Σcount = 1
    ].(
        Customer { email = email; name = name }
    );
}

entity Sales
{
    snapshot mutable.Sales source;

    → Customer customer* = source.customer.[
        let c=this in source.customer.[email = c.email].name.Σcount <= 1
    ].(
        Customer { email = email; name = name }
    );
}

entity Customer
{
    Text email;
    Text name?;
}

entity Order
{
    Customer customer;
    Text orderNumber;
}

entity Sales
{
    snapshot mutable.Sales source;

    → Customer customer* = source.customer.[
        let c=this in source.customer.[email = c.email].Σcount = 1
    ].(
        Customer { email = email; name = name }
    );

    → Order order* = source.order.[customerEmail ∈ customer.email.Σ].(
        Order {
            customer = customer.[email = customerEmail];
            orderNumber = orderNumber;
        }
    );
}

var status = 0;
status := 25;

var Integer id* = {};
id := s.supplier.id;

var id1 = 0;
id1 := s.supplier.id;     // static cardinality constraint check failure

var Integer id2* = {};
id2 := s.supplier.id;     // ok

var B b* = { A { x = 1 }, A { x = 2 } };

var String message;

var String message;

var String names*;       // uninitialised
var String others* = {}; // initialised with the empty extension

var String message;
message := "hello";
print message;           // legal

var String s;
var String t = s + "a";  // static error: s may be uninitialised