-
Notifications
You must be signed in to change notification settings - Fork 0
Scripts/make arxiv #9
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Changes from all commits
847f6fc
8412186
3042751
29e108c
b546bb0
8c3de77
d154f03
35eee2b
d80fd02
3eed064
f5bf197
0d51bfb
da8a31e
6a24c1c
94aaa75
aa06840
3d653b6
7fc7d20
4a95716
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
| Original file line number | Diff line number | Diff line change | ||||
|---|---|---|---|---|---|---|
|
|
@@ -3,7 +3,7 @@ \section{Determinism and Confluence} | |||||
| \label{sec:determinism} | ||||||
|
|
||||||
| Throughout this section we work under the standing assumptions | ||||||
| summarised in \cref{sec:assumptions}. | ||||||
| summarised in the Standing Assumptions section. | ||||||
|
Contributor
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Revert to Replacing
Apply this diff to restore best practice: -summarised in the Standing Assumptions section.
+summarised in \cref{sec:assumptions}.📝 Committable suggestion
Suggested change
🤖 Prompt for AI Agents |
||||||
|
|
||||||
| We sketch the concurrency discipline, define independence, and state the | ||||||
| main confluence theorems for tick-level execution, working with RMG | ||||||
|
|
||||||
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -3,7 +3,7 @@ \section{Introduction} | |
| \label{sec:intro} | ||
|
|
||
| Modern computation is built on mutable state and loosely specified | ||
| concurrency. As systems become distributed, multi-core, and | ||
| concurrency. As systems become distributed, multicore, and | ||
| AI-mediated, this leads to nondeterminism, opaque failure modes, | ||
| unreproducible behavior, and fundamentally incomplete provenance. | ||
|
|
||
|
|
@@ -22,36 +22,39 @@ \section{Introduction} | |
| (\cref{thm:tick-confluence,thm:two-plane,thm:global}); and | ||
| \item the \emph{entire} interior evolution of a computation is stored | ||
| in a compact \emph{provenance payload} attached to a single edge, | ||
| providing an information-complete ``holographic'' encoding. | ||
| yielding an information-complete holographic encoding. | ||
| \end{itemize} | ||
|
|
||
| The technical starting point is algebraic graph transformation using the | ||
| double--pushout (DPO) approach in adhesive categories, together with the | ||
| Recursive Metagraph (RMG) object model we define in Section~\ref{sec:rmg}. | ||
| We extend this setting with: | ||
| Our technical starting point is algebraic graph transformation via | ||
| double-pushout (DPO) graph rewriting in adhesive categories. We pair this with | ||
| the Recursive Metagraph (RMG) object model introduced in | ||
| Section~\ref{sec:rmg}. We extend this setting with: | ||
|
|
||
| \begin{enumerate}[leftmargin=*] | ||
| \item a precise notion of RMG state and its category; | ||
| \item a two-plane concurrent operational semantics with | ||
| attachment--then--skeleton publication, together with | ||
| confluence results: tick-level determinism and two-plane | ||
| commutation (Theorems~\ref{thm:tick-confluence} and | ||
| \ref{thm:two-plane}), and, under standard rewrite-theory | ||
| hypotheses, global confluence (Theorem~\ref{thm:global}); | ||
| \item a provenance payload calculus giving \emph{computational | ||
| \ref{thm:two-plane}), and---under the standing assumptions and | ||
| standard rewrite-theoretic conditions---global confluence | ||
| (Theorem~\ref{thm:global}); | ||
|
Comment on lines
37
to
+41
Contributor
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. 🧹 Nitpick | 🔵 Trivial Spell out or cross-reference the exact hypotheses behind “global confluence” “under the standing assumptions and standard rewrite-theoretic conditions—global confluence (Theorem~\textbackslash ref{thm:global})” is still pretty opaque at intro level. Right now a reader has no idea whether that means “termination + local confluence on the skeleton” or something more bespoke. I’d either (a) add an explicit pointer to where those conditions are enumerated (table/section/definition), or (b) mirror the theorem’s statement more literally here so you’re not hand-waving the hypotheses in the most prominent summary paragraph. 🤖 Prompt for AI Agents |
||
| \item a provenance payload calculus yielding \emph{computational | ||
| holography}; | ||
| \item an MDL-based quasi-pseudometric on observers, the \emph{rulial | ||
| distance}, and a correspondence between RMG derivations and | ||
| multiway systems that clarifies the relationship to Wolfram's | ||
| Ruliad. | ||
| \end{enumerate} | ||
|
|
||
| We deliberately keep the system-level \AION{} stack\footnote{% | ||
| We keep the system-level \AION{} stack\footnote{% | ||
| Pronounced ``eye-ON'' (rhymes with \emph{aeon}), with stress on the second syllable.} | ||
| (AIONOS, Echo, Wesley, etc.) mostly offstage in this paper, mentioning | ||
| it only to motivate the mathematics. The companion ``\COMPUTER{}'' | ||
| paper will build on these results to define the full machine model and | ||
| operating system. | ||
| (AIONOS, Echo, Wesley, etc.) largely offstage, mentioning it only to | ||
| motivate the mathematical structure; we assume only that implementations | ||
| respect the axioms and invariants stated in Sections~\ref{sec:rmg}--\ref{sec:discussion}, | ||
| with scheduling, representation, and persistence details intentionally | ||
| out of scope. A companion ``\COMPUTER{}'' paper will build on these | ||
| results to define the full machine model and operating system. | ||
flyingrobots marked this conversation as resolved.
Show resolved
Hide resolved
|
||
|
|
||
| \medskip | ||
| \noindent | ||
|
|
@@ -63,18 +66,19 @@ \section{Introduction} | |
| deterministic semantics independent of scheduler serialization | ||
| order; | ||
| \item \emph{Two-plane commutation} (Theorem~\ref{thm:two-plane}): | ||
| attachment and skeleton updates can be applied in either order up to | ||
| isomorphism, via a fibration structure; | ||
| attachment and skeleton updates commute up to isomorphism; | ||
| \item \emph{Worldline uniqueness} (Corollary~\ref{cor:worldline-uniqueness}): | ||
| global uniqueness of complete derivation worldlines up to typed | ||
| open graph isomorphism, extending per-tick commutation to | ||
| scheduler-independent whole runs; | ||
| under the standing assumptions (tick confluence, two-plane | ||
| commutation, conditional global confluence, and holography), the | ||
| boundary data $(S_0,P)$ determines the interior derivation uniquely | ||
| up to typed open graph isomorphism, extending per-tick commutation | ||
| to whole-run semantics; | ||
| \item \emph{Computational holography} (Theorem~\ref{thm:holography}): | ||
| the boundary data $(S_0,P)$ is information-complete with respect to | ||
| the interior evolution, enabling reconstruction of the full | ||
| derivation volume; | ||
| \item \emph{Rulial distance} (Theorem~\ref{thm:rulial-triangle}): | ||
| an MDL-based quasi-pseudometric on observers that quantifies the | ||
| complexity of translating between different views of the same | ||
| computation. | ||
| the triangle-inequality property of an MDL-based quasi-pseudometric | ||
| on observers, capturing the complexity of translating between | ||
| different computational views. | ||
| \end{enumerate} | ||
Uh oh!
There was an error while loading. Please reload this page.