The Calculus of Everything (Part I) and The Theory of Everything? (Part II)

⟨Part I of II⟩ The Calculus of Everything A Computational Perspective on Physical Interaction via Structural Operational Semantics (SOS) A Tutorial Introduction to Structural Operational Semantics (SOS) for Physicists preparing to read ⟨Part II of II⟩:“The Theory of Everything?” Claus Brabrand Center for Computing Education Research (CCER) IT University of Copenhagen (ITU) Copenhagen, Denmark [email protected] Abstract The Standard Model of particle physics is traditionally specified through a Lagrangian density and interpreted using the machinery of quantum field theory. In this paper we explore an alternative and entirely standard formalism for describing interactions, structure, and the stepwise evolution of systems over time. Structural Operational Semantics (SOS) is the half-century-old foundation for the formal semantics of programming languages and, by extension, the design of compilers, interpreters, type systems, static analyses, process calculi, model checking, and verified compilation. In the SOS view, particles become processes,interaction vertices become inference rules, and amplitudes decorate transitions. Probabilistic predictions are, in principle, compatible with the Born rule applied to derivations in the resulting transition system. Even at a descriptive level, this recasting provides a useful structural perspective on quantum electrodynamics: when expressed in SOS, unlabeled transition systems induce an asynchronous operational reading, in which emission and absorption are represented as temporally separated events (steps), while labeled transition systems induce a synchronous reading, in which emission and absorption are treated as a single coordinated interaction across spatial separation. Once expressed in SOS form, the Standard Model becomes amenable to decades of computational techniques: analysis (conservation invariants), comparison (e.g. asynchronous vs. synchronous formulations), verification (internal consistency), validation (alignment with experiment), and simulation through execution or compilation. This does not alter physics—it rephrases it in a mathematically precise, compositional language used in theoretical computer science: The Calculus of Everything.1 This paper ⟨ Part I of II ⟩ serves as a tutorial introduction to SOS for physicists, and simultaneously as an entry point for SOS-familiar computer scientists engaging with physical models: quantum and relativistic behavior appear as further instances in a lineage of process systems, expressible in familiar operational terms. 1 Aka “The Universal Calculus.” In the 17th century Newton developed the calculus of continuous change, while Leibniz proposed a Characteristica Universalis, a symbolic calculus for all knowledge. Here we suggest a modern continuation of that vision: a calculus for the unfolding of events in the universe. 1 Introduction Structural Operational Semantics (SOS) was developed by Gordon Plotkin in 1981 during an extended sabbatical at Aarhus University in Denmark [ 33 ]. Over the last half century, SOS has become a standard formalism for describing and reasoning about computational processes: it underpins the formal semantics of modern programming languages and, by extension, the design of compilers, interpreters, type systems, process calculi, static analyses, and model checkers. This paper explores the consequences of viewing physical interactions through a computational, structural, and operational perspective. Instead of describing the Standard Model via a Lagrangian density and deriving predictions through the machinery of perturbative quantum field theory, we consider what changes when physical interactions are expressed as inference rules over labelled transition systems. In this setting, particles are represented as processes; interaction vertices as rules; and amplitudes as annotations on transitions. Probabilistic predictions are, in principle, compatible with applying the Born rule to derivations, although this aspect is not developed further here. Physics and computer science traditionally employ distinct formalisms and descriptive languages: • Physics: The Standard Model is specified compactly through a Lagrangian formulation, with predictions obtained via Feynman diagrams, renormalization, and perturbative expansions [30]. • Computer Science: SOS provides rule-based, compositional descriptions of interacting systems, supporting explicit reasoning about equivalence, simulation, compositionality, and invariants [34, 40]. Recasting aspects of the Standard Model in SOS form does not alter the underlying physics or its empirical predictions. Rather, it reformulates them in a rule-based and compositional format, making them accessible to decades of established techniques from programming-language theory and concurrency. These include methods for reasoning,analysis,comparison,simulation,verification, Claus Brabrand and validation of interacting systems, such as bisimulation, equivalence checking, congruence formats, modal logics, and mechanized verification. These tools provide alternative ways to compare formulations, identify invariants, and expose structural regularities that may be less apparent when working exclusively with differential equations. Connections between physics, logic, and computation have a long history [ 1 ], but an explicit structural operational semantics for interactions in the Standard Model has not previously been articulated. This paper forms ⟨ Part I of II ⟩ of a two-paper series. Here we introduce the operational machinery—relations, inference rules, labelled transition systems, structural congruence, and invariants—in a form intended to be accessible to physicists and readers unfamiliar with SOS. ⟨ Part II of II ⟩ explores how the same operational framework may be applied to physical interaction domains, using synchronization rules as a means to examine structural commonalities across different settings. These developments are exploratory and are presented as a conceptual extension of the present formalism. Disclaimer. Nothing in this work should be interpreted as suggesting that the universe is a digital computer, that it executes a program, or that it is being run as a simulation. The term “computational semantics” refers solely to the use of established mathematical tools from the theory of programming languages and process calculi for describing and analyzing interaction structures. The framework developed here is intended as a descriptive and formal perspective, not as an ontological claim about the nature of reality. 2 Evolving Perspectives on the Universe The history of physics can be viewed as a succession of changing perspectives on how physical systems are described and reasoned about, each redefining what it means to model, analyze, and predict their behavior. The Classical Perspective. In the seventeenth century, Isaac Newton developed the calculus as a mathematical language for continuous change. It provided a precise mathematical formalism in which motion, force, and causality could be expressed and predicted. The success of this calculus of motion marked the beginning of physics as a quantitative science. The Symbolic Perspective. While Newton used calculus to describe motion in nature, Gottfried Wilhelm Leibniz envisioned something broader: a Characteristica Universalis, a universal symbolic calculus for knowledge. He imagined reasoning itself as calculation—a view that later resonated through logic, mathematics, and computer science. In spirit, the present work draws on this idea by treating physical description as a matter of formal symbolic reasoning, rather than as a claim about the nature of reality. The Mechanical Perspective. For over two centuries, physics followed Newton’s classical vision: a deterministic system governed by continuous equations of motion. Pierre-Simon Laplace distilled this view into a philosophy of predictability. In computational terms, this corresponds to a stateful, total-function semantics, in which every configuration has exactly one successor state. Reasoning about physical systems thus became reasoning by calculation. The Statistical Perspective. In the late nineteenth century, Ludwig Boltzmann and James Clerk Maxwell introduced probability into mechanics, formulating the statistical laws of thermodynamics [ 3 , 24 ]. Even when underlying laws are deterministic, the collective behavior of large numbers of particles can only be described through distributions and averages. Entropy emerged as a bridge between microscopic dynamics and macroscopic irreversibility, extending ideas initiated by Clausius [ 6 ]. This marked a shift toward reasoning about physical systems in terms of information content rather than individual trajectories, a connection later formalized by Shannon [ 35 ]. In computational terms, this corresponds to the emergence of probabilistic state semantics. The Relativistic Perspective. At the turn of the twentieth century, Albert Einstein replaced Newton’s absolutes with a dynamic geometric description of space and time. In the Special Theory of Relativity (1905) and later the General Theory of Relativity (1915), spatial and temporal coordinates were unified within a fourdimensional manifold, spacetime, whose curvature encodes gravitational effects. While the resulting models remain continuous and law-governed, the descriptive focus shifted from mechanical forces to geometric structure. The Quantum Perspective. Almost simultaneously, Max Planck introduced the quantum of action, and Albert Einstein the quantum of light, revealing that energy exchange occurs in discrete units. Continuous trajectories were replaced by quantized transitions. Quantum mechanics, developed by Bohr, Heisenberg, and Schrödinger, introduced intrinsic probabilistic descriptions and treated measurement as an interaction between system and apparatus. In computational terms, this marks a shift from a deterministic total-function view to a nondeterministic transition semantics, in which a configuration may evolve into multiple possible successor states. At the same time, it corresponds, in semantic terms, to a move from continuous evolution to discrete transition structure. The Informational Perspective. By the mid-twentieth century, information emerged as a central analytic concept. Wheeler’s slogan “It from Bit” [ 39 ] captured this shift, while Landauer and Bennett established links between information processing and thermodynamics [2, 18]. Feynman and Deutsch showed that quantum systems could be modeled as information processors [ 8 , 15 ]. Physical behavior was increasingly described in informational terms. The Computational Perspective. More recently, informational descriptions have been extended into explicitly computational ones. Lloyd quantified physical limits on computation [ 20 , 21 ], while Tegmark argued for mathematical descriptions of physical models [ 37 ]. Other authors proposed discrete computational models of physical processes [ 16 , 41 , 43 ]. In parallel, diSessa demonstrated that rule-based, executable models can capture core aspects of physical behavior [ 10 , 12 ], representing a step toward the operational viewpoint adopted here. The Semantic Perspective. The present work continues this trajectory but shifts the focus from ontology to formalism. Rather than asking what physical reality is, it asks how physical interactions can be described and reasoned about. By importing formal tools from computer science—relations,inference systems,transition systems,invariants,congruences,equivalences,simulation, and validation—we propose a semantic perspective for physical modeling: the computational semantics of physics: The Calculus of Everything — Part I of II Experimental Theoretical Phenomenon Semantics REPRESENT VALIDATE EXPERIMENT OBSERVE EXPERIMENT → THEORY EXPERIMENT ← THEORY CHARACTERIZATION STATE KNOWLEDGE TRANSITION 5 THEORY 0 2 4 6 8 5 7 9 13 EVOLVE 𝛾 𝛾➜𝛾 ' VERIFY STATICS DYNAMICS Figure 1: From experimentally observed phenomena to formal semantic descriptions and back again—a computationalsemantics perspective on physical modeling. The Calculus of Everything. In concert, these perspectives reveal a gradual shift toward increasingly explicit, rule-based descriptions. From continuous motion to geometric structure, from probabilistic ensembles to discrete transitions, the formalisms used to describe physical systems have become progressively more operational and compositional. From determinism to nondeterminism. Viewed from a semantic perspective, this historical arc corresponds to a transition from deterministic to nondeterministic descriptions. Classical mechanics describes evolution as a total function: 𝑓:𝑆→𝑆, where each state, 𝑠∈𝑆 , has a unique successor state, 𝑠′∈𝑆 . Statistical and quantum theories generalize this to relations: 𝑓:𝑆→2𝑆, in which a configuration may evolve into a set of possible successor states. From a relational perspective, this requires no additional machinery: nondeterminism is captured directly by allowing a state simply to be in relation with multiple successors. In computer science, 𝑆 is a state space; in physics, it corresponds to the set of admissible system configurations. Despite using different mathematical formalisms, both disciplines describe system evolution as structured valid movement through such spaces. The present work seeks to reconcile these perspectives within a single, compositional framework—a calculus for describing the evolution of interacting systems. The next section develops this framework from first principles, beginning with the notion of a relation. 3 Framework for Computational Physics Figure 1 proposes a framework for working with the computational semantics of physical modeling, inspired by analogous models from computing [ 5 , 23 , 36 ]. We describe each of the ten steps (0)–(9) and give forward references to where they will be introduced in this paper. Thus, Figure 1 also serves as a road map for the structure of the paper, including mild spoilers of what will be covered. These steps are not meant to prescribe a scientific method, but to make explicit, in operational terms, stages of reasoning already familiar in physics. We now summarize the ten steps: (0) Observe: The process begins with observing a physical phenomenon in the experimental domain (e.g., emission and absorption of photons). These empirical observations form the raw input for subsequent formalization. (1) Characterize: Observables are identified, measured, and described. This yields a structured description of relevant quantities and relations (e.g., amplitude, frequency, energy). (2) Abstract: From the characterized data, regularities and invariants are abstracted (see §4), preparing the ground for a theoretical representation within the semantic domain. (3) State (Static Systems): The abstracted entities are formalized as configurations or states (see §4.1). In the photon example, this corresponds to representing a wave as a particle state 𝛾𝑘. (4) Implement: The static representation is instantiated within a rule system—typically a structural operational semantics (SOS) (see §4.1 and §4.2). This defines how configurations can evolve and interact. (5) Evolve (Dynamic Systems): The semantics defines transitions between configurations (see §4.2), such as 𝛾→𝛾′ , capturing the system’s operational evolution. (6) Verify: The semantic rules are checked for internal consistency, soundness, and closure (see §5). Verification ensures that the formal model is self-coherent before empirical testing. (7) Model: The verified statics and dynamics together constitute a coherent model (see §5). This model provides a formal, operational description of the system’s behavior. (8) Validate: The model’s predictions are compared against observed phenomena (see §7). Validation tests whether the formal semantics adequately accounts for the observed phenomena within the intended scope of the model. (9) Consolidate Knowledge: Successful validation consolidates theoretical and experimental understanding. The resulting knowledge feeds back into future observation and the reformulation of semantics. Beyond these ten steps (0–9), the overall process naturally extends into further iterative cycles of stepwise refinement. These successive passes revisit and progressively sharpen or extend the representation, the semantics, and the empirical grounding. Concrete instances of such refinement cycles correspond to the subsequent step ranges (10–19), and—at a larger scale—even (20–29). Please note that statics (step 3) concerns the “representation-of - information” (i.e. data), whereas dynamics (step 5) concerns the “transformation-of -representation-of -information” (computation). 2 2 In continental Germanic languages (Danish, Dutch, German, Norwegian, and Swedish), this parallelism is especially transparent because compound nouns are formed by concatenation, e.g., Informationsrepræsentation and Informationsrepræsentationstransformation (shown here in Danish). Claus Brabrand 4 Descriptive Semantics Inspired by Gordon Plotkin’s seminal “A Structural Approach to Operational Semantics” [ 33 ] and following the expository structure of [ 32 ], this section develops the foundational semantic machinery on which the remainder of the framework rests. 4.0 Fundamental Building Block: The Relation Before constructing a calculus for interaction, we must first identify the most primitive structure on which such a framework can rest. Seen from a semantic perspective, both physics and computing can be described in terms of a single underlying primitive: the relation—a formal connection between elements, states, or events. In physics this notion is typically implicit, embedded in equations, symmetries, and causal dependencies; in computing it is made fully explicit as the basic building block of meaning. Everything that follows—inference, transition, interaction, invariance, and equivalence—will be constructed from this single, “atomic” idea: the relation. From Intuition to Definition. At an intuitive level, a relation specifies what is-related-to what. In computing, for example, (1+2)*3 →3*3 →9, where → denotes an operational evaluation step; whereas in physics, 238U⇝234Th⇝234Pa, where ⇝ denotes radioactive decay. In both cases, each arrow represents a single transition in the underlying relation. Formally, a (binary) relation 𝑅over a set 𝑆isasubset: 𝑅⊆𝑆×𝑆, where a pair (𝑠, 𝑠′) ∈ 𝑅 indicates that 𝑠 is-related-to 𝑠′ under 𝑅 , commonly written in infix notation as 𝑠 𝑅 𝑠′. Concretely, (3*3,9) ∈ →,(238U,234Th) ∈ ⇝. For improved readability, both relations also admit a more HomoSapiens–friendly binary infix shorthand syntax: 3*3 →9,238U⇝234Th. Non-examples are expressed using negated membership: (3*3,8)∉→,(238U,235U)∉⇝, indicating that 3*3 does not evaluate to 8 , and that 238 Udoes not decay into 235 U. Both can also be written in the corresponding reader-friendly binary infix notation: 3*3 ↛8,238U⇝235U. Properties that Enable Reasoning. The familiar structural properties of relations—reflexivity, symmetry, transitivity, and antisymmetry—form the logical backbone of reasoning in both computing and physics. They allow us to understand how systems compose, evolve, and propagate effects. Common properties include: •Reflexive: ∀𝑠∈𝑆:𝑠 𝑅 𝑠. •Symmetric: ∀𝑠,𝑠′:𝑠 𝑅 𝑠′⇒𝑠′𝑅 𝑠. •Transitive: ∀𝑠, 𝑠′,𝑠′′ :(𝑠 𝑅 𝑠′∧𝑠′𝑅 𝑠′′) ⇒ 𝑠 𝑅 𝑠′′. •Anti-symmetric: ∀𝑠,𝑠′:(𝑠 𝑅 𝑠′∧𝑠′𝑅 𝑠) ⇒ 𝑠=𝑠′. Unsurprisingly, equality ( = ) is an equivalence relation (reflexive, symmetric, and transitive), whereas the “less than” relation ( < ) is transitive but neither reflexive nor symmetric. Reflexive–Transitive Closure. Composing steps yields the socalled reflexive–transitive closure of 𝑅, written 𝑅∗: 𝑠 𝑅∗𝑠′iff ∃𝑛≥0 : 𝑠=𝑠0𝑅 𝑠1𝑅 . . . 𝑅 𝑠𝑛=𝑠′. Reflexivity allows zero steps ( 𝑠 𝑅∗𝑠 ), and transitivity allows arbitrarily many steps to compose. In computing: (1+2)*3 →∗9. In physics: 238U⇝∗234Pa. Unary Relations (Predicates). A unary relation classifies individual elements rather than relating pairs. Judgments such as: ⊢even 𝑛⊬even 𝑛 state that 𝑛 either does or does not belong to the unary relation of even numbers; alternatively written as 𝑛∈ ⊢even or 𝑛∉⊢even. Unary relations arise throughout both computing and physics. In computing, typing judgments such as: ⊢int 3⊬int true classify the type of 3 as an integer and true as not an integer. In physics, property judgments such as: ⊢stable 4 2He ⊬stable 238 92U classify 4 2He as stable and 238 92Uas not stable (aka, unstable). Beyond Binary Relations. Relations may have higher arity: 𝑅⊆𝑆𝑛. Unary relations express predicates (e.g. even numbers); ternary relations express multi-variable laws such as 𝑥+𝑦=𝑧, 𝐹 =𝑚𝑎, 𝐸 =𝑚𝑐2. Functions as Deterministic Relations. A function is a singlevalued relation: (𝑥,𝑦) ∈ 𝑓∧ (𝑥,𝑦′)∈𝑓⇒𝑦=𝑦′. This ensures that every input has exactly one admissible output, matching the conventional view of a function 𝑓 : 𝑋→𝑌 . Equivalently, a function may be seen as a relation 𝑓 : 𝑋→ 2 𝑌 whose image sets all have cardinality 1. Relaxing this single-valuedness yields nondeterministic or probabilistic relations: 𝑓:𝑋→2𝑌, where an input may relate to multiple (or weighted) outputs. From a relational perspective, nothing fundamentally changes—the same underlying structure 𝑅⊆𝑋×𝑌 accommodates both deterministic and nondeterministic behavior without additional machinery. Parallel Structure of Physics and Computing. Both disciplines describe relations among configurations in a state space. In computing, such relations are made explicit: operational semantics specifies, step-by-step, how one configuration evolves into the next. In physics, the same relational structure is typically implicit, encoded in differential equations, conservation laws, and causal The Calculus of Everything — Part I of II dependencies. A central aim of this framework is to make these parallel structures explicit and express them within a shared semantic language. 4.1 Static Systems (Inference Systems) Having established relations as the atomic fabric of computing—and seen how the same perspective can also be applied to physics—we now proceed to ask: How are such relations specified (defined)? In computing, the canonical way to specify relations intensionally is to employ inference systems, which define relations via axioms and rules of inference. From Description to Construction. A rule has the form: <premises> <conclusion> [Name] and generates the smallest relation closed under those rules (its inductive closure). 3 In physics, this mirrors how a small number of fundamental laws generate large families of admissible configurations within a given modeling framework. Inference System = Axiom(s) + Rule(s). Inference systems specify relations by combining two kinds of judgments: • Axioms: rules with no premises; they introduce base judgments that are unconditionally true and thus admitted. • Rules: rules with one or more premises; they extend the relation by declaring that if the premises hold, then the conclusion may be inferred. A common source of confusion concerns the role of premises. Only premises that refer to the same relation being defined contribute to its inductive (recursive) structure. Premises involving other, predefined relations are legitimate and do not introduce recursion; they instead impose so-called side conditions. Some authors place such side conditions above the inference bar, while others write them explicitly alongside (next to) the rule. Both conventions are equivalent. The essential distinction is that an axiom is any rule without recursive premises, whereas a rule of inference may depend on earlier instances of the same relation. As an example, consider the unary predicate ⊢pos 𝑛 , meaning “ 𝑛 is positive.” Assuming the pre-defined mathematical relation > , one may write: 𝑛>0 ⊢pos 𝑛[Pos] Here, 𝑛> 0appears as a premise. Since > is already a pre-defined relation, it acts as a side condition rather than as a recursive premise. The rule may therefore be written equivalently as: ⊢pos 𝑛[Pos] where 𝑛>0. Both formulations define the same rule; only premises referring to the same relation introduce (potentially mutual) recursion. 3 Formally, this is the least fixed point obtained by successively applying the rules until no new elements appear—a well-defined and well-understood construction in domain theory and operational semantics, grounded in the study of lattice structures [40]. 4.1.0 Mathematics Example: Even Numbers We define the even numbers via the unary relation ⊢even 𝑛 as follows: ⊢even 0[Zero] ⊢even 𝑛 ⊢even 𝑛+2[Next] The inference system consisting of the axiom [Zero] and the rule [Next] inductively generates the (infinite) set of even numbers: ⊢even={0,2,4,6, . . . }. Derivation Trees. Aderivation tree is a finite tree built from axioms and rules. Axioms appear at the top, the conclusion at the bottom, and rules connect them through intermediate nodes. Each node is an instance of a rule, and its children are instances of the rule’s premises. A derivation tree therefore serves as a proof that the corresponding judgment is derivable within the inference system. For example, the following derivation tree demonstrates that 4 is derivable as an even number; constituting as proof that 4 is even: ⊢even 0[Zero] ⊢even 2[Next] ⊢even 4[Next] Reading Rules, Building Derivations, & Reasoning. Rules may be read bottom-up (deduction) or top-down (induction); both are legitimate and equivalent forms of reasoning. The set of all judgments for which derivation trees exist constitutes the inductive closure of the inference system. Syntax Constructors. Inductive definitions do not only describe relations; they also define syntactic structures. Just as the rules [Zero] and [Next] generate the even numbers, we may introduce a corresponding syntactic category of expressions, defined by the grammar: 𝐸::=Zero |Next(𝐸). which allow the explicit construction of composite structures: Next(Next(Zero)). This notation exposes the inductive organization of expressions that is usually left implicit in standard mathematical syntax. 4.1.1 Computing Example: Arithmetic Expressions Syntax vs. Semantics. Programming languages separate form from meaning. A grammar specifies how expressions are constructed and written (syntax), while semantic rules specify how they behave and are to be interpreted or executed. This distinction mirrors similar separations in linguistics [17]. Syntax. The syntax of a simple arithmetic language is generated by: 𝐸::=𝑁numeric constants 𝐸::=𝐸1+𝐸2addition expressions which inductively defines expressions such as: 1,1+2,(1+2)+3,(1+2)+(3+4). Here, parentheses are used to unambiguously group constituents, which is the common approach; alternatively, grouping could be encoded explicitly in the syntax—via a dedicated syntactic rule 𝐸::=(𝐸)—which we do not do here. Claus Brabrand 4.1.2 Physics Ex.: Compositional Structure of Matter Having defined relations via rules, we mirror the same construction in physics, where rules are used to describe how composite structures are built from simpler constituents. Fundamental postulates play the role of axioms, while laws of composition act as inference rules. Together, they define relations over configurations used to represent matter. Constructors. We introduce constructors for composing matter using conventional physics notation. Writing 𝐶(𝑋,𝑌 ) denotes a structure 𝐶containing substructures 𝑋and 𝑌: Quarks 𝑞::=𝑈|𝐷(up &down) Leptons 𝑙::=𝐸|¯ 𝐸(electron &position) Baryons 𝑏::=𝑃(𝑞, 𝑞,𝑞) | 𝑁(𝑞,𝑞,𝑞)(proton &neutron) Atoms 𝑎::=𝐻(𝑏, 𝑙 )(hydrogen) Axioms (Fermions). The axioms introduce quarks and leptons: 𝑈[Up] 𝐷[Down] 𝐸[Electron] ¯ 𝐸[Positron] Rules (Baryons). The following rules describe how baryons are composed from quarks: 𝑢 𝑢′𝑑 𝑃(𝑢,𝑢′,𝑑)[Proton] 𝑢 𝑑 𝑑′ 𝑁(𝑢,𝑑,𝑑′)[Neutron] Rules (Atoms). Atoms are composed by combining baryons and leptons; here is the rule for Hydrogen: 𝑝 𝑒 𝐻(𝑝, 𝑒)[Hydrogen] Larger atoms are constructed analogously. For instance, Helium may be represented schematically as a composite of two protons, two neutrons, and two electrons: 𝑝1𝑝2𝑛1𝑛2𝑒1𝑒2 He(𝑝1, 𝑝2, 𝑛1, 𝑛2, 𝑒1, 𝑒2)[Helium] Example Derivation (Hydrogen). The following derivation tree establishes that a hydrogen configuration is derivable within the system: 𝑈[Up] 𝑈′[Up] 𝐷[Down] 𝑝=𝑃(𝑈,𝑈 ′, 𝐷)[Proton] 𝐸[Electron] 𝐻(𝑝, 𝑒 )[Hydrogen] These rules admit two distinct kinds of ill-formed structures. Some are excluded syntactically by the grammar itself, while others are excluded semantically by the static semantics introduced later: Syntactic Exclusion. Certain combinations, e.g. 𝑃(𝑈, 𝑈, 𝑈 ) , do not match any constructor and therefore admit no derivation tree; e.g., the premise of [Proton] requires two up and one down quark. Semantic Exclusion. Other grammatically admissible expressions (e.g. 𝐻(𝑁, 𝐸) or 𝐻(𝑃, ¯ 𝐸) ) are excluded by semantic typing constraints (introduced later in §5.1). 4.2 Dynamic Systems (Transition Systems) Having defined the static structure of computation and physics through inference systems, we now turn to their dynamic counterpart: transition systems. Whereas inference systems characterize which configurations are admissible, transition systems describe how such configurations may change via a sequence of well-defined steps. From Static to Dynamic.Inference rules generate the set of admissible configurations. Transitions describe their possible stepwise evolution, that is, the changes that may occur among them. Formally, a transition system consists of a set of states 𝑆 together with a binary relation →⊆ 𝑆×𝑆 indicating how one state may lead to another: 𝑠→𝑠′meaning: state 𝑠transitions to state 𝑠′. A finite chain of transitions 𝑠0→𝑠1→ · · · → 𝑠𝑛 represents an evolution of the system through successive steps. As before, the reflexive–transitive closure →∗ denotes zero-or-more transitions. In many settings, one distinguishes a subset of terminal configurations 𝐹⊆𝑆, in which no further transition is defined. 4.2.1 Computing Example: Evaluation of Expressions We return to the earlier example of arithmetic expressions, now focusing on their dynamic behavior: how expressions are evaluated by a sequence of transition steps, such as 2+2 →4. Semantics. The meaning of expressions is given by semantic rules, which specify how syntactic expressions are evaluated to produce values. For addition, we assume a semantic operation ⊕ on numbers (mathematical addition) and define transition rules that connect syntax (+) to this semantic level: (1) Evaluate the left operand first, one step: 𝑒1→𝑒′ 1 𝑒1+𝑒2→𝑒′ 1+𝑒2 [Add1] (2) Evaluate the right operand, one step: 𝑒2→𝑒′ 2 𝑛1+𝑒2→𝑛1+𝑒′ 2 [Add2] (3) Perform the (addition) operation: 𝑛1⊕𝑛2=𝑛 𝑛1+𝑛2→𝑛[Add] The symbol + below the line is purely syntactic, whereas the symbol ⊕ in the premise denotes the semantic operation being applied. The metavariables 𝑒1, 𝑒2 range over expressions, and 𝑛1,𝑛2 range over numeric values. Together, these rules define the transition relation for addition. Analogous rules define multiplication, replacing + with * and ⊕ with ⊗. As mentioned earlier, we use parentheses only to disambiguate syntax, but they could be handled explicitly by the following rule: (𝑒)→𝑒[Par] Note that this would not affect the intended evaluation behavior, but it would introduce an extra transition step. The Calculus of Everything — Part I of II Evaluation Example. Consider the expression (1+2)+(3+4) . The transition rules yield: (1+2)+(3+4) →3+(3+4) →3+7 →10. Equivalently: (1+2)+(3+4) →∗10. 4.2.2 Physics Example: Asynchronous QED A structurally analogous transition system arises in a simplified operational representation of quantum electrodynamics (QED), in which electrons emit and absorb photons. We consider configurations involving electrons, positrons, and photons, composed spatially: Syntax of configurations: 𝑆::=𝑒− 𝑝(electron with momentum 𝑝) ::=𝑒+ 𝑝(positron with momentum 𝑝) ::=𝛾𝑞(photon with momentum transfer 𝑞) ::=𝑆1|𝑆2(spatial composition). The operator | denotes spatial composition, representing configurations in which multiple entities coexist adjacently. Asynchronous Semantics (Transition Rules). Emission and absorption are represented as two separate transition steps, linked by an intermediate photon configuration: 𝑝=𝑝′+𝑞 𝑒− 𝑝→𝑒− 𝑝′|𝛾𝑞 [Emit] 𝑝+𝑞=𝑝′ 𝛾𝑞|𝑒− 𝑝→𝑒− 𝑝′ [Absorb] An example transition sequence is: 𝑒− 𝑝1|𝑒− 𝑝2→𝑒− 𝑝′ 1|𝛾𝑞|𝑒− 𝑝2→𝑒− 𝑝′ 1|𝑒− 𝑝′ 2. (The coloring is used solely to trace energy transfer for expository purposes; it is not part of the syntax or semantics.) The photon 𝛾𝑞 appears explicitly as an intermediate configuration, representing the transfer of energy–momentum between the two electrons. Creation and Annihilation. Additional rules model pair creation and annihilation: 𝑞1+𝑞2=𝑝1+𝑝2 𝛾𝑞1|𝛾𝑞2→𝑒− 𝑝1|𝑒+ 𝑝2 [Create] 𝑝1+𝑝2=𝑞1+𝑞2 𝑒− 𝑝1|𝑒+ 𝑝2→𝛾𝑞1|𝛾𝑞2 [Annihilate] These rules describe individual, asynchronous transition steps in which energy–momentum conservation is enforced locally at each rule application. Interpretation. In this asynchronous representation, emission and absorption appear as separate transition steps connected by an intermediate photon. A complementary synchronous representation, introduced later, combines such steps into a single coordinated transition. The two views provide different operational perspectives on the same interaction patterns. Composition of Transitions. Transitions compose naturally: if 𝑠→𝑠′ and 𝑠′→𝑠′′ , then 𝑠→∗𝑠′′ . This allows extended evolutions to be described as compositions of local steps. For example: 𝑒− 𝑝1|𝑒− 𝑝2→∗𝑒− 𝑝′ 1|𝑒− 𝑝′ 2. The same composition principle underlies the evaluation of expressions: (1+2)+(3+4) →∗10. Relation to Statics. Each transition relates configurations that are admissible under the static inference rules. In computing, evaluation preserves typing; in the present physical models, transitions preserve the relevant static invariants (such as charge and energy–momentum): if ⊢𝑥𝑠:xand 𝑠→𝑠′,then ⊢𝑥𝑠′:x. The transition rules presented here are illustrative and intentionally partial. They serve to demonstrate how an operational, transitionbased description can be applied in a physical setting, rather than to provide a complete physical semantics. 4.3 Interaction (Labelled Transition Systems) To make the role of labels precise, we first examine a canonical computing example that shows how interactions can be represented operationally and that later serves as inspiration for a synchronous representation of QED. 4.3.1 Computing Example: Communicating Systems We now enrich transitions with labels that record the kind of action that occurs. In Milner’s Calculus of Communicating Systems (CCS) [ 25 , 26 ], processes (ranged over by the meta-variable P) perform labelled output ( ¯ 𝑎 ) and input ( 𝑎 ) actions, synchronizing when complementary actions meet: ¯ 𝑎Sync ←→←→ 𝑎 where ¯ 𝑎 and 𝑎 denote complementary actions (output and input, respectively) on a communication channel 𝑎. Syntax: P::=0|𝑎.P|¯ 𝑎.P|P|P The constant 0(Nil, aka inaction) denotes the inactive process: a system with no further actions to perform, serving as the identity element of parallel composition. The operator | denotes parallel composition (running side-by-side). Rules for labelled transitions: The core system has five rules: 𝑎.P𝑎 −→ P [In] ¯ 𝑎.P¯ 𝑎 −→ P [Out] Pℓ −→ P′ P|Qℓ −→ P′|Q [Left]Qℓ −→ Q′ P|Qℓ −→ P|Q′ [Right] P𝑎 −→ P′Q¯ 𝑎 −→ Q′ P|Q𝜏 −→ P′|Q′[Sync] Each rule specifies how a process performs an observable action or participates in a composite interaction: • No transitions originate from 0; hence, no rules are given for it. Claus Brabrand • [In]: the process 𝑎. Pis ready to perform an input on channel 𝑎 . When the input occurs, the prefix is consumed and the process continues as P.4 • [Out]: the process ¯ 𝑎. Pperforms an output on channel 𝑎 and proceeds as P. • [In] &[Out]: the label ( 𝑎 or ¯ 𝑎 ) records the action performed and determines which complementary action it may synchronize with. • [Left] &[Right]: transitions of either component are lifted to the composite system. • [Sync]: complementary actions 𝑎 and ¯ 𝑎 resolve into an internal synchronization step. The prefixes disappear, and the system continues as P ′| Q ′ , producing the silent action 𝜏 (invisible to the external context). Operationally, an output performs its send and becomes its continuation; an input receives and likewise proceeds. When the two meet, their interaction is completed internally as a single 𝜏 transition. Here, 𝜏 serves as a marker of a completed exchange: an interaction that has occurred but leaves no externally visible trace. Example (synchronization): ¯ 𝑎.0|𝑎.0𝜏 −→ 0|0. Here an output on 𝑎 from the first component meets an input on 𝑎 from the second, producing a single internal 𝜏 step. The communication occurs between the two processes involved; beyond this, it is hidden from an external observer. The final state is equivalent to 0. In §5.3, we will consider behavioural equivalences that identify such non-identical processes as behaviourally equivalent, for example: 0|0≡0, since both are incapable of further actions and thus exhibit the same observable (inactive) behavior. Full CCS. The fragment above captures the core operational behavior of CCS. In its complete form, the calculus extends this with nondeterministic choice ( 𝑃+𝑄 ), restriction ( 𝑃\𝐿 ), relabelling ( 𝑃[𝑓] ), and recursion (or iteration). 5 These extensions make CCS expressive enough to model a wide range of communicating systems, but for present purposes the minimal fragment above suffices to illustrate labeled transitions and synchronization. Modeling analogy (optional physical reading). It can be useful to keep a physical reading in mind as an analogy: an input 𝑎.𝑃 may be viewed as a component prepared to accept an incoming interaction of some kind 𝑎 , while an output ¯ 𝑎.𝑃 may be viewed as a component prepared to initiate one. The silent action 𝜏 then marks a completed internal coordination step. Parallel composition 𝑃|𝑄 represents spatial coexistence of physical entities that may interact, while choice 𝑃+𝑄 represents alternative transition paths. Restriction and relabeling control what is externally observable and how labels are interpreted. This analogy is used only as intuition for the 4 CCS abstracts away the data transmitted and records only that communication occurred on channel 𝑎. The later 𝜋-calculus [27] extends CCS to include value passing, most notably the passing of channel names. 5 Recursion and iteration are computationally equivalent: each can simulate the other. A language with either one (together with conditionals) is already Turing-complete. CCS is therefore expressive enough to model unbounded or repeating processes with either recursion or iteration. labeled-transition style and does not assert a physical identification of CCS constructs. CCS microworld example (emission and absorption). As a simple illustration, we model a small “microworld” in CCS in which a star repeatedly emits photons and a plant repeatedly absorbs them (with growth abstracted away): Star def =photon.Star (recursive photon emission) Plant def =photon.Plant (recursive photon absorption) World def =Star |Plant (parallel composition) 4.3.2 Physics Example: Synchronous QED We revisit quantum electrodynamics (QED), now using a labeled transition system to represent interaction patterns in which emission and absorption are treated as a single coordinated step. This synchronous representation contrasts with the earlier asynchronous transition system, and is introduced here as an operational perspective inspired by labeled transition systems in computing. In this representation, electrons may perform emit or absorb actions, and complementary actions occurring in adjacent configurations may synchronize. Labels record the kind of interaction performed (e.g., emission or absorption), while synchronization combines such complementary actions into a single internal transition. Syntax of configurations: As before, configurations represent spatial arrangements populated with matter (electrons and positrons). In contrast to the asynchronous model, photons do not appear as independent configurations; instead, they function solely as mediators of synchronous energy exchange in synchronization events: 𝑆::= 𝑒− 𝑝electron (with momentum 𝑝), ::= 𝑒+ 𝑝positron (with momentum 𝑝), ::= 𝑆|𝑆spatial adjacency, ::= ∅empty configuration. The synchronous rules below mirror their asynchronous counterparts, with the crucial distinction that transitions now carry labels describing the interaction being performed. 4.3.3 Labeled transition rules (Synchronous QED) The synchronous representation retains only the minimal ingredients needed to describe coordinated energy exchange: an electron may emit or absorb a photon, and adjacent configurations may synchronize these complementary actions into a single internal transition. As in CCS, structural rules propagate local transitions through spatial context. Physical axioms (local interactions): 𝑝=𝑝′+𝑞 𝑒− 𝑝 emit 𝛾𝑞 −−−−−→ 𝑒− 𝑝′ [Emit]𝑝+𝑞=𝑝′ 𝑒− 𝑝 absorb 𝛾𝑞 −−−−−−−→ 𝑒− 𝑝′ [Absorb] Synchronization (interaction): 𝑆1 emit 𝛾𝑞 −−−−−→ 𝑆′ 1𝑆2 absorb 𝛾𝑞 −−−−−−−→ 𝑆′ 2 𝑆1|𝑆2 𝜏 −→ 𝑆′ 1|𝑆′ 2 [Sync] The Calculus of Everything — Part I of II Figure 2: Feynman diagram for two–electron scattering via photon exchange corresponding to: (𝑒− 𝑝1|𝑒− 𝑝2)𝜏 −→ (𝑒− 𝑝1 ′|𝑒− 𝑝2 ′) . Structural rules (context propagation): 𝑆1 ℓ −→ 𝑆′ 1 𝑆1|𝑆2 ℓ −→ 𝑆′ 1|𝑆2 [Left]𝑆2 ℓ −→ 𝑆′ 2 𝑆1|𝑆2 ℓ −→ 𝑆1|𝑆′ 2 [Right] Explanation. The rules [Emit] and [Absorb] represent local energy–momentum exchange actions within this synchronous representation. Parameters such as 𝑝′ and 𝑞 are implicitly existentially quantified, standing for values that satisfy the relevant conservation constraints. The rule [Sync] combines a complementary emission and absorption into a single internal (silent) 𝜏 transition. As in CCS, 𝜏 denotes an internally resolved interaction that leaves no externally observable action label. The rules [Left] and [Right] lift local transitions through larger spatial configurations. Diagrammatic interpretation. The same interaction can be depicted by the Feynman diagram in Figure 2. Vertices correspond to local transition rules ([Emit] and [Absorb]), while edges represent intermediate configurations. In the synchronous transition-system representation, the photon line corresponds to the internal 𝜏 synchronization that connects an emission action on one side with a matching absorption action on the other. From the perspective of the labeled transition system, the entire interaction is represented as a single internal transition: (𝑒− 𝑝1|𝑒− 𝑝2)𝜏 −→ (𝑒− 𝑝1 ′|𝑒− 𝑝2 ′), with the diagram providing a graphical trace of how this synchronized step can be decomposed into local interaction rules. 4.4 Asynchronous vs. Synchronous QED Semantics Figure 3 presents a side-by-side comparison of two deliberately simplified semantic representations of photonic energy exchange, expressed respectively as an (unlabeled) transition system (TS) to the left versus a labeled transition system (LTS) to the right. The purpose of this comparison is not to introduce new physical assumptions, but to illustrate how the same interaction structure can be described at different levels of operational granularity. Asynchronous semantics (TS). In an (unlabeled) transition system, interaction is represented as a sequence of distinct transitions. Each transition captures a local change of configuration, and multistage interactions are expressed by explicit intermediate states. In the present example, emission and absorption appear as separate steps, with the photon represented as an intermediate configuration linking them. This representation is useful when intermediate states or propagation structure are of interest. Synchronous semantics (LTS). In a labeled transition system, transitions carry labels that record the type of action performed. Complementary labeled actions can be combined by synchronization rules into a single internal transition. In this representation, emission and absorption are treated as a coordinated interaction (handshake) step, and the intermediate photon configuration is not represented explicitly. Instead, its role is captured symbolically by the labels and the synchronization rule. TS vs. LTS. The distinction between TS and LTS is therefore a distinction in semantic granularity. A TS represents interaction as a sequence of explicit configuration changes, whereas an LTS permits certain multi-step patterns to be represented as atomic composite transitions. Neither representation is more “correct” than the other; each emphasizes a distinct perspective and different structural aspects of the same underlying interaction. Interpretive intuition. The two semantic representations may be read as corresponding to distinct observational perspectives. In the asynchronous view (observer-external perspective), emission and absorption are described as temporally separated events connected by a propagating photon across space and time. In the synchronous view (photon-internal perspective), the same interaction is represented as a single coordinated 𝜏 -transition: along the photon’s worldline, no time elapses between emission and absorption (zero proper time). This contrast reflects a difference in semantic description, not a claim about physical ontology. Modeling tradeoffs. Asynchronous semantics exposes intermediate configurations and is well-suited for reasoning about stepwise evolution. Synchronous semantics abstracts away intermediate detail and is advantageous when reasoning about interactions primarily in terms of their combined effect. Effective modeling often involves switching between these two descriptions, depending on which structural features are relevant to the analysis at hand. Terminology. The terms asynchronous and synchronous are used here purely in an operational sense. They refer to whether an interaction is represented as multiple successive transitions or as a single combined transition within a semantic model. No ontological or physical claim is intended by this terminology; it serves only to distinguish alternative levels of abstraction in the description. 4.5 The Strong Force: Quantum Chromodynamics In quantum chromodynamics (QCD), interactions among quarks are governed by color charge. In parallel with the QED examples above, we present a deliberately simplified operational representation of intra-baryon color interaction, expressed as a labeled transition system. The purpose is not to model QCD in full detail, but to illustrate how color exchange can be described structurally within the same semantic framework. Claus Brabrand let print_system s = "E[" ^ string_of_int s.emitter ^"]" ^"|"^print_photon_set s.photons ^"|A["^ string_of_int s.absorber ^"]" Transition Implementation. let () = Random.self_init () type step_label = |Emit of level |Absorb of level let step_emit s = match swith |{emitter =e;photons = ps; absorber =a} when e>0-> let k = 1 + Random.int e in let e'=e-kin let p ={level =k}in Some ({ emitter = e'; photons = p :: ps; absorber = a }, Emit k) |_->None let pick_random xs = let n = List.length xs in let i = Random.int n in let rec remove k acc = function | [] -> failwith "pick_random" | y :: ys -> if k=0then (y, List.rev acc @ ys) else remove (k-1) (y :: acc) ys in remove i [] xs let step_absorb s = match swith |{emitter =e;photons = ps; absorber =a} when ps <> [] -> let (p, ps')=pick_random ps in Some ({ emitter = e; photons = ps'; absorber =a+p.level }, Absorb p.level) |_->None let step_ea s = match step_emit swith |Some _as se -> se |None -> step_absorb s let step_ae s = match step_absorb swith |Some _as sa -> sa |None -> step_emit s let step s = if Random.bool () then step_ea selse step_ae s ⟨ 3,0,0 ⟩ ⟨ 2,1,0 ⟩ ⟨ 1,2,0 ⟩ ⟨ 0,3,0 ⟩ ⟨ 2,0,1 ⟩ ⟨ 1,1,1 ⟩ ⟨ 1,0,2 ⟩ ⟨ 0,2,1 ⟩ ⟨ 0,1,2 ⟩ ⟨ 0,0,3 ⟩ Figure 7: Execution space for initial level 3, shown up to level-distribution equivalence as splits (𝐸, 𝑄, 𝐴) . Emission steps move down; absorption steps move right. Evaluation Trace. let print_label =function |Emit k -> "--Emit[" ^ string_of_int k ^ "]-->" |Absorb k->"--Absorb[" ^ string_of_int k ^ "]-->" let rec eval_trace s = match step swith |None -> Printf.printf "%s\n" (print_system s); s |Some (s', lbl) -> Printf.printf "%s %s\n" (print_system s) (print_label lbl); eval_trace s' Execution Example. Starting from: E[3] | {} | A[0] let s_ex = { emitter = 3; photons = []; absorber = 0; } let () = ignore (eval_trace s_ex) A typical run produces: E[3] | {} | A[0] –Emit[1]–> E[2] | { g[1] } | A[0] –Emit[1]–> E[1] | { g[1], g[1] } | A[0] –Absorb[1]–> E[1] | { g[1] } | A[1] –Emit[1]–> E[0] | { g[1], g[1] } | A[1] –Absorb[1]–> E[0] | { g[1] } | A[2] –Absorb[1]–> E[0] | {} | A[3] In configurations where both emission and absorption are enabled, the implementation may choose either transition. In all cases, the static judgment 𝑆⊢S3is preserved throughout the evaluation. 6.2 Model Checking (Exploring all Trajectories) In the previous section we saw that simulation explores one trajectory of a system by performing one concrete execution of the SOS rules. In the toy emission–absorption model this produced, for example, the following evolution of the intermediate-token multiset The Calculus of Everything — Part I of II 𝑄(shown as a list of token levels): {} →[1]→[2,1]→[1,2,1]→[2,1]→[1]→{}. This reflects one particular pattern of nondeterministic choices during execution. Simulation therefore answers: “What is one possible evolution of the model?” Model checking, in contrast, explores all possible evolutions of a model: all possible rule applications and all possible nondeterministic choices. Even in this small example, starting from an initial configuration such as E[3] | {} | A[0] , there are multiple possible evolutions. Model checking verifies that a temporal property holds for every evolution—not merely for a single run. 6.2.1 Astronomy Example: Stellar Fusion We now consider a richer transition-system example commonly presented in astronomy: an abstract model of stellar evolution and end states. The aim is to determine whether all possible transition paths of the model satisfy a given property. Simulation corresponds to exploring one path ( ∃ ), while model checking corresponds to exploring all paths (∀). Representation. A stellar configuration is represented by a pair: (Phase,𝑚), where Phase is a symbolic stage label and 𝑚 is a mass parameter (in solar masses, 𝑀⊙). A transition is written: (Phase1,𝑚) → (Phase2,𝑚′), with 𝑚′=𝑚 unless a rule explicitly changes the mass parameter. The guarded transition rules below define a simple stage progression and partition behavior by mass: (H,𝑚) → (He,𝑚) (He,𝑚) → (C,𝑚) (C,𝑚) → (O,𝑚) (C,𝑚) → (Ne,𝑚) (C,𝑚) → (Na,𝑚) 𝑚<8 (Ne,𝑚) → (Mg,𝑚) 𝑚<8 (Na,𝑚) → (Mg,𝑚) 𝑚<8 (Mg,𝑚) → (WhiteDwarf,𝑚) 𝑚≥8 (Ne,𝑚) → (O,𝑚) 𝑚≥8 (Na,𝑚) → (Ne,𝑚) 𝑚≥8 (O,𝑚) → (Si,𝑚) 𝑚≥8 (Si,𝑚) → (Fe,𝑚) 8≤𝑚<25 (Fe,𝑚) → (NeutronStar,𝑚) 𝑚≥25 𝑚′=0.9×𝑚 (Fe,𝑚) → (BlackHole,𝑚′) For simplicity, we assume that a BlackHole retains 90% of its precollapse mass (i.e. 𝑚′= 0 . 9 ×𝑚 ), representing mass ejection in an abstract way. Example. For 𝑚=1𝑀⊙, one valid trace is: (H,1)→(He,1) → (C,1) → (Ne,1)→(Mg,1)→(WhiteDwarf,1). 7 We use an informal past-time operator Previously(Si). This can be encoded in standard LTL through auxiliary propositions tracking whether silicon has occurred earlier. Model checking. Model checking is a technique for automatically checking a model 𝑀 (specified as a transition system) against a temporal property 𝜑 over execution paths. If 𝑀|=𝜑 , the property holds for all paths; if 𝑀|=𝜑 , a counterexample path, violating the property 𝜑, is returned. Temporal logics. Properties are often expressed in formalisms such as Linear Temporal Logic (LTL) and Computation Tree Logic (CTL). Here, “temporal” refers to modalities over execution paths in a transition system, not to physical time. The operators used below have their standard meanings: • ∃ – there exists an execution path • ∀ – for all execution paths •^– eventually (along a path) •□– always (along a path) Automated verification. Model checking amounts to exploring all rule applications from an initial configuration. Figure 7 shows the complete (finite) execution space of the toy emission–absorption model with initial level 3, presented up to level-distribution equivalence. Each node is labeled (𝐸, 𝑄, 𝐴) , indicating how the total level is distributed between emitter, intermediate tokens, and absorber; emission steps move down, absorption steps move right. Returning to the stellar model, Table 2 summarizes several example properties and their status under automated model checking. Properties (1) and (2) hold for all paths, while (3) does not; a counterexample path is the following, not producing silicon (Si): H→He →C→Ne →Mg →WhiteDwarf. 6.3 Theorem Prover Atheorem prover can be used to mechanically reason about an operational semantics by encoding its rules and establishing properties that hold for all derivations generated by those rules. In this setting, invariants are treated as logical statements over the transition system, and proofs are carried out by induction on the structure of derivations (as in §5.2, but mechanized). Once an operational semantics is expressed as a collection of inference rules, it can be encoded in a proof assistant such as Rocq [ 38 ], Lean [ 7 ], Twelf [ 31 ], or Isabelle [ 29 ]. These tools support automated verification by mechanically discharging large classes of proof obligations derived from the rules. 8 We do not cover theorem provers in depth in this paper, but sketch the role they play in reasoning about operational models. As an illustration, consider the QED-inspired operational model introduced earlier. The transition rules [Emit],[Absorb], and [Sync] can be encoded directly as inference rules in a proof assistant. One may then state and prove properties that are preserved by all valid derivations, such as the invariance of numeric annotations assigned by a typing discipline. Such proofs proceed by structural induction on the derivation of transitions, mirroring the reasoning principles discussed in §5.2. More generally, mechanized reasoning can be used to derive properties that are not stated explicitly in the rules themselves. These include constraints on which configurations are reachable, relationships between components of the state, and fixed-point 8 Here, “automated” means that the prover can carry out proof steps without human intervention once the specification and proof strategy are fixed. Claus Brabrand Table 2: Example properties over stellar-evolution models. (#) Property (informal specification) Formal specification 𝜑in LTL M|=𝜑Counterexample if M |=𝜑 (1) All stars end as a WhiteDwarf,NeutronStar,orBlackHole?∀□(Terminal → (WD ∨NS ∨BH)) ✓— (2) If a star collapses (producing iron), has it produced silicon? ∀□(Fe →Previously(Si))7✓— (3) All stars eventually produce silicon? ∀□(¬Si →^Si) × H→He→C→Ne→Mg→WhiteDwarf (for 𝑚<8) or equilibrium configurations of the transition system. Making such properties explicit often helps clarify the consequences of the chosen operational rules and the structure of the resulting semantic model. 7 Validation (Relating Models to Observations) The preceding sections have focused on descriptive,analytic, and automated reasoning over operational models. A natural next question is how such models might be related to empirical observations. In the present paper, we do not attempt such validation. Instead, we outline—at a high level—what validation would mean in an operational semantics–based approach. In general, validation concerns the relationship between a formal model and the phenomena it is intended to represent. Within an SOS framework, this relationship is indirect: the semantics specifies a space of possible behaviors, and validation amounts to assessing whether observed patterns can be expressed, reproduced, or constrained within that space under appropriate abstractions. This differs from direct prediction, and places emphasis on structural correspondence rather than numerical forecasting. The companion paper ⟨ Part II of II ⟩ explores these questions further by extending the interaction patterns introduced here and examining their consequences as conceptual models. That work is explicitly exploratory in nature: it investigates whether a small set of operational rules can serve as a unifying descriptive vocabulary across disparate physical domains. No claim is made that such models replace existing physical theories or provide definitive explanations. Whether any such operational reconstructions ultimately prove useful is an open question. Their value, if any, lies in offering an alternative structural perspective—one that invites comparison, critique, and dialogue across disciplines, rather than asserting empirical authority. 8 Related & Foundational Work Research connecting computation and physics can be broadly grouped into three strands: (1) digital or simulation-based accounts of physical systems, (2) information-theoretic perspectives on physical law, and (3) formal semantic frameworks originating in computer science. The present work draws inspiration from all three, but pursues a distinct objective: it develops a methodological and representational reinterpretation of physical interaction using rule-based structural operational semantics (SOS), without adopting any ontological position about the nature of the physical world. 8.1 Digital Physics Zuse’s Rechnender Raum [ 43 ] proposed a discrete, cellular-automaton–like view of space. Fredkin’s Digital Mechanics [ 16 ] and related work explored reversible computation as a candidate substrate for physical dynamics. Wolfram’s rule-based investigations [ 41 ] pursued similar ideas using simple computational rules. These approaches typically advance explicit ontological claims— namely, that physical reality itself is fundamentally discrete or computational. The present work deliberately avoids such commitments. Its aim is not to characterize what the world is, but to provide a precise semantic language for describing and reasoning about physical interaction patterns. 8.2 The Simulation Hypothesis The Simulation Hypothesis [ 4 ] considers the possibility that advanced agents might simulate entire physical histories. This proposal concerns the hypothetical implementation or execution context of a model, rather than the structure of the laws being modeled. The framework developed here is orthogonal to such questions. It provides a formalism for specifying and analyzing operational models of interaction, independently of any claims about who or what might execute those models. To avoid any ambiguity: This work does not suggest that the universe is a computer. Rather, it uses established computational formalisms as a language for describing and reasoning about physical systems. 8.3 Information-Theoretic Foundations Landauer’s principle [ 18 ] and Bennett’s work on the thermodynamics of computation [ 2 ] established deep connections between information processing and physical constraints. Wheeler’s “It from Bit” perspective [ 39 ] and Zurek’s edited volume [ 42 ] further advanced information-centric viewpoints. Feynman [ 15 ] and Deutsch [ 8 ] formalized quantum simulation as an analytical tool, while Lloyd and collaborators [19–22] quantified limits on physical computation. Much of this work emphasizes discrete state changes, information flow, and computational constraints, but typically does not provide a general compositional semantics. The present work contributes such a semantics by importing the machinery of SOS, allowing interaction structures to be expressed explicitly as rules and supporting meta-theoretic reasoning about invariants, equivalences, and behavior. 8.4 Computational Physics and Andrea diSessa diSessa’s work on computational physics [ 9 , 11 , 13 , 14 ] demonstrated that physical systems can be explored through stepwise state-update procedures. His microworld environments (such as Boxer and Newton’s World) enabled learners to engage with physical phenomena through executable models grounded in local rules. These systems were intentionally pedagogical and procedurally expressive, but were not designed as formal semantic frameworks. They did not provide explicit inference systems, compositional The Calculus of Everything — Part I of II operators, or meta-theoretic reasoning principles such as invariant preservation or contextual equivalence. Their emphasis lay in executable behavior rather than in formal reasoning about the structure of that behavior. The present work complements this line of research by developing a general semantic calculus: interactions are specified by inference rules, static properties by judgments, and global properties by structural induction. Where diSessa demonstrated that physical systems can be explored computationally, the contribution here is to show how such systems can be given a precise formal semantics amenable to analysis and proof. 8.5 Formal Semantics and Process Calculi Structural Operational Semantics, introduced by Plotkin [ 33 ] and further developed by Winskel [ 40 ], Nielson & Nielson [ 28 ], and Pierce [ 32 ], provides a rule-based methodology for describing and reasoning about interacting systems. The present work adapts this semantic tradition to the domain of physics-inspired models. Relations, inference systems, transition systems, labeled transition systems, invariants, simulations, and equivalences are applied here as representational tools, not as claims about physical ontology. Section 4 develops these constructions in detail. 8.6 Summary Previous work at the interface of computation and physics has often emphasized either ontological interpretations (e.g., discrete or simulated universes) or information-centric reformulations of physical law. The contribution of the present work is different: it introduces a formal, compositional, and operational semantics for describing physical interaction structures using the established tools of structural operational semantics. The framework is methodological rather than ontological, and provides a precise language in which physical theories can be expressed, compared, and analyzed. 9 Conclusion This paper has presented a structural-operational perspective on physical interaction, using the rule-based and compositional machinery of structural operational semantics as a descriptive framework. The aim has not been to replace existing physical theories, nor to offer new empirical claims, but to explore how established semantic techniques from computer science can be used to articulate interaction structures in a precise and explicit way. By expressing interactions as inference rules and transitions, the framework highlights structural regularities, supports compositional reasoning, and enables the application of well-developed analytical and automated techniques. Throughout, the emphasis has remained methodological: the work investigates how physical models can be represented,compared, and analyzed using a common operational vocabulary, rather than how physical phenomena should be interpreted or explained. Much remains open. The examples developed here are intentionally simplified and serve primarily as illustrations of the approach. The broader question—whether and to what extent operational semantics can provide useful structure or insight for working physicists and chemists—remains a matter for exploration and critique. It is our hope that this paper encourages such dialogue, particularly at the interface between computing and the physical sciences, without presuming any particular outcome. On the Use of AI (Artificial Intelligence) AI-assisted language tools (specifically, OpenAI’s ChatGPT) were used during the preparation of this manuscript to support editorial and expository tasks, including phrasing refinement, structural reorganization, and the exploration of alternative ways of presenting material. All scientific ideas, conceptual developments, technical arguments, and interpretations in this work are entirely the author’s own. Any suggestions generated by the AI were treated as prompts for reflection and were independently evaluated, verified, and developed by the author. The AI did not introduce new scientific claims, nor did it contribute original research results. Following the terminology of [ 5 ], AI assistance in this work was limited to Prompt,Review, and Orchestrate tasks. Responsibility for the technical content, scientific judgments, and overall framing of the manuscript rests solely with the author. References [1] John C. Baez and Mike Stay. 2011. Physics, Topology, Logic and Computation: A Rosetta Stone. New Structures for Physics (2011), 95–172. arXiv:0903.0340 [quantph] doi:10.1007/978-3-642-12821-9_2 [2] Charles H. Bennett. 1982. The Thermodynamics of Computation—A Review. International Journal of Theoretical Physics 21, 12 (1982), 905–940. doi:10.1007/ BF02084158 Reviews reversible computation and its thermodynamic implications.. [3] Ludwig Boltzmann. 1896. Vorlesungen über Gastheorie. J.A. Barth, Leipzig. Introduces the statistical foundation of thermodynamics and the concept of entropy as a measure of disorder.. [4] Nick Bostrom. 2003. Are You Living in a Computer Simulation? Philosophical Quarterly 53, 211 (2003), 243–255. doi:10.1111/1467-9213.00309 [5] Claus Brabrand. 2025. What Does It Mean to Program in the Age of AI?. In Proceedings of Dagstuhl Seminar 25311 on Generative AI for Programming Education. Schloss Dagstuhl–Leibniz Center for Informatics, Dagstuhl, Germany. To appear. [6] Rudolf Clausius. 1850. On the Mechanical Theory of Heat, with Applications to the Steam Engine and to the Physical Properties of Bodies. Annalen der Physik 155, 3 (1850), 500–524. Introduced the concept of entropy and the second law of thermodynamics.. [7] Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. 2015. The Lean Theorem Prover (Version 4.0). Proceedings of the 25th International Conference on Automated Deduction (CADE-25) (2015), 378–388. https://leanprover.github.io. [8] David Deutsch. 1985. Quantum Theory, the Church–Turing Principle and the Universal Quantum Computer. Proceedings of the Royal Society of London A 400, 1818 (1985), 97–117. doi:10.1098/rspa.1985.0070 Lays the theoretical foundation for quantum computation and links computation to physical law.. [9] Andrea A. diSessa. 1982. Computers in Physics Education. American Journal of Physics 50, 11 (1982), 955–962. [10] Andrea A. diSessa. 1982. Unlearning Aristotelian Physics: A Study of Knowledge-Based Learning. Cognitive Science 6, 1 (1982), 37–75. doi:10.1207/ s15516709cog0601_2 [11] Andrea A. diSessa. 1986. Artificial Worlds and Real Experience. In The Thinking Computer. Academic Press, 105–124. [12] Andrea A. diSessa. 1988. Knowledge in Pieces. Constructivism in the Computer Age (1988), 49–70. [13] Andrea A. diSessa. 1993. Toward an Epistemology of Physics. Cognition and Instruction 10, 2–3 (1993), 105–225. [14] Andrea A. diSessa. 2000. Changing Minds: Computers, Learning, and Literacy. MIT Press. [15] Richard P. Feynman. 1982. Simulating Physics with Computers. International Journal of Theoretical Physics 21, 6/7 (1982), 467–488. doi:10.1007/BF02650179 Introduces the concept of quantum simulation and the foundations of quantum computing.. [16] Edward Fredkin. 2003. An Introduction to Digital Philosophy. International Journal of Theoretical Physics 42, 2 (2003), 189–247. doi:10.1023/A:1023984015141 Claus Brabrand [17] Daniel Jurafsky and James H. Martin. 2023. Speech and Language Processing (3rd ed.). Pearson, Upper Saddle River, NJ. Draft, available at https://web.stanford. edu/~jurafsky/slp3/. [18] Rolf Landauer. 1991. Information is Physical. Physics Today 44, 5 (1991), 23–29. doi:10.1063/1.881299 Classic statement that information cannot be separated from its physical embodiment.. [19] Seth Lloyd. 2000. Ultimate Physical Limits to Computation. Nature 406 (2000), 1047–1054. doi:10.1038/35023282 Shows that physical laws impose computable limits on information processing.. [20] Seth Lloyd. 2002. Computational Capacity of the Universe. Physical Review Letters 88, 23 (2002), 237901. doi:10.1103/PhysRevLett.88.237901 [21] Seth Lloyd. 2006. Programming the Universe: A Quantum Computer Scientist Takes on the Cosmos. Knopf, New York. Describes the universe as a quantum computer processing information through physical interactions.. [22] Seth Lloyd and Y. Jack Ng. 2004. Computational Limits to the Physical World. Scientific American 291, 5 (2004), 52–61. doi:10.1038/scientificamerican1104-52 Estimates quantum mechanical limits of computation and measurement in the universe.. [23] Ole Lehrmann Madsen, Birger Møller-Pedersen, and Kristen Nygaard. 1993. Object-Oriented Programming in the BETA Programming Language. AddisonWesley. [24] James Clerk Maxwell. 1860. Illustrations of the Dynamical Theory of Gases. Philos. Mag. 19 (1860), 19–32. Early development of kinetic theory and statistical treatment of gases.. [25] Robin Milner. 1980. A Calculus of Communicating Systems. Lecture Notes in Computer Science 92 (1980). [26] Robin Milner. 1989. Communication and Concurrency. Prentice Hall. [27] Robin Milner. 1999. Communicating and Mobile Systems: The Pi-Calculus. Cambridge University Press. [28] Hanne Riis Nielson and Flemming Nielson. 1992. Semantics with Applications: An Appetizer. Springer, Berlin. Introductory text on semantics, relations, inference systems, and type theory.. [29] Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. 2002. Isabelle/HOL: A Proof Assistant for Higher-Order Logic. LNCS, Vol. 2283. Springer. https: //isabelle.in.tum.de. [30] Michael E. Peskin and Daniel V. Schroeder. 1995. An Introduction to Quantum Field Theory. Westview Press. [31] Frank Pfenning and Carsten Schürmann. 1999. System Description: Twelf — A Meta-Logical Framework for Deductive Systems. In Proceedings of the 16th International Conference on Automated Deduction (CADE-16) (LNCS, Vol. 1632). Springer, 202–206. [32] Benjamin C. Pierce. 2002. Types and Programming Languages. MIT Press, Cambridge, MA. Pedagogical development of programming-language semantics beginning from relations and inference systems.. [33] Gordon D. Plotkin. 1981. A Structural Approach to Operational Semantics. Technical Report FN-19. DAIMI, Aarhus University, Aarhus, Denmark. Foundational paper introducing Structural Operational Semantics.. [34] Gordon D. Plotkin. 1981. A Structural Approach to Operational Semantics. Technical Report DAIMI FN-19. University of Aarhus, Aarhus, Denmark. https: //homepages.inf.ed.ac.uk/gdp/publications/SOS.pdf Reprinted in Journal of Logic and Algebraic Programming, 2004. [35] Claude E. Shannon. 1948. A Mathematical Theory of Communication. Bell System Technical Journal 27, 3 (1948), 379–423. doi:10.1002/j.1538-7305.1948.tb01338.x Defines information entropy and connects it formally to probabilistic reasoning.. [36] Jakob Staugaard, Jens Bennedsen, Christoph Seidl, Sebastian Nicolajsen, Mathias Fink, and Claus Brabrand. 2024. Visualizing the Conceptual Framework of Object Orientation for Novice Programmers. In Proceedings of the 54th Frontiers in Education Conference (FIE 2024). IEEE, Washington, DC, USA. To appear. [37] Max Tegmark. 2014. Our Mathematical Universe: My Quest for the Ultimate Nature of Reality. Knopf, New York. Argues that reality itself is a mathematical structure and can be understood as information.. [38] The Coq Development Team. 2024. The Coq Proof Assistant Reference Manual. Inria. https://coq.inria.fr. [39] John Archibald Wheeler. 1990. Information, Physics, Quantum: The Search for Links. In Complexity, Entropy, and the Physics of Information, W. H. Zurek (Ed.). Addison-Wesley, Redwood City, CA, 3–28. Expanded version of Wheeler’s 1989 lecture introducing “It from Bit.”. [40] Glynn Winskel. 1993. The Formal Semantics of Programming Languages: An Introduction. MIT Press, Cambridge, MA. [41] Stephen Wolfram. 2002. A New Kind of Science. Wolfram Media, Champaign, IL. Argues that simple computational rules can generate physical complexity and potentially underpin natural law.. [42] Wojciech Hubert Zurek (Ed.). 1990. Complexity, Entropy, and the Physics of Information. Addison-Wesley, Redwood City, CA. Influential edited volume connecting information theory, thermodynamics, and quantum mechanics.. [43] Konrad Zuse. 1969. Rechnender Raum (Calculating Space). Friedrich Vieweg und Sohn, Braunschweig. Proposes that the universe is a cellular automaton performing computation.. A Physics Notation & Syntax Summary of main sub-atomic particles used in the paper: Fermions :𝑓::=𝑞|ℓquark & lepton Quarks :𝑞::=𝑈|𝐷up & down quark Leptons :ℓ::=𝐸|¯ 𝐸electron (negatron) & positron Baryons :𝑏::=𝑃+|𝑁0proton & neutron Particles :𝑝::=𝑞|ℓ|𝑏sub-atomic matter particles Gauge Boson :𝐺::=𝛾|𝑔photon & gluon