---
last_review: "2026-05-07"
last_reviewer: "-"
documented_code: [ ]
---

```{tags} administrator, reference
```

# LinkAhead Data Model Formal Specifications

See also: [Data Model Overview](/explanation/general/data-model)

## Core Entities and Fundamental Relations

The following defines the main entity types and their properties in FOPL:

| Entity Type    | FOPL Definition              | Description                                                                  |
|----------------|------------------------------|------------------------------------------------------------------------------|
| **Entity**     | {math}`\text{Entity}(e)`     | General entity type; all other major types are subtypes                      |
| **RecordType** | {math}`\text{RecordType}(r)` | A class/type definition that structures Records                              |
| **Property**   | {math}`\text{Property}(p)`   | An attribute definition with name, datatype, and constraints                 |
| **Record**     | {math}`\text{Record}(x)`     | An instance of one or more RecordTypes; holds concrete data                  |
| **File**       | {math}`\text{File}(f)`       | Represents a reference to an actual file on the file system                  |
| **DataType**   | {math}`\text{DataType}(d)`   | Primitive or composite data type (TEXT, INTEGER, DATETIME, FILE, LIST, etc.) |

## Fundamental Predicates and Axioms

### Identity and Naming

:::{math}
\forall e : \text{Entity}(e) \rightarrow \exists \text{id}, \text{name} : \text{HasID}(e, \text{id}) \land \text{HasName}(e, \text{name})
:::

where {math}`\text{HasID}(e, \text{id})` means entity $e$ has unique identifier $\text{id}$, and {math}`\text{HasName}(e, \text{name})` means entity $e$ has name $\text{name}$.

:::{math}
\forall e_1, e_2 : \text{Entity}(e_1) \land \text{Entity}(e_2) \land \text{HasID}(e_1, \text{id}) \land \text{HasID}(e_2, \text{id}) \rightarrow e_1 = e_2
:::

Identity is functionally determined by ID.

### RecordType Structure

:::{math}
\forall r : \text{RecordType}(r) \rightarrow \exists \text{props}, \text{parents} : \\
\text{HasProperties}(r, \text{props}) \land \text{HasParents}(r, \text{parents}) \land (\text{parents} \neq \emptyset \lor r \text{ is root})
:::

:::{math}
\forall r : \text{RecordType}(r) \land \text{HasParents}(r, \text{parents}) \land r' \in \text{parents} \rightarrow \\
\text{RecordType}(r') \land (r' \neq r)
:::

Parents must be distinct RecordTypes; this prevents self-inheritance.

:::{math}
\forall r : \text{RecordType}(r) \rightarrow \exists p : \text{HasProperties}(r, p)
:::

RecordTypes can have zero or more Properties attached.

### Property Definition and Attachment

:::{math}
\forall p : \text{Property}(p) \rightarrow \exists \text{dtype}, \text{unit}, \text{desc} : \\
\text{HasDataType}(p, \text{dtype}) \land \text{HasUnit}(p, \text{unit}) \land \text{HasDescription}(p, \text{desc})
:::

:::{math}
\forall p : \text{Property}(p) \land \text{HasDataType}(p, \text{dtype}) \rightarrow \text{DataType}(\text{dtype})
:::

:::{math}
\forall r : \text{RecordType}(r) \land p \in \text{HasProperties}(r) \rightarrow \\
\exists \text{imp} : \text{HasImportance}(p, \text{imp}) \land (\text{imp} \in \{\text{obligatory}, \text{recommended}, \text{suggested}\})
:::

Properties attached to RecordTypes have an importance level.

:::{math}
\forall r : \text{RecordType}(r) \land \text{HasProperties}(r, p_1) \land \text{HasProperties}(r, p_2) \land p_1 \neq p_2 \rightarrow \\
\neg \exists \text{name} : \text{HasName}(p_1, \text{name}) \land \text{HasName}(p_2, \text{name})
:::

A RecordType cannot have duplicate property names.

### Record Instantiation

:::{math}
\forall x : \text{Record}(x) \rightarrow \exists rt : \text{HasRecordType}(x, rt) \land \text{RecordType}(rt) \land rt \neq \emptyset
:::

Every Record must have at least one RecordType.

:::{math}
\forall x : \text{Record}(x) \land \text{HasRecordType}(x, rt) \rightarrow \\
\forall p \in \text{HasProperties}(rt) : \text{HasImportance}(p, \text{obligatory}) \rightarrow \\
\exists \text{val} : \text{HasPropertyValue}(x, p, \text{val}) \land \text{val} \neq \text{null}
:::

Records must provide values for all obligatory properties of their RecordTypes.

:::{math}
\forall x : \text{Record}(x) \land \text{HasRecordType}(x, rt_1) \land \text{HasRecordType}(x, rt_2) \land rt_1 \neq rt_2 \rightarrow \\
\neg(\exists \text{conf} : \text{ConflictingProperties}(rt_1, rt_2, \text{conf}))
:::

Multiple RecordType membership is allowed unless properties conflict.

:::{math}
\forall x : \text{Record}(x) \rightarrow \forall p : \text{HasPropertyValue}(x, p, \text{val}) \rightarrow \\
\exists rt : \text{HasRecordType}(x, rt) \land p \in \text{HasProperties}(rt)
:::

A Record can only have values for properties defined in its RecordTypes.

### Property Values and DataTypes

:::{math}
\forall x : \text{Record}(x) \land p : \text{Property} \land \text{val} : \\
\text{HasPropertyValue}(x, p, \text{val}) \land \text{HasDataType}(p, \text{dtype}) \rightarrow \\
\text{MatchesType}(\text{val}, \text{dtype})
:::

Property values must conform to their declared datatype.

:::{math}
\forall \text{dtype} : \text{DataType}(\text{dtype}) \rightarrow \\
(\text{dtype} = \text{TEXT} \lor \text{dtype} = \text{INTEGER} \lor \text{dtype} = \text{DOUBLE} \lor \\
\text{dtype} = \text{DATETIME} \lor \text{dtype} = \text{FILE} \lor \text{dtype} = \text{BOOLEAN} \lor \\
\exists rt : \text{dtype} = \text{REFERENCE}(rt))
:::

:::{math}
\forall \text{dtype}, \text{element\_dtype} : \text{DataType}(\text{dtype}) \land \text{dtype} = \text{LIST}(\text{element\_dtype}) \rightarrow \\
\text{DataType}(\text{element\_dtype})
:::

LIST is a parameterized container type.

:::{math}
\forall x : \text{Record}(x) \land p : \text{Property} \land \text{HasDataType}(p, \text{REFERENCE}(rt)) \land \\
\text{HasPropertyValue}(x, p, \text{val}) \rightarrow \text{Record}(\text{val}) \land \text{HasRecordType}(\text{val}, rt)
:::

Reference properties point to Records of a specific RecordType.

### Inheritance and Property Propagation

:::{math}
\forall r : \text{RecordType}(r) \land \text{HasParents}(r, \{r_1, r_2, \ldots, r_n\}) \rightarrow \\
\forall r_i \in \{r_1, \ldots, r_n\} : \forall p_i \in \text{HasProperties}(r_i) : \\
p_i \in \text{HasProperties}(r)
:::

Inherited properties are not duplicated.

:::{math}
\forall r : \text{RecordType}(r) \land \text{HasParents}(r, \text{parents}) \land \\
\text{parent\_props} = \bigcup\{\text{HasProperties}(r_p) \mid r_p \in \text{parents}\} \rightarrow \\
\text{HasProperties}(r) \supseteq \text{parent\_props}
:::

A RecordType inherits all properties from all parents.

:::{math}
\forall x : \text{Record}(x) \land \text{HasRecordType}(x, rt) \land \text{HasParents}(rt, \text{parents}) \rightarrow \\
\forall \text{parent} \in \text{parents} : \text{HasRecordType}(x, \text{parent})
:::

Records implicitly satisfy parent RecordTypes (virtual inheritance).

### File References

:::{math}
\forall f : \text{File}(f) \rightarrow \exists \text{path} : \text{FilePath}(f, \text{path}) \land \text{path is valid}
:::

:::{math}
\forall f : \text{File}(f) \rightarrow \exists x : \text{Record}(x) \land \text{LinkedTo}(x, f)
:::

Files can be linked to Records.

:::{math}
\forall f : \text{File}(f) \land \text{LinkedTo}(x, f) \rightarrow \\
\forall p \in \text{CustomProperties}(x, f) : \text{Property}(p) \land \text{HasPropertyValue}(x, p, \text{val})
:::

Files linked to Records can have custom properties.

### Identifiability (for Data Synchronization)

:::{math}
\forall rt : \text{RecordType}(rt) \rightarrow \exists \text{id\_props} : \\
\text{IsIdentifiable}(rt, \text{id\_props}) \land \text{id\_props} \subseteq \text{HasProperties}(rt)
:::

:::{math}
\forall x_1, x_2 : \text{Record}(x_1) \land \text{Record}(x_2) \land \text{HasRecordType}(x_1, rt) \land \\
\text{HasRecordType}(x_2, rt) \land \text{IsIdentifiable}(rt, \text{id\_props}) \rightarrow \\
\left(\forall p \in \text{id\_props} : \text{HasPropertyValue}(x_1, p, v) \land \text{HasPropertyValue}(x_2, p, v)\right) \\
\leftrightarrow x_1 = x_2
:::

Identifiable properties uniquely determine record equality.

---

## Derived Predicates and Constraints

### Type Hierarchy Consistency

:::{math}
\forall r : \text{RecordType}(r) \rightarrow \neg(\exists \text{cycle} : r \in \text{Parents}^*(r))
:::

No circular inheritance allowed; {math}`\text{Parents}^*` is the transitive closure.

:::{math}
\text{Ancestors}(r) := \{r' \mid \exists n \geq 0 : r' \in \text{Parents}^n(r)\}
:::

Ancestors includes the type itself and all parent hierarchy.

### Data Integrity Constraints

:::{math}
\forall x : \text{Record}(x) \rightarrow \\
(\exists \text{val} : \text{HasPropertyValue}(x, p, \text{val}) \land \text{val} \neq \text{null}) \lor \\
(\exists rt : \text{HasRecordType}(x, rt) \land p \in \text{HasProperties}(rt) \land \\
\neg(\text{HasImportance}(p, \text{obligatory})))
:::

Every Record has values only for required or defined optional properties.

:::{math}
\forall p : \text{Property}(p) \rightarrow \neg(\exists r_1, r_2 : \\
\text{HasProperties}(r_1, p) \land \text{HasProperties}(r_2, p) \land \\
\text{HasDataType}(p, d_1) \land \text{HasDataType}(p, d_2) \land d_1 \neq d_2)
:::

A Property globally has exactly one datatype across all uses.

### Importance-Based Property Requirements

:::{math}
\forall x : \text{Record}(x) \land rt : \text{HasRecordType}(x, rt) \rightarrow \\
\forall p \in \text{AllProperties}(rt) : \\
(\text{HasImportance}(p, \text{obligatory}) \rightarrow \text{HasPropertyValue}(x, p) \neq \text{null}) \land \\
(\text{HasImportance}(p, \text{recommended}) \rightarrow \text{optional}) \land \\
(\text{HasImportance}(p, \text{suggested}) \rightarrow \text{optional})
:::

:::{math}
\text{AllProperties}(rt) := \text{HasProperties}(rt) \cup \\
\bigcup\{\text{HasProperties}(r_p) \mid r_p \in \text{Ancestors}(rt)\}
:::

Collect all properties including inherited ones.

## Model Semantics

### Domain

The universe of discourse consists of:

- **Entities:** RecordTypes, Properties, Records, Files
- **Values:** Atomic values (integers, text, dates, etc.) and compound values (lists, references)
- **Operations:** Property attachment, inheritance, synchronization

### Interpretation

- {math}`\text{HasRecordType}(x, rt)` = Record {math}`x` is an instance conforming to RecordType
  {math}`rt`
- {math}`\text{HasPropertyValue}(x, p, v)` = Record {math}`x` has property {math}`p` with value
  {math}`v`
- {math}`\text{HasProperties}(rt, p)` = Property {math}`p` is attached to RecordType {math}`rt`
- {math}`\text{HasParents}(rt, \text{parents})` = RecordType {math}`rt` inherits from the set of
  RecordTypes in {math}`\text{parents}`
- {math}`\text{HasImportance}(p, \text{imp})` = Property {math}`p` has importance level
  {math}`\text{imp}` in its declaring context

## Query Semantics (LQL Mapping to FOPL)

The LinkAhead Query Language (LQL) translates to FOPL as follows:

| LQL Query                                 | FOPL Translation                                                                                                                                                                                                                            |
|-------------------------------------------|---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|
| `FIND Guitar`                             | {math}`\exists x : \text{Record}(x) \land \text{HasRecordType}(x, \text{Guitar})`                                                                                                                                                           |
| `FIND RECORD WITH price > 1000`           | {math}`\exists x : \text{Record}(x) \land \text{HasPropertyValue}(x, \text{price}, v) \land v > 1000`                                                                                                                                       |
| `FIND Guitar WHICH REFERENCES A Musician` | {math}`\exists x, y : \text{Record}(x) \land \text{Record}(y) \land \text{HasRecordType}(x, Guitar) \land \text{HasRecordType}(y, Musician) \land \text{HasPropertyValue}(x, p, y) \land \text{HasDatatype}(p, \text{REFERENCE}(Musician))` |