AREST.tex

\documentclass[10pt,twocolumn]{article}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{amsmath,amssymb,amsthm}
\usepackage{mathtools}
\usepackage{hyperref}
\usepackage{listings}
\usepackage[margin=0.75in]{geometry}

\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{proposition}{Proposition}
\newtheorem{corollary}{Corollary}
\theoremstyle{definition}
\newtheorem{definition}{Definition}

\lstset{
  basicstyle=\small\ttfamily,
  breaklines=true,
  frame=single,
  xleftmargin=0.5em,
  xrightmargin=0.5em,
}

\title{\textbf{Compiling Facts into Applications}}

\author{Samuel Lippert\\Drivly Inc}

\date{}

\begin{document}
\maketitle

\begin{abstract}
A database schema, a family of state-machine workflows, and a REST API with hypermedia navigation are usually three artifacts kept in sync by hand. They are one object. Backus's Applicative State Transition system~\cite{backus78} carries a $\mathit{FILE}$ store it never structures; Codd's relations~\cite{codd70} supply the structure, Object-Role Modeling~\cite{halpin08} supplies the processes, and the representation function $\rho$ identifies them: set membership is function application. An \emph{application} is then this object, and running it is finite reduction over a finite fact population, which is what makes it algorithmic at all. The mapping's faithfulness rests on the formalisms it instantiates, and the only informal residue is the registered platform layer, an enumerable surface that coincides with the decidability frontier. The object is self-similar: it rewrites its own schema and contains isolated copies of itself, so a tenant is a sub-store and a tenant's tenants are sub-sub-stores, and each is a full instance carrying the same guarantees. A reference implementation is available~\cite{arest}.
\end{abstract}


\section{Foundation}\label{sec:foundation}

Three abbreviations are overloaded terms: \emph{AST} is Backus's Applicative State Transition~\cite[Sec.\,14]{backus78}, not the compiler's syntax tree; \emph{ORM} is Halpin's Object-Role Modeling~\cite{halpin08}, not the persistence pattern; \emph{FP} and \emph{FFP} are Backus's function-level systems~\cite[Secs.\,11,\,13]{backus78}. The construction assumes these.

At the bottom there are two things, and they are the same thing. A set is its characteristic function, so for a population $P$ the membership question $x \in P$ and the application $P\,x$ are one act: \textbf{membership is application}. The fact base is therefore not data beside a program; it \emph{is} the function space, and Backus's representation function $\rho$~\cite[Sec.\,13.3]{backus78}, which maps an object to the function it denotes, is the reflection exposing a fact as the function it already is. A fact type $\langle\mathit{CONS}, s_1, \ldots, s_n\rangle$~\cite[Sec.\,11.2.4]{backus78} is a constructor of roles; populate the roles and the resulting fact is resolved by looking up its type:
\begin{align}
(\rho\langle x_1, \ldots, x_n\rangle)\!:\!y = (\rho\,x_1)\!:\!\langle\langle x_1, \ldots, x_n\rangle, y\rangle. \label{eq:metacomp}
\end{align}
This is metacomposition~\cite[Sec.\,13.3.2]{backus78}. It is the only mechanism in the paper, and every later view (a constraint, a transition, a link, an API response) is an instance of it. The combining forms it composes are also Backus's~\cite[Sec.\,11.2.4]{backus78}: composition $f\circ g$, the selectors, the equality test $\mathit{eq}$, the constant $\bar{x}$, and the empty sequence $\varphi$.

\smallskip\noindent Backus builds an AST system from three parts~\cite[Sec.\,14.3]{backus78}: an applicative subsystem (an FFP system), a state $D$ that is its set of definitions, and transition rules carrying inputs to outputs and $D$ to $D'$. The state is a sequence of cells with fetch $\uparrow\!n\!:\!D$ and store $\downarrow\!n\!:\!\langle x, D\rangle$~\cite[Secs.\,13.3.4,\,14.3]{backus78}. One cell is named $\mathit{FILE}$ and ``the system maintains'' its contents, but Backus declines to structure them: ``we have not said how the system's file, queries or updates are structured''~\cite[Sec.\,14.4.4]{backus78}. AREST fills exactly that hole.

\begin{definition}[AREST]\label{def:arest}
An \emph{Applicative REpresentational State Transfer} system is a Backus AST system~\cite[Sec.\,14]{backus78} whose $\mathit{FILE}$ cell contains a population $P$ (Definition~\ref{def:pop}) of a schema $S$ (Definition~\ref{def:schema}), and whose definition cells $\mathit{DEFS}$ hold the FFP objects~\cite[Sec.\,13]{backus78} compiled from FORML\,2 readings together with those registered by the runtime. REST operations are applications of the system function~(\ref{eq:sys}).
\end{definition}

A small declaration fixes the picture. In FORML\,2~\cite{halpin10}, each reading is one elementary fact:
\begin{lstlisting}
Order(.OrderId) is an entity type.
Customer(.Name) is an entity type.
Order is placed by Customer.
Each Order is placed by exactly one
  Customer.
Customer ships Order.
State Machine Definition 'Order' is for
  Noun 'Order'.
Status 'In Cart' is initial in
  State Machine Definition 'Order'.
Transition 'place' is from
  Status 'In Cart'.
Transition 'place' is to
  Status 'Placed'.
Transition 'place' is triggered by
  Fact Type 'Customer places Order'.
Transition 'ship' is from
  Status 'Placed'.
Transition 'ship' is to
  Status 'Shipped'.
Transition 'ship' is triggered by
  Fact Type 'Customer ships Order'.
\end{lstlisting}
Each reading is atomic, and each maps to a column: the entity references to keys, the binary fact types to foreign keys, the uniqueness reading to a restriction, and the transition facts to the machine's rows. The decomposition into atomic facts \emph{is} the mapping to the relational schema, and together they compile to a table, a foreign key, a uniqueness restriction, and a transition that fires when its trigger fact enters $P$. A \texttt{POST /orders} request creates an Order and returns its status with the actions available from it; following the \texttt{place} action advances the machine to \texttt{Placed}, after which the representation offers \texttt{ship} and no longer \texttt{place}.

\smallskip\noindent\textbf{Finite, therefore algorithmic.} The population is a finite set. This is not a modeling convenience but the precondition of computation: an algorithm is finite, so whatever an application computes lives in the finite fragment. Finiteness is meant per operation. Each system step terminates over the current finite $P$, while the event stream is unbounded over time, so the object stays algorithmic at every point. Finiteness earns the guarantees the rest of the paper reads off: evaluation is finite model-checking, so it is decidable; the reflection of~(\ref{eq:metacomp}) is consistent without Scott's domains, because the function space over a finite set is itself a finite set; and derivation reaches a least fixed point in finitely many steps (Lemma~\ref{lem:finite}). The place where this stops, namely the arbitrary registered functions of Definition~\ref{def:reg} whose termination is in general undecidable, is the only point at which general computation re-enters, and Corollary~\ref{cor:boundary} makes it an enumerable fact set.


\section{ORM over Backus's AST}\label{sec:mapping}

We fix the objects the rest of the paper quantifies over by reading them off ORM 2 as NORMA implements it~\cite{halpin08,norma}.

\begin{definition}[Schema]\label{def:schema}
A \emph{vocabulary} is a set of object types, each a \emph{value type} (self-identifying, typed by a data type) or an \emph{entity type} (identified by a preferred uniqueness constraint over one role, simple, or several, compound), together with a set $F$ of fact types, each $\mathit{arity}(f)$ roles played by object types. An entity's identifier is \emph{auto-generated} iff its identifying data type is auto-generating (counter, UUID, timestamp, or surrogate) and \emph{supplied} otherwise. $\mathit{Val}$ is the union of the value-type domains and the entity identifiers. A \emph{schema} $S$ comprises $F$, a constraint set $C_S$ (uniqueness, mandatory, frequency, ring, value-comparison, subset, equality, exclusion, value, and cardinality constraints, each alethic or deontic~\cite{norma}), a derivation-rule set $R_S$ (Definition~\ref{def:derive}), a set of state machines, and the reference schemes. $S$ is the compiled content of $\mathit{DEFS}$.
\end{definition}

\begin{definition}[Population]\label{def:pop}
A \emph{population} of $S$ is a finite set
\[
P \;\subseteq\; \textstyle\bigcup_{f\in F}\,\{f\}\times\mathit{Val}^{\mathit{arity}(f)},
\]
with finite \emph{active domain} $\mathit{adom}(P)$, the set of values occurring in $P$. A ground fact $g$ is \emph{true} in $P$ if $g\in P$, \emph{false} if its paired negation fact is in $P$, and \emph{unknown} otherwise; under the closed-world assumption on a noun, unknown collapses to false. Membership is the characteristic function of $P$, so $g\in P$ and $P\,g$ are one act.
\end{definition}

\noindent Entity and fact types populate $\mathit{FILE}$, while constraints and derivations are relational restrictions and compositions over $P$, and the retrieval operators are Codd's adequate $\theta_1$: projection, natural join, tie, and restriction~\cite[Sec.\,2.2]{codd70}. We write restriction as $\mathit{Filter}(p)\!:\!X$, the elements of a relation $X$ satisfying a predicate $p$; this is Codd's $\theta$-restriction~\cite[Sec.\,2.3.5]{codd72}, with constants entering as literal relations. The equality patterns used below, compositions of $\mathit{eq}$ with selectors and constants, reduce to the restriction of $\theta_1$, while value ranges take the inequality~$\theta$. Indeed every constraint of Definition~\ref{def:schema} compiles to a restriction whose predicate falls in one of two families, a cardinality count against declared bounds or a membership test against a target population (the comparison constraints taking the inequality~$\theta$), with polarity the only parameter separating symmetric from asymmetric and subset from exclusion. ORM elementary facts are in fifth normal form by construction~\cite{halpin08}, so the named relations are the cells themselves and navigation needs no separate query language. Each leg of the map is now discharged by the formalism it instantiates.

\begin{definition}[Fragment]\label{def:fragment}
$R$ is the set of FORML\,2 readings that declare the constructs of Definition~\ref{def:schema}: object-type and reference-scheme declarations, elementary fact-type readings, the listed constraints, projective derivation readings (Definition~\ref{def:derive}), and state-machine readings whose trigger is an elementary fact type. Pronoun-correlated clauses and nested objectification lie outside $R$ and are rejected. A declared name may not contain a formal item of the grammar as a substring; the compiler refuses such a name at ingestion, and the determinism of Proposition~\ref{prop:spec} rests on this hypothesis.
\end{definition}

\begin{proposition}[Specification and executable]\label{prop:spec}
$\mathit{parse}$ is total on $R$, $\mathit{compile}\circ\mathit{parse}$ is well defined, and $\mathit{nf}=\mathit{verbalize}\circ\mathit{compile}\circ\mathit{parse}$ is idempotent with $\mathit{nf}(r)\sim r$ for the kernel equivalence $\sim$ of $\mathit{compile}\circ\mathit{parse}$, where the executable of $r$ is $\rho(\mathit{compile}(\mathit{parse}(r)))$.
\end{proposition}
\begin{proof}
Each sentence of $R$ falls in one keyword-delimited family and, under the name hypothesis of Definition~\ref{def:fragment}, parses deterministically, and NORMA exhibits the round trip for all constraint kinds~\cite{norma}, so $\mathit{parse}$ is total and $\mathit{compile}\circ\mathit{parse}$ is a function, injective on $R/{\sim}$ by construction of $\sim$. $\mathit{verbalize}$ emits the primary reading of a compiled object~\cite{halpin06}, a sentence of $R$ that re-parses to that object, so $\mathit{nf}\circ\mathit{nf}=\mathit{nf}$ and $\mathit{nf}(r)\sim r$. Executability is $\rho$~\cite[Sec.\,13.4]{backus78}.
\end{proof}

\noindent A state machine is itself a set of facts (a status, its transitions, and the trigger fact type of each), and advancing it is one AST step, not a second machine. Backus's transition is single: on input $x$ the system forms $(\mathit{SYSTEM}\!:\!x)$, evaluates it under the current definitions, and obtains $\mu(\mathit{SYSTEM}\!:\!x)=\langle o,d\rangle$ with $o$ the output and $d$ the next state~\cite[Sec.\,14.3.1]{backus78}; the state is frozen during evaluation~\cite[Sec.\,14.6]{backus78}. Where Backus's subsystem branches on a $\mathit{KEY}$ cell through five clauses~\cite[Sec.\,14.4.2]{backus78}, AREST routes on the addressed entity,
\begin{align}
\mathit{SYSTEM}\!:\!x = (\rho\,(\uparrow\!\mathit{entity}(x)\!:\!D))\!:\!\uparrow\!\mathit{op}(x), \label{eq:sys}
\end{align}
so new operations and new entity types extend $D$ without disturbing one another.

\begin{definition}[Command]\label{def:stages}
For schema $S$, input $I$, and population $P$,
\[
\begin{aligned}
\mathit{resolve}_S &: I\times P \to P, &
\mathit{derive}_S &: P\to P,\\
\mathit{validate}_S &: P\to P\times\mathcal{P}(\mathit{Val}^{*}), &
\mathit{emit}_S &: P\times\mathcal{P}(\mathit{Val}^{*})\to O,
\end{aligned}
\]
where $\mathit{resolve}_S$ adds the entity and fact instances named by $I$, minting a fresh identifier exactly when the reference scheme is auto-generating; $\mathit{derive}_S=\mathit{lfp}(F_S,\cdot)$ (Definition~\ref{def:derive}); $\mathit{validate}_S(P)=(P,V)$ with $V$ the violation set (Definition~\ref{def:violation}); and $\mathit{emit}_S$ builds the representation $O$. A \textsc{create} command is
\begin{align}
\mathit{create}(I)=\mathit{emit}_S\circ\mathit{validate}_S\circ\mathit{derive}_S\circ\mathit{resolve}_S(I,\cdot), \label{eq:create}
\end{align}
committing the derived population iff $V$ has no alethic violation, otherwise leaving $D$ unchanged.
\end{definition}

\begin{definition}[Violation]\label{def:violation}
For a constraint $c\in C_S$, $V_c=(\rho\,c)\!:\!P$ is the finite set of bindings that offend $c$, and $V=\bigcup_{c\in C_S}V_c$. An alethic $c$ rejects the commit when $V_c\neq\varphi$; a deontic $c$ warns and commits. The message returned is the canonical reading of $c$ (Proposition~\ref{prop:spec}).
\end{definition}

\begin{definition}[Derivation rules]\label{def:derive}
A derivation rule in $R_S$ is a role path projected onto a head: each derived role is bound to a path variable, to a calculated value (a function of finitely many bound values, an aggregate reducing a finite bag to one scalar), or to a constant~\cite{norma}. A rule is \emph{fully derived} ($*$), \emph{derived and stored} ($**$, materialized), or \emph{semi-derived} ($+$, also directly assertable). Heads are \emph{projective}: no derivation rule introduces a fresh entity. The immediate-consequence operator is $F_S(P)=P\cup\{\,$heads derivable from $P$ by one rule$\,\}$. Entity introduction is confined to $\mathit{resolve}_S$ and to state-transition rules, each guarded by a positive event~\cite{norma}.
\end{definition}

\begin{proposition}[Single transition]\label{prop:onestep}
The live state-machine step is the AST transition $\mu(\mathit{SYSTEM}\!:\!x)=\langle o,d\rangle$. Reconstruction $\mathit{machine}(s_0,E)=\mathit{foldl}\;\mathit{transition}\;s_0\;(\mathit{order}_\tau E)$ is a $\rho$-application over the event facts, not a transition.
\end{proposition}
\begin{proof}
A triggering event is the input $x$ and the current status a fact in $D$, and folding it forward is one AST step, with $D$ frozen throughout~\cite[Secs.\,14.3.1,\,14.6]{backus78}. The function $\mathit{machine}$ is an FFP expression over the event facts, its $\mathit{foldl}$ derived from Backus's $\mathit{while}$~\cite[Sec.\,11.2.4]{backus78}, evaluated within such a step, so it is a $\rho$-application (Proposition~\ref{prop:derive}) used for migration and audit; it alone orders by each event's occurrence timestamp $\tau$, while the live step takes events in arrival order. The two orders are Halpin's valid time and transaction time~\cite[Sec.\,13.6]{halpin08}: $\tau$ is a role of the event fact itself, ordinary data, so $\mathit{order}_\tau$ is derivable from $E$, whereas arrival order is the log's and is no fact of the domain.
\end{proof}

\begin{lemma}[Finiteness]\label{lem:finite}
If no value-introducing rule of $R_S$ lies on a cycle of the derivation dependency graph, then for every finite $P$ the least fixed point $\mathit{lfp}(F_S,P)$ exists, equals the least model of $R_S$ above $P$, and is reached by iteration in finitely many steps.
\end{lemma}
\begin{proof}
By Definition~\ref{def:derive} a head is projective, so $F_S$ introduces no entity. The value-introducing rules, lying on no cycle, form a directed acyclic subgraph and produce finitely many values, each a function of finitely many inputs; let $\hat{P}$ be the resulting finite extension of $\mathit{adom}(P)$. Every remaining rule introduces no value, so $F_S$ is monotone over the finite powerset of facts above $\hat{P}$. The least fixed point exists by Knaster--Tarski~\cite{tarski55}. It equals the least model because each negated role path reads only settled facts and computes a finite-set anti-join whose value is fixed across the derivation rounds, so $F_S$ remains monotone~\cite{vanemden76} under negation. It is reached by iteration in at most $|P_{\max}|-|P|$ steps~\cite{kleene52}, where $P_{\max}$ is that finite fact space. The one input-unbounded source of fresh values is an auto-generated reference scheme in $\mathit{resolve}_S$ or a state-transition rule, which mints one surrogate per guarded step, outside $F_S$.
\end{proof}

\begin{corollary}[The hypothesis is a query]\label{cor:finitecheck}
The hypothesis of Lemma~\ref{lem:finite} is decidable by a restriction over $D$ itself. Which fact types a rule reads and which it derives are among the schema facts describing $\mathit{DEFS}$, and a rule's body is the $\mathit{impl}$ of its definition tuple (Definition~\ref{def:reg}), so the dependency graph and the bodies are data. Value introduction is syntactic: a body applies a definition with $s_{\mathit{origin}}=\mathit{registered}$ (the boundary~(\ref{eq:boundary})) or a value-constructing base operation (arithmetic, $\mathit{length}$, dynamic application); every other operation rearranges atoms already in $\mathit{adom}(P)$ or quoted in the rule. The check --- no such rule on a dependency cycle --- is finitely many reachability queries, evaluated when $\mathit{DEFS}$ changes (Section~\ref{sec:boundary}) and refused like any alethic violation, while acyclic invention remains admissible by the proof of Lemma~\ref{lem:finite}.
\end{corollary}

\begin{theorem}[Completeness of state transfer]\label{thm:complete}
Let $S$ satisfy the hypothesis of Lemma~\ref{lem:finite}. For input $I$ and state $D$, $\mathit{create}(I)$ (Definition~\ref{def:stages}) yields $\langle o,D'\rangle$ with $P'=\mathit{resolve}_S(I,P)$, $P''=\mathit{lfp}(F_S,P')$, $V=\bigcup_{c\in C_S}(\rho\,c)\!:\!P''$, and $o$ the representation of $(P'',V,\mathit{links})$; and $D'=D[\mathit{FILE}\mapsto P'']$ if $V$ has no alethic violation, else $D'=D$.
\end{theorem}
\begin{proof}
$P''$ exists and is finite by Lemma~\ref{lem:finite}. $\mathit{validate}_S$ applies each $c\in C_S$ as a restriction over $P''$ (Definition~\ref{def:violation}), and $\mathit{emit}_S$ builds $o$ from $P''$, $V$, and the links (Theorem~\ref{thm:hateoas}). The commit rule is Definition~\ref{def:stages}.
\end{proof}

\begin{theorem}[HATEOAS as generated projection]\label{thm:hateoas}
For an entity $e$, call a control \emph{valid} iff it is an outgoing transition from $\mathit{status}(e)$, or its target fact type places $e$ in one role and its remaining roles are reachable through the uniqueness structure. Then
\begin{align}
\mathit{links}(e)=\mathit{nav}(e)\cup\mathit{transitions}(\mathit{status}(e)) \label{eq:links}
\end{align}
is a $\theta_1$ expression over $P$ and $S$, and it is \emph{complete}: it contains every valid control and only valid controls.
\end{theorem}
\begin{proof}
$\mathit{transitions}(s)$ projects the transition facts restricted to $s$, and $\mathit{nav}(e)$ projects, for each fact type on $e$, the peer control (spanning unique constraint), the child controls (a non-spanning constraint makes the remaining roles children of the constrained key), and the related collections. Each is a projection over a restriction composing $\mathit{eq}$ with selectors and constants, an equality $\theta$-restriction~\cite[Sec.\,2.3.5]{codd72}, hence within Codd's $\theta_1$~\cite[Sec.\,2.2]{codd70}. The validity criterion above is exactly the generation rule, so a control is emitted iff it is valid, which is completeness.
\end{proof}

\noindent \emph{Generating} this set is the novel step. Fielding~\cite{fielding00} fixed hypermedia as a constraint but left the controls for the server author to write by hand, and prior formal treatments model the \emph{client}'s traversal as a machine over the representations it receives~\cite{zuzak11}. Equation~(\ref{eq:links}) works the other side of the wire: the set is complete and current as a function of $P$ and $S$, there are no hand-written links and no undocumented endpoints, and so a client, or an agent reading the API, has no undocumented affordance to hallucinate. A transition graph may cycle; the discipline that keeps every entity live is itself a reading, the deontic obligation that each cycle carry some exit transition, which ensures liveness without demanding structural acyclicity.

\begin{proposition}[Derivability]\label{prop:derive}
Every value in the representation $\mathit{repr}(e)$, namely the selectors on $e$'s facts, the derived facts, the constraint violations, and $\mathit{links}(e)$, is $(\rho\,f)\!:\!P$ for some object $f$.
\end{proposition}
\begin{proof}
Selectors, derivation rules, and constraints are $\rho$-applications by construction, and the links are $\theta_1$ (Theorem~\ref{thm:hateoas}), themselves $\rho$-applications. No value arises outside $\rho$.
\end{proof}

\begin{corollary}[No middleware]\label{cor:middleware}
Authentication, authorization, validation, rate limiting, and transformation are each a restriction, a derivation, or a fact over $P$, never a layer outside $\rho$.
\end{corollary}
\begin{proof}
By Proposition~\ref{prop:derive} every value is a $\rho$-application. Authorization is a derivation (``a User may access a Domain iff the User belongs to an Organization that manages it''), validation is $\mathit{validate}_S$ (Theorem~\ref{thm:complete}), a rate limit is a cardinality constraint over timestamped request facts, and transformation is composition.
\end{proof}

\noindent The claim is semantic, not topological: a deployment may still run proxies, queues, caches, and gateways, but their application-level policy is denoted inside $P$ rather than specified outside the object. What is usually a stack of request-intercepting services is, here, a few more readings.

\begin{corollary}[Streaming]\label{cor:stream}
A subscription is a $\rho$-application that has not yet been evaluated against the current $D$, and an external event is a fact entering $P$ through $\downarrow$.
\end{corollary}
\begin{proof}
Storing into a cell with $\downarrow$ changes $D$, so every $\rho$-application over that cell re-evaluates against the new state (Proposition~\ref{prop:derive}), and a subscriber is exactly such an application awaiting its next evaluation. A webhook, a queue message, and a sensor reading enter $P$ by the same $\downarrow$, so externally fired and fact-fired updates are indistinguishable to the evaluator.
\end{proof}

\noindent No separate pub-sub layer, event bus, or callback registry is required.

\smallskip\noindent\textbf{Platform binding.} A runtime registers its own functions into $\mathit{DEFS}$, so a fact applied to one of them yields the corresponding effect:
\begin{align*}
(\rho\,\mathit{fact})\!:\!\mathit{render} &\to \mathit{widget}, \\
(\rho\,\mathit{fact})\!:\!\mathit{httpFetch} &\to \mathit{response}, \\
(\rho\,\mathit{fact})\!:\!\mathit{upsert} &\to D'.
\end{align*}
A browser registers rendering functions, a server registers $\mathit{httpFetch}$ and $\mathit{upsert}$, and one $\mathit{SYSTEM}$ serves browser, server, and storage by varying $\mathit{DEFS}$ rather than the logic. Binding a user interface is then registering a $\mathit{render}$ function, so a fact renders itself. Functions that touch external state run during $\mathit{resolve}_S$, and those that consume the representation run after $\mathit{emit}_S$, which keeps $\mathit{derive}_S$ pure over $P$.

\smallskip\noindent $\rho$ and the whole-state accessor $\rho\mathit{DEFS}$ are Backus's~\cite[Secs.\,13.3,\,14.3.3]{backus78}, and the latter grants a program access to all of $D$ ``for any purpose, including the essential one of computing the successor state.'' Backus represents $D$ as an object precisely because ``in AST systems we shall want to transform $D$ by applying functions to it''~\cite[Sec.\,13.5]{backus78}; this is the licence Section~\ref{sec:boundary} uses for self-modification.

\smallskip\noindent Deletion needs no special operation: an entity that reaches a status with no outgoing transitions has $\mathit{links}(e)=\varphi$ by Theorem~\ref{thm:hateoas} and is excluded from query results by restriction. This is logical deletion; physical reclamation is a compaction that preserves the restricted population $\rho$ observes.

\smallskip\noindent\textbf{Negation.} ORM's negation is open-world and explicit. NORMA admits it inside derivation role paths, where a step, a root, or a branch may be negated~\cite{norma}, under the three-valued reading of Definition~\ref{def:pop}, verbalized ``it is not true that,'' ``it is known to be false that,'' and ``it is not known to be false that.'' An epistemic falsity, verbalized ``it is known to be false that,'' enters $P$ as an explicit negation fact and is never inferred from absence. A negated role path is an inference from absence. It evaluates to a finite-set anti-join, the mirror of Restrict, over the settled facts it reads. Lemma~\ref{lem:finite} is undisturbed because that anti-join is a single finite-set operation of fixed value over the settled population. The epistemic operators are decidable queries against the settled population, not rules that grow it. The one groundedness condition is on state-transition rules: an add or delete may not occur under negation or disjunction, and each disjunctive branch must carry a positive event~\cite{norma}, so a step's \emph{effect} is positive and negation guards the condition and never the head.


\section{Cells, Tenancy, and Self-Similarity}\label{sec:cells}

RMAP~\cite{halpin08} assigns each entity its own cell, the 3NF row of facts depending on its key, so $D$ is a sequence of cells and, by~\cite[Sec.\,14.7]{backus78}, ``a cell in one store may contain another entire store.''

\begin{definition}[Cell isolation]\label{def:iso}
At most one step may write a given cell of $D$ at a time, and steps writing disjoint cells run concurrently.
\end{definition}

\noindent The recalculation a write forces is bounded to the entity's cell and the role-player cells its constraints can reach, a scope the schema fixes at compile time. A constraint whose scope spans cells imposes an obligation: commits touching a shared scope must serialize. The cardinality family discharges it at the constrained key itself, a single writer per scope key that generalizes Definition~\ref{def:iso}.

\smallskip\noindent\textbf{Consistency and availability.} The choice a network partition forces, Brewer's consistency versus availability~\cite{gilbert02}, is already made per noun by the modal and world-assumption declarations. An alethic constraint over a closed-world noun with a single writer is CP: under partition the commit is refused rather than risk the invariant. A deontic constraint over an open-world noun is AP: the local step accepts optimistically, warns, and reconciles at commit, where $\mathit{validate}_S$ (Theorem~\ref{thm:complete}) runs against the authoritative $P$. The posture is chosen by the schema rather than fixed globally, and it tunes with a constraint's \emph{slack}: a cardinality constraint far from its bound needs no coordination and stays available, while one at its bound serializes at the constrained key (Definition~\ref{def:iso}). Local evaluation is optimistic feedback and never a security boundary, because acceptance is decided at commit. Among peers sharing $P$, an event is accepted exactly when it adds no alethic violation, so the constraint set is itself the consensus predicate, with safety from deterministic replay and liveness from the single-writer cell. Beyond two peers the shared event log needs a total order; among anonymous peers a hash-chained log supplies it, a signature carries identity, and a schema modification is admitted only under a deontic authorization constraint, so ordering, validity, identity, and permission compose from the formalism already present, each peer validating independently.

\smallskip\noindent\textbf{Tenancy.} A tenant is this mechanism one level up: a cell whose contents is an entire store, so $P$ is partitioned into per-tenant blocks.

\begin{proposition}[Tenant isolation]\label{prop:tenant}
For stores $D_a$ and $D_b$ in sibling tenant cells, no address well-formed in $D_a$ denotes a cell of $D_b$. Isolation is preservation of addressability under $\uparrow$ and $\downarrow$.
\end{proposition}
\begin{proof}
$D_b$ is the contents of a cell that is not a cell of $D_a$, and $\uparrow$ and $\downarrow$ resolve only cells of their store argument~\cite[Secs.\,13.3.4,\,14.3]{backus78}, so no fetch or store expression formed over $D_a$ denotes a cell of $D_b$.
\end{proof}

\noindent Isolation is therefore a property of the shape of the state rather than a check: wrong-tenant access is not forbidden but unaddressable, and the row-level perimeter usually built for this has nothing to do.

\smallskip\noindent\textbf{Sub-tenancy.} The containment recurses. A tenant's store may itself hold tenant cells, each an entire store, to any finite depth, so the tenant tree is a tree of nested sub-stores. Every node is a full instance, since Corollary~\ref{cor:closure} holds per store, so a tenant carrying its own $\mathit{DEFS}$ is an application builder who may in turn have tenants, while one inheriting its parent's is the ordinary data-isolated case. Visibility follows containment: a parent reaches into its children because their stores are cells in its own, and a child cannot address upward or sideways (Proposition~\ref{prop:tenant}). This is the isolation and visibility model of a platform-of-platforms, with no access machinery beyond the nesting.

Two recursions issue from one decision. Because Backus made $D$ a first-class object, it can be \emph{transformed} (the system rewrites its own schema, Section~\ref{sec:boundary}) and it can \emph{contain itself} (the nested stores above). The system evolves itself and holds isolated copies of itself, and both fall out of the same move.


\section{Closure and the Enumerable Boundary}\label{sec:boundary}

Self-modification is an ordinary step: the addressed entity is $\mathit{DEFS}$ and the operation is $\mathit{compile}\circ\mathit{parse}$, with the new objects entering through $\downarrow\!\mathit{DEFS}$.

\begin{corollary}[Closure]\label{cor:closure}
A self-modifying step changes only $\mathit{DEFS}$ and the schema facts describing it; the evaluator, parser, compiler, verbalizer, and registered functions are unchanged. After a step whose operation is $\mathit{compile}\circ\mathit{parse}$ on readings $R'\subseteq R$, Definitions~\ref{def:schema}--\ref{def:derive}, Propositions~\ref{prop:spec} and~\ref{prop:derive}, Lemma~\ref{lem:finite}, and Theorems~\ref{thm:complete} and~\ref{thm:hateoas} hold for every later step over $D'$.
\end{corollary}
\begin{proof}
No statement's argument depends on $D$ being fixed: Proposition~\ref{prop:spec} rests on the grammar and the kernel quotient, while the others range over $P$ and $S$, which now include the new content. Ingestion is itself a $\mathit{create}$ step, so it is subject to $\mathit{validate}_S$ (Theorem~\ref{thm:complete}): a schema whose alethic constraints the current $P$ violates is rejected, so a migration stages as derivations or deontic rules until $P$ complies.
\end{proof}

\noindent This is what makes a tenant's own schema (Section~\ref{sec:cells}) safe, and it is the first of the two recursions. The second is the boundary at which the guarantees stop.

\begin{definition}[Registered function]\label{def:reg}
A definition in $\mathit{DEFS}$ is a tuple $\langle\mathit{name},\mathit{dom},\mathit{cod},\mathit{origin},\mathit{impl}\rangle$ with $\mathit{origin}\in\{\mathit{compiled},\mathit{registered}\}$. A \emph{compiled} definition has $\mathit{impl}=\rho(o)$ for a compiled object $o$, total and decidable over finite $P$. A \emph{registered} definition has $\mathit{impl}$ supplied by the host runtime and is in general partial.
\end{definition}

\begin{corollary}[Enumerable boundary]\label{cor:boundary}
The informal surface of the system is the restriction
\begin{align}
\mathit{Filter}(\mathit{eq}\circ[s_{\mathit{origin}},\overline{\mathit{registered}}])\!:\!\mathit{DEFS}, \label{eq:boundary}
\end{align}
a $\rho$-application (Proposition~\ref{prop:derive}), and it coincides with the decidability frontier.
\end{corollary}
\begin{proof}
By Definition~\ref{def:reg} a compiled definition is finite reduction over a finite population, so it is decidable and total, whereas a registered definition is arbitrary host code whose termination is in general undecidable. The restriction~(\ref{eq:boundary}) selects exactly the registered definitions, which is exactly the line at which Turing-complete computation re-enters.
\end{proof}

\noindent A noun backed by an external system sits on this line: its population is fetched by a registered function, and its facts enter under the open-world assumption~\cite{halpin08}. A deontic constraint over such facts is sound but not complete: a reported violation is genuine, while under the open world the absence of one guarantees nothing. Informality is not removed but localized to a queryable fact set, and the trusted base (the parser, the compiler, the verbalizer, and the registered functions) is precisely what~(\ref{eq:boundary}) returns.

\smallskip\noindent A registered definition that shadows a compiled definition of the same name, and is observationally equal to it, contributes no informality: its meaning is the compiled definition's, decidable by Definition~\ref{def:reg}, and the shadow may be dropped without changing any value. Eq.~(\ref{eq:boundary}) is therefore read over the unshadowed registered definitions, so an optimizing runtime does not widen the boundary. The licence for such optimization is Backus's algebra of programs~\cite[Sec.\,12.2]{backus78}: the laws are equations between the forms the compiled objects represent, so an object may be transformed, ahead of time or at registration, into any equivalent of itself.


\section{Conclusion}

The gap between domain knowledge and running software, where requirements drift and production breaks, is usually treated as inevitable. It is avoidable. An application is a finite mathematical object: Backus's state machine over Codd's relations and ORM's facts, with every value a $\rho$-application over $P$ (Proposition~\ref{prop:derive}). Software opens the gap only by pretending to be something other than the object it already is. Stating it plainly closes the gap, because the schema is the database, the readings are the executable, the links are the population, and the workflow is the transition, and none of them was ever separate. Fielding's remaining constraints~\cite{fielding00} follow: statelessness because each step is a pure transition on $D$, cacheability because a representation is a function of $P$, layering because cells are location-independent, and code-on-demand because the readings that extend the system are themselves data. The operational surface maps into the object the same way: versioning is the event stream, migration is ingestion staged by Corollary~\ref{cor:closure}, and auditability is the derivation chain, recorded and answerable on demand. What remains outside the object is enumerable (Corollary~\ref{cor:boundary}), and what is inside is finite (Lemma~\ref{lem:finite}), so it is decidable, and so it is, for once, something a machine can be trusted to have gotten right.

\section*{Acknowledgments}

Claude (Anthropic) assisted with implementation and manuscript preparation. The architectural decisions and the composition of FFP/AST with REST are the author's.

\bibliographystyle{plain}
\begin{thebibliography}{13}

\bibitem{backus78}
J. Backus, ``Can Programming Be Liberated from the von Neumann Style? A Functional Style and Its Algebra of Programs,'' \emph{Commun.\ ACM}, 21(8):613--641, 1978.

\bibitem{codd70}
E.F. Codd, ``A Relational Model of Data for Large Shared Data Banks,'' \emph{Commun.\ ACM}, 13(6):377--387, 1970.

\bibitem{codd72}
E.F. Codd, ``Relational Completeness of Data Base Sublanguages,'' in \emph{Data Base Systems}, Courant Computer Science Symposia 6, Prentice-Hall, 1972, pp.~65--98.

\bibitem{halpin08}
T. Halpin and T. Morgan, \emph{Information Modeling and Relational Databases}, 2nd ed., Morgan Kaufmann, 2008.

\bibitem{halpin10}
T. Halpin and J.P. Wijbenga, ``FORML 2,'' in \emph{Enterprise, Business-Process and Information Systems Modeling (EMMSAD)}, LNBIP 50, pp.~247--260, 2010.

\bibitem{halpin06}
T. Halpin and M. Curland, ``Automated Verbalization for ORM 2,'' in \emph{OTM Workshops}, pp.~1181--1190, 2006.

\bibitem{vanemden76}
M.H. van Emden and R.A. Kowalski, ``The Semantics of Predicate Logic as a Programming Language,'' \emph{J.\ ACM}, 23(4):733--742, 1976.

\bibitem{tarski55}
A. Tarski, ``A lattice-theoretical fixpoint theorem and its applications,'' \emph{Pacific J.\ Math.}, 5(2):285--309, 1955.

\bibitem{kleene52}
S.C. Kleene, \emph{Introduction to Metamathematics}, North-Holland, 1952.

\bibitem{fielding00}
R.T. Fielding, ``Architectural Styles and the Design of Network-based Software Architectures,'' Ph.D. dissertation, Univ.\ of California, Irvine, 2000.

\bibitem{zuzak11}
I. Zu\v{z}ak, I. Budiseli\'{c}, and G. Dela\v{c}, ``Formal Modeling of RESTful Systems Using Finite-State Machines,'' in \emph{Proc.\ ICWE}, LNCS 6757, pp.~346--360, 2011.

\bibitem{gilbert02}
S. Gilbert and N. Lynch, ``Brewer's Conjecture and the Feasibility of Consistent, Available, Partition-Tolerant Web Services,'' \emph{ACM SIGACT News}, 33(2):51--59, 2002.

\bibitem{norma}
T.~Halpin and M.~Curland, NORMA (Natural Object-Role Modeling Architect), open-source reference implementation, \url{https://github.com/ormsolutions/NORMA}.

\bibitem{arest}
S.~Lippert, AREST, open-source reference implementation, \url{https://github.com/graphdl/arest}.

\end{thebibliography}

\end{document}