\documentclass[12pt]{article}

\usepackage{amsmath,amssymb,amsthm}
\usepackage{tikz}
\usepackage{tikz-cd}
\usetikzlibrary{positioning}
\usepackage{graphicx}
\usepackage[margin=1in]{geometry}
\usepackage{everypage}
\usepackage{xcolor}
\usepackage{hyperref}
\usepackage[capitalise,noabbrev]{cleveref}
\usepackage{booktabs}
\usepackage{longtable}
\usepackage{tabularx}
\usepackage{array}
\usepackage{ragged2e}
\usepackage{enumitem}
\usepackage{microtype}
\usepackage{listings}
\usepackage{pdflscape}
\usepackage{url}

\hypersetup{
  colorlinks=true,
  linkcolor=blue!45!black,
  citecolor=green!35!black,
  urlcolor=blue!55!black,
  pdftitle={From Categorical Schemas to Physical Plans: Compiling CatDB into Relational, Graph, Document, and Vector Execution},
  pdfauthor={Matthew Long; The YonedaAI Collaboration}
}

\newtheorem{theorem}{Theorem}[section]
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}
\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}
\newtheorem{example}[theorem]{Example}

\newcommand{\prior}{\textsc{supported by prior literature}}
\newcommand{\paperproved}{\textsc{proved in this paper}}
\newcommand{\enghyp}{\textsc{engineering hypothesis}}
\newcommand{\openclaim}{\textsc{open conjecture}}
\newcommand{\specclaim}{\textsc{speculative}}
\newcommand{\CatDB}{\textsc{CatDB}}
\newcommand{\code}[1]{\texttt{#1}}
\newcommand{\status}[1]{\par\noindent{\normalfont\textit{Status.} #1.}\par}
\newcommand{\sem}[1]{\left[\!\left[#1\right]\!\right]}
\newcommand{\Bag}{\mathcal B_{\mathrm{fin}}}
\newcommand{\IR}{\mathsf{IR}}
\newcommand{\Exact}{\mathsf{Exact}}
\newcommand{\Residual}{\mathsf{Residual}}
\newcommand{\Approx}{\mathsf{Approximate}}
\newcommand{\Unsupported}{\mathsf{Unsupported}}
\newcolumntype{L}[1]{>{\RaggedRight\arraybackslash}p{#1}}
\newcolumntype{Y}{>{\RaggedRight\arraybackslash}X}

\setlength{\emergencystretch}{3em}
\setlist{itemsep=0.25em,topsep=0.4em}
\lstset{
  basicstyle=\ttfamily\footnotesize,
  breaklines=true,
  breakatwhitespace=false,
  columns=fullflexible,
  frame=single,
  rulecolor=\color{black!20},
  showstringspaces=false
}

\definecolor{grokgray}{RGB}{110,110,110}
\AddEverypageHook{%
  \ifnum\value{page}=1
    \begin{tikzpicture}[remember picture,overlay]
      \node[
        rotate=90,
        anchor=south,
        font=\Large\sffamily\bfseries\color{grokgray},
        inner sep=0pt
      ] at ([xshift=38pt,yshift=0.52\paperheight]current page.south west)
      {GrokRxiv:2026.07.catdb-physical-compilation\quad
       [\,cs.DB\,]\quad
       23 Jul 2026};
    \end{tikzpicture}
  \fi
}

\title{From Categorical Schemas to Physical Plans:\\
Compiling \CatDB{} into Relational, Graph, Document,\\
and Vector Execution}
\author{Matthew Long \\
\textit{The YonedaAI Collaboration} \\
\textit{YonedaAI Research Collective} \\
Chicago, IL \\
\texttt{matthew@yonedaai.com} $\cdot$ \url{https://yonedaai.com}}
\date{23 July 2026}

\begin{document}
\maketitle

\begin{abstract}
A semantic data layer still has to produce physical work.  If it takes row
execution away from the database engine, it also gives up much of the mature
optimizer it was meant to use.  This paper specifies a provisional compilation
contract for \CatDB{}, a proposed data platform whose schemas and mappings are
immutable, typed, versioned artifacts.  A bounded canonical query passes
through an explicitly directional read mapping and becomes a typed
bag-relational intermediate representation.  The compiler then marks each
backend operation as exact, residual, approximate, or unsupported before it
emits a parameterized realization.  SQLite and PostgreSQL are the first
targets.  Graph, document, RDF, vector, and polystore execution remain future
preservation boundaries, not implemented backends.

The contract includes an immutable query artifact, a finite-bag denotation,
typed path expansion, logical operators, capability manifests, realization
certificates, three distinct cache layers, normalized result equivalence, and
a lineage comparison.  Within the admitted fragment, required scalars and
pure total predicates combine with projection, typed path navigation, and
inner equijoins.  We prove on paper that well-witnessed path expansion
preserves types, an exact compositional lowerer preserves the fragment's
abstract denotation, and a cached artifact can be reused exactly when all
declared semantic and physical dependencies remain unchanged.  These results
belong to the stated mathematical model.  They do not show that a compiler or
backend adapter exists.

The implementation evidence is not present.  The manuscript reports no
\CatDB{} query compiler, query-planner crate, SQLite or PostgreSQL connector,
generated SQL artifact, captured native plan, differential result, performance
result, Haskell query oracle, or Lean query theorem.  The central ``outside the
hot execution path'' claim therefore remains an \enghyp{}.  The evaluation
plan is designed to catch semantic mismatches, silent approximations, cache
errors, row-dependent compilation, and unacceptable overhead.  The candidate
contribution is narrower than a new optimizer.  It would preserve versioned
semantic intent through a capability-checked handoff, while native engines
keep access-path selection, join ordering, and row processing.
\end{abstract}

\tableofcontents

\section{Introduction}
\label{sec:introduction}

\subsection{Plain-language problem}

An analyst asks for customers and their qualifying orders.  One source stores
the relationship as a foreign key.  Another uses a graph edge, while a third
nests the order inside a document.  A semantic layer can give these structures
one typed name, but that name does not execute the query.  The compiler still
has to decide what the backend preserves, what must run elsewhere, and which
requests it cannot answer faithfully.  It also has to make those decisions
without putting a categorical interpreter inside every row scan.

Database engines already handle logical rewrites, access-path selection, join
ordering, pipelining, parallelism, and cost-based choice
\cite{SelingerEtAl1979AccessPath,Graefe1994Volcano,Graefe1995Cascades}.
Federated systems, mediators, adapters, and ontology-based access already
rewrite queries across heterogeneous sources
\cite{ShethLarson1990Federated,Wiederhold1992Mediators,BegoliEtAl2018Calcite,CalvaneseEtAl2017Ontop}.
\CatDB{} should not rename that work and present it as a categorical
contribution.  The systems question here is smaller: can typed schema mappings
provide a stable semantic boundary before a conventional backend optimizer
takes control?

The proposed boundary is:
\[
\boxed{
\begin{array}{c}
\text{immutable schema, mapping, and query artifacts}\\
\downarrow\\
\text{typed path expansion and semantic normalization}\\
\downarrow\\
\text{capability-checked logical realization}\\
\downarrow\\
\text{parameterized backend statement}\\
\downarrow\\
\text{native physical plan and row execution}.
\end{array}}
\]
\CatDB{} would own the first three stages.  SQLite, PostgreSQL, or another
selected engine would own most of the last two.  The realization must leave
enough evidence to explain that handoff, invalidate caches correctly, and
compare the result with an independent evaluator.

\subsection{Research question and central hypothesis}

The research question is:

\begin{quote}
\emph{Can a bounded query over a categorical schema be compiled through
versioned mappings into backend-native execution while preserving its
declared semantics and keeping semantic compilation outside the per-row hot
path?}
\end{quote}

The central hypothesis is written so that an implementation can disprove it:

\begin{quote}
A bounded \CatDB{} query can be expanded through immutable typed mappings,
lowered into a capability-checked logical realization, and emitted as
parameterized SQLite or PostgreSQL SQL, with ordinary database operators
executing rows and no \CatDB{} semantic callback or row-dependent compilation
for a fixed query shape.
\end{quote}

The hypothesis does not make compilation free or every query pushable.  It
does not give SQLite and PostgreSQL identical semantics, and one logical plan
need not determine one native physical plan.  Graph, document, RDF, and vector
semantics also do not become lossless relational operators by assumption.

\subsection{Contributions}

The provisional specification has seven parts.

\begin{enumerate}
  \item It defines immutable query, mapping, capability, policy, and
  realization artifacts, with exact dependency identities rather than a
  single opaque plan key.
  \item It gives a typed finite-bag semantics for a first query fragment:
  required scalar fields, pure total predicates, projection, path navigation,
  and inner equijoins.
  \item It separates semantic expansion from backend realization and requires
  each operation to receive one of four dispositions:
  \(\Exact\), \(\Residual\), \(\Approx\), or \(\Unsupported\).
  \item It supplies paper proofs for type preservation, abstract exact-lowering
  preservation, and dependency-complete cache reuse.
  \item It describes separate SQLite and PostgreSQL contracts, including
  typing, constraints, prepared statements, native-plan evidence, and
  invalidation boundaries.
  \item It provides a preservation matrix for graph, document, RDF, vector,
  Arrow, Substrait, and polystore boundaries without claiming those backends
  are implemented.
  \item It gives an experiment and reproducibility contract whose failure
  conditions include semantic mismatch, silent approximation, cache
  confusion, and per-row compiler work.
\end{enumerate}

\subsection{Evidence labels}

We use the following labels throughout:

\begin{itemize}
  \item \prior{} means that a cited primary paper, standard, or official
  backend document establishes the referenced background result or facility.
  \item \paperproved{} means that this manuscript contains a complete argument
  under explicit assumptions.  It does not mean machine-checked.
  \item \enghyp{} means a proposed design or measurable systems claim for
  which the required implementation evidence does not yet exist.
  \item \openclaim{} means a question for which neither this paper nor the
  current artifacts supply a proof or decisive experiment.
  \item \specclaim{} marks a possible extension outside the committed initial
  profile.
\end{itemize}

No statement in this paper is labeled machine-checked or experimentally
supported.

\section{Evidence and current claim boundary}
\label{sec:evidence}

\subsection{Evidence cut}

This manuscript uses the evidence dossier dated 22 July 2026 as its source
cut.  That dossier verifies primary literature for query optimization,
federation, ontology-based access, cross-model systems, vector search,
portable plans, and the official SQLite and PostgreSQL facilities cited
below.  It also audits the \CatDB{} repository.  The audit found a bounded
schema and mapping foundation from the preceding semantic-model work, but no
P2 execution implementation.

\begin{table}[ht]
\centering
\small
\begin{tabularx}{\textwidth}{L{0.28\textwidth} L{0.19\textwidth} Y}
\toprule
Artifact class & Status at evidence cut & Consequence for this paper \\
\midrule
Finite schema and mapping definitions & available from P1 & notation may be reused; no P2 execution claim follows \\
Query profile and finite query evaluator & absent & query semantics here are a paper specification \\
Rust query or planner crate & absent & no compiled-\CatDB{} claim \\
SQLite storage connector & absent & SQL examples are proposed realizations \\
PostgreSQL storage connector & absent & parity and plan claims are untested \\
Generated SQL and typed parameters & absent & no emission result is reported \\
Captured backend plan & absent & no native-plan observation is reported \\
Result and lineage differential & absent & no semantic equivalence is experimentally supported \\
P2 performance benchmark & absent & no overhead or hot-path number is reported \\
Haskell query oracle & absent & no cross-language query result is reported \\
Lean query theorem & absent & no machine-checked P2 theorem is claimed \\
\bottomrule
\end{tabularx}
\caption{P2 evidence boundary.  ``Absent'' means absent from the audited
evidence cut, not impossible or permanently unplanned.}
\label{tab:evidence-boundary}
\end{table}

\subsection{Claims the evidence does support}

\status{\prior}

The literature supports several ingredients independently.  Cost-based
relational optimization and extensible physical operator frameworks are
established \cite{SelingerEtAl1979AccessPath,Graefe1994Volcano,Graefe1995Cascades}.
Federated and mediated architectures are established
\cite{ShethLarson1990Federated,Wiederhold1992Mediators}; distributed
optimization has long had to model shipping and remote costs
\cite{MackertLohman1986RStar}.  Calcite demonstrates a modular framework for
heterogeneous query planning \cite{BegoliEtAl2018Calcite}, while Trino
documents connector-specific pushdown \cite{TrinoPushdown}.  Ontop
demonstrates mapping-aware rewriting from an ontology-facing query language
to relational sources \cite{CalvaneseEtAl2017Ontop}.  These facts motivate
the architecture but do not validate its \CatDB{} realization.

SQLite officially documents SQL preparation, byte-code statements, automatic
reprepare conditions, explain facilities, per-statement counters, constraints,
typing, strict tables, and JSON functions
\cite{SQLitePrepare,SQLiteExplain,SQLiteEQP,SQLiteStmtStatus,SQLiteStmtCounters,SQLiteForeignKeys,SQLiteCreateTable,SQLiteDatatypes,SQLiteStrict,SQLiteJSON}.
PostgreSQL 18 officially documents preparation, generic and custom plan
behavior, replanning conditions, structured explain output, query-planning
settings, data types, and constraints
\cite{PostgreSQL18Prepare,PostgreSQL18Explain,PostgreSQL18Planner,PostgreSQL18Types,PostgreSQL18Constraints}.
These are backend capabilities, not measurements of a \CatDB{} adapter.

\subsection{Claims deliberately withheld}

The paper does not claim:

\begin{itemize}
  \item that categorical semantics improve SQL runtime;
  \item that \CatDB{} generates correct SQLite or PostgreSQL SQL today;
  \item that a warm semantic cache implies a warm backend native-plan cache;
  \item that explain text is a stable cross-version correctness oracle;
  \item that PostgreSQL generic and custom plans have equal behavior;
  \item that SQLite affinity and PostgreSQL scalar types automatically share
  one equality or collation;
  \item that every schema equation can be lowered as a native constraint;
  \item that graph, document, RDF, or vector operators are implemented;
  \item that an approximate nearest-neighbor result establishes identity,
  equality, or categorical law; or
  \item that P1 Rust or Lean evidence proves any P2 execution property.
\end{itemize}

\section{Prior art and candidate delta}
\label{sec:prior-art}

\subsection{Relational optimization}

System R established dynamic-programming access-path and join-order selection
as a practical cost-based optimization model
\cite{SelingerEtAl1979AccessPath}.  Volcano separated extensible operators and
exchange mechanisms \cite{Graefe1994Volcano}; Cascades organized
transformation rules and search \cite{Graefe1995Cascades}; Eddies explored
runtime adaptation \cite{AvnurHellerstein2000Eddies}.  These systems own the
physical choices that \CatDB{} should preserve, not displace.  The proposed
\CatDB{} realization ends before native scan, index, join algorithm,
parallelism, memory, and scheduling decisions.

The candidate delta is therefore not ``categorical cost-based optimization.''
It is an upstream semantic artifact that records why a logical relationship
exists, which versioned mappings expanded it, and which backend features
preserve it.  Whether that extra boundary is useful at acceptable cost is an
\enghyp{}.

\subsection{Federation, mediators, and adapters}

Federated databases explicitly address distribution, heterogeneity, and
autonomy \cite{ShethLarson1990Federated}.  Mediator architectures place
domain-specific processing between applications and data sources
\cite{Wiederhold1992Mediators}.  R* studied distributed query costs and
shipping choices \cite{MackertLohman1986RStar}.  Calcite provides a mature
logical/physical planning and adapter framework
\cite{BegoliEtAl2018Calcite}; Trino exposes which operations a connector can
push down \cite{TrinoPushdown}.  BigDAWG uses islands, shims, and casts to
coordinate heterogeneous engines \cite{DugganEtAl2015BigDAWG}.

\CatDB{}'s proposed distinction is that source-to-domain meaning is an
immutable typed mapping with explicit preservation and loss, not only a
catalog entry, adapter rule, or cast.  This is a representation and
governance claim until a compiler demonstrates that the artifacts compose,
diagnose changes, and produce competitive plans.

\subsection{Ontology-based access and standardized mappings}

RDF defines graph and dataset concepts; SPARQL defines graph query semantics;
R2RML defines relational-to-RDF mappings
\cite{W3CRDF11Concepts,W3CSPARQL11Query,W3CR2RML}.  Ontop is a direct
prior-art baseline for mapping-aware query rewriting over relational
databases \cite{CalvaneseEtAl2017Ontop}.  A serious \CatDB{} evaluation must
compare mapping expressiveness, rewrite coverage, diagnostics, and execution
overhead against this lineage.  ``Typed mappings'' alone are not a novelty
claim.

The candidate delta is a single versioned operational record spanning
categorical path equations, query expansion, backend dispositions, lineage,
and cache dependencies across more than an RDF-to-relational setting.  That
span is not demonstrated in the present evidence.

\subsection{Cross-model systems and portable interchange}

AsterixDB is an established semistructured database system
\cite{AlsubaieeEtAl2014AsterixDB}; GQL standardizes a property-graph language
\cite{ISOIEC39075_2024}.  Arrow standardizes an in-memory columnar format
\cite{ApacheArrowColumnar}.  Substrait proposes portable compute plans and an
extension mechanism \cite{SubstraitSpecification,SubstraitAbout,SubstraitExtensions}.
These are distinct layers.  Arrow does not by itself specify semantic query
intent, and a Substrait extension does not by itself prove that two engines
give equivalent results.

\CatDB{} could eventually lower its logical IR to Substrait or exchange
record batches through Arrow.  Both remain \specclaim{} in this paper.  The
initial executable target is a smaller relational subset with explicit
SQLite and PostgreSQL contracts.

\subsection{Vector execution and proof boundaries}

HNSW, Faiss, and Milvus establish approximate nearest-neighbor techniques and
vector-system baselines
\cite{MalkovYashunin2020HNSW,JohnsonDouzeJegou2021Faiss,WangEtAl2021Milvus}.
Approximation changes the result contract: recall, distance metric, index
parameters, nondeterminism, and candidate limits become observable semantics.
\CatDB{} therefore classifies ANN as \(\Approx\), never silently as
\(\Exact\).  Similarity can generate candidates for later reconciliation; it
cannot establish semantic identity or a path equation by itself.

Mechanized SQL semantics such as HoTTSQL show that proof-oriented query
rewrite validation is possible for carefully defined languages
\cite{ChuEtAl2017HoTTSQL}.  This paper's three proofs are conventional
mathematics over a much smaller abstract IR.  No generated SQL proof or
machine-checked compiler theorem is claimed.

\section{Compilation architecture}
\label{sec:architecture}

\subsection{Four layers and one ownership boundary}

\status{\enghyp}

\begin{figure}[ht]
\centering
\begin{tikzpicture}[
  box/.style={draw,rounded corners,align=center,minimum width=0.82\textwidth,
              minimum height=0.62cm,fill=blue!4},
  arr/.style={->,thick}
]
\node[box] (a) {A. Semantic artifacts: schema, mapping, query, policy revisions};
\node[box,below=0.42cm of a] (b) {B. Typed logical query: expanded paths, normalized records and bags};
\node[box,below=0.42cm of b] (c) {C. Capability-aware realization: dispositions, SQL template, parameters, residuals};
\node[box,below=0.42cm of c,fill=green!5] (d) {D. Backend-native plan and execution: scans, indexes, joins, buffers, rows};
\draw[arr] (a) -- (b);
\draw[arr] (b) -- (c);
\draw[arr] (c) -- (d);
\draw[dashed,thick] ([xshift=-0.46\textwidth,yshift=-0.2cm]c.south)
  -- ([xshift=0.46\textwidth,yshift=-0.2cm]c.south)
  node[midway,below=2pt] {\small \CatDB{} / native optimizer ownership boundary};
\end{tikzpicture}
\caption{Proposed compilation layers.  Layer D is observed and measured but
not reconstructed as a categorical evaluator.}
\label{fig:architecture}
\end{figure}

Layer A identifies meaning.  Layer B has backend-independent typed operators.
Layer C chooses a declared backend realization and records every non-exact
boundary.  Layer D belongs to the native engine.  A planner may inspect
backend statistics or explain evidence, but it must not pretend to control
every physical choice.

\subsection{Compile time, prepare time, and row time}

The phrase ``outside the hot path'' is ambiguous unless time is partitioned:

\begin{description}
  \item[Semantic compile time] parses or loads immutable artifacts, validates
  dependencies, expands mappings, types paths, and constructs logical IR.
  \item[Realization time] consults the capability manifest, chooses
  exact/residual dispositions, emits a statement template and typed
  parameters, and creates lineage rules.
  \item[Backend prepare time] asks SQLite or PostgreSQL to parse, analyze,
  rewrite, compile, or plan the statement according to the backend contract.
  \item[Row time] scans, filters, joins, projects, serializes, and transfers
  data, plus any explicitly declared residual operator.
\end{description}

The central hypothesis permits fixed query-shape compilation and realization
before execution.  It permits backend preparation and backend-controlled
replanning.  It permits a residual operator only when the realization marks
it and measures its cost.  It is falsified when a fixed query shape invokes
the semantic compiler or a semantic callback once per row.

\subsection{Failure is an output}

Compilation is a total diagnostic process even when realization is partial.
For each logical node it returns an exact translation, an explicit residual,
an approved approximation, or a stable unsupported diagnostic.  A query
whose output contract cannot be met has no executable realization.  It does
not fall through to a best-effort query while retaining an exact label.

\section{Mathematical framework}
\label{sec:framework}

\subsection{Schemas, paths, and read mappings}

We reuse only the following P1 notation.  A finite schema presentation
\(S\) has entities, typed generating arrows, attributes into a fixed scalar
typeside, and equations between parallel entity paths.  A typed path
\(p:A\rightsquigarrow B\) is an endpoint-compatible list of generators.
Composition is traversal-order concatenation.  These definitions describe a
presentation; they do not assert that the presented category is finite or
that arbitrary presented equality is decidable.

Query rewriting requires directionality beyond a generic schema functor.
A source-to-domain mapping need not be invertible.  We therefore do not
``run a functor backward'' by assumption.

\begin{definition}[Read-rewrite witness]
\label{def:rewrite-witness}
\status{\enghyp}
Let \(T\) be the query-facing schema and \(S\) a source-facing schema.  A
read-rewrite witness
\[
M:T\rightsquigarrow_{\mathrm{read}} S
\]
is an immutable artifact that assigns every admitted query-facing entity,
attribute, and traversed path a well-typed source expression and records:
\begin{enumerate}
  \item its source and target schema revisions;
  \item the validated mapping revisions from which the assignment was
  derived;
  \item required equations and identity assumptions;
  \item totality, cardinality, scalar, and nullability preconditions; and
  \item an information disposition for each assignment.
\end{enumerate}
\end{definition}

Such a witness may be authored directly, derived from a lawful mapping in a
direction that supports reads, or rejected as unavailable.  It is not an
inverse unless an inverse law is separately established.

\subsection{Scalars, records, and finite bags}

\begin{definition}[Query-v1 scalar profile]
\label{def:scalars}
\status{\enghyp}
The initial query profile uses required values from a fixed set of scalar
domains.  Each admitted domain has a canonical codec, a total equality
relation, a declared order when comparison is permitted, and a declared
collation when textual comparison is permitted.  Null, missing, non-finite
floating values, implicit coercion, locale-dependent comparison, and volatile
functions are outside the profile.
\end{definition}

A record type is a finite ordered list
\(\rho=\langle \ell_1:\tau_1,\ldots,\ell_n:\tau_n\rangle\) with distinct
labels.  Its values form
\(\sem{\rho}=\prod_i D_{\tau_i}\).  For a set \(X\), define the finite-bag
space
\[
\Bag(X)=\{m:X\to\mathbb N\mid \mathrm{supp}(m)\text{ is finite}\}.
\]
Bag union adds multiplicities.  Every query in the admitted fragment denotes
a finite bag of records.  No implicit duplicate elimination occurs.

\subsection{Expressions and predicates}

Scalar expressions are constants, typed parameters, field projections, and
admitted typed attributes reached through already-expanded source paths.
A predicate is pure and total.  Its denotation is a function
\(\sem{\varphi}:\sem{\rho}\to\{\mathsf{true},\mathsf{false}\}\).
There is no third truth value in query-v1.

\begin{definition}[Normalized logical query]
\label{def:logical-query}
\status{\enghyp}
For a schema \(S\), a normalized logical query is generated by:
\[
\begin{array}{rcl}
Q &::=&
\mathsf{Scan}(A,\alpha)
\mid \mathsf{Select}_{\varphi}(Q)
\mid \mathsf{Project}_{\pi}(Q)\\
&&{}\mid \mathsf{Join}_{\theta}(Q_1,Q_2)
\mid \mathsf{Navigate}_{p,\beta}(Q),
\end{array}
\]
where \(A\) is an entity, \(\alpha,\beta\) are aliases, \(\varphi\) is a
typed total predicate, \(\pi\) is a typed record projection, \(\theta\) is a
conjunction of equalities between same-domain required fields, and
\(p:A\rightsquigarrow B\) is a typed path from the input entity.
\end{definition}

\(\mathsf{Navigate}\) is semantic syntax.  Normalization replaces it with
the scans and inner equijoins selected by a read-rewrite witness and physical
storage mapping.  The resulting core IR uses only scan, select, project, and
inner equijoin.

\subsection{Bag denotation}

Fix a finite instance and a record encoding for each entity.  A scan returns
one record per entity occurrence with multiplicity inherited from the
physical relation.  Selection keeps the multiplicity of records satisfying
its predicate.  Projection sums multiplicities of input records that map to
the same projected record.  Inner join multiplies multiplicities for matching
pairs:
\[
\sem{\mathsf{Join}_{\theta}(Q_1,Q_2)}(r_1\bowtie r_2)
=\sem{Q_1}(r_1)\cdot\sem{Q_2}(r_2)
\]
when \(\theta(r_1,r_2)\) is true, with multiplicities summed when distinct
pairs encode the same output record.

This denotation fixes duplicate behavior.  It does not model SQL nulls,
outer joins, grouping, ordering, limits, recursion, updates, exceptions, or
approximate search.

\section{Immutable query artifacts}
\label{sec:query-artifact}

\begin{definition}[Immutable query artifact]
\label{def:query-artifact}
\status{\enghyp}
An immutable query artifact is a canonical serialized record
\[
\mathcal Q=(q,\sigma,\mu,\pi,\Gamma,P,O)
\]
where \(q\) is a stable query identifier; \(\sigma\) is the query-facing
schema revision; \(\mu\) is the ordered list of read-rewrite and storage
mapping revisions; \(\pi\) is the query-profile version; \(\Gamma\) is the
ordered typed parameter context; \(P\) is normalized semantic syntax; and
\(O\) is an output contract containing record type, bag semantics, scalar
codecs, error behavior, snapshot requirement, and lineage policy.
\end{definition}

The artifact is content-addressed after canonical serialization.  A mutable
name may point to a new artifact, but must not alter the bytes behind an
existing digest.  Stable identifiers are not substitutes for content
digests: both are recorded.

\subsection{Parameter and result contracts}

Parameter values are not embedded in the query identity.  The context
\(\Gamma=\langle x_1:\tau_1,\ldots,x_k:\tau_k\rangle\) fixes order, domain,
codec, range restrictions, and whether a value class can affect backend plan
choice.  Runtime values are separately hashed when a result cache or
parameter-sensitive physical decision requires them.

The output contract \(O\) fixes:

\begin{itemize}
  \item ordered field labels and scalar domains;
  \item bag rather than set semantics;
  \item canonical scalar decoding;
  \item equality and collation policy;
  \item snapshot or transaction expectation;
  \item error-versus-empty-result behavior;
  \item source-record and transformation lineage granularity; and
  \item whether result order is semantically irrelevant.
\end{itemize}

Because query-v1 has no ordering operator, comparison normalizes a result bag
independently of physical row order.  A driver that happens to return rows in
one order supplies no ordering guarantee.

\subsection{Rejected artifact states}

An artifact is rejected before realization if any path is ill typed, any
referenced revision is unavailable, an assignment is directionally
ambiguous, a parameter lacks a codec, a predicate is partial or volatile, an
output field is duplicated, or the query requests a feature outside its
declared profile.  Rejection is stable with respect to the same immutable
inputs.

\section{Running Customer/Order query}
\label{sec:running-example}

\subsection{Canonical schema}

One query runs through the whole example, so each compilation stage can be
checked against the last.  Its canonical schema has the entities
\(\code{Customer}\), \(\code{Order}\), and \(\code{Account}\);
arrows
\[
\begin{aligned}
\code{placedBy}&:\code{Order}\to\code{Customer},\\
\code{accountOf}&:\code{Customer}\to\code{Account},\\
\code{billedTo}&:\code{Order}\to\code{Account},
\end{aligned}
\]
and equation
\[
\code{billedTo}
=\code{placedBy};\code{accountOf}.
\]
The attributes used here are
\[
\code{customerName}:\code{Customer}\to\code{string},
\qquad
\code{orderTotal}:\code{Order}\to\code{decimal}.
\]
The notation comes from P1.  This paper does not import any P1 runtime
evidence.

\subsection{Canonical request}

The request takes a required decimal parameter,
\(\code{minimumTotal}\), and returns the ordered record
\[
\langle
\code{customerId},\code{customerName},
\code{orderId},\code{orderTotal}
\rangle
\]
for each order whose \(\code{orderTotal}\) is at least that value.  It reaches
the customer through \(\code{placedBy}\).  Duplicate rows remain in the
result, and the request does not specify an output order.

In semantic syntax:
\[
\begin{split}
Q_{\mathrm{co}}={}&
\mathsf{Project}_{c.id,\ c.customerName,\ o.id,\ o.orderTotal}\\
&\left(
\mathsf{Select}_{o.orderTotal\geq :minimumTotal}
\left(
\mathsf{Navigate}_{placedBy,c}
(\mathsf{Scan}(\code{Order},o))
\right)\right).
\end{split}
\]

\subsection{Source realization assumptions}

The proposed relational storage mapping uses two tables:
\[
\begin{array}{l}
\code{catdb\_customer(id, name, account\_id)},\\
\code{catdb\_order(id, customer\_id, billed\_account\_id, total)}.
\end{array}
\]
Every field used by \(Q_{\mathrm{co}}\) is required.  In the mapping witness,
\(\code{order.customer\_id}=\code{customer.id}\) realizes
\(\code{placedBy}\).  The witness maps \(\code{customerName}\) to
\code{customer.name} and \(\code{orderTotal}\) to \code{order.total}.  The
relationship is total only if every visible order has a matching customer in
the query snapshot.  A disabled or violated foreign key does not establish
that fact.

\subsection{Normalized logical plan}

Expanding the path and normalizing the navigation gives:
\[
\begin{aligned}
J_{\mathrm{co}}={}&
\mathsf{Join}_{o.customer\_id=c.id}
(\mathsf{Scan}(\code{catdb\_order},o),
 \mathsf{Scan}(\code{catdb\_customer},c)),\\
F_{\mathrm{co}}={}&
\mathsf{Select}_{o.total\geq :minimumTotal}(J_{\mathrm{co}}),\\
L_{\mathrm{co}}={}&
\mathsf{Project}_{c.id,\ c.name,\ o.id,\ o.total}(F_{\mathrm{co}}).
\end{aligned}
\]

This logical plan does not prescribe a join algorithm.  SQLite can choose its
own nested loops and indexes.  PostgreSQL can choose nested-loop, hash, or
merge strategies from its statistics and optimizer rules.  \CatDB{} records
the logical equality and observes whichever native plan the engine selects.

\subsection{Illustrative SQL templates}

The proposed SQLite template is:
\begin{lstlisting}[language=SQL]
SELECT c.id AS customer_id,
       c.name AS customer_name,
       o.id AS order_id,
       o.total AS order_total
FROM catdb_order AS o
INNER JOIN catdb_customer AS c
        ON o.customer_id = c.id
WHERE o.total >= ?1
\end{lstlisting}

PostgreSQL uses the same statement shape with its parameter syntax:
\begin{lstlisting}[language=SQL]
SELECT c.id AS customer_id,
       c.name AS customer_name,
       o.id AS order_id,
       o.total AS order_total
FROM catdb_order AS o
INNER JOIN catdb_customer AS c
        ON o.customer_id = c.id
WHERE o.total >= $1
\end{lstlisting}

No \CatDB{} compiler has emitted or executed either listing.  They are test
oracles for a future implementation.  The parameter has a declared decimal
codec and must be bound, not interpolated into the SQL text.

\section{Mapping and path expansion}
\label{sec:expansion}

\subsection{Expansion algorithm}

\status{\enghyp}

Let \(M:T\rightsquigarrow_{\mathrm{read}}S\) be a read-rewrite witness.
Expansion \(E_M\) recursively substitutes:

\begin{enumerate}
  \item query-facing entities with source entity expressions;
  \item each traversed generator with its witness path or relationship
  expression;
  \item attributes with typed source expressions;
  \item canonical predicates with source-domain predicates only when the
  scalar codec and comparison law are exact; and
  \item output fields with explicit source-to-canonical decoders.
\end{enumerate}

Substitution normalizes adjacent paths by traversal-order concatenation.
Every intermediate endpoint is checked.  The expansion result includes an
ordered derivation whose nodes identify the original query expression,
mapping assignment, source expression, type judgment, preservation
disposition, and source artifact digest.

\subsection{Direction and non-invertibility}

If a source-to-domain mapping \(F:S\to T\) exists but supplies no read-rewrite
witness for a requested \(T\)-expression, expansion stops.  Object merging,
value normalization, object synthesis, and information loss can prevent
inverse query rewriting.  The compiler must not infer an inverse from naming
similarity or from the existence of \(F\).

For composed witnesses \(M_1:T\rightsquigarrow U\) and
\(M_2:U\rightsquigarrow S\), the artifact records both revisions and the
composed expansion.  It also records any strengthening of preconditions.
Composition may turn an exact operation into a residual or unsupported one;
dispositions form part of the composition result.

\subsection{Type preservation}

\begin{proposition}[Typed path expansion]
\label{prop:type-expansion}
\status{\paperproved}
Let \(M:T\rightsquigarrow_{\mathrm{read}}S\) assign every generator
\(f:A\to B\) traversed by a query a typed source path
\[
M(f):M(A)\rightsquigarrow M(B).
\]
Extend \(M\) to paths by mapping the empty path to the empty path and
concatenating assigned paths in traversal order.  If
\(T\vdash p:A\rightsquigarrow B\), then
\[
S\vdash M(p):M(A)\rightsquigarrow M(B).
\]
\end{proposition}

\begin{proof}
Proceed by induction on the length of \(p\).  If \(p\) is empty at \(A\),
then \(M(p)\) is the empty path at \(M(A)\), which is typed
\(M(A)\rightsquigarrow M(A)\).

For the inductive step, write the traversal-order path as
\(p=p';f\), where
\(T\vdash p':A\rightsquigarrow C\) and \(f:C\to B\).
By the induction hypothesis,
\(S\vdash M(p'):M(A)\rightsquigarrow M(C)\).
By the witness premise,
\(S\vdash M(f):M(C)\rightsquigarrow M(B)\).
The target of \(M(p')\) equals the source of \(M(f)\), so typed path
composition gives
\[
S\vdash M(p');M(f):M(A)\rightsquigarrow M(B).
\]
Traversal-order substitution defines this composite to be \(M(p)\).
\end{proof}

\begin{remark}[Scope of the proposition]
The proposition proves endpoint typing from a well-formed witness.  It does
not prove that a witness exists, that it preserves equations, cardinality,
null behavior, scalar meaning, multiplicity, or performance.  Those are
separate validation and realization obligations.
\end{remark}

\section{Capability manifests and dispositions}
\label{sec:capabilities}

\subsection{Versioned capability manifest}

\begin{definition}[Capability manifest]
\label{def:capability-manifest}
\status{\enghyp}
A capability manifest for backend \(b\) is an immutable record
\[
C_b=(b,v,\kappa,\mathcal T,\mathcal O,\mathcal K,\mathcal X,
      \mathcal P,\mathcal E)
\]
containing:
\begin{itemize}
  \item backend kind \(b\), exact version \(v\), build or extension
  fingerprint \(\kappa\);
  \item supported scalar types, codecs, comparisons, and collations
  \(\mathcal T\);
  \item supported logical operators and expression fragments
  \(\mathcal O\);
  \item constraint and integrity facilities \(\mathcal K\);
  \item transaction, isolation, snapshot, cancellation, and streaming
  behavior \(\mathcal X\);
  \item preparation, parameter, and native-plan policy \(\mathcal P\); and
  \item evidence interfaces \(\mathcal E\), such as structured explain output
  or stable statement counters.
\end{itemize}
\end{definition}

A manifest is descriptive and testable, not a marketing capability list.
Each entry identifies its source: normative backend documentation,
connector-level test evidence, or an explicit assumption awaiting a test.
Changing a backend library version, compile option, enabled extension,
collation, session setting, or connector feature creates a new manifest
revision when the change can affect realization or results.

\subsection{Four dispositions}

\begin{definition}[Realization disposition]
\label{def:disposition}
\status{\enghyp}
For a logical operation \(n\), backend manifest \(C_b\), and execution policy
\(\omega\), capability checking returns exactly one of:
\[
\begin{array}{ll}
\Exact(w) & \text{backend realization with an exactness witness }w;\\
\Residual(r) & \text{declared non-backend operator }r\text{ with placement};\\
\Approx(a) & \text{approved approximation contract }a;\\
\Unsupported(d) & \text{stable diagnostic }d\text{ and no executable plan}.
\end{array}
\]
\end{definition}

An exactness witness identifies the logical node, emitted backend fragment,
scalar and multiplicity assumptions, snapshot requirement, and the rule
whose denotation is asserted equal.  A residual identifies where rows move,
which fields are needed, how many rows or bytes are estimated, and which
semantics the residual evaluator implements.  An approximation identifies
the metric, quality contract, parameters, and provenance annotation.  An
unsupported diagnostic identifies the failed obligation and the minimum
capability or rewrite needed.

\subsection{Capability checking is conjunctive}

An operator is exact only if every relevant dimension is exact.  SQL syntax
support is insufficient.  For the predicate
\(\code{o.total >= :minimumTotal}\), exactness requires the source value,
parameter, binding codec, backend comparison, collation if applicable, and
result decoding to share the declared scalar semantics.  For the navigation
join, exactness requires endpoint types, key equality, requiredness,
multiplicity, and snapshot behavior.  One unsupported child prevents an
exact parent unless a declared residual repairs the gap.

\begin{table}[ht]
\centering
\small
\begin{tabularx}{\textwidth}{L{0.21\textwidth} L{0.23\textwidth} Y}
\toprule
Dimension & Exact evidence required & Typical failure \\
\midrule
Typing & codec and domain agreement & affinity or implicit coercion changes comparison \\
Truth & pure two-valued predicate & null introduces unknown \\
Multiplicity & bag-preserving operator & implicit distinct or object flattening duplicates rows \\
Navigation & total relationship and matching key & missing target or nonunique join key \\
Snapshot & declared visibility point & sources read at incomparable times \\
Error & matching failure behavior & conversion failure becomes null or dropped row \\
Lineage & complete row transformation rule & residual loses source identifiers \\
\bottomrule
\end{tabularx}
\caption{Exactness is a conjunction of obligations, not a synonym for
``pushdown supported.''}
\label{tab:exactness-dimensions}
\end{table}

\subsection{Profile-v1 capability matrix}

\begin{table}[ht]
\centering
\small
\begin{tabularx}{\textwidth}{L{0.27\textwidth} L{0.18\textwidth} Y}
\toprule
Feature & Initial disposition & Reason \\
\midrule
Required canonical scalars & exact when codec manifest passes & bounded cross-backend domain \\
Pure total comparison & exact when scalar/order policy passes & two-valued fragment \\
Projection & exact & field selection and renaming only \\
Typed total path navigation & exact through inner equijoin when key contract passes & running vertical slice \\
Inner equijoin & exact when domains, nullability, and multiplicity agree & admitted bag operator \\
Parameterized SQL & required & separates query shape from values \\
Null and missing values & unsupported & three-valued and missing semantics not fixed \\
Outer joins & unsupported & null introduction not fixed \\
Aggregation and grouping & unsupported & duplicate and numeric rules not fixed \\
Order, limit, and ties & unsupported & stable order contract not fixed \\
Volatile functions & unsupported & purity and repeatability violated \\
Floating/approximate equality & unsupported & no portable exact domain \\
ANN vector search & approximate only & recall and metric are observable \\
Recursive traversal & unsupported & termination and backend parity not fixed \\
Updates and write propagation & unsupported & bidirectional semantics belong to P8 \\
Cross-source transaction & unsupported & no atomic snapshot contract \\
\bottomrule
\end{tabularx}
\caption{Admitted and excluded first-slice features.}
\label{tab:profile}
\end{table}

\section{Logical lowering and preservation}
\label{sec:lowering}

\subsection{Core target algebra}

The abstract target algebra has bag scans, selection, projection, and inner
equijoin with the same typed scalar functions as
\Cref{sec:framework}.  A backend realization may serialize these operators
as SQL, but the theorem in this section concerns an abstract target
denotation, not a specific SQL implementation.

\begin{definition}[Exact lowerer]
\label{def:exact-lowerer}
\status{\enghyp}
An exact lowerer \(L\) for the normalized core fragment is defined
compositionally:
\[
\begin{aligned}
L(\mathsf{Scan}(R,\alpha))&=\mathsf{BScan}(R,\alpha),\\
L(\mathsf{Select}_{\varphi}(Q))&=
  \mathsf{BSelect}_{L(\varphi)}(L(Q)),\\
L(\mathsf{Project}_{\pi}(Q))&=
  \mathsf{BProject}_{L(\pi)}(L(Q)),\\
L(\mathsf{Join}_{\theta}(Q_1,Q_2))&=
  \mathsf{BJoin}_{L(\theta)}(L(Q_1),L(Q_2)).
\end{aligned}
\]
For every scan, expression, predicate, projection, and equality, the
realization certificate states that its target interpretation equals the
logical interpretation under the declared record encoding.
\end{definition}

\subsection{Exact lowering theorem}

\begin{proposition}[Denotation preservation for the admitted core]
\label{prop:lowering}
\status{\paperproved}
Let \(Q\) be a well-typed finite query generated by scan, select, project, and
inner equijoin.  Suppose:
\begin{enumerate}
  \item source scans are finite and their target record encodings preserve
  each record and multiplicity;
  \item every lowered scalar expression, predicate, projection, and equality
  has the same total denotation as its logical source;
  \item both source and target use the finite-bag definitions in
  \Cref{sec:framework}; and
  \item execution observes the same source snapshot.
\end{enumerate}
Then the abstract exact lowerer preserves denotation:
\[
\sem{L(Q)}_{\mathrm{target}}=\sem{Q}_{\mathrm{logical}}.
\]
\end{proposition}

\begin{proof}
Proceed by structural induction on \(Q\).

\emph{Scan.}  For \(Q=\mathsf{Scan}(R,\alpha)\), premise 1 says that
\(\mathsf{BScan}(R,\alpha)\) returns exactly the encoded logical records with
the same finite multiplicities at the same snapshot.  Thus the two bags are
equal.

\emph{Selection.}  Let
\(Q=\mathsf{Select}_{\varphi}(Q_0)\).  By the induction hypothesis,
\(\sem{L(Q_0)}=\sem{Q_0}\).  For each record \(r\), premise 2 gives
\(\sem{L(\varphi)}(r)=\sem{\varphi}(r)\).  Logical and target selection
therefore either retain or discard the same record.  When retained, each uses
the input multiplicity; hence the output multiplicities agree pointwise.

\emph{Projection.}  Let
\(Q=\mathsf{Project}_{\pi}(Q_0)\).  By induction the input bags agree, and by
premise 2 the projections map each input record to the same output record.
For any output \(s\), both semantics assign the sum of multiplicities of all
input records \(r\) for which \(\pi(r)=s\).  The summation index and every
summand agree, so output multiplicities agree.

\emph{Inner equijoin.}  Let
\(Q=\mathsf{Join}_{\theta}(Q_1,Q_2)\).  By induction the left and right input
bags agree.  Premise 2 gives the same truth value for \(\theta(r_1,r_2)\) on
every pair.  For a matching pair, both semantics contribute the product of
the two input multiplicities to the merged output record; for a nonmatching
pair, both contribute zero.  Both sum contributions when more than one pair
encodes the same output.  Therefore every output multiplicity agrees.

These cases exhaust the core grammar.  Premise 4 rules out differences caused
by reading different snapshots.  Hence the finite result bags are equal.
\end{proof}

\begin{remark}[What the theorem does not prove]
\label{rem:not-sql-proof}
The theorem is conditional on exact primitive realizations.  It does not show
that SQLite SQL, PostgreSQL SQL, a driver codec, a connector, or emitted
lineage satisfies those premises.  Establishing those facts requires the
differential and backend tests in \Cref{sec:experiments}.  A future
machine-checked development would also need an explicit SQL semantics or a
verified refinement to the driver-visible subset.
\end{remark}

\subsection{Realization certificate}

\begin{definition}[Realization certificate]
\label{def:realization-certificate}
\status{\enghyp}
An executable realization is paired with a canonical certificate
\[
\mathcal R=(h_Q,h_S,h_M,h_C,h_\omega,L,D,\mathrm{stmt},\Gamma_b,O_b,\Lambda),
\]
where the hashes identify the query, schemas, mappings, capability manifest,
and policy; \(L\) is normalized logical IR; \(D\) assigns dispositions to
every node; \(\mathrm{stmt}\) is the parameterized backend template;
\(\Gamma_b\) is the backend binding layout; \(O_b\) is the backend decoding
contract; and \(\Lambda\) is the lineage derivation.
\end{definition}

The certificate is evidence about what the compiler intended.  It is not a
certificate of backend correctness until tests establish the primitive
premises and bind the evidence to an exact backend and connector version.

\subsection{Residual plans}

A residual plan splits \(L\) at an explicit boundary.  The backend subplan
projects every field required by the residual and lineage evaluator.  The
certificate records transfer schema, predicted rows and bytes, ordering
assumptions, memory policy, and failure semantics.  Result comparison covers
the complete backend-plus-residual composition.  A residual is not a failure
by itself; an undeclared residual is.

\section{SQLite realization contract}
\label{sec:sqlite}

\subsection{Why SQLite is the first executable target}

SQLite provides a compact embedded environment, a documented preparation API,
prepared-statement counters, explain interfaces, ordinary indexes and joins,
foreign keys, strict tables, and a controllable file-backed fixture
\cite{SQLitePrepare,SQLiteStmtStatus,SQLiteStmtCounters,SQLiteForeignKeys,SQLiteStrict}.
That makes it useful for the first vertical slice.  It does not make SQLite
semantically simple: dynamic typing, affinity, collation, foreign-key
configuration, and explain instability all affect the contract
\cite{SQLiteDatatypes,SQLiteExplain,SQLiteEQP}.

\subsection{Pinned manifest}

The SQLite capability manifest must record at least:

\begin{itemize}
  \item exact library version, source identifier when available, compile
  options, binding crate version, and connector revision;
  \item database encoding, collation set, strict-table policy, and JSON
  extension assumptions;
  \item foreign-key enforcement state for every connection;
  \item transaction and snapshot mode;
  \item allowed scalar storage classes and canonical codecs;
  \item parameter binding API and error mapping;
  \item explain and statement-counter interfaces used as evidence; and
  \item reprepare behavior visible through counters.
\end{itemize}

SQLite foreign keys are configured per connection, so a schema declaration
alone does not prove total navigation
\cite{SQLiteForeignKeys}.  The acceptance harness must query the live setting,
attempt violating writes in an isolated fixture, and record the outcome.

\begin{definition}[Portable decimal-v1 codec]
The initial portable scalar profile admits
\(\mathsf{Decimal64}(p,s)\) only when
\[
  0\le s\le p\le 18,\qquad
  v=m\,10^{-s},\qquad |m|<10^p,
\]
with signed integer mantissa \(m\). The canonical bytes encode the profile
revision, \(p\), \(s\), and the two's-complement signed 64-bit mantissa in one
declared byte order. SQLite stores and binds \(m\) as \code{INTEGER}; the scale
belongs to the immutable type, not to row text. Comparison pushdown is exact
only for equal \((p,s)\) domains. A conversion that changes scale must prove
exact divisibility and absence of overflow, otherwise it is residual or
unsupported. PostgreSQL \code{numeric} values enter the portable subset only
when their decoded value round-trips to the same bounded mantissa. Text
collation is never used for decimal order.
\end{definition}

\subsection{Type and constraint lowering}

The initial profile should use \code{STRICT} tables when the pinned SQLite
version and connector support them, while still validating exact codec
behavior \cite{SQLiteStrict}.  SQLite's storage classes and affinity rules
remain relevant; a declared decimal domain cannot be assumed exact merely
because a column name or declaration contains ``decimal''
\cite{SQLiteDatatypes}. The first vertical slice uses the bounded
\(\mathsf{Decimal64}(p,s)\) profile above and tests its round trip, range,
ordering, parameter binding, and rejection boundaries. Wider precision and
mixed-scale arithmetic remain unsupported until they receive a separate
profile.

Primary keys, unique constraints, not-null constraints, checks, and foreign
keys are available but have specific documented behavior
\cite{SQLiteCreateTable,SQLiteForeignKeys}.  A path equation spanning multiple
relationships generally is not lowered by pretending one row-local check can
enforce it.  It becomes a validation query, trigger-backed engineering choice,
or application obligation, with its discharge site recorded.

\subsection{Preparation and evidence}

SQLite's prepare interfaces compile SQL into a prepared byte-code statement
\cite{SQLitePrepare}.  The connector must distinguish:

\begin{enumerate}
  \item a warm semantic compilation cache;
  \item a warm \CatDB{} realization cache containing the SQL template and
  binding layout; and
  \item a live prepared SQLite statement on a particular connection.
\end{enumerate}

The experiment logs preparation count, reprepare count, full-scan steps,
sorts, automatic indexes, virtual-machine steps, and statement memory where
the official counters expose them
\cite{SQLiteStmtStatus,SQLiteStmtCounters}.  These metrics diagnose physical
behavior; they do not prove result correctness.

SQLite warns that both raw \code{EXPLAIN} and
\code{EXPLAIN QUERY PLAN} output can change between releases
\cite{SQLiteExplain,SQLiteEQP}.  Tests may archive the raw output and extract
version-scoped diagnostics, but must not use cross-version text matching as a
semantic oracle.  Stable correctness assertions compare normalized results,
errors, and lineage.

\subsection{Running-query acceptance}

For \(Q_{\mathrm{co}}\), a future SQLite acceptance bundle must contain:

\begin{itemize}
  \item canonical schema, mapping, query, capability, and policy artifacts;
  \item fixture DDL, data, indexes, pragma state, and snapshot boundary;
  \item normalized logical IR and node dispositions;
  \item the exact SQL bytes and ordered parameter binding;
  \item an independent finite-evaluator result and lineage bag;
  \item decoded SQLite result and lineage bag;
  \item equality comparison, including duplicate cases;
  \item raw explain evidence and stable statement counters; and
  \item cold, warm-realization, and warm-prepared latency distributions.
\end{itemize}

Until this bundle exists, the SQL in \Cref{sec:running-example} remains an
illustrative target.

\section{PostgreSQL realization contract}
\label{sec:postgresql}

\subsection{Portable subset before backend extensions}

PostgreSQL is the second target.  Its initial purpose is not to showcase every
backend feature, but to test the same declared query-v1 subset under a
different type, transaction, planner, and driver environment.  A query can be
portable even when native physical plans differ.  The parity contract compares
logical results, errors, scalar values, and lineage, not identical join
algorithms.

\subsection{Pinned manifest}

The PostgreSQL manifest records:

\begin{itemize}
  \item exact server major and minor version, driver and connector versions,
  enabled extensions, database encoding, locale, and collations;
  \item table and column types, domains, constraints, indexes, and statistics
  snapshot;
  \item transaction isolation, read-only state, and snapshot procedure;
  \item session planner settings and resource settings relevant to the run;
  \item prepared-statement policy, including automatic, generic, or custom
  behavior;
  \item binary or text parameter/result codecs and their versioned tests; and
  \item exact \code{EXPLAIN} options and permission boundary.
\end{itemize}

PostgreSQL data types are richer than the initial \CatDB{} scalar profile
\cite{PostgreSQL18Types}.  The connector must select an exact representation;
it must not equate similarly named source and canonical types without
round-trip, comparison, overflow, and error tests.

\subsection{Preparation and native planning}

PostgreSQL \code{PREPARE} separates parse, analysis, and rewrite work from
later execution, while planning may use generic or custom plans and may
change after relevant definition or statistics changes
\cite{PostgreSQL18Prepare}.  Therefore a \CatDB{} realization key does not
name one permanent PostgreSQL physical plan.  The evidence record identifies
the plan policy and parameter class.  Experiments report generic, custom, and
automatic modes when skewed parameters could matter.

\code{EXPLAIN} can expose plan structure, estimates, actual rows and time,
buffers, settings, memory, serialization, and other details depending on
options and privileges \cite{PostgreSQL18Explain}.  \code{ANALYZE} executes
the statement, so tests use isolated read fixtures or a rollback-safe protocol.
Explain evidence is stored as structured JSON where supported, together with
the exact command, settings, and server version.

\subsection{Constraints and semantic obligations}

PostgreSQL supports not-null, check, unique, primary-key, exclusion, and
foreign-key constraints, but their documented semantics set limits
\cite{PostgreSQL18Constraints}.  A check condition is satisfied by true or
null, which differs from query-v1's required two-valued predicate unless
not-null evidence also exists.  A check is not a sound mechanism for arbitrary
cross-row invariants.  A foreign key can support a total-navigation claim only
when column nullability, key uniqueness, constraint validation, transaction
visibility, and any deferral policy all match the witness.

\subsection{Running-query parity}

The PostgreSQL vertical slice reuses \(Q_{\mathrm{co}}\), the same canonical
fixtures, output contract, and oracle result as SQLite.  Backend DDL and scalar
codecs may differ, but the normalized result bag and lineage bag must match.
The bundle additionally records estimated and actual cardinalities, buffers,
planning and execution times, plan-cache mode, and planner settings.  A
difference is classified as:

\begin{enumerate}
  \item a connector or compiler defect;
  \item an undeclared capability difference;
  \item an invalid portable-profile assumption;
  \item an oracle defect; or
  \item an expected native physical difference with equal semantics.
\end{enumerate}

No category is assigned without a minimal reproducer and preserved evidence.

\section{Constraints, residuals, and failure semantics}
\label{sec:constraints}

\subsection{Three discharge sites}

\status{\enghyp}

Every semantic obligation has a meaning and a discharge site.  The initial
sites are:

\begin{description}
  \item[Static] path typing, artifact totality, output typing, and syntactic
  profile membership are checked before backend access.
  \item[Native] a backend constraint or operator discharges the obligation
  under a pinned manifest and live configuration.
  \item[Validation or residual] an explicit query, incremental checker, or
  local operator produces evidence when no native mechanism exactly matches.
\end{description}

A higher-level invariant may remain unresolved.  The compiler reports it
rather than converting ``not natively enforced'' into ``false'' or
``unimportant.''

\subsection{The account path equation}

The running schema declares
\(\code{billedTo}=\code{placedBy};\code{accountOf}\).
With relational columns, the equality can be tested by joining orders,
customers, and accounts and comparing the two account identifiers.  That
validation query is different from a static categorical derivation and
different from a native row-local constraint.  Its result is snapshot-scoped:
success on one snapshot does not prove all future writes preserve the law.

If \(Q_{\mathrm{co}}\) traverses only \(\code{placedBy}\), the account
equation need not be evaluated per row merely because it exists in the
schema.  Its validation state is a dependency only if the selected mapping,
policy, or query relies on the equation.  This selective obligation graph is
important to keeping unrelated semantics out of the row path.

\subsection{Partial source availability}

The initial single-source relational slice fails closed when its required
source or snapshot is unavailable.  A future federated profile may allow a
partial result only if the query artifact declares a partial-answer semantics,
the result carries missing-source provenance, and the consumer accepts it.
Returning an incomplete bag under the exact result contract is a semantic
mismatch.

\subsection{Error normalization}

The result comparator treats errors as typed outcomes.  It distinguishes at
least artifact rejection, unsupported capability, parameter-codec failure,
source connection failure, backend statement failure, cancellation, timeout,
snapshot failure, residual failure, and result-decoding failure.  Backends
need not use the same raw error text.  Connectors map documented cases to a
versioned canonical class and retain the raw diagnostic as evidence.

\subsection{Information loss}

Projection intentionally loses fields but preserves the declared output
contract.  Other loss is more consequential.  Flattening a document can lose
missing-versus-null distinctions; graph lowering can lose edge identity;
relational-to-RDF mapping can alter term construction; vector search is
approximate; cross-model casts can lose ordering or multiplicity.  Each such
boundary receives an explicit loss record.  An exact label is unavailable
when the loss can affect the query's result contract.

\section{Plan caches, dependencies, and invalidation}
\label{sec:caching}

\subsection{Three caches, not one}

\status{\enghyp}

\CatDB{} distinguishes:

\begin{enumerate}
  \item the \emph{semantic compilation cache}, which stores typed expansion
  and logical IR for immutable semantic artifacts;
  \item the \emph{realization cache}, which stores capability-checked
  dispositions, a backend statement template, bindings, decoders, residuals,
  and lineage rules; and
  \item the \emph{backend statement or native-plan cache}, which is scoped to
  a SQLite connection or PostgreSQL session and remains partly
  backend-controlled.
\end{enumerate}

``Warm plan'' is otherwise too imprecise to reproduce.  A benchmark labels
each layer independently and records whether backend preparation, reprepare,
or replanning occurred.

\subsection{Dependency-complete keys}

\begin{definition}[Semantic compilation key]
\label{def:semantic-key}
The semantic cache key is
\[
K_s=H(q,\sigma,\mu,\pi,\nu),
\]
where \(q\) is the canonical query digest, \(\sigma\) the ordered digests of
the query's validated schema dependency closure, \(\mu\) the ordered mapping
and rewrite-witness dependency digests, \(\pi\) the query-profile revision,
and \(\nu\) the semantic compiler implementation revision. The closure names
every referenced object, arrow, equation, scalar codec, constraint, and
validation witness. The artifact retains the full schema revisions for
provenance, but a new revision may reuse \(K_s\) only when a validator emits a
compatibility witness proving that this complete referenced closure is
unchanged.
\end{definition}

\begin{definition}[Realization key]
\label{def:realization-key}
The realization key is
\[
K_r=H(K_s,b,C_b,\omega,\lambda,\chi),
\]
where \(b\) identifies the backend family, \(C_b\) is the complete capability
manifest digest, \(\omega\) is the execution-policy digest, \(\lambda\) is
the storage-layout and statistics-class digest, and \(\chi\) identifies the
lowerer and connector implementation revisions.
\end{definition}

The key does not generally include parameter values, because a statement
template is parameterized.  If a \CatDB{} policy makes a value-sensitive
realization choice, it includes a declared parameter class.  PostgreSQL may
still select a custom plan for a particular execution, and SQLite may
automatically reprepare under documented conditions.  Those native events are
evidence attached to an execution, not proof that \(K_r\) was incorrectly
formed.

\subsection{Invalidation events}

The following events can invalidate \(K_s\): query changes, a change inside
the validated schema or mapping dependency closure, rewrite-witness changes,
scalar-profile changes, or semantic compiler revision changes. An unrelated
schema edit does not force a global flush, but reuse under the new revision is
forbidden until the dependency validator emits the compatibility witness.
The following can invalidate \(K_r\) without invalidating \(K_s\): backend
version or build changes, extension changes, collation changes, storage
mapping or index-policy changes, connector changes, execution-policy changes,
or a statistics-class decision used by the \CatDB{} planner.

Backend caches have additional lifetimes.  Closing a SQLite connection loses
its prepared statement.  PostgreSQL sessions and prepared statements have
server-defined replanning and invalidation behavior
\cite{PostgreSQL18Prepare}.  SQLite may automatically recompile a prepared
statement \cite{SQLitePrepare}.  \CatDB{} logs these events when observable
but does not redefine them.

\subsection{Cache-soundness proposition}

\begin{proposition}[Dependency-complete cache reuse]
\label{prop:cache}
\status{\paperproved}
Let a deterministic compiler \(C\) take the dependency tuple
\[
d=(q,\sigma,\mu,\pi,\nu,b,C_b,\omega,\lambda,\chi)
\]
and return either a stable diagnostic or a realization artifact.  Let
\(K=H(\operatorname{canon}(d))\), where canonical serialization is injective
over admitted dependency tuples and \(H\) is collision-free for the tuples
under consideration.  Consider a cache protocol that authorizes reuse exactly
when keys are equal and otherwise recomputes or explicitly revalidates.  The
protocol authorizes reuse exactly when all declared dependencies in \(d_0\)
and \(d_1\) are unchanged, and every reuse it authorizes is sound.
\end{proposition}

\begin{proof}
First suppose every declared dependency is unchanged.  Then
\(\operatorname{canon}(d_0)=\operatorname{canon}(d_1)\), so the keys agree.
Determinism gives \(C(d_0)=C(d_1)\).  Returning the cached diagnostic or
realization therefore returns the same artifact the compiler would produce,
which is sound.

Conversely, suppose at least one declared dependency changes.  Injectivity of
canonical serialization gives
\(\operatorname{canon}(d_0)\neq\operatorname{canon}(d_1)\).  Collision freedom
on the admitted tuples gives \(K_0\neq K_1\).  The artifact stored under
\(K_0\) therefore cannot be returned by an authorized successful lookup for
\(K_1\).  Reusing it by ignoring the changed dependency would violate the
cache protocol and is not established sound by determinism, because the
compiler is permitted to depend on every declared component.

Thus the protocol authorizes reuse exactly under equality of all declared
dependencies, each authorized reuse returns the deterministic compiler result,
and any declared change requires a miss or explicit revalidation.
\end{proof}

\begin{remark}[Assumptions and practical hashing]
The proposition states an ideal key contract.  Real implementations use
finite cryptographic digests, so collision resistance replaces literal
collision freedom and canonicalization tests become part of the acceptance
suite.  The proposition also does not say that the declared dependency set is
complete.  Tests must mutate each candidate dependency and verify the
expected hit, miss, or revalidation transition.
\end{remark}

\subsection{Negative-cache entries}

Stable unsupported diagnostics may be cached under the same dependency
discipline.  This avoids repeating expensive validation for a known
unsupported query without converting the diagnostic into permanent policy.
A new capability manifest, mapping, or compiler revision creates a new key
and can make the query realizable.

\section{Cross-model preservation boundaries}
\label{sec:cross-model}

\subsection{Why a relational first slice is not a universal model}

The title names relational, graph, document, and vector execution because the
research program must state how their boundaries differ.  It does not imply
that one completed compiler currently targets all four.  The only proposed
first executable slice is relational SQLite, followed by a PostgreSQL
portable subset.

\begin{table}[ht]
\centering
\small
\begin{tabularx}{\textwidth}{L{0.17\textwidth} L{0.28\textwidth} L{0.31\textwidth} Y}
\toprule
Boundary & Candidate preservation & Typical residual or loss & Status \\
\midrule
Relational targets & required scalar fields, total arrows as key relationships, projection, filter, inner equijoin, selected native constraints & arbitrary path laws, null/missing semantics, undeclared collation, cross-source identity & initial relational target \\
Property graph/GQL & entity and relationship types, selected path traversals, explicit edge properties & edge identity, path multiplicity, variable-length path semantics, graph-specific constraints & design analysis only \\
RDF/SPARQL & named resources, predicates, graph patterns, mapping-based access & open-world assumptions, blank nodes, term construction, entailment regime, dataset scope & design analysis only \\
Document & object fields, arrays with declared order or bag policy, selected nested navigation & missing versus null, heterogeneous shapes, array position, duplicate field behavior & design analysis only \\
Vector/ANN & vector-valued attributes, metric and index request, candidate provenance & approximation, recall, nondeterministic ties, training/index state, identity inference & approximate candidate only \\
Polystore & engine assignment, casts, data/query shipping, island boundaries & cast loss, snapshot mismatch, source autonomy, cross-engine cost error & future planning work \\
Arrow & typed record-batch exchange & semantic mappings, query intent, constraints, snapshots & interchange candidate only \\
Substrait & portable relational-plan structure and extensions & \CatDB{} mapping provenance, backend extension parity, exact scalar profile & plan-interchange candidate only \\
\bottomrule
\end{tabularx}
\caption{Preservation matrix.  Each non-relational row is a research
boundary, not implementation evidence.}
\label{tab:cross-model}
\end{table}

\subsection{Property graphs}

GQL gives a standardized property-graph language boundary
\cite{ISOIEC39075_2024}.  A \CatDB{} entity may correspond to a vertex label
and a generator to an edge label, but the correspondence is not automatic.
A graph can distinguish parallel edge identity, attach properties to edges,
and assign multiplicity to paths in ways that a total functional arrow does
not preserve.  Variable-length traversal adds termination and duplicate
questions outside query-v1.

A future graph capability manifest must state whether a relationship is
functional, whether endpoint and edge identity are both returned, how path
walks are counted, how labels and properties are typed, and how graph
snapshots are obtained.  A single-hop functional relationship may lower
exactly under those conditions.  General graph pattern matching remains
unsupported until its semantics enter the profile.

\subsection{RDF and ontology-mediated access}

RDF graphs, SPARQL solutions, R2RML term maps, and entailment regimes have
their own normative semantics
\cite{W3CRDF11Concepts,W3CSPARQL11Query,W3CR2RML}.  \CatDB{} must not equate a
closed finite total instance with an open RDF graph.  A future mapping has to
record IRI and literal construction, blank-node scope, named-graph selection,
entailment assumptions, and multiplicity behavior.

Ontop is a necessary comparative baseline because it already answers
SPARQL queries through mappings over relational databases
\cite{CalvaneseEtAl2017Ontop}.  A \CatDB{} study should use equivalent
source data and query families, then compare expressiveness, rewrite time,
SQL, result semantics, mapping-change diagnostics, and provenance.  Without
that comparison, claims of a categorical advantage over ontology-based data
access would be premature.

\subsection{Documents}

Document systems can preserve nested structure that a flat relational view
must reconstruct.  SQLite JSON functions make JSON queryable, but SQLite
does not acquire a new native JSON storage class merely because those
functions exist \cite{SQLiteJSON}.  A document capability manifest must
distinguish absent fields from explicit null, arrays from bags, stable array
position from unspecified result order, scalar heterogeneity from one typed
domain, and duplicate-key parser policy.

For a bounded, required, homogeneous nested field, a path can be exact.
Unnesting an array multiplies rows and requires an explicit bag rule.
Flattening an object can lose containment or order.  Those decisions belong
in the realization certificate and result oracle.

\subsection{Vectors}

Vector execution is different because the common operator is approximate.
HNSW and large-scale GPU similarity search establish the performance
motivation and tradeoffs \cite{MalkovYashunin2020HNSW,JohnsonDouzeJegou2021Faiss};
Milvus supplies a purpose-built vector-system baseline
\cite{WangEtAl2021Milvus}.  A vector capability manifest must pin dimension,
element type, normalization, distance metric, index family, construction
parameters, search parameters, filters, tie policy, and index revision.

The result artifact records that candidates were generated approximately.
It carries distance or score, source vector and model provenance, index
revision, and measured quality profile.  No threshold converts a probable
match into canonical identity without a separate reconciliation decision.

\subsection{Arrow, Substrait, and polystore composition}

Arrow may reduce serialization costs at process boundaries and standardize
columnar buffers \cite{ApacheArrowColumnar}.  Substrait may provide a portable
relational-plan encoding and an extension mechanism
\cite{SubstraitSpecification,SubstraitExtensions}.  BigDAWG shows that
heterogeneous execution also requires explicit engine islands, shims, and
casts \cite{DugganEtAl2015BigDAWG}.  These are complementary candidates:
\CatDB{} could provide semantic identity and obligations, Substrait a compute
plan, Arrow data exchange, and a polystore layer engine routing.

The experiment must nevertheless measure whether adding an interchange layer
helps or merely adds conversion overhead for embedded SQLite.  Initial
SQLite execution may be simpler through a direct connector.  Arrow and
Substrait are not architectural requirements until an acceptance test
justifies them.

\section{Normalized results and lineage}
\label{sec:results-lineage}

\subsection{Result normalization}

\begin{definition}[Normalized result equivalence]
\label{def:result-equivalence}
\status{\enghyp}
For query artifact \(\mathcal Q\) with output record type \(\rho\), a backend
result normalizer:
\begin{enumerate}
  \item decodes each field through the declared canonical scalar codec;
  \item rejects extra, missing, null, malformed, or out-of-range fields;
  \item orders fields by the output contract;
  \item forms a canonical byte representation of each record; and
  \item counts equal record encodings to produce a finite bag.
\end{enumerate}
Two successful executions are equivalent when these bags are identical.
Two failed executions are equivalent when their canonical error classes and
required evidence agree.
\end{definition}

Sorting may be used as a comparison implementation, but it does not add an
ordering guarantee to the query.  Decimal and date values are compared after
canonical decoding, not as untyped driver strings.  Duplicate-sensitive
fixtures are mandatory because set comparison would miss join and projection
errors.

\subsection{Lineage atoms and expressions}

For the initial single-source slice, a lineage atom is
\[
\ell=(\text{source revision},\text{entity},\text{stable row key}).
\]
A query result row carries a finite provenance expression built from atoms,
mapping and query revision identifiers, and the transformations that combined
or projected them.  Scan introduces an atom; selection retains its input
lineage; projection retains the contributing lineage; inner join combines the
left and right evidence.  A residual or approximation adds an explicit
transformation node.

The initial comparison need not solve arbitrary provenance equivalence.  It
uses a canonical normalized lineage form for the bounded operator fragment.
The form must distinguish two duplicate result rows with different sources
even when their visible values coincide.

\begin{definition}[Lineage mode]
Each query result contract selects one versioned mode:
\[
  \mathsf{RequiredAtoms},\qquad
  \mathsf{RequiredNormalized},\qquad
  \mathsf{NoneAllowed}.
\]
The first two require the lowerer to preserve exactly the columns and
transformations needed by the declared lineage contract. \(\mathsf{NoneAllowed}\)
may prune lineage work only when the request, policy, audit, and comparison
contract do not require it. A connector cannot silently downgrade a required
mode. The decision and resulting projection are recorded in the realization
certificate.
\end{definition}

\subsection{Why values alone are insufficient}

Two plans can produce equal visible values while drawing from different source
records, using different mappings, or omitting evidence.  Such a difference
matters when users ask whether a result survives a schema change or which
source version contributed.  P2 therefore tests both value bags and lineage
bags.  Full semiring provenance belongs to the broader P13 program; this paper
requires only enough structure to falsify the first compiler slice.

\section{Experimental evaluation plan}
\label{sec:experiments}

\subsection{Principles}

No experiment in this section has been run.  The plan is part of the
\enghyp{} acceptance contract.  A valid report preserves failed outputs,
records exact revisions, separates compile, realization, preparation, and
row time, and publishes raw observations with the analysis.

Every run records:

\begin{itemize}
  \item repository commit and dirty-state manifest;
  \item compiler, connector, Haskell, and Lean revisions when present;
  \item schema, mapping, query, policy, capability, and fixture digests;
  \item hardware, operating system, process limits, backend versions and
  build options;
  \item DDL, data-generation seed, statistics procedure, indexes, and source
  snapshot;
  \item SQL template, ordered parameters, normalized IR, dispositions,
  residuals, and lineage rules;
  \item warm/cold state of all three caches;
  \item latency distributions rather than one timing;
  \item rows and bytes at every material boundary;
  \item backend call counts and prepare/replan/reprepare observations;
  \item native explain or counter evidence; and
  \item normalized results, lineage, errors, and comparison verdicts.
\end{itemize}

\subsection{Experiment matrix}

\small
\begin{longtable}{L{0.08\textwidth} L{0.23\textwidth} L{0.28\textwidth} L{0.22\textwidth}}
\caption{Planned P2 experiments.}\label{tab:experiments}\\
\toprule
ID & Question & Required evidence & Falsification condition \\
\midrule
\endfirsthead
\toprule
ID & Question & Required evidence & Falsification condition \\
\midrule
\endhead
\code{P2-E01} & Does parsing, expansion, and normalization produce one typed IR? & fixtures for identity, composition, valid and invalid paths; canonical IR and diagnostics & nondeterminism, ill-typed accepted path, or unexplained mismatch \\
\code{P2-E02} & Does an independent finite evaluator implement the declared bag semantics? & hand-computed duplicate-sensitive cases and property tests & disagreement with hand oracle or unstable result \\
\code{P2-E03} & Does SQLite match the oracle? & emitted SQL and parameters, decoded values, lineage, errors, SQLite manifest & any unclassified value, bag, error, or lineage mismatch \\
\code{P2-E04} & Does PostgreSQL match the portable subset? & same canonical cases for each pinned major, with PostgreSQL manifest & any unclassified cross-backend or oracle mismatch \\
\code{P2-E05} & Are unsupported features rejected? & negative fixtures for null, outer join, aggregation, order/limit, volatile calls, recursion, updates & executable exact plan or unstable diagnostic \\
\code{P2-E06} & Are residuals visible and correct? & forced non-pushdown case, transfer schema, rows/bytes, residual trace, oracle comparison & hidden local work or semantic mismatch \\
\code{P2-E07} & Is approximation labeled? & vector-candidate fixture, metric/index parameters, quality and provenance record & result labeled exact or identity inferred automatically \\
\code{P2-E08} & Are semantic cache transitions correct? & one-at-a-time mutation of query, schema, mapping, profile, compiler revision & stale hit or unnecessary miss outside stated policy \\
\code{P2-E09} & Are realization cache transitions correct? & mutations of backend, capability, policy, layout, lowerer, connector & stale realization or conflated cache layer \\
\code{P2-E10} & Does the semantic layer stay outside row time? & stack/profile traces and call counts across growing row counts with fixed shape & compiler/semantic callback count grows with rows \\
\code{P2-E11} & Are parameter-sensitive plans measured honestly? & skewed values; PostgreSQL auto/generic/custom; SQLite reprepare counters & values hidden, one mode generalized, or events conflated \\
\code{P2-E12} & Is compiled execution competitive with a fair native baseline? & equivalent parameterized native SQL, cold/warm distributions, confidence intervals & declared noninferiority threshold fails \\
\code{P2-E13} & Does capability rejection catch scalar and collation mismatches? & adversarial Unicode, decimal, range, comparison, and codec fixtures & silent coercion or different normalized result \\
\code{P2-E14} & Does plan evidence explain material choices? & estimates, actuals, buffers/counters, settings, row/byte flows & plan claim without versioned native evidence \\
\code{P2-E15} & Can another environment reproduce the result? & clean checkout protocol, locked fixtures, machine-readable summary, checksums & documented run cannot be repeated or evidence is missing \\
\bottomrule
\end{longtable}
\normalsize

\subsection{Semantic compilation benchmarks}

The compilation suite varies entities, generators, path length, query nodes,
mapping-chain length, and rejected obligations independently.  It measures
schema loading only when not already cached, path expansion, type checking,
logical normalization, capability checking, SQL emission, and artifact
serialization separately.  The existing program target of less than
\(100\) ms for a 100-object schema is a target, not a result.

Mapping validation and query expansion are separated.  A benchmark that
revalidates all mappings on every query execution measures a different
architecture from one that consumes immutable validated artifacts.  Both may
be useful, but their cache state must be named.

\subsection{Execution baselines}

The fair native baseline for \(Q_{\mathrm{co}}\) is a human-reviewed
parameterized SQL statement with the same schema, data, indexes, transaction,
parameter values, output fields, bag behavior, and driver decoding.  It is not
an unparameterized literal query, a different projection, or a statement run
under different cache conditions.

At minimum, compare:

\begin{enumerate}
  \item native prepare plus execute;
  \item cold \CatDB{} compile, realize, prepare, and execute;
  \item warm semantic compile but cold realization and prepare;
  \item warm semantic and realization caches but cold backend prepare;
  \item warm semantic and realization caches with a reusable prepared
  statement; and
  \item a forced residual plan.
\end{enumerate}

The program's provisional noninferiority target is less than ten percent
median overhead for cached execution against the fair native baseline.  A
warm realization lookup is provisionally expected to be at least ten times
faster than uncached physical realization.  These thresholds are
pre-registered targets only.  Failing them revises the claim; it is not
filtered out as an inconvenient run.

\subsection{Datasets and selectivity}

The running fixture includes:

\begin{itemize}
  \item one customer with multiple qualifying orders;
  \item distinct customers with equal visible names;
  \item orders exactly at, below, and above the decimal threshold;
  \item duplicate visible projections with distinct stable row keys;
  \item boundary scalar values and adversarial text;
  \item invalid relationship data in a fixture where enforcement is
  intentionally disabled; and
  \item enough scale and skew to change plausible native plan choices.
\end{itemize}

Scale points should include tiny correctness fixtures, medium in-memory
fixtures, and larger fixtures that exceed relevant caches.  PostgreSQL
statistics are refreshed under a recorded procedure.  SQLite indexes and
pragma settings are identical across comparable runs.

\subsection{Cost and cardinality evidence}

For each logical and physical boundary, report estimated and actual rows,
estimated and actual transferred bytes where measurable, source calls, and
selectivity.  PostgreSQL structured explain evidence can expose estimates,
actuals, buffers, settings, and other metrics
\cite{PostgreSQL18Explain}.  SQLite counters expose different information
\cite{SQLiteStmtCounters}; missing metrics are reported as unavailable rather
than estimated from undocumented plan text.

A later cost model can include source latency, transfer volume, join
cardinality, remote compute price, freshness, transformation cost,
provenance-retention cost, consistency, and source load.  P2 only constructs
the evidence needed to test a first planner boundary.

\subsection{Hot-path falsification}

The central systems claim fails under any of the following:

\begin{enumerate}
  \item a semantic compiler or mapping interpreter is invoked once per input
  or output row for a fixed query shape;
  \item a row value triggers row-dependent semantic recompilation rather than
  declared backend planning or a bounded parameter-class choice;
  \item an unsupported operation executes through an unrecorded fallback;
  \item an approximate operator is reported as exact;
  \item normalized value or lineage equivalence fails;
  \item cache reuse ignores a changed declared dependency;
  \item the prepared statement or native-plan state is misreported; or
  \item the pre-registered performance threshold fails on the stated workload.
\end{enumerate}

Failure of one backend does not establish that the architecture is impossible,
but it does falsify the associated backend and workload claim.  The
manuscript and claim ledger must then narrow the scope.

\subsection{Threats to benchmark validity}

Compile-time microbenchmarks can be dominated by allocation, serialization,
filesystem state, or debug builds.  Execution benchmarks can be dominated by
page cache, network placement, client decoding, or result size.  Prepared
statement tests can accidentally compare a cached native plan with an uncached
\CatDB{} path.  PostgreSQL parameter skew can make one generic/custom plan
policy misleading.  SQLite explain output can change across versions.

Mitigations include randomized run order, separated process and connection
lifetimes, fixed warmup rules, repeated distributions, recorded build modes,
server/client clock separation where needed, exact result consumption, and
published raw data.  Benchmarks should report wall time and component
measurements without subtracting inconvenient work.

\section{Reproducibility protocol}
\label{sec:reproducibility}

\subsection{Artifact bundle}

Each experiment run creates an append-only bundle:

\begin{lstlisting}
run/
  manifest.json
  environment.json
  artifacts/
    schema.json
    mappings.json
    query.json
    capability.json
    policy.json
  fixtures/
    ddl.sql
    data-manifest.json
    seed.txt
  compilation/
    logical-ir.json
    dispositions.json
    realization.json
    statement.sql
    parameters.json
  execution/
    result.json
    lineage.json
    errors.json
    native-plan.json
    counters.json
    trace.json
  comparison/
    oracle-result.json
    oracle-lineage.json
    verdict.json
  metrics/
    observations.csv
    summary.json
  checksums.txt
\end{lstlisting}

The bundle contains failures as well as successes.  Raw source credentials,
personal data, and secrets are excluded; synthetic fixtures are preferred for
the first slice.  The manifest points to exact repository and tool revisions
and records whether the tree was dirty.

\subsection{Independent oracle}

The finite evaluator implements the paper denotation directly, without
calling the SQL emitter or backend connector.  Sharing scalar codecs may be
practical, but any shared component is named because it reduces
independence.  Hand-computed tiny cases test the oracle.  Property tests
generate finite required-scalar inputs for scan, select, project, and join.
The Haskell reference model may later serve as another oracle, but no such P2
oracle exists at the evidence cut.

\subsection{Verification sequence}

The required order is:

\begin{enumerate}
  \item validate artifact schemas and hashes;
  \item run positive and negative semantic fixtures;
  \item compare the independent evaluator with hand cases;
  \item run SQLite differential correctness and lineage;
  \item run SQLite cache and hot-path traces;
  \item run PostgreSQL portable-subset correctness and lineage;
  \item run parameter and plan-policy experiments;
  \item run fair native performance comparisons;
  \item reproduce from a clean environment; and
  \item submit the frozen manuscript and artifact digest to domain,
  database-systems, adversarial, code, reproducibility, and readability
  review.
\end{enumerate}

No performance claim is accepted before correctness and lineage gates pass.
No paper claim is labeled machine-checked merely because a Lean file compiles
some P1 definition.

\subsection{Statistical reporting}

Latency reports include sample count, warmup and exclusion rules fixed in
advance, median, selected quantiles, dispersion, and confidence interval or
bootstrap procedure.  Throughput reports identify concurrency, client count,
backpressure, result consumption, and duration.  A result table links each
summary number to raw observations.  Multiple machines or backend versions
are reported separately before any aggregate.

\section{Current implementation status}
\label{sec:implementation-status}

As of the 23 July 2026 evidence cut, this paper is a provisional formal and
systems design.  There is no accepted P2 vertical slice.  Specifically:

\begin{itemize}
  \item no versioned query-v1 serialized profile has been implemented;
  \item no independent finite query evaluator has been implemented;
  \item no Rust \code{catdb-query} or \code{catdb-planner} evidence is
  present;
  \item no Rust \code{catdb-storage-sqlite} or
  \code{catdb-storage-postgres} evidence is present;
  \item no compiler-generated SQL or typed parameter artifact is present;
  \item no SQLite or PostgreSQL native plan has been captured for a
  \CatDB{} query;
  \item no normalized result or lineage differential has been run;
  \item no semantic/realization/backend cache transition suite has been run;
  \item no hot-path trace or performance benchmark has been run;
  \item no Haskell P2 query oracle exists; and
  \item no Lean theorem checks the P2 query or lowering laws.
\end{itemize}

The internally accepted P1 schema, path, and mapping slices supply bounded
inputs to P2.  They do not supply the missing query, realization, connector,
differential, or measurement evidence.  The SQL listings in this manuscript
are specification examples, not captured compiler output.

\subsection{Implementation roadmap}

The minimum vertical slice is:

\begin{enumerate}
  \item freeze the query-v1 schema and canonical fixtures;
  \item implement the independent finite-bag evaluator;
  \item add immutable query and capability artifacts to the Rust semantic IR;
  \item implement versioned lineage modes and measure required versus
  permitted-minimal projection width before backend optimization;
  \item implement typed expansion and normalization for
  \(Q_{\mathrm{co}}\);
  \item implement exact SQLite capability checking, SQL emission, typed
  binding, result decoding, and lineage;
  \item pass \code{P2-E01}--\code{P2-E10} for SQLite;
  \item implement the PostgreSQL portable-subset connector;
  \item pass \code{P2-E04}, \code{P2-E11}, and the cross-backend subset;
  \item add reproducible benchmark packaging; and
  \item only then revise this paper with measured results.
\end{enumerate}

Graph, document, RDF, vector, Arrow, Substrait, and polystore work begins only
after the relational correctness contract is stable enough to expose what
must be generalized.

\section{Limitations and threats to validity}
\label{sec:limitations}

\subsection{Narrow query language}

Query-v1 excludes many operations required by real analytics: nulls, outer
joins, aggregation, grouping, ordering, limits, windows, recursion, updates,
and approximate numeric semantics.  The finite-bag theorem becomes useful
only as these features receive explicit semantics.  Expanding the grammar
will add proof and backend obligations; it should not be done by treating SQL
syntax availability as equivalence.

\subsection{Total functional path bias}

The schema profile's arrows are total functions.  Many real relationships are
optional, many-to-many, temporal, uncertain, or contradictory.  Encoding
them as bridge entities may be possible but changes query shape and user
meaning.  Property graphs and RDF can represent relationships that do not fit
this bounded profile naturally.

\subsection{Mapping-witness burden}

An explicitly directional read witness prevents unsafe inversion, but it
requires substantial authoring and validation.  Automatic schema matching
could propose assignments, yet suggestions do not establish meaning.  The
program has not measured whether witness reuse reduces maintenance enough to
justify the additional semantic artifacts.

\subsection{Backend-semantic gap}

The abstract lowering theorem assumes exact primitive realizations.  Real SQL
engines have nulls, coercions, collations, transaction effects, errors,
planner changes, and driver behavior.  Differential tests can find mismatches
but do not prove all executions correct.  Formal refinement to a precisely
modeled SQL subset would strengthen the result at substantial cost.

\subsection{Native-plan observability}

Explain and counters reveal only what the backend exposes.  PostgreSQL
\code{EXPLAIN ANALYZE} changes measurement conditions and executes the query;
SQLite explain formats are unstable across versions
\cite{PostgreSQL18Explain,SQLiteExplain,SQLiteEQP}.  Absence of an observed
semantic callback is not by itself proof that every runtime path avoids one.
Profiling, call counting, and code inspection must agree.

\subsection{Performance generalization}

SQLite and PostgreSQL results on synthetic Customer/Order data will not
generalize automatically to remote federation, graph traversal, document
unnesting, vector search, or distributed execution.  Hardware, data skew,
indexes, driver choices, cache state, and result size can reverse comparisons.
The evaluation therefore scopes every result to a manifest and workload.

\subsection{Provenance cost}

Lineage improves auditability but can increase projection width, transfer,
storage, and comparison cost.  The first lineage form is intentionally
bounded.  Full provenance semantics and compression strategies belong to P13.
P2 must compile the explicit lineage mode, reject any silent downgrade, and
report required-lineage and policy-permitted minimal-lineage execution
separately rather than hiding the cost. No zero-cost abstraction or negligible
overhead is assumed; early fixtures and microbenchmarks record added columns,
bytes, allocations, and latency before an optimization claim is allowed.

\subsection{No update semantics}

The paper addresses reads.  An exact read mapping need not support safe
write-back.  Inversion, lenses, target constraints, authority, conflicts, and
multi-source ambiguity belong to the bidirectional-mappings program.  Nothing
here authorizes writes through a canonical query.

\subsection{No distributed-consistency result}

The snapshot premise in \Cref{prop:lowering} is local and abstract.
Cross-source consistent snapshots, replica convergence, causal ordering, and
CAP-style tradeoffs are not solved by semantic compilation.  A federated
result must state its consistency and freshness contract; P2 does not provide
one.

\section{Open questions}
\label{sec:open-questions}

\begin{enumerate}
  \item What smallest scalar profile has identical, useful behavior across the
  finite evaluator, Rust, SQLite, PostgreSQL, and later Haskell?
  \item Which wider-precision or mixed-scale decimal profile can extend
  \(\mathsf{Decimal64}(p,s)\) without weakening cross-backend exactness?
  \item Which read-rewrite witnesses can be derived from lawful categorical
  mappings, and which require explicit view definitions?
  \item What decidable fragment of path equations is useful for query
  normalization without introducing an unbounded equality procedure?
  \item When does equation-based rewriting reduce work, and when does it make
  planner estimates or provenance harder to interpret?
  \item How should semantic and physical statistics be versioned so that a
  realization cache is neither unsound nor needlessly cold?
  \item Which SQLite binding exposes preparation flags, statement counters,
  cancellation, and streaming with the least hidden work?
  \item Which PostgreSQL driver exposes typed codecs, cancellation, streaming,
  prepared-plan policy, and structured evidence sufficiently for the
  reproducibility bundle?
  \item How should a residual evaluator enforce memory and backpressure limits
  while preserving bag and error semantics?
  \item Can a normalized lineage algebra remain compact enough for ordinary
  interactive queries?
  \item Is Arrow beneficial at the embedded SQLite boundary, or should it be
  reserved for process and network exchange?
  \item Can Substrait represent the admitted logical plan without a custom
  extension, and what \CatDB{} evidence necessarily remains outside it?
  \item Which property-graph path fragment corresponds exactly to the total
  functional-arrow profile?
  \item How should document missing values, arrays, and heterogeneous fields
  enter an extended type system?
  \item What quality and provenance contract is sufficient for an ANN operator
  to participate safely as a candidate generator?
  \item What benchmark demonstrates that versioned mappings reduce repair
  surface rather than merely relocating configuration?
  \item Which paper-level lowering lemmas have enough value and stable scope to
  mechanize in Lean?
\end{enumerate}

These are not rhetorical future-work items.  Each can change the admissible
profile, cache keys, evidence format, or central performance claim.

\section{Conclusion}
\label{sec:conclusion}

The physical-compilation claim has a narrow boundary.  Typed, versioned
mappings expand a canonical query into source meaning, and the logical IR
fixes its records, finite bags, predicates, projections, and inner joins.  A
versioned capability manifest marks each operation as exact, residual,
approximate, or unsupported.  The resulting realization contains a
parameterized statement and its evidence.  SQLite or PostgreSQL still chooses
the scans, indexes, joins, and row-execution details.

The three paper proofs cover the abstract design: well-witnessed path
expansion preserves endpoints, exact compositional lowering preserves the
admitted finite-bag denotation, and dependency-complete cache keys permit sound
reuse under the stated assumptions.  These are not compiler or backend
results.  The repository still lacks the query language, evaluator, planner,
connectors, generated statements, differential results, native-plan captures,
hot-path traces, benchmarks, Haskell oracle, and Lean query theorem needed to
validate the systems claim.

The next credible milestone is one complete Customer/Order vertical slice.  It
needs immutable inputs, typed expansion, SQLite emission, independent result
and lineage equivalence, explicit cache states, native evidence, and a trace
showing that semantic work does not scale with the row count for a fixed query
shape.  PostgreSQL parity would then use the same portable contract.  Graph,
document, vector, Arrow, Substrait, and polystore claims remain preservation
analysis until those gates pass and each later backend supplies its own
evidence.

\appendix

\section{Formal typing rules for the core fragment}
\label{app:typing}

Let \(\Sigma\) map relations and aliases to record types, and let \(\Gamma\)
map parameters to scalar domains.  Expression typing has the expected rules:
\[
\frac{\ell:\tau\in\rho}{\Gamma;\rho\vdash \ell:\tau},
\qquad
\frac{x:\tau\in\Gamma}{\Gamma;\rho\vdash :x:\tau}.
\]
For a declared total comparison on \(\tau\):
\[
\frac{\Gamma;\rho\vdash e_1:\tau\qquad
      \Gamma;\rho\vdash e_2:\tau}
     {\Gamma;\rho\vdash e_1\geq e_2:\mathsf{bool}}.
\]
No coercion rule is present.  A comparison between decimal and text is
ill-typed even if a backend would coerce it.

Query typing includes:
\[
\frac{\Sigma(R)=\rho}
     {\Sigma;\Gamma\vdash\mathsf{Scan}(R,\alpha):\Bag(\alpha.\rho)}
\]
and
\[
\frac{\Sigma;\Gamma\vdash Q:\Bag(\rho)\qquad
      \Gamma;\rho\vdash\varphi:\mathsf{bool}}
     {\Sigma;\Gamma\vdash\mathsf{Select}_{\varphi}(Q):\Bag(\rho)}.
\]
If projection expressions \(e_i\) have types \(\tau_i\), then:
\[
\frac{\Sigma;\Gamma\vdash Q:\Bag(\rho)\qquad
      \Gamma;\rho\vdash e_i:\tau_i\ (1\leq i\leq n)}
     {\Sigma;\Gamma\vdash
      \mathsf{Project}_{\ell_i=e_i}(Q):
      \Bag(\langle\ell_1:\tau_1,\ldots,\ell_n:\tau_n\rangle)}.
\]
For join:
\[
\frac{
 \Sigma;\Gamma\vdash Q_1:\Bag(\rho_1)\quad
 \Sigma;\Gamma\vdash Q_2:\Bag(\rho_2)\quad
 \Gamma;\rho_1\!\times\!\rho_2\vdash\theta:\mathsf{bool}}
 {\Sigma;\Gamma\vdash
  \mathsf{Join}_{\theta}(Q_1,Q_2):\Bag(\rho_1\!\oplus\!\rho_2)}.
\]
The labels of \(\rho_1\) and \(\rho_2\) must be disjoint after alias
qualification.

\section{Running-query derivation sketch}
\label{app:derivation}

Let
\[
\begin{aligned}
\rho_o={}&\langle
o.id:\mathsf{uuid},
o.customer\_id:\mathsf{uuid},
o.total:\mathsf{decimal}\rangle,\\
\rho_c={}&\langle
c.id:\mathsf{uuid},
c.name:\mathsf{string}\rangle.
\end{aligned}
\]
The two scans have types \(\Bag(\rho_o)\) and \(\Bag(\rho_c)\).  Both sides
of \(o.customer\_id=c.id\) have type \(\mathsf{uuid}\), so the join predicate
is total Boolean under the required-field profile.  The join has type
\(\Bag(\rho_o\oplus\rho_c)\).  The parameter context contains
\(:minimumTotal:\mathsf{decimal}\), so
\(o.total\geq :minimumTotal\) is a typed total predicate.  The four projected
expressions have types
\[
\mathsf{uuid},\quad\mathsf{string},\quad
\mathsf{uuid},\quad\mathsf{decimal}.
\]
Consequently \(L_{\mathrm{co}}\) has the output type:
\[
\Bag\left(
\left\langle
\begin{array}{l}
customerId:\mathsf{uuid},\\
customerName:\mathsf{string},\\
orderId:\mathsf{uuid},\\
orderTotal:\mathsf{decimal}
\end{array}
\right\rangle\right).
\]

The derivation becomes invalid if either join key is nullable, the UUID
codecs disagree, the decimal comparison is not exact, or the source
relationship does not have the totality required by the navigation witness.
Such facts cannot be repaired by the typing tree alone.

\section{Review-time claim checklist}
\label{app:claim-checklist}

\small
\begin{longtable}{L{0.31\textwidth} L{0.18\textwidth} L{0.39\textwidth}}
\caption{Claims to inspect during paper review.}\label{tab:claim-checklist}\\
\toprule
Claim & Present label & Required promotion evidence \\
\midrule
\endfirsthead
\toprule
Claim & Present label & Required promotion evidence \\
\midrule
\endhead
Typed path expansion preserves endpoints & proved in this paper & optional Lean theorem and fixture cross-check \\
Abstract exact lowering preserves bag denotation & proved in this paper & machine-checking plus primitive-refinement work for stronger claim \\
Dependency-complete cache reuse is sound & proved in this paper & canonicalization/hash tests and mutation suite \\
SQLite realization is correct & engineering hypothesis & \code{P2-E03} value, error, and lineage differential \\
PostgreSQL portable subset is correct & engineering hypothesis & \code{P2-E04} cross-backend differential \\
Semantic compilation stays outside row time & engineering hypothesis & \code{P2-E10} trace and call-count evidence \\
Cached overhead is below target & engineering hypothesis & \code{P2-E12} fair distributions \\
Mappings improve integration maintenance & open in P2 & P4 integration-complexity experiment \\
Graph/document lowering is exact for a useful fragment & open & formal profile and differential connector evidence \\
Vector execution is safe as candidate generation & open & quality, provenance, and reconciliation study \\
\bottomrule
\end{longtable}
\normalsize

\bibliographystyle{plain}
\bibliography{references}

\end{document}
