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.