Formal Foundations and Operational Semantics

Operational Semantics (Meta-MeTTa)

The Meta-MeTTa paper provides a formal operational semantics following the standard pattern: an algebra of states (monad), a structural congruence (algebra of the monad), and rewrite rules (state transitions). MeTTa's execution state is a four-register tuple \(\langle i, k, w, o \rangle\):

• \(i\) — input register: where queries are issued
• \(k\) — knowledge base: the AtomSpace containing rewrite rules and data
• \(w\) — workspace: intermediate computation (not externally observable, enabling coarse-grained bisimulation)
• \(o\) — output register: final results

Six named rewrite rules define all state transitions:

• Query: matches an input term against equality rules in \(k\), producing substituted results in \(w\)
• Chain: continues matching workspace terms against \(k\) (iterative deepening)
• Transform: applies a transform pattern from \(i\) against \(k\), producing rewritten terms in \(w\)
• AddAtom / RemAtom: modify the knowledge base (with variants for input-driven and knowledge-driven triggers)
• Output: moves insensitive workspace terms (no further matches possible) to the output register

The guard insensitive(t, k) — meaning no unifiable equality rule exists for term \(t\) in knowledge base \(k\) — is the termination condition that moves results to output. Terms in the grammar include lists (ordered), multisets (unordered, with {...} syntax imposing commutativity), and comprehensions (intensionally defined collections that generalize let/letrec to streams and remote data). Bindings come in three modes: linear (\(\leftarrow\), consuming), repeated (\(\Leftarrow\), non-consuming), and peek (\(\leftharpoonup\), read-only).

Bisimulation and Implementation Correctness

The operational semantics recovers a notion of barbed bisimulation adapted from the asynchronous \(\pi\)-calculus: queries in the input register serve as barbs (observable actions). Two MeTTa computations are bisimilar if they produce the same observable behavior at the input/output boundary, regardless of internal workspace transitions. This provides a formal criterion for proving that independent implementations are correct: any compliant MeTTa client must be bisimilar to the specification. The paper demonstrates this by proving that the compilation from MeTTa to the \(\rho\)-calculus preserves bisimulation (Theorem 1: \(S_1 \approx S_2 \Leftrightarrow [\![S_1]\!]_M \approx [\![S_2]\!]_M\)), establishing that MeTTa programs compiled to Rholang behave identically to their source semantics.

ρ-Calculus Foundation

MeTTa's concurrency model is grounded in the reflective higher-order \(\rho\)-calculus, which treats programs as asynchronous processes communicating over channels. This enables parallelized execution without blocking, where names are quoted processes (\(@\mathrm{Term}\)) and processes can introspect their own structure via dereference (\(*\mathrm{Name}\)). The compilation to Rholang (\(\rho\)-calculus implementation language) provides the bridge to ASI Chain's secure decentralized execution.

Resource-Bounded Semantics

Meta-MeTTa §6 extends the four-register state to a five-register model \(\langle i, k, w, o; eos \rangle\) where \(eos\) tracks effort objects (EOs) — computational resource tokens analogous to Ethereum's gas. Each rewrite rule is reprised with resource bounds: transitions are permitted only when sufficient EOs remain, and each operation deducts a cost determined by a polymorphic cost function \(\#\). This enables MeTTa execution on decentralized networks where denial-of-service protection requires metered computation. A second correctness theorem (Theorem 2) proves that the resource-bounded compilation to Rholang also preserves bisimulation.

MeTTa-4 Semantic Model

The whitepaper describes MeTTa-4 as the target semantic model providing clean small-step operational semantics aligned with surface syntax. Core features: committed choice by default, delimited nondeterminism via explicit operators, atomic Space operations via the for construct with transactional semantics.

Minimal MeTTa Instruction Set

The reference implementation defines a minimal instruction set — an "assembly language for MeTTa" — sufficient to implement the full MeTTa interpreter in MeTTa itself. Minimal MeTTa uses normal evaluation order (arguments passed unevaluated) and comprises 8 core operations:

• (eval <atom>) — One step of evaluation: for pure MeTTa, searches (= <atom> $X) in the AtomSpace and returns all matches; for grounded atoms, calls the foreign function. Returns NotReducible if no match found.
• (chain <atom> <var> <template>) — Evaluate <atom>, then substitute all occurrences of <var> in <template> with each result. This is the mechanism for controlling evaluation order in a normal-order language.
• (function <body>) / (return <atom>) — Evaluate <body> in a loop until (return <atom>) is reached, providing function abstraction with explicit termination. Returns (Error NoReturn) if evaluation ends without a return.
• (unify <atom> <pattern> <then> <else>) — Pattern-matching conditional: returns <then> with merged bindings on match, <else> otherwise.
• (cons-atom <head> <tail>) / (decons-atom <expr>) — Expression construction and deconstruction (head/tail operations).
• (collapse-bind <atom>) — Collect all non-deterministic evaluation results into a single expression with their bindings (inference control).
• (superpose-bind ...) — Complement of collapse-bind: inject filtered results back into the evaluation plan.

Additional instructions include (metta <atom> <type> <space>) for invoking the full interpreter within MeTTa, (evalc <atom> <space>) for evaluation in a specified context space, and (context-space) for accessing the current working space.

Turing Completeness

The minimal instruction set is Turing complete, demonstrated by a full Turing machine implementation in minimal MeTTa: tape representation as ($head $hole $tail), state transitions via pattern matching on ($rule $state $char), and head movement via cons-atom/decons-atom operations on the tape structure. The machine halts when the state matches HALT. Each minimal instruction is a total function — partiality is expressed through Empty (branch elimination).

The HE reference interpreter is itself written in minimal MeTTa, with performance-critical paths implemented as Rust functions injected via (call-native ...). The metta operation bridges both levels: it analyzes the input atom and returns an execution plan in minimal MeTTa that includes Rust-backed steps.

Relationship to MOPS

The Meta-MeTTa operational semantics (MOPS) and the minimal instruction set offer complementary formalizations. MOPS' Query and Chain rewrite rules correspond to minimal MeTTa's eval. MOPS' Transform corresponds to unify. Minimal MeTTa's chain instruction has no direct MOPS analogue — it provides explicit sequencing absent from the more declarative MOPS model. Where MOPS provides the mathematical foundation for bisimulation proofs, the minimal instruction set provides the concrete implementable substrate.

(Provenance: repo-doc, hyperon-experimental docs — minimal MeTTa specification; publication, Meredith et al. 2023)