Skip to content

Information System Model — Formal Semantics

Note: For the interested reader, this section provides the rigorous mathematical foundation for the IS-Model, combining Type Theory for structural definitions and Set Theory for multi-tenant Context topologies. The uninterested reader can skip this chapter because the core concepts have already been described narratively in the previous sections.

Type Theory

Following standard type theory notation (e.g., Pierce), we formalize the structural constraints of the model. The graph model is rooted in two absolute base abstract Types: Entity and Relation. (Note: The Property base Type, which governs embedded values, exists outside this topological instance model since its data fields lack an independent graph identity).

Typing Relation

Let \(x\) be a concrete instance in the graph. We define two distinct predicates to separate the native structural shape from polymorphic conformance:

  1. Declared Type: We write \(\text{declaredType}(x) = T\) to indicate the exact concrete Type \(T\) assigned to the instance at creation.
  2. Subtype Conformance: We write \(x \models U\) to indicate that \(x\) conforms to Type \(U\).

Single Instantiation Rule: An instance is natively declared under exactly ONE concrete Type (which defines its base shape).

\[ \text{declaredType}(x) = T \implies \forall T' \neq T, \text{declaredType}(x) \neq T' \]

Subtyping (Inheritance)

We write \(S <: T\) to indicate that Type \(S\) is a subtype (specialization) of Type \(T\). Following the principle of safe substitution (Rule of Subsumption), any instance conforms to its declared Type and to all its supertypes:

\[ x \models U \iff \text{declaredType}(x) <: U \]

(Note: Every type is trivially a subtype of itself, so \(T <: T\) and \(x \models \text{declaredType}(x)\) are always true).

Base Type Constraints:

  • Let \(\mathbb{I}\) be the set of all graph instance Types. A graph instance Type is exclusively either an Entity or a Relation.

    \[ \forall T \in \mathbb{I}, \quad T <: Entity \oplus T <: Relation \]

The foundation of the model defines four core topological Types descending from the graph base Types: Resource and Facet (descending from Entity), and IsRelatedTo and ConsistsOf (descending from Relation). Every concrete graph instance must be of a Type that extends one of these four (or, in the case of ConsistsOf, it can instantiate the base Type itself, as it is uniquely concrete among the foundational topologies).

Core Type Constraints:

  • Resource and Facet are mutually exclusive Entity branches.

    \[ T <: Entity \implies (T <: Resource \oplus T <: Facet) \]

  • IsRelatedTo and ConsistsOf are mutually exclusive Relation branches.

    \[ T <: Relation \implies (T <: IsRelatedTo \oplus T <: ConsistsOf) \]

  • IsRelatedTo strictly connects a source Resource to a target Resource (where \(IRT\) denotes an IsRelatedTo schema definition):

    \[ IRT <: IsRelatedTo \implies \text{source}(IRT) <: Resource \land \text{target}(IRT) <: Resource \]

  • ConsistsOf strictly connects a source Resource to a target Facet (where \(CO\) denotes a ConsistsOf schema definition):

    \[ CO <: ConsistsOf \implies \text{source}(CO) <: Resource \land \text{target}(CO) <: Facet \]

System Fields

Every instance is formally equipped with base properties. We denote the existence of a property field \(p\) on an instance \(x\) as \(\exists p(x)\).

  • Universal Identification and Provenance:

    \[ \forall x : Entity \cup Relation, \exists \text{id}(x) \land \exists \text{metadata}(x) \]

  • Relation-exclusive Behavior:

    \[ \forall e : Relation, \exists \text{propagationConstraint}(e) \]

Formal Topological Uniqueness Invariants

To ensure deterministic operations, unambiguous garbage collection, and prevent "double-counting" during polymorphic queries, the IS-Model enforces the following structural uniqueness invariants on the global graph topology:

1. Facet Exclusivity (Single Ownership): A Facet instance is intrinsically a characterizing aspect of a single Resource instance. It must be attached via exactly one ConsistsOf instance globally. In other words, a Facet instance cannot be attached to multiple Resource instances, nor can it be attached via multiple ConsistsOf instances to the same Resource instance.

\[ \forall f \mid \text{declaredType}(f) <: Facet, \quad \exists! e_{co} \mid \text{declaredType}(e_{co}) <: ConsistsOf \land \text{target}(e_{co}) = f \]

(Note: Because \(e_{co}\) is strictly unique for any given \(f\), the contextual dependency formula \(C(f) = C(e_{co})\) is mathematically absolute).

2. IsRelatedTo Polymorphic Uniqueness: Two specific Resource instances cannot be linked via multiple IsRelatedTo instances belonging to the same polymorphic lineage. If two distinct IsRelatedTo instances link the exact same source and target Resource instances, neither Relation instance's Type can be a subtype of the other. This prevents semantic redundancy (e.g., preventing a generic Hosts relation and a specialized MyHosts <: Hosts relation from existing simultaneously linking the same two Resource instances). Re-asserting the same semantic connection through a more specialized type makes no sense; the correct operational pattern is to delete the generic relation and create the specialized one, since polymorphic queries (which are enabled by default) will still return it when querying the supertype.

\[ \forall e_1, e_2 \mid (\text{source}(e_1) = \text{source}(e_2) \land \text{target}(e_1) = \text{target}(e_2) \land e_1 \neq e_2) \implies \neg(\text{declaredType}(e_1) <: \text{declaredType}(e_2) \lor \text{declaredType}(e_2) <: \text{declaredType}(e_1)) \]

Conversely, parallel IsRelatedTo instances linking the same two Resource instances are explicitly permitted if they belong to entirely orthogonal polymorphic branches (e.g., a Discovers relation and a Uses relation), as they capture orthogonally distinct semantic interactions.

Set Theory for Context Membership

The multi-tenant nature of the IS-Model is underpinned by set theory rules governing Context membership for concrete instances.

Let \(C(x)\) represent the set of Contexts to which an instance \(x\) (an Entity instance or a Relation instance) belongs.

General Relation Context Intersection

For any Relation instance \(e\) (whether IsRelatedTo or ConsistsOf) linking a source Resource instance \(r\) to a target Entity instance \(t\), the Relation instance can only exist in Contexts where both the source and target instances exist.

\[ C(e) \subseteq C(r) \cap C(t) \]

Explanation: You cannot define a Relation instance in a Context if one of its two endpoints is missing from that Context. The Relation instance is strictly constrained by the intersection of the visibility of the two instances it connects. Specifically for IsRelatedTo instances, their presence is strictly bounded by this intersection rule, but they are not automatically present just because the intersection exists. They require explicit mathematical addition to the Context set. Even if two Resource instances share multiple Contexts, the link between them only exists in the specific subset of those Contexts where it was explicitly created or added. It is not an implicit auto-join.

Facet Context Dependency

A Facet instance \(f\) is intrinsically tied to the ConsistsOf instance \(e_{co}\) that connects it to its parent Resource instance \(r\). A Facet instance cannot exist independently of this ConsistsOf instance.

\[ C(f) = C(e_{co}) \]

By applying the general intersection rule, it follows that the Facet instance can only exist in a subset of the Contexts where its parent Resource instance exists:

\[ C(f) \subseteq C(r) \]

Explanation: It is mathematically impossible for a Facet instance to exist in a Context without its parent Resource instance.

Resource Context Union

The presence of a Resource instance \(r\) in a Context is exactly the union of all Contexts of its attached Facet instances \(f_i\).

\[ C(r) = \bigcup_{i} C(f_i) \]

Explanation: A Resource instance exists in a Context if and only if it has at least one Facet instance in that Context.

Avalanche State Transitions

Let \(e\) be a Relation instance with source \(r\) and target \(t\). We denote the propagation constraints as \(e_{add}\) and \(e_{remove}\). Let \(C_{src}\) be the context from which the instance is being shared, and \(C_n\) be the destination Context.

  • Add Propagation: Adding \(r\) to \(C_n\) from \(C_{src}\) implies adding both \(e\) and \(t\) to \(C_n\) if the constraint is propagate and the relation is visible in the source Context.

    \[ \text{Add}(r, C_n \leftarrow C_{src}) \land C_{src} \in C(e) \land (e_{add} = propagate) \implies \text{Add}(t, C_n) \land \text{Add}(e, C_n) \]

  • Direct Relation Add: Adding a Relation instance directly to Context \(C_n\) requires its source to already exist in \(C_n\). The target is automatically pulled into \(C_n\) to satisfy the relation constraint, regardless of its add propagation constraint.

    \[ \text{Add}(e, C_n) \implies C_n \in C(r) \land \text{Add}(t, C_n) \]

  • Topological Cleanup: Removing an instance from Context \(C_n\) automatically drops all connected Relation instances in \(C_n\).

    \[ \text{Remove}(x, C_n) \implies \forall e \mid (C_n \in C(e) \land (\text{source}(e) = x \lor \text{target}(e) = x)), \text{Remove}(e, C_n) \]

  • Remove Propagation: Removing \(r\) from \(C_n\) implies removing \(t\) from \(C_n\) if the constraint is cascade. Let \(E_{rem}\) be the set of relations being removed in the current transaction avalanche.

    \[ \text{Remove}(r, C_n) \land (e_{remove} = cascade) \implies \text{Remove}(t, C_n) \]

    If the constraint is cascadeWhenOrphan, \(t\) is removed only if no other incoming Relation instances to \(t\) exist in the candidate post-state of \(C_n\). (Note: Since ConsistsOf instances can only target Facet instances, if \(t\) is a Resource instance, the formula effectively only counts incoming IsRelatedTo instances).

    \[ \text{Remove}(r, C_n) \land (e_{remove} = cascadeWhenOrphan) \land (\not\exists e' \mid C_n \in C(e') \land e' \notin E_{rem} \land \text{target}(e') = t) \implies \text{Remove}(t, C_n) \]

Reference Counting

An instance \(x\) is physically destroyed from the global graph (Garbage Collected) if and only if the set of its Contexts becomes empty.

\[ |C(x)| = 0 \iff C(x) = \emptyset \implies x \text{ is physically deleted} \]