Meta-MeTTa Paper
Draft — This content has not been approved for publication.
How to Use This Source
This map covers two complementary foundational documents for the MeTTa language:
- Meta-MeTTa: an operational semantics for MeTTa (Meredith, Goertzel, Warrell, Vandervorst, May 2023). ~39K chars. arXiv:2305.17218. Formal operational semantics grounded in process algebra (λ/π/ρ-calculus tradition). Provides an algebra of states, Plotkin-style rewrite rules, bisimulation, effort-object metering, and a provably correct compilation to the rho-calculus.
- MeTTa Specification (Potapov, August 2021). ~45K chars. Internal specification document. Defines the language's type system (gradual, arrow, dependent, grounded), pattern matching semantics, equality chaining, evaluation model, and non-determinism.
Relationship between the two: The Specification (2021) defines what MeTTa does — its types, pattern matching, evaluation loop, and non-determinism. Meta-MeTTa (2023) defines how to reason about MeTTa — providing the formal apparatus (state algebra, bisimulation, compilation correctness) needed for independent implementations and verified compilers. Together they constitute the closest thing to a "Yellow Paper" for MeTTa.
Reading strategy: For language users, start with the Specification §2–4 (notation, types, pattern matching). For implementers, start with Meta-MeTTa §3 (algebra of states, rewrite rules). For blockchain/decentralization context, see Meta-MeTTa §6 (effort objects). Cross-reference the "Cards Grounded" column to find wiki articles that already synthesize each section.
Section / Chunk Map — Meta-MeTTa (Meredith et al., 2023)
| § | Section | Key Content | Cards Grounded |
|---|---|---|---|
| 1 | Introduction and Motivation | MeTTa as a language for humans and AGIs to write AGI behavior. Paper serves the role of a JVM specification or Ethereum Yellow Paper. | MeTTa Programming Language |
| 2 | Towards a Common Language for Computational Dynamics | Physics/CS/math agreement on computation shape: algebra of states + laws of motion. Four worked examples: λ-calculus (β-reduction), π-calculus (COMM rule), rho-calculus (reflective higher-order, name = @Term), JVM (register machine, non-WYSIWYG). Distinction between WYSIWYG and register-based semantics. | Foundation material — no dedicated card; informs MeTTa Full |
| 3 | MeTTa Operational Semantics | Core of the paper. Grammar of Terms (lists, multisets, comprehensions, atoms). Bindings (linear ←, repeated ⇐, peek ↼). Four-register state machine: \(\langle i, k, w, o \rangle\) (input, knowledge, workspace, output). Rewrite rules: Query, Chain, Transform, AddAtom, RemAtom, Output. insensitive(t, k) guard. McBride 1-holed contexts for extensional terms. | MeTTa Full, MeTTa Implementations |
| 3.1 | Rationale | Benefits: effective program equality (bisimulation), independent implementations, meta-level computation (type checking, model checking, macros, computational reflection). Correct-by-construction methodology. | MeTTa Full |
| 3.2 | Meta-level Computation | AGIs will model and adapt MeTTa's computation model. Meta-circular evaluators are legitimate presentations. | No dedicated card — future enrichment target |
| 4 | Ground Literals and Builtins | Required ground types: Booleans, signed/unsigned 64-bit integers, 64-bit floats, strings. Polymorphic operations \(+\) and \(*\). Transition rules for each type (BoolAdd, NumAdd, StrAdd, etc.). | Hyperon Experimental (implements these) |
| 5 | Bisimulation | Two approaches: Leifer-Milner-Sewell (heavy) vs. barbed bisimulation adapted from asynchronous π-calculus. Query in input space serves as barb. Bisimulation provides correctness criterion for compilation schemes. | No dedicated card — enrichment target for MeTTa Full |
| 6 | The Cost of Transitions | Network access tokens (§6.1). Ethereum's gas model (§6.2). MeTTa effort objects (EOs): polymorphic cost function \(\#\), commutative group on EOs, fifth register \(eos\) in expanded state. All rewrite rules reprised with resource bounds and signed terms \(t_{\chi(p,eo)}\). | ASI Chain Full, MeTTaTron (F1R3FLY blockchain integration) |
| 7 | Compiling MeTTa to rho-calculus | Three semantic functions: \([\![-]\!]_C\) (configuration — state to channels), \([\![-]\!]_E\) (evaluation — processes data), \([\![-]\!]\) (term transliteration). Channels for each register (i, k, w, o). Theorem 1: \(S_1 \approx S_2 \Leftrightarrow [\![S_1]\!]_M \approx [\![S_2]\!]_M\) (bisimulation-preserving). §7.3 extends to resource-bounded rholang. Theorem 2: analogous correctness for resource-bounded translation. | MeTTaTron, MeTTa Implementations |
| 8 | Conclusion and Future Work | Two versions presented (private + decentralized). Future: apply OSLF to derive spatial and behavioral types for MeTTa. | No dedicated card |
Section / Chunk Map — MeTTa Specification (Potapov, 2021)
| § | Section | Key Content | Cards Grounded |
|---|---|---|---|
| 0–1 | Scope and Introduction | Internal representation and semantics of MeTTa. Designed for grounded knowledge representation and reasoning with inference control and neural-symbolic integration. | MeTTa Programming Language |
| 2 | Notation | Symbols (Unicode names, grounded = references to external data/code). Expressions as trees, Lisp-style surface syntax. Atomspace as program container with pattern matching. @root self-reference. Metagraph vs. tree storage out of scope. | MeTTa Full |
| 3 | Basic Types | Gradual typing (type ? for untyped). Arrow types (->) with multi-argument support. Dependent types (e.g. (: Mortal (-> Human Type)), propositions-as-types). Grounded types via regex + constructor lambdas. No separate type constructors — any typed symbol is a constructor. Currying not automatic. Expressions starting with non-arrow-typed symbols are tuples, not applications. | MeTTa Full |
| 4 | Static Pattern Matching | Variables ($x prefix). Unification with asymmetric variable binding (query variables prioritized). Multi-occurrence constraint. Comma-joined conjunctive queries. Type-aware matching (type inference at insert-time or query-time). match and transform as grounded entry points. Expression enrichment: types as supplementary annotations (not structural), extensible to embeddings and attention values. | MeTTa Full, MeTTa Implementations |
| 5 | Equalities | = for chaining pattern matcher queries. Directed (not symmetric) — (= a b) means a can be transformed to b, not vice versa. Conditional matches with unify. Type-level equalities (e.g. (= (TCons $a (List $a)) (List $a))). Probabilistic truth values as type inhabitants (PLN-style TV example). | MeTTa Full, PLN Full (TV example) |
| 6 | One Step of Evaluation | Grounded stand-alone symbols → self. Non-arrow-typed head → tuple (self). Arrow-typed grounded head → evaluate subexpressions, then execute. Other expressions → equality query (= e $t). Conditional match resolution via recursive equality queries or grounded execution. | MeTTa Full |
| 7 | Interpretation and Non-determinism | Local Atomspace as evaluation queue. Step-by-step worked examples: Peano arithmetic \((+ (S\,Z) (S\,Z))\), if-then-else, truth-value propagation (And (Human Socrates) (Human Sam)). Non-total functions as both functions and type constructors. Non-determinism: multiple equality matches → multiple evaluation branches. Directed equalities enable causal generative models. Subset-sum solver example. Sampler primitive for concurrent evaluation. | MeTTa Full |
Key Concepts Cross-Reference
| Concept | Meta-MeTTa § | Specification § | Notes |
|---|---|---|---|
| Algebra of states / term grammar | §3 | §2 | Meta-MeTTa is more formal (monad + structural congruence); Spec is more practical |
| Pattern matching / unification | §3 (rewrite rules) | §4 | Meta-MeTTa defines unify() as primitive; Spec details variable binding semantics |
| Equality / chaining | §3 (Query, Chain rules) | §5 | Meta-MeTTa: formal transition; Spec: worked examples with conditional matches |
| Ground types and builtins | §4 | §3 (grounded types) | Meta-MeTTa lists required types; Spec shows regex-based registration API |
| Evaluation model | §3 (Output rule) | §6–7 | Spec provides the step-by-step interpreter model absent from Meta-MeTTa |
| Type system | — | §3 | Gradual/arrow/dependent types specified only in the Spec |
| Non-determinism | §3 (multiset semantics) | §7 | Meta-MeTTa: structural (multisets imply non-deterministic order); Spec: semantic (multiple equality matches) |
| Bisimulation / program equality | §5 | — | Only in Meta-MeTTa; Spec does not formalize equivalence |
| Resource metering / effort objects | §6 | — | Only in Meta-MeTTa; enables decentralized execution |
| Compilation to rho-calculus | §7 | — | Only in Meta-MeTTa; proves bisimulation-preserving correctness |
| Propositions-as-types / truth values | — | §3, §5 | Spec shows PLN-style TV integration via type-level equalities |
Enrichment Targets
Sections from these papers that are not yet fully reflected in existing wiki cards:
| Gap | Source | Target Card | Priority |
|---|---|---|---|
| Four-register state machine \(\langle i, k, w, o \rangle\) and formal rewrite rules | Meta-MeTTa §3 | MeTTa Full | High |
| Bisimulation as correctness criterion for implementations | Meta-MeTTa §5 | MeTTa Full or new subcard | High |
| Effort objects and resource-bounded transitions | Meta-MeTTa §6 | ASI Chain Full, MeTTaTron | High |
| MeTTa → rho-calculus compilation and Theorems 1–2 | Meta-MeTTa §7 | MeTTaTron or new subcard | Medium |
Gradual typing with type ? and arrow-type evaluation semantics | Spec §3, §6 | MeTTa Full | High |
| Asymmetric variable binding in pattern matching | Spec §4 | MeTTa Full | Medium |
| Directed equalities as causal generative models | Spec §5, §7 | MeTTa Full | Medium |
| Non-determinism model (multiple equality matches, subset-sum example) | Spec §7 | MeTTa Full | Medium |
| Expression enrichment framework (types, embeddings, attention values) | Spec §4 remark | MeTTa Full, ECAN Full | Low |
| OSLF-derived spatial/behavioral types (future work) | Meta-MeTTa §8 | Not actionable yet | Low |
Best-Source-For Shortcuts
- "What does a correct MeTTa implementation look like?" → Meta-MeTTa §3 (rewrite rules) + §5 (bisimulation)
- "How does MeTTa's type system work?" → Spec §3 (gradual/arrow/dependent/grounded types)
- "How does pattern matching work internally?" → Spec §4 (variable binding, conjunctive queries, type-awareness)
- "How does MeTTa evaluate expressions?" → Spec §6–7 (one-step evaluation, interpreter loop, worked examples)
- "How does MeTTa handle non-determinism?" → Spec §7 (multiple equality matches, directed equalities, causal models)
- "How does MeTTa run on a blockchain?" → Meta-MeTTa §6 (effort objects) + §7.3 (resource-bounded rholang compilation)
- "What is the formal relationship between MeTTa and the rho-calculus?" → Meta-MeTTa §7 (semantic functions, Theorem 1)
- "How does MeTTa support PLN-style reasoning?" → Spec §5 (TV type inhabitants, And-rule propagation example)
Source Cards
- Meta-MeTTa (Meredith et al., 2023) — ID 3271, ~39K chars
- MeTTa Specification (Potapov, 2021) — ID 3750, ~45K chars
Tags
Discussion