A language supporting nested RM

Introduction

Predica (single-page version) is a formal language for:

• defining types with precise constraints
• annotating types with meta‑data
• expressing queries over well‑defined domains

It is well suited to Database Management Systems and also provides a rigorous foundation for defining legality in laws, contracts, and other normative systems.

Example schema written in Predica

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");

Queries written in Predica

The following query returns the names of suppliers that supply the part whose identifier is P2:

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

The formal semantics of Predica is defined by the logical denotations of queries. In this case:

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)

The query demonstrates universal quantification. It returns the suppliers that supply every red part:

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

Its logical denotation is:

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

Queries can use aggregation. This query returns the suppliers for which every part they ship is red:

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

Its logical denotation is:

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

Relational Model notes

My Relational Model notes examine the mathematical foundations of relational databases, the relationship between data and predicates, database constraints, information decomposition, and the view update problem. They also explore nested relational models and ways of applying relational theory to practical database systems.