# MeTTa

> MeTTa, Hyperon's AGI language, implemented in SWI-Prolog, with `metta` as its
> Python surface. Atoms are Python values, spaces are queryable stores,
> equations rewrite, and any Python library maps onto those forms. Every line
> below is a signature, an exact return shape, or a contract you cannot guess.
> Names here are checked against the live engine and the real file tree by
> `check.sh`'s `llms` lane, so a rename breaks the build instead of misleading
> you. That covers call heads, paths and the library roster, and it does NOT
> cover the name of a distribution published elsewhere: nothing here owns an
> oracle for one, and a lane reading a sibling checkout would go red for that
> checkout's reasons. This file said `metta-fabric-pc` for a package that calls
> itself `metta-fabricpc` until 2026-09-03, and the lane had no opinion.
> Counts are dated; treat an undated number as unverified.

## Every source of information in this repository

Prose can drift; the first four rows cannot, because a gate lane regenerates or
re-runs them.

| source | what it is | kept true by |
|---|---|---|
| `examples/**/*.metta` | 258 executable programs, the semantics documentation, in 20 chapters numbered to 22 whose order is the order a reader meets each construct. Read these BEFORE writing down what MeTTa can express | every one runs in the `examples` gate lane; `tests/data/example_skips.txt` names the five that do not, each with its reason |
| `tests/data/syntax_introductions.txt` | the construct each example chapter introduces, so a file uses nothing it has not met | the `cumulative-syntax` gate lane, which also carries a permanent negative control it must keep catching |
| `website/reference/metta-*.md` | 24 pages reproducing source signatures and docstrings | `extensions/python/tools/reference.py` |
| `website/reference/metta-libraries.md` | every library's own `(@doc ...)` atoms | `extensions/python/tools/libdoc.py` |
| `tests/prolog/suites/*/*.plt` | plunit suites over the engine itself, grouped by the engine unit each one tests | the `plunit` gate lane |
| `extensions/python/tests/*/test_*.py` | blackbox, hypothesis-fuzzed, in the same 20 chapters `examples/` uses, plus `conformance/` for the arbiters and `repository/` for the tests whose subject is this repository | the `pytest` gate lane |
| `extensions/python/examples/language-feature-examples/**/*.py` | one Python file per shipped MeTTa example, written with no MeTTa source text, answering alpha-equal to its original or explicitly declining a structured-residue form, and pinned to an inference budget. Read these for how a MeTTa program is spelled in Python | the `twins` REPORT lane |
| `CODEC.md` | the wire codec: the tagged form every atom crosses as, what a new binding implements | `extensions/python/tools/codecdoc.py`, whose tables come from `tests/codec/corpus.json` |
| `extensions/python/metta/vocabularies.py` | the catalog's value vocabularies as StrEnum classes, one per `(vocabulary ...)` row; each member IS its wire word and encodes as its symbol, and bare words stay the runtime escape hatch | `extensions/python/tools/vocabgen.py`, the `vocab-sync` gate lane |
| `README.md` | the tour, and the argument for the design | |
| `CHANGELOG.md` | every user-facing change, with the reasoning | |
| `website/guide/*.md` | 15 pages of prose: concepts, run-query, spaces, atoms-terms, python-functions, define, structures, threads, observability, notebook, contract, getting-started, where-code-runs, pettorch | |
| `website/tutorials/*.md` | 9 numbered lessons, atoms through graph-view | |
| `website/integrations/*.md` | dataframes, pydantic, duckdb, SQLite blobs, arrays and embeddings, http routes | |
| `website/reasoning/*.md` | weighted relations, matchers and measure | |
| `extensions/python/examples/*/*.py` | runnable Python programs, each printing checked claims through `_common.py`: `check(label, got, expected)` raises `CheckFailed` rather than asserting, because `python -O` strips an assert while the print under it still runs, and `done(name)` refuses to print its OK line when nothing was checked, so an example that verified nothing cannot report success; the six under `gallery/` also check adjacent emitted-MeTTa and output comments plus bilingual `@example` atoms | the `examples` and `gallery` gate lanes |
| `extensions/python/notebooks/tour.ipynb` | the notebook surface, every structural argument a built term | the `notebook` lane |
| `engine/**/*.pl` | `engine/metta.pl` engine bootstrap loading the twelve `engine/metta/*.pl` units (terms, operators, input_guards, types, type_aliases, type_unions, effects, space_hooks, runtime, control, interop, registration), `engine/translator.pl` compilation facade over the six `engine/translator/*.pl` units (analysis, lowering, folding, special_forms, typing, runtime), `engine/spaces.pl` store facade over the eight `engine/spaces/*.pl` units (catalog, lifecycle, foreign, bounded_matching, native_matching, segment_matching, generic_join, arrow_products), `engine/filereader.pl` loader over `engine/filereader/source_lifecycle.pl`, `engine/parser.pl` reader and writer (with `engine/reader.c`, 923 lines of C parsing shipped-grammar sources and handing back each source's signature and declaration summaries from the same walk when `engine/reader.so` is built beside it; the Prolog grammar stays the specification, the custom-token path, and the fallback), `engine/json_codec.pl` the one JSON door this repository reads and writes through (with `engine/json_codec.c`, 1,219 lines of C answering a document exactly as `library(json)` answers it or declining to it, when `engine/json_codec.so` is built beside it), `engine/kernel.pl` the performance vocabulary beyond the conforming stdlib, `engine/type_rules.pl` the typing registry, `engine/translator_rules.pl` the translator rule registry, `engine/support_graph.pl` derived-artifact dependencies, plus `engine/specializer.pl`, `engine/duals.pl`, `engine/scc.pl`, `engine/tracer.pl`, `engine/trs.pl` and `engine/narrowing.pl` metatheory, `engine/prelude.metta`. Each unit is a plain source file consulted by its umbrella, so predicate ownership and load order are the umbrella's | |
| `engine/ext_points.pl` | every extension seam, each declared with its KIND. Five of them, and the count of each: `host_service` 87, `service` 58, `ownership` 36, `event` 14, `declaration` 13. The first three are contributed BY an extension, the two service kinds are defined by the engine and called by one (`clauses_from/2`). The contract for extending the engine | `ext_points.plt` |
| `lib/lib_*/` | 38 MeTTa libraries, implemented in `.metta`, `.pl`, or both, loaded with `!(import! &self (library lib_x))`; from Python the write door imports them, `m += lib.x` | `extensions/python/tests/ch08_data/test_library_door.py` |
| `lib/builtin_mods/*` | modules the engine SHIPS, imported by bare name: `!(import! &self skel)` | `builtin_modules` |
| `extensions/*/extension.pl` | one control file per seat, read when argv carries `extensions` and never read without it; a seat's `entry(engine, _)` loads only where its declared needs hold and its `entry(host, _)` is recorded for the seat's own runtime to consult, so the engine names neither a host nor a backend | |
| `extensions/node/src/*.ts` | MeTTa as a TypeScript library, the engine embedded in a Node process over swipl-wasm and the seam's second consumer: interned atoms, spaces as collections, lazy thenable answers, a lowered-source `define`, a traced generator `define`, host `op`s the engine calls back into, and `using` scopes. `extensions/node/bridge.pl` is its Prolog half and calls published surface only | the `node-binding` gate lane, and `extensions/python/tests/ch21_another_language_at_the_seam/test_node_binding.py` answers the same corpus in both hosts |
| `extensions/cmetta/cmetta.h`, `extensions/cmetta/cmetta.c` | the engine embedded in a C process through SWI's own foreign interface, the seam's third consumer and the only one IN the engine's process, so it reads `term_t` directly and has no wire codec. `extensions/cmetta/bridge.pl` is its Prolog half and calls published surface only | the `c-binding` gate lane, and `extensions/python/tests/ch21_another_language_at_the_seam/test_c_binding.py` requires this seat and the Python host to answer the same programs |
| `EXTENDING.md`, `DEVELOPING.md` | writing an extension; working on the engine | |
| `KERNEL.md` | every head the translator gives meaning to, core or derived, with the reason and the numbers | the `kernel-ledger` and `kernel-ledger-selftest` gate lanes |
| `check.sh` | the gate. `GATE_ONLY=1 sh check.sh` is what CI blocks on | |
| `extensions/python/metta/*.py` | the library. `extensions/python/metta/_space.py` is the `MeTTa` context and the `Space` handle; a leading `_` means internal | |

Counts re-measured 2026-09-06. The `llms` lane derives every explicit count in
this table, checks the library roster and every backticked path, rejects names
the live engine does not know, and asks the reverse question too: every
engine-known call head the example corpus exercises must be named here.

## Install and first call

The distribution is `pymetta` and the module it installs is `metta`.
`pip install 'pymetta[engine]'` after `apt install swi-prolog` (or
`brew install swi-prolog`, or `winget install SWI-Prolog.SWI-Prolog`), which
needs SWI-Prolog 9.3+ and Python 3.12+. The engine tree, the libraries and the
codec corpus ride in the wheel; the `engine` extra adds `janus-swi`, the
bridge to the SWI on the machine, and it is the only part a plain
`pip install pymetta` leaves out. Without it the package still imports and the
first engine call names the command for your platform. `pip install .` from a
checkout is the same thing, and `METTA_PATH` points an installed `metta` at a
clone's engine tree instead of the bundled one.

Run one MeTTa file with `sh run.sh path/to/program.metta`. Add `--verbose`
before the path when the program's authoring diagnostics matter, including
equation-head interpretation and source-reload reports; the default suppresses
informational messages. Python callers make the same choice with
`MeTTa(verbose=True)`.

```python
from metta import MeTTa, S, V, G, ground, Expression, equation, rules, parse, forms
from metta.vocabularies import EffectClass
context = MeTTa()                         # owns one engine context
m = context.self                          # the home Space, bound as &self
m.run("(= (f) 1) !(f) !(+ 1 2)")         # [[Grounded(1)], [Grounded(3)]]
context.close()                           # or `with MeTTa() as m:`
```

`m` in every block below is that home SPACE. The two receivers differ and the
difference is checked: a context carries the evaluation doors and forwards them
home (`run`, `eval`, `match`, `add`, `define`, `op`, `transaction`, `limits`,
`stats`, `trace`, `debug`, `space`, `close`) plus the collection protocols,
while storage and introspection stay on the space and are reached as
`context.self.atoms()` (`atoms`, `type`, `cast`, `digest`, `source`, `save`,
`is_function`, `arities`, `builtins`, `space_names`, `lint`, `derivation`,
`effect_plan`, `subscribe`, `watch`, every declaration verb). Asking the
context for a space door raises an `AttributeError` naming `m.self`, rather
than a bare one. Two contexts are two engines' worth of state in one process,
so a library never has to own the global one.

Module-level `metta.run/match/eval/add/remove/parse/fn/trace` act on one lazily
created default engine, for scripts that never need a second space.

```python
metta.llms() -> None    # print THIS file to stdout, the way help() prints
```

`python -m metta llms` prints the same document from a shell. `llms.txt` ships
inside the wheel beside the engine tree, so an install answers it without a
checkout, and it never pages: the door writes and returns whatever stdout is.

`metta.config` is the process-wide `Config` object. Inspect all four settings
with `config.as_dict()` and set them atomically with
`config.configure(stack_limit=..., heartbeat_interval=...,
declaration_limit=..., display_rows=...)`. The stack byte ceiling and Janus
heartbeat interval freeze after the first engine starts; declaration expansion
and displayed-row limits remain live. Set the same values before import with
`METTA_STACK_LIMIT`, `METTA_HEARTBEAT_INTERVAL`, `METTA_DECLARATION_LIMIT`, and
`METTA_DISPLAY_ROWS`; invalid or nonpositive values stop import by name.

## Atoms: built in Python, no engine call

`S.likes` is the symbol `likes`; `S["+"]`, `S["my-name"]` for non-identifiers.
`V.x` is the variable `$x`. `ground(obj)` / `G(obj)` wraps a Python value.
Applying a symbol builds an expression: `S.likes(S.Ada, S.Music)` ->
`(likes Ada Music)`. `Expression` collects any iterable into one ordered
atom: `Expression((S.f, 1, 2))` is `S.f(1, 2)`.
`parse("(f $x)")` reads exactly one form without evaluating it.
`forms("(a) (b)")` reads every top-level form without evaluating any.
Root builders `if_`, `and_`, `or_`, `not_`, and `in_` spell language heads
that are Python keywords or need variadic folding without raw bracket syntax.

FOURTEEN ATTRIBUTE NAMES ON `S` ARE OPERATOR WORDS, NOT SPELLINGS. Python's
`operator` module owns these words, and `S.<word>` reaches the engine head the
word NAMES rather than a symbol spelled like the word. Thirteen reach a head
and `S.floordiv` refuses, for the reason given under the table:

| `S.<attr>` | builds | | `S.<attr>` | builds |
|---|---|---|---|---|
| `S.eq` | `==` | | `S.add` | `+` |
| `S.ne` | `!=` | | `S.sub` | `-` |
| `S.lt` | `<` | | `S.mul` | `*` |
| `S.le` | `<=` | | `S.mod` | `%` |
| `S.gt` | `>` | | `S.truediv` | `/` |
| `S.ge` | `>=` | | `S.pow` | `pow-math` |
| `S.neg` | `(- 0 x)` | | `S.floordiv` | refused, see below |

So `S.sub(a, b)` is `(- a b)`, a SUBTRACTION, and nothing downstream can tell:
it stores, matches, digests and round-trips like any other expression. If you
wanted a symbol named `sub`, the bracket door gives it exactly:
`S["sub"]` is `sub`, and `S["add"]` is `add`. That is the general rule
(brackets are exact, attributes map) applied to a case where the map is a
lookup table rather than the underscore-to-hyphen rewrite, so unlike
`S.car_atom` -> `car-atom` the name you typed is not visibly present in what
you get.

The failure this produces is quiet. A relation genuinely named `sub`, built
with `S.sub(a, b)`, is stored as arithmetic; a later query for `sub` facts
answers `[]` against a graph that obviously connects, and the first suspicion
falls on the query rather than on the write.

`S.floordiv` REFUSES rather than guessing, because its settled image is
composite (`floor-math` over `/`) and no single head spells it. `S.neg` is
composite too but settled, so it builds `(- 0 x)`.

Four kinds, all immutable with `__slots__` and one-subpattern
`__match_args__`: `Symbol`, `Variable`, `Grounded`, `Expression`. So
`match atom: case Expression([head, *args]): ...`, `case Symbol(name):`,
`case Grounded(value):` all bind.
`Expression.head`, `.args`, `.children`. Free functions in `metta.atoms`:
`unify`, `substitute`, `order_key`, `arrow`, `typed`, `fresh`, `seg`, and
`register_object_repr` with its `unregister_` twin to control how a foreign
object prints as an atom. `metta.wire` owns `encode`, `decode` and
`atom_from_wire`.
The atom's OWN methods carry the rest: `a.alpha_eq(b)` for equality modulo
variable renaming, `a.map(f)` to rewrite every subterm, `a.vars` for the
variables it contains (so `not a.vars` is the ground test), and `repr(a)` for
the laid-out reading, the same layout `(pretty-atom $x)` gives on the MeTTa
side.
The object-level round trip is `bindings = pattern.unify(fact)` followed by
`template.subs(bindings)`. Its keys are variable atoms, not their names;
`Atom.subs` also accepts a query `Row` directly.
`metta.paths.path("profile", "age", to=V.age)` occupies an opaque handle's
pattern position, reads only those live attributes after the stored match, and
binds the reached value. `metta.paths.Key("name")` selects a subscription key
instead.
`metta.spaces.object_view(obj, relation="py-field")` exposes the same object's
current public fields as `(py-field obj name value)` atoms. Pass another
relation name to avoid colliding with an application's existing facts. Compose
it with a stored space through `spaces.union`, or register it directly so
adding a field atom calls `setattr`.

Arithmetic and logic operators BUILD terms, ALWAYS, whether or not an operand
is a variable: `S.x + 1` is `(+ x 1)` and `G(2) + G(3)` is `(+ 2 3)`, not `5`.
Unwrap with `.value` when Python arithmetic is what you meant.
`&` `|` `~` build `and`/`or`/`not`, `^` builds `xor`, `<<` and `>>` build
`bit-shift-left` and `bit-shift-right`, `**` builds `pow-math`, unary `-`
builds the subtraction image `(- 0 $n)`, unary `+` answers the identical atom,
`abs()` builds `(abs-math $n)`, `math.floor`, `math.ceil`, `math.trunc` and
`round` build their `-math` heads, `@` builds the library-provided name
`matmul`, and `//` lowers through `floor-math`.
Rich COMPARISONS do not build: `a < b` and friends answer Python
booleans in the engine's own `msort` order (so atoms sort), and `a == b`
is ordinary Python equality. Comparing an atom with a plain Python value
refuses and the message names the three ways out. A comparison TERM is spelled
at the bracket door, `S[">="](V.n, 60)`, or built by `a.eq(b)`, `a.ne(b)`,
`a.lt(b)`, `a.le(b)`, `a.gt(b)` and `a.ge(b)`; `a.alpha(b)` builds
`(=alpha a b)`. `Expression.__bool__` raises on comparison
and boolean heads, so `if S[">"](V.x, 1):` is refused rather than
silently truthy.

The MeTTa `==` is `(-> $a $b Bool)`, two independent type variables, and it
asks no type question at all: it is identity of the two evaluated operands.
So `!(== 1 "S")`, `!(== True 1)` and `!(== 1 a)` all answer `False` rather
than refusing, `!(!= 1 "S")` answers `True`, and `!(== (collapse ...) ())`
compares the collapsed tuple. This engine refused a cross-type pair until
2026-08-30; nothing does now. `=alpha` carries no arrow declaration and takes
anything, comparing modulo variable renaming. Python's `a == b` answers
`False` across kinds for the same reason.

## Running and querying: exact return shapes

```python
m.run(src, *, timeout=, inferences=)
                       -> list[list[Atom]], one inner list per ! directive
m.eval(target, *more, timeout=, inferences=, under=, theory=, interpreter=)
                 -> list[Atom | Undefined] | list[list[Atom | Undefined]]
m.match(*patterns, where=, limit=, timeout=, inferences=, under=, into=) -> Answers
m.answers(target, *, timeout=, inferences=, under=, theory=, interpreter=) -> Answers
m.sample(query, *, k=10, seed=7) -> list[Atom]
m.prepare(*patterns, where=) -> Prepared; .solve(given=...) many times, .columns
m.parse(src) -> Atom
m.register_token(pattern, constructor) -> None
m.unregister_token(pattern) -> None
m.load(path, *, timeout=, inferences=) -> list[list[Atom]]
m.save(path, format="metta"|"fast") -> int   (atomic, fsynced)
m.source() -> str   direct atoms as loadable MeTTa; exactly m.save(format="metta")
m.digest() -> str, 64-hex content hash of the space, store-independent
```

`target` may be a string or an already-built atom. `bind()` maps BARE SYMBOLS
(not `$vars`) to Python objects, which cross by identity, not by copy or repr:
`with m.bind(v=tensor): m.eval("(gated v)")` scopes that binding over every
call inside the block. A target with no applicable rule is returned as the
unreduced term; `eval_status()` names that path `not-reducible`.

Variables shared across query patterns join: `m.match(S.p(V.x,V.y), S.p(V.y,V.z))`.
`where=` is a term the engine evaluates per match: `where=S[">="](V.n, 60) & S["<="](V.n, 70)`.
`into=` builds fields by matching column names, or rebuilds a complete
constructor expression captured in one column.

`under=` changes the annotation algebra for either a relational match or a
call. Ten carriers ship. The answers below are one program's: two facts tagged
`0.6` and `0.3` reaching one head through a rule tagged `1.0`.

| carrier | combine, extend | answers | |
|---|---|---|---|
| `bag` | `+` `*` | `0.9` | the default when `under=` is omitted |
| `bool` | `max` `*` | `0.6` | |
| `set` | `max` `*` | `0.6` | combine is idempotent, so multiplicity collapses |
| `counting` | `+` `*` | `2` | an engine aggregate crossing no answer rows |
| `ranked` | `max` `*` | `0.6` | orders highest first |
| `prob` | `+` `*` | `0.9` | orders highest first |
| `tropical` | `min` `+` | `1.3` | orders cheapest first |
| `budget` | `min` `+` | `1.3` | ascending like tropical, spent rather than distance |
| `prov` | `plus` `times` | `(plus (times 1.0 0.6) (times 1.0 0.3))` | a TERM, not a number |
| `amplitude` | `amplitude-add` `amplitude-multiply` | refuses | outside its declared fragment |

Ten are objects: `metta.bool`, `.bag`, `.counting`, `.set`, `.ranked`,
`.tropical`, `.prob`, `.prov`, `.budget` and `.amplitude`. The bare name works
wherever an object does, `under="budget"`.

`metta.vocabularies.Semiring` names the closed set: `bool`, `bag`, `counting`,
`set`, `ranked`, `tropical`, `prob`, `prov`, `budget`, `amplitude`.

`metta.vocabularies.AlgebraLaw` names the accepted set: `combine-associative`,
`combine-commutative`, `extend-associative`, `extend-commutative`,
`left-distributive`, `right-distributive`, `combine-idempotent`,
`combine-zero-identity`, `extend-one-identity`, `extend-zero-annihilates`,
`contraction`, `associative`, `commutative`, `distributive`, `idempotent`.

| algebra-law alias | expands to |
|---|---|
| `associative` | `combine-associative`, `extend-associative` |
| `commutative` | `combine-commutative` |
| `distributive` | `left-distributive`, `right-distributive` |
| `idempotent` | `combine-idempotent` |
| `contraction` | `contraction` |

`under=counting` answers one `TaggedAnswer` whose `.annotation` is the count
and whose `.value` is `()`, the empty value saying no proposition row was
manufactured; every carrier yields `TaggedAnswer` with `.annotation`, `.plan`,
`.why()` and `.under(other)`. A `prov` tag is a symbolic term over the source
tags, so an interpreter outside the engine can walk it, which is how one
query's fused derivation carries derivatives; `.why()` renders the retained derivation and `.under(other)` reinterprets that
same derivation without querying again, including under an algebra whose
operations are plain Python callables. `amplitude` refuses until
`m.annotations` declares its fragment with the capabilities `finite`,
`contractive` and `staged`.
`with metta.under(carrier):` supplies the task-local default and an explicit
keyword wins. `metta.current_algebra()` reads back which of the three is in
force, following the same precedence a query does, per-call carrier over task
scope over the current context's `annotations` row, and answering `None` when
none of the three is present rather than reporting execution's implicit
Boolean default as a declaration. It answers from inside an operation the
engine has already entered, which is what `metta.current_space()` does for the
other half of the ambient state.
`m.match(q, under=ranked)[:3]` is the three best, and it reaches the provider
as `limit=3` when the space is foreign, its `(source ...)` discipline is not
`linear`, it declares `emits("best-first")`, its effective algebra is the
carrier the query selected, and the query is one pattern with no `where=`.
Short of all five it pulls the shared cursor and orders here, so the answers
are the same either way and only the work changes. `(top 3 ...)` is the
language-side form, under the three declarations Contracts names.
`m.sample(q, k=10, seed=7)`
samples with replacement from implicit `(rate n)` tags using a local seeded
generator.

THREE DIFFERENT QUESTIONS WEAR THE WORD "PROBABILITY" AND EACH HAS ITS OWN
MECHANISM. Picking the wrong one answers a number that means something else,
so choose by the question you are asking:

- is this PROPOSITION true, and how confident am I: `lib_pln`, `lib_pln2`, and `lib_nars`
  truth functions. The value belongs to the fact.
- what VALUE does this quantity take, over a distribution: `lib_measure`
  holds transparent weighted superpositions, where `ws-normalize` makes a
  distribution and `ws-sample!` draws from it, its bang naming the choice it
  makes. `lib_distribution` maps one distribution, combines independent ones,
  conditions an explicit joint law, and asks named probability questions. The
  value belongs to the quantity.
- how did this DERIVATION combine the tags it passed through: `under=`, above.
  The value belongs to the proof.

For the value question, import `lib_distribution` and write a finite law as
`((weight value) ...)`. Choose the head by the question:

- `(ws-map fun dist)` pushes one distribution through a pure unary function.
- `(ws-map2-independent fun left right)` pushes the product of two independent
  distributions through a binary function. If the values are correlated, put
  `(Pair left right)` values in one joint distribution and use `ws-map`.
- `(ws-mass-at-least dist threshold)` answers the inclusive probability
  `P(X >= threshold)`.
- `(ws-prob-gt-independent left right)` answers the strict independent win
  probability `P(X > Y)`; it is not stochastic dominance, total variation, or
  comparison of expectations.
- `(ws-condition-joint joint observed)` conditions `(weight (Pair input
  output))` rows on an exact input and returns the output distribution.
- `(ws-average-independent (dist ...))` gives the arithmetic-mean distribution
  for mutually independent numeric inputs.
- `(ws-add-bernoulli-independent dist p)` adds an independent zero-or-one trial
  with `p` in `[0, 1]`.

Each head normalizes relative weights and merges equal outcomes at their first
position. Empty input, negative or nonfinite weights, and all-zero mass answer
an `Error` whose message states the repair.

`under=prob` is the THIRD of those. It weights a derivation and is not a random
variable's distribution, so a query asking what a height is will not get one
from it; that is `lib_measure`'s question. Keeping the three apart is what lets
a fact carry a truth value AND range over a distributed quantity AND be reached
by a weighted proof, without any one of them overwriting another.

`with m.capture() as output:` collects printed text in `output.text` without
changing either return shape. `with m.atomic():` makes each whole call one
transaction; `with m.speculative():` runs each call against a snapshot and
discards its writes, so `m.run("!(add-atom &self (f 1))")` inside one leaves
nothing behind. Both scope every CALL in the block, the Python write doors
included: `m.add`, `m.remove`, `del m[pattern]`, `m.transfer` and `m.clear`
inside a speculative block leave nothing behind, and inside an atomic one
each is its own committing transaction. Per CALL is the whole contract: a
later call does not see what an earlier one wrote in a speculative block, and
a raise does not undo a call an atomic block already committed.
`m.transaction(callable)` is the boundary that spans SEVERAL calls, and there
is no with-block form of it, because SWI's transaction/1 and snapshot/1 take
a closed goal and an engine refuses to yield out of either.
`with metta.speculate():` is the same discarded execution scope for the lazy
module-tier default context.

`Rows` is a list of `Row` with `.columns`, and `Answers`, which is what `match`
and `answers` hand back, is the lazy replayable cursor carrying every door
below. `row.x` and `row["x"]` both work.
`rows.one()` (exactly one), `.first()`, `.column(name)` -> that column's atoms,
`.group_by(name)` -> a dict from each column atom to its `Rows` slice,
`.table()` -> dict of columns decoded to Python values, `.to_dicts()` -> plain
mappings, `.to_df()` / `.to_pl()` -> pandas / polars, `.build(column, cls)`
rebuilds one named column, and `.build(cls)` rebuilds the sole constructor
column. Both keep `cls` for type checkers.
`.pipe(fn, *args)` chains, `_repr_html_` renders in notebooks.

`m.assuming(*facts)` is a with-block where those facts exist and then do not.
`m.batch()` collects `add()` calls and crosses once at exit.
`m.limits(timeout=, inferences=, stack=)` sets scoped defaults for every call
inside; `stack` is SWI's combined-stack ceiling in bytes.

## The three seams anything plugs into

It is a KERNEL because the point is what plugs into it. **Lower it**: host
code becomes equations (`@m.define`, translator rules). **Extend it**: the
engine calls your code (Python operations, Prolog predicates, C foreign
predicates, reader tokens). **Back it**: the atoms live elsewhere, because a
space is an interface, so SQLite, DuckDB, NetworkX, a live object, another
process or MORK can BE a space and still join with a native one. A
table-backed space is one declaration,
`(bridge (edge $a $b) (row edges (a $a) (b $b)))`, from which every provider
operation derives in both directions: a match becomes a WHERE, a repeated
variable `WHERE a = b`, `take` a LIMIT, an add an INSERT. EXTENDING.md is the
long form and names all nine seams; forking should never be the answer.

## Spaces

`ctx.space(name)` selects on the `MeTTa` context and `ctx.space()` or
`metta.space()` creates a fresh one, a context manager whose exit drops it;
`m.copy()` clones contents into a fresh anonymous
space through the bulk door, so equations copy as equations and keep running.
`m.drop()` clears a space and releases its name: a drop clears the whole life,
atoms, equations, subscriptions, import markers and tabling state. Named spaces
compile into their own module, so two spaces can define the same function.
`(context-space)` names the space the running code is in, and
`metta.current_space()` reports it from inside an operation.

`m.add(*atoms)`, `m.remove(atom)`, `m.atoms()`, `len(m)`, `m.clear()`,
`m.space_names()`, `m.name`, and `metta.tables.add(m, head, source)` reads
polars / pandas / mappings / iterables into `(head v1 .. vn)` facts and
answers how many.

The write family is VARIADIC where n-ary is the meaning, each shape one
engine crossing inside one transaction: `a.transfer(x, y, to=b)` moves one
occurrence per atom between spaces, `m.remove(x, y, z)` counts the found
while the one-atom call keeps its truth value, `m.eval(t1, t2)` answers one
group per term under one bind scope, and `x.unify(y, z)` is SIMULTANEOUS,
every operand agreeing under one substitution or the answer is None.
`+=` and `-=` classify their operand the same way, so the fact stream one
door stores the other subtracts (`m -= [(S.Edge, a, b), (S.Edge, b, c)]`).
`-=` takes ONE occurrence per element, Counter's grain, which is what makes
it `+=`'s inverse; `remove()` is that same grain reporting absence; and
`del m[pattern]` is the drain, every unifying occurrence in one crossing.
MeTTa spells the pair `subtract-atom` and `remove-atom`. The `MeTTa` context speaks the same protocols as its own space,
so `m += lib.dict`, `len(m)`, `atom in m`, `m[pattern]` and `del m[...]`
work on the process home directly; `bool(m)` is always True, since a space
is a handle rather than a value that dwindles.

`metta.spaces` composes spaces without copying: `union(*spaces)` reads a set as
one, `overlay(front, back)` reads both and writes to the front, `readonly(s)`
refuses writes by capability, `mapped(s, shape)` is a shape view from one
declaration, and `diff(a, b)` says HOW two spaces differ where `digest()` only
says THAT they do. Each ANSWERS a provider, not a space, so attach it to query
it: `metta.attach("&all", metta.spaces.overlay(front, back))` then
`all.match(...)` joins across both layers with `where=`, `under=` and Answers,
where the composed object's own `match(pattern)` is the provider protocol's
narrow one. Each composes STORAGE and is a provider, not an evaluation
context: equations reachable through one are data, and read back by `atoms()`
without firing, unless that provider declares `rules`.

`metta.structures` holds the stores worth having: `AlphaSet` (atoms modulo
variable renaming), `PatternMap` (a MutableMapping keyed by atoms),
`MatchIndex` (many patterns, one atom, which match), `LiveView` (a materialised
view kept current by the space's own writes), `ClosureView` (reachability over a
stored relation, tabled from birth, which is what makes a closure over CYCLIC
or symmetric data terminate at all: the same reachability written as recursive
equations does not terminate over a cycle, so reach for this rather than
writing the rules), `TabledMap` (a computed cache that stays correct).

`&metta` is the space in which the library describes itself, and it is where
every declaration below is stored. The catalog describes its own kinds there:
`(kind head argspec...)` rows declare each declaration's shape,
`(vocabulary name value...)` rows declare the value sets, and
`(claim vocab value property...)` rows attach per-value facts. A
`(policy axis knob default)` row names each engine decision point and its
shipped choice. There is exactly one row for each of agenda, algebra,
atomicity, caching, delivery, determinism, dispatch, equality, errors,
fidelity, merge, order, reaction-order, save-format, source-kind, storage,
transaction-mode, typing, volatility and world, twenty of
them. `tests/checks/check_policy_inventory.py` asks the running catalog for
those rows and the semiring ordering claims, joins them to their implementation
seams, and rejects multiline `member/2` or `memberchk/2` lists, Python
`Literal[...]`, and Python list/set membership that bypass the catalog. The
immediately preceding annotation may exempt only mechanism-internal,
arbiter-owned-language-law, codec-version-identity, or
documented-collision-decision, with a reason and an existing local source line
or symbol. Only catalog preset terms in `engine/spaces.pl` and the generated
`metta.vocabularies` output are authority rather than independent lists. One
generic checker validates every `&metta` write against them, a violation is a hard
error naming the atom, the position and the argspec, and a head with no kind
row passes untouched, so third-party declaration kinds are ordinary data
until their author declares a kind row for them.

Function dispatch has six axes. Match `(dispatch-default $axis $value)` in
`&metta` to read their shipped defaults, and add
`(dispatch-policy f NoMatchEnum NoMatchFail)` to override one axis for one
function. The axes are `MismatchEnum`, `NoMatchEnum`, `EvaluationOrderEnum`,
`FunctionResultEnum`, `ClauseFailedEnum`, and `OutOfClausesEnum`; each axis's
accepted values are published by its same-named vocabulary row. Remove the
override atom to restore the default immediately.

## Python functions as MeTTa functions

```python
@m.op(effect=EffectClass.pureStructural)
def hypot(a: float, b: float) -> float: ...
```

Effect metadata is required, with `effect=` the canonical spelling for new
code and an existing `(effect name class)` declaration atom retained as a
compatibility input. The remaining options are `name=`,
`transport="encoded"|"raw"`, `declarations=` (ordinary Atom claims),
`arities=`, and `inverse=` (the callable that runs it backwards).
`m.unregister_op(name)` removes every arity and declaration. A coroutine
operation answers a FutureSpace immediately rather than suspending the call:
the future IS a space, so awaiting it is matching it, and `(async-op <name>
<future-space> launch|landing)` makes both ends observable. Landing is
published after the future settles, so an await that has returned says the
operation is terminal and says nothing about whether a landing subscriber has
run yet; wait on that subscriber's own signal when the observation is what you
need.

The ordered `EffectClass` members are `pureStructural`, `readOnlyLookup`,
`nondeterministicReadOnly`, `writesState`, and `oracleIO`. A plan's class is
the strongest member: `EffectClass.compose(effects)` folds that join and an
empty plan is `pureStructural`. Registering a generator or a generator inverse
LIFTS the class to at least `nondeterministicReadOnly` rather than refusing, so
`effect="pureStructural"` on a generator is accepted and reflects
`nondeterministicReadOnly`. Every registration publishes its canonical
`(effect name class)` row in `&metta`; missing metadata refuses before engine
state changes and names all five remedies. The retired input spellings map as
`immutable -> pureStructural`, `stable -> readOnlyLookup`, and
`volatile -> oracleIO`. Only the canonical names appear in `EffectClass` and
reflection.

The Python name is the MeTTa name, VERBATIM, and nothing is rewritten. Hyphens
are MeTTa's convention and Python cannot spell one, so ask: `name="p-digit"` on
`op`, `@m.define(name="p-sum")`, `rename=` on `integrate.module_ops`.
An operation name must also read as one symbol: a delimiter, variable spelling,
literal, or registered reader token is refused before either registry changes.
The same holds inside a compiled body, where a called name is resolved exactly
as written, so a hyphenated engine function is reached through an alias
equation the body can spell, `(= (sqrt_math $x) (sqrt-math $x))`.

Reader classes are full-token regular expressions. `m.register_token(pattern,
constructor)` gives the constructor the complete matched lexeme and accepts an
Atom or any value `encode` accepts; registering the same pattern replaces its
constructor, and `m.unregister_token(pattern)` removes it. Source has the same
door as `!(register-token! "[A-Z][0-9]+" tagged)`, which parses a later `A7` as
`(tagged "A7")`; `unregister-token!` removes that class. The shipped number and
string literals are rows in the same declared mapping, visible through
`metta_reader_token_class/3`. Registration changes later parses only.

Annotations become declarations in the engine's idiom: a `TypeVar` is
parametric, a `Union` declares one arrow per member, `Callable[[int],int]` ->
`(-> Number Number)`, `tuple[int,str]` -> elementwise, and
`Annotated[int,"metres"]` retains `Number` in the arrow while publishing its
metadata as a matchable `(Annotated Number "metres")` claim. An ATOM in
annotation position IS the type, which is the escape hatch for a MeTTa type no
Python class spells: `def speak(a: S.Animal) -> S.Sound` declares
`(-> Animal Sound)`, and the doc's `(@type ...)` field carries the same atom.
A generator is
nondeterministic, one answer per yield; returning `None` answers nothing, which
is why an `Optional` return declares the value type. An annotation the runtime
cannot resolve, a `TYPE_CHECKING`-only import for instance, drops only its own
parameter: the ones that resolve still declare, and a call form that does reach
the unresolved one is refused naming that parameter. An unannotated callable
makes no type claim. `(arguments name atoms)` asks for Atom wrappers after
ordinary evaluation, while an `Atom` annotation receives the written term
before evaluation. Only `(effect name pureStructural)` licenses the AUTOMATIC
cache, the one nobody asked for. A written declaration is carried out as
written whatever the class says: `!(memoize f)`, `!(memoize-exact f)`,
`!(tabled (f $x))` and `(cache f force)` cache a body that prints, writes a
space or is declared `oracleIO`. Two refusals remain and neither judges a
body: a name no function answers to, and a predicate SWI already tables, which
`force` does not open. These
policy atoms live in `&metta`; `(op name arity raw_det|raw_many)` records raw
transport.

`@m.define` compiles the Python BODY into MeTTa equations. Calling the resulting
`Defined` evaluates in its owning space and returns every engine answer;
`S.name(...)` stages the term explicitly, while `.py` keeps the plain function.
There is no unsupported-construct list. A body may say `try`/`except`/`else`/
`finally` and `raise`, which ride the engine's own error algebra (a raise
PRODUCES through `throw`, the body runs under `catch`, `except` matches by
MRO NAMES so a custom hierarchy matches as `isinstance` would, and `as e`
reconstructs the live instance); dict and set literals, which lower to
`lib_dict`'s `dict-space` and reach it through `get-value`, `dict-has`,
`dict-put`, `dict-remove`, `dict-size` and the view methods, comprehensions
included; `type X = T`, which IS the rewrite rule it reads as; and `global`,
which is a pragma over the definition module. `&`, `|`, `^`, `~`, `<<`, `>>`
and `//` are engine builtins, so they pay no host crossing. Anything else
odd becomes a visible host island inside the equation, run per application
and never at decoration time, which is what `py(...)` spells explicitly. The
refusals that remain cite their ground in one of the two languages: an
unresolvable name is Python's own NameError, a `nonlocal` targets a frame no
stored equation outlives, and a `finally` reading a name its `try` rebinds
is a stale read the compiler names.
Inside a compiled body `match(pattern, template)` is LOWERED rather than run,
against `(context-space)`; a leading handle, space parameter or `"&kb"` names
another space, and two or more patterns before the template are the engine's
own conjunction `(, p q)`, the same join the read door spells as `m[p1, p2]`.
A Python `match` STATEMENT is a `case`: its arms lower to flat case rows over
the subject, so an `Empty` arm answers for a subject with no answers, and an
arm carrying a guard or an as-name nests the arms from there under a variable
row.
Stacked clauses become a first-match dispatcher. It takes `name=`, and
`prolog=` to make a Prolog file the function with the Python kept as the
reference twin. A local assignment such as `result: int = value`
becomes the enforceable in-place claim `(: $result Number)` inside its `let*`.
The parsed AST also supplies each definition's absolute source span, source
docstring, lexical free variables, and a conservative effect class through
`Defined.source_span`, `.doc`, `.free_variables`, and `.effect`; each clause joins the classes of the
operations it calls, stacked clauses join again, and `source-span`,
`free-variable`, and the resulting `effect ... <class>` atom reflect in
`&metta`. Replacement and `clear()` retire stale facts. `Defined.pure` remains
the compatibility projection of
`Defined.effect is EffectClass.pureStructural`.
`@rules` executes a generator with one rule-local `Var` per parameter and
returns its yielded equations as ordinary atoms. Defined calls stage only in
that scope. `equation(lhs).to(rhs)` statically keeps both halves on one Python
type and derives from the first-class longhand `S["="](lhs, rhs)`. Inside a
compiled generator, `yield from call(...)` delegates only when the callee's
nondeterminism is known; an ambiguous engine call refuses with the two explicit
spellings instead of splicing the call's children.
`m.define(cls)` declares a class into a space: `(: ...)` atoms, one accessor
equation per field for an expression-image class, and its methods registered as
functions, so the class crosses with its behavior. Python's class hierarchy IS
a subtype relation, so declaring `Animal` and then `Dog(Animal)` stores
`(:< Dog Animal)` and `get-type` on a `(: Rex Dog)` widens to `[Dog, Animal]`.
Only DECLARED classes and REAL bases become edges, which keeps `object`, a
NamedTuple's `tuple`, an enum's `Enum` and a virtual `abc` registration out.
`m.type(atom)` is the other verb and is unrelated: it answers that atom's first
`get-type`.
`m.fn.superpose(...)` calls an engine function from Python and answers every
answer; `m.fn["car-atom"]` is the exact door for a head outside Python's
identifier grammar, and `.compiled`, `.equations` and `.type` on the handle read
its clauses, its stored equations and its declared type. The namespace is not
callable, so `m.fn("superpose")` is a TypeError. Module-level `metta.fn` is a
different thing, the symbol namespace a compiled body writes `fn.add` against.
`m.register_prolog(source=..., path=..., names=...)` registers Prolog
predicates directly, which is the fast path: 2 inferences a call against 20 for
the same operation through an encoded `m.op`, measured 2026-09-06 by
`python -m benchmarks.extension_cost` from `extensions/python`, which subtracts
its driver so each figure is one call's marginal cost.
`extensions/python/llms.txt` carries the whole tier table.
`m.register_foreign_library(path, entry=, names=)` loads a compiled `.so`.
`m.unregister_prolog(extension)` releases everything one extension registered.

## Types and cast

Types are optional atoms: `(: Ann Person)`, `(: age (-> Person Number))`.
An arrow may carry ANNOTATIONS in its own brackets,
`(: twice (-[det]-> Number Number))`, and it then governs execution and
compilation exactly as the plain `->` does: `!(twice "s")` is a `BadArgType`
either way. The stored atom, `get-type`, the docs and source export all retain
the written spelling. The brackets hold one slot or two, and the ORDER is
fixed: a determinism word from `metta.vocabularies.Determinism`, one of `det`,
`semidet` and `nondet`, then optionally an `EffectClass` member. One slot
leaves the class at `oracleIO`, the top, and a class ALONE is not an arrow:
`(: f (-[oracleIO]-> Number Number))` is refused as a declaration that types
the symbol rather than calls to it. `(-[nondet,readOnlyLookup]-> Number
Number)` publishes `(effect f nondeterministicReadOnly)`, because a `nondet`
product joins its class with that one. Both slots must be CONCRETE: a `$name`
in either is refused at the declaration, because a product variable has no
runtime consumer, and so are a nested product and an annotation on a
translated form. A plain `->` is `(-[nondet,oracleIO]->)`, which is why it
promises nothing. `(pragma! verify-cardinality true)` is what turns a
determinism claim into a runtime check; without it the claim is trusted.
`(: Count (Alias Number))` defines a transparent structural alias. Aliases
expand inside tuples and full arrows in their declaration owner's scope;
reflection retains the written declaration. An alias of `Atom` preserves
the same argument mask and result finality as `Atom` itself.
`(| Number String)` is a union type, usable wherever a type goes: an argument,
a result, a tuple field, an alias right side. A value is admitted when SOME
member admits it; a value whose own type is a union is admitted only when EVERY
alternative is, under one assignment of the type variables they share, so
`(| Number String)` fits `(| Number String Bool)` and not `(| Number Bool)`.
Nested unions flatten, a repeated member is one member, a one-member union is
that member, and `(|)` or an improper union raises a type-syntax error rather
than standing as a type nothing satisfies. `|` heads a union only where a type
is read: `(|-> ($x) ...)` is still a lambda and `(| a b)` is still data.
`Atom` and `%Undefined%` keep each family's own meaning inside a union, and a
union naming `Atom` is an ordinary evaluated, checked parameter rather than an
evaluation mask. Testing a union-typed value does NOT narrow it: there is no
occurrence typing, so a later use still faces the whole union. `match-types`
and the `type-cast` built on it compare written types by unification with
wildcards and do not decompose a union; union membership is the argument and
result relation.
A typed mismatch answers an `Error` value whose reason is `BadArgType` or
`IncorrectNumberOfArguments`, so a MeTTa program can handle it with `if-error`.
`(add-typing-rule! name family actual expected outcome)` adds a module-scoped
checker rule; `outcome` is `accept`, `(refuse reason)`, or `defer`, and
`remove-typing-rule!` withdraws it. Families are `ordinary`, `derived`,
`reporting`, `witness`, `arrow-arity`, `widening`, `declared-widening`, and `metatype`.
User rules run
before the shipped declarations. A named refusal appears in the resulting
`BadArgType`; the confluence report lists its user/user and user/shipped
overlaps as conditional proof obligations.
`m.cast(value, type)` returns the value or raises `CastError` naming the types
the value does admit. Its bound type observation uses `witness`: the wildcard
applies to the target only, so an unknown actual cannot establish a concrete
target. This is stricter than ordinary typed-call acceptance. Aliases inherit
that rule and ordinary user refusals. `Atom`, `%Undefined%` and `_` are unchecked. The
metatypes `Atom`, `Variable` and `Expression` mask evaluation: a parameter
declared with one receives its argument as written at every door, and a call
whose declared result is the metatype `Atom` answers as produced where any
other declared result re-enters evaluation, so `!(car-atom ((+ 1 2) b))` is
`3` and a caller that wants a call's value in a masked position names it
first with `let`. Minimal MeTTa's `eval` is one equality step over retained
source equations; NotReducible is a control result only `chain`, `function`,
and `metta-thread` observe raw, an application boundary retains an
irreducible call as written, and a function frame distinguishes a produced
marker from an irreducible body. A user type
declared with `(: Payload DontEvalType)` is also an evaluation mask: a function
parameter of type `Payload` receives its written argument unevaluated. The
declaration is required; no type-name convention enables the behavior. A float
or signed-i64 integer has type `Number`; a wider integer has type `BigInt`. A
`BigInt` satisfies a declared `Number` parameter, while a `Number` does not
satisfy `BigInt`. Arithmetic stays exact and result typing follows the result
width. `bool` spells `Bool` before `int` is classified by that boundary. The
target is positional-only, and a concrete Python class target is also the
static return type of `cast`, `convert.build` and `Rows.build`.
An expression with no arrow-typed head is typed element by element. Once its
head has an arrow, the arrow controls the application: an under-applied call
has no type answer and does not fall back to a tuple type.
The empty expression is the unit value: `get-type` and `get-type-space` report
its type as `(->)`. That is an observer rule; argument checking continues to
treat `()` as gradual rather than forcing a unit-type constraint.
A state cell has type `(StateMonad $t)`: `(new-state 0.4)` is
`(StateMonad Number)` and arithmetic on it is a `BadArgType`, so a cell is
dereferenced with `get-state` before use. `get-metatype` classifies a NAME by
whether this engine holds a function for it, so it answers `Grounded` for
`car-atom`, for a literal, and for a name the running program has just given
an equation, and `Symbol` for `nop`, `hyperpose`, `sealed`, a name nothing
defines, and every space handle and state cell, `&self` included. What a
handle or a cell IS is read with `get-type`, which answers `SpaceType` and
`(StateMonad $t)`.
`metta.State[T](value, space=None)` is the Python handle: `.value` reads and
writes the same engine cell, `__metta__` carries it across any atom boundary,
and the write answers `true` rather than the cell. Because a cell is an
ordinary atom it also serves as a mutable TAG, so an algebra that dereferences
it reads the current weight on every match.
`m.arities(name)`, `m.is_function(name)` (visible from here),
`m.is_function_here(name)` (has clauses HERE), `m.builtins()` (every
registered function and translator special form, sorted without duplicates);
each is a `Space` method, so any space handle answers for its own view.

## Declarations: how a space behaves, written as atoms

Each head-named method below writes one atom into `&metta` and returns it;
removing that atom withdraws the declaration. Coherence is checked eagerly in
the same transaction as the write, so a new entry that could disagree with an
existing one fails there, naming both, rather than on the first query in their overlap.
A variant-identical `(: name type)` row is likewise refused and names the first
row; distinct arrows for one function remain valid overloads. A public batch
is checked before its first write, so `m.add(declaration, declaration)` leaves
neither copy behind.

```python
m.handles(pattern, "Exact"|"Partial"|"Sound"|"Refuse", det=)
        how faithfully a space answers one query shape. Exact licenses pushing
        the caller's bound down to the provider; Partial and Sound stay
        candidates the engine re-unifies; Refuse makes the query a loud error
        instead of a silent partial answer. (in $x) at a position matches only
        queries arriving with it bound, so a scan-only source is three words.
m.emits("depth"|"fair"|"best-first")                 answer order
m.merge(pattern, "depth"|"fair"|"best-first")        how answers merge
m.consumption("linear"|"repeated"|"peek")            consumption discipline; writes (source <space> <kind>)
m.atomicity("transactional"|"atomic-single"|"best-effort")
m.context("closed-world"|"open-world")               what absence means
m.on_error(pattern, "keep"|"empty"|"abort")
m.image(type_name, "opaque"|"transparent"|"auto")    how values cross
m.algebra(name, *, combine, extend, zero, one, laws=(), carrier=(),
          requires=(), order=None)
        add one catalog algebra; equational laws are exhaustively checked over
        the finite carrier before they may license answer fusion
        A declared algebra is OWNED BY THE SPACE THAT DECLARES IT: the row's
        last field is that context, and lookup reads it before falling back to
        the shipped presets, whose owner is `global`. The same key annotations
        use, so a sibling space does not inherit it. Equational checking runs
        in the declaring space's equation module, so a MeTTa equation defined
        there certifies the algebra that names it.
metta.algebra(name, *, plus, times, zero, one, laws=(), carrier=(),
              requires=(), order=None) -> DeclaredAlgebra
        construct an arbitrary algebra through the callable `metta.algebra`
        module, whose plus and times may be plain Python callables; it targets
        the space `metta.current_space()` names, so inside `with scratch:` the
        row is owned by `scratch`. Ten carriers ship, tabled under `under=`
        above, and each is also an object
m.annotations(algebra, *, capabilities=())
m.annotations(operation, algebra, *, capabilities=())
        choose any declared algebra for this space or an operation; required
        capabilities are checked before the catalog row lands. This row is
        keyed by the same context the algebra row above is owned by
m.add_tagged_fact(tag, proposition)     store ordinary (fact tag proposition)
m.add_tagged_rule(tag, head, *premises) store the generic threaded rule form
m.match(query, under=algebra) / m.answers(call, under=algebra)
        return annotated answers; these are the only public algebra evaluators
m.sample(query, *, k=10, seed=7)
        stable weighted selection from nonnegative `(rate n)` tags
m.admits(type_name)                 only TYPE-carrying atoms enter
m.capacity(limit)                   an add beyond LIMIT is refused loudly
m.reacts(pattern, operation, priority=)  stored as an (on ...) atom
m.agenda("declaration"|"recency"|"specificity"|"priority"|"user",
         function=None)
        which reaction fires first when several match one write. declaration
        is the default and the order they were declared; user names a MeTTa
        function that SCORES a reaction. Every policy ties on declaration
        order and an undeclared priority reads as 0.
m.events("at-most-once"|"at-least-once"|"per-write-exactly",
         "ordered"|"unordered")
        what a foreign context's change events promise. Subscribability is a
        promise about the context, not an inference from its write methods: a
        context that declares nothing refuses subscribe, bridge and reaction
        naming the missing capability. A Python provider says the same thing
        by overriding delivers(); a native space needs no declaration.
```

## Observability

```
m.trace(src, max_events=10_000, *, filter=, timeout=, inferences=)
                                                     -> Trace of TraceEvent
        (depth, kind, term, answer); kinds "call" and "exit", and a reduction
        that fails leaves a call with no exit
        Trace is a list; .stopped names the bound that cut it, one of
        Limit.events, .memory, .inferences, .timeout and .stack, or None when
        the run finished; .truncated is the yes-or-no reading of the same fact
        max_events bounds the RECORDING, timeout and inferences bound the RUN;
        either way the events recorded so far are answered, never discarded
        filter= names the functions to record, before those bounds apply, and
        takes a symbol, a string, a bound handle like m.fn.double, or several
m.debug(src, *, on=, inferences=) -> Debugger of Stop
        breakpoints, suspension, stepping, resume. Iterating runs the program
        to each breakpoint; the loop body is where it is SUSPENDED and leaving
        the body resumes that same execution. on= names the functions that stop
        it, `d.step()` stops at the very next reduction and lasts one advance,
        `d.breakpoints` is a live set, `d.answers` is what the program produced.
        Close it or leave its with-block: a session holds a wrapper on every
        compiled function until it does. No timeout, by design; inferences
        bound the whole session so a resume cannot run forever
m.derivation(target, depth=None, *, timeout=, inferences=) -> list[Derivation]
        proof trees in MeTTa terms: .rules, .facts, .complete, .truncations
m.why(pattern) -> str            one empty match explained in words
rows.why()                       pattern miss, failed join, or rejecting guard
m.lint() -> list[lint.Finding]   the silently-wrong class, from stored structure
        `# metta: ok(<kind>)` on a statement, or on the line above the lint
        CALL to cover a space built entirely from Python, suppresses that one
        kind there; it is kept as a (lint-intent ...) atom, not dropped as a
        comment
metta.lint.lint_file(path, m=None)   the same findings anchored to file:line
m.effect_plan(target) -> EffectPlan(operations, effect), translates and follows
        nested compiled calls without executing the target
m.eval_status(target) / m.run_status(src)  each answer paired with the path that
        produced it: "value" (equation, builtin or special form applied),
        "not-reducible" (no rule applied, the answer is the term itself),
        "empty" (branch pruned, answer None). A pruned branch and an unevaluated
        term are different things the answers alone cannot tell apart.
m.stats()      with-block yielding .inferences (deterministic, gate on this),
               .cputime, .walltime, .gc_count, .gc_freed, .gc_time, .table_bytes
m.profile(src) -> (groups, EngineProfile), per predicate
m.profile_extension(src, extension=, names=)  only YOUR functions
m.prolog()                    the engine's own interactive toplevel
metta.engine().info() -> versions of metta, janus, swi_prolog, python, metta_path
```

Errors: `MettaError` is the base, then `EngineError`, `MettaSyntaxError`,
`CastError`, `CompileError`, `SourceNotFound`,
`MettaResultError`, `AssertionFailure`, `TransportFailure`, and `ResourceLimitError` with
`TimeLimitError` and `InferenceLimitError` under it, plus `Interrupted`.
Remote-backend authors use `metta.errors.is_transport_failure(error)` to
classify an absent connection, timeout, or closed stream before choosing retry
or abandonment; ordinary application errors answer false.
`AssertionFailure` means a `(test ...)` or `(assert ...)` claim was false, not
that the engine broke; `.operation`, `.actual`, and `.expected` are structured
fields for a harness.
`Rows.raise_for_errors()` and `Answers.raise_for_errors()` are the explicit
bridge from `(Error culprit reason)` values to `MettaResultError`: one raises
plainly, several as an `ExceptionGroup`, and a clean collection returns itself
for chaining.
`MettaOperationError(EngineError)` is a builtin refusing a value, with the parts
as data: `.operation` is what the source wrote (`+`, `min-atom`), `.kind` the
formal's functor, `.expected` and `.culprit` the type and offending value.
`metta.errors.NotReducible` is how a deterministic operation says "no answer"
rather than failing: raising it makes the call fail rather than error, which is
a semi-deterministic MeTTa function's way of declining. A generator needs no
signal, since yielding nothing already is one. A SPACE PROVIDER declines
differently, through `should_run` and `refusal` under Foreign spaces below.
`CastError` lives in `metta.casting`, beside the `cast` it names, and the rest
of the family in `metta.errors`.
Type checkers get the closed `SaveFormat` set from `metta.vocabularies`.
Atom kinds are the type: a space name is a `Handle` and a call head is a
`Symbol`.

## Concurrency, transactions, bounds

Engine calls belong to the thread that made the engine. `m.pool(workers)` gives
each worker its OWN attached engine, which is what makes the calls genuinely
concurrent (measured 2026-08-15: 1.94x, 3.90x and 7.26x at 2, 4 and 8 workers).
Its `map(fn, items)` handles unary work and `starmap(fn, argument_rows)` spreads
each row into a multi-argument call; both preserve input order.
`m.parallel(*targets)` evaluates targets at once; `hyperpose` is the same thing
under its MeTTa name, written `!(hyperpose (t1 t2))` in source and reached from
Python as `m.fn.hyperpose`. `metta.aio.AsyncMeTTa` runs engine calls on one worker
thread behind `async`; `metta.parallel.engine_thread()` and `metta.current_space()`
report the crossing.
`metta.channel(max=)` creates a mailbox. `send` may block on capacity,
`recv(deadline=)` waits, and `try_recv()` takes a waiting term or returns
`None` immediately; close it with a context manager.

In MeTTa, `(transaction EXPR)` and `(atomically EXPR)` run one atomic block.
Both answer EVERY answer their body has and commit or roll back the whole
answer set; `transaction` compiles its body into the call site, `atomically`
takes the body as an unreduced atom and evaluates it, so only `atomically`
can run a body the program computed.

`m.transaction(callable)` and the `@m.transactional` decorator run a callable in
one engine transaction. Control signals cannot be eaten by the evaluation they
stop, not even by a program's own `(catch ...)`: a bound, a Ctrl-C and an
`interrupt()` all reach a running goal, the same reasoning that puts
`KeyboardInterrupt` outside `Exception`.

An ordinary transaction cannot undo an external effect after it commits. For
that boundary, declare `space.compensates(operation, recovery)`, then run each
forward term through `with space.saga(receipts) as saga: saga.run(term)`.
Committed `writesState` and `oracleIO` steps leave queryable
`(did operation args result)` receipts. Exceptional exit compensates them in
reverse commit order; a failed compensation keeps its receipt for an explicit
`saga.rollback()` retry.

## Integrating any library

`metta.convert`: `project(obj) -> Projected` whose `.atom` is the constructor
expression, `build(atom)` -> object (returning the atom unchanged when it
cannot), `register_type`, `unregister_type`, `declarations`, `auto_image`.
Dataclasses, enums, pydantic models and annotated classes all cross; enums
project to symbols. A class owner can instead implement `obj.__metta__()` and
`Class.__from_metta__(*fields)` for a two-way conversion without process-wide
registration; pass the class as `build(atom, Class)`. `@space.define` on a
class declares it INTO the space
for the round trip; the separate record decorator is gone. Use the direct
`space.define(Class, accessors=False, methods=False)` form when the type may
cross but its fields or public methods must not become MeTTa callables. The
keyword-only decorator form is not supported.

`metta.integrate`: `module_ops(m, module, names=, effect=, prefix=, rename=,
transport="raw")` registers a whole module's callables, `facts(m, atoms)` bulk-writes,
`wrap_callable(m, name, target, effect=)`,
`wrap_object(m, name, obj, methods, effects=)`, `reflect(m, name, obj)`,
`install_reflection_ops(m)`, `integrate(m, target)`, `Integration`,
`SpaceProvider`, `entry_points(group=)` for unloaded discovery,
`load_entry_point(name, group=)` for explicit provider/library loading, and
`discover(m)` for integrations. An integration may declare `METTA_REQUIRES` as
entry-point names; discovery checks missing names and cycles, then installs in
dependency order. Installation is idempotent for a live space, and dropping a
space releases its installation record. Pair `register_object_type`,
`register_repr`, and `register_reflector` with their exact `unregister_` twins
when an integration or test stops owning those process-wide hooks.
Entry-point groups: `metta.integrations`, `metta.spaces`, `metta.libraries`.

`metta.arrays`: one operation vocabulary over any DLPack library.
`install(m, default=xp)` makes numpy, torch or JAX first-class with the same
words; `namespace_of`, `is_array`, `data_of`, `ARRAY_OPS`, and `EmbeddingStore`
with an exact faiss backend. `EmbeddingStore.keys()` lists stored atom keys and
`EmbeddingStore.vector_for(key)` retrieves a key's original vector.
`EmbeddingStore` registers `(name-knn $q $k)` and
`(name-embed $key)` as OPERATIONS rather than backing a space, so it is called
beside a match rather than being one. `install` returns the names it
registered, 44 of them with numpy as the default, and every one carries a
`(-> ...)` declaration. `broadcast-shape` is a CLP(FD) relation over shape
expressions, so it computes compatible shapes, runs backwards to infer
dimensions, and rejects incompatible shapes before a tensor is materialised.
`Shape(...)` builds the dimension metadata an
`Annotated[DLTensor, Shape(...)]` annotation carries, so `get-type` derives an
elementwise or `matmul` result shape before any array exists.

`metta.tables`: `declare(...)` writes one ctx-scoped bridge declaration into
`&metta` and `TableBridge` derives every provider operation from it, so a
DB-API connection (the `Executes` slice) answers MeTTa matches.
`metta.space(backing={"edge": 2}, journal=path, sync="flush")` is journalled
and crash-recovering. Reopen an old schema once with
`metta.space(backing={"new": 2}, journal=path, rename={"old": "new"})`; every
old head must occur, the journal is atomically rewritten, and the next open
omits `rename`. `metta.space(journal=path)` without a schema refuses.
Likewise,
`metta.space(backing=url)` mounts a remote store; both ride the one
space-factory door rather than their own modules.

## Foreign spaces and the backend seam

A space can be backed by anything, and the seam is universal rather than
per-backend. From Python, implement `Matcher` / `Enumerable` / `Adder` /
`BulkAdder` / `Remover` / `Clearer` / `Planner` / `Transactional` / `CustomMatch`
and call `metta.foreign.register_provider(runtime, name, provider)` with a name
starting with `&`; or subclass `SpaceProvider`. `can_run(capability, **request)`
declares that the operation exists. Override
`should_run(capability, **request)` to accept or decline each concrete request,
and `refusal(capability, **request)` to give a declined request its own reason.
For example, an add policy reads `request["atom"]`; it runs before the write,
including before any bulk write.
Capabilities are declared, not guessed: `match`, `enumerate`, `add`, `add-many`,
`remove`, `clear`, `subscribe`, `plan`, `rules`, and an unsupported operation
refuses loudly rather than degrading. A provider's `match` may yield
`Answer(theta, *, value=, residue=, k=)` instead of a plain atom: `theta` binds
the query's variables, `value` is the answer atom unified with the pattern, and
`k` is the provider's own annotation, which orders answers under `under=ranked`
and becomes the tag under `under=prov`. That is how a store's own score, a
cosine or a confidence, weights a derivation. `rules` is a promise about what a space
HOLDS, not about which methods a provider has, so nothing derives it: without
it a space holds DATA, and an equation written there is refused rather than
stored where it could never fire. Conjunctive queries route per conjunct, so
a foreign space joins with a native one; on such a conjunction `rows.why()`
prints which conjunct went where and whether its class was exact.
`BoundedMatcher.match(pattern, *, limit=)` may stop at the caller's count only
when `MatchClassifier.pushdown(pattern)` says `"exact"`; ignoring the limit is
always sound. `Snapshotter.snapshot() -> tuple[Atom, ...]` makes a provider
reifiable, and `WorldCommitter.commit_world(base, removed, added)` is the
provider-owned atomic boundary for landing that world's checked multiset diff.

From Prolog, `engine/ext_points.pl` declares every seam WITH ITS KIND: an EVENT runs
for effect and every handler runs; an OWNERSHIP seam is claimed by the first
handler that succeeds and declined by failing; a DECLARATION is a fact table read
as data; a SERVICE runs the other way, a predicate the ENGINE defines that an
extension may CALL. Declaring a seam of any kind EXPORTS it from the engine's
module, so published is a fact the module system holds rather than a comment,
and the two surface walks ask the module system for it. The service list is
the whole permitted inward surface
(text: `swrite/2`, `sdisplay/2`, `sdisplay_with_names/3`, `sread/2`,
`metta_symbol_writable/1`, `metta_unwritable_symbol/2`,
`metta_reader_token_class/3`, `metta_reader_token_source/2`;
source: `metta_source/2` for a context's declared source discipline,
`parse_metta_source/2` with `parsed_form_parts/4` to take one form
apart, `active_source_program/1` to detect a definition batch,
`current_working_dir/1` for what a relative path resolves against,
`observe/3` with `observation_begin/0`, `observation_commit/0`,
`observation_discard/0` and `observation_defer/2` for the post-commit event
stream a scope buffers and then publishes or drops, the last of them pairing a
commit goal with its rollback so a launch happens only after the transaction
commits, `metta_ensure_source_observation/0` to bring the source observer into
a process that did not boot with it, and `metta_vocabulary_value/2` so a
library validates an option against the same declared vocabulary the engine
reads;
compiler: `metta_special_form_head/1`, every head the translator gives special
meaning, so a linter, a completion list or the Python MeTTa.builtins() call asks
a question instead of reading the compiler's clause table. That read was what the
Python shim and lib/lib_reflect/lib_reflect.metta both did, and both answered short and
silently the moment the translator became a module of its own, and
`recompile_function_impl/1` rebuilds one function after a dispatch decision,
with `recompile_function_impl_in/2` naming the module to rebuild it in;
errors: `throw_metta_type_error/3`, `rethrow_metta_operation_error/2`,
`refuse_unbound_input/2`;
context: `current_metta_module/1`, `current_metta_space/1`, `space_module/2`,
`metta_module_space/2`, `metta_space_name/1`, and `eval_metta_in_module/3` to
run an expression in the module a space compiles into, plus `metta_source/2`
to read the declared consumption discipline of a context;
platform: `metta_requires/1` for a Prolog source to declare the platform
capability it needs, so a build without it refuses the file at load instead of
half-loading it, and `metta_require_platform/2` for a form to refuse by name,
with what the absence costs, rather than raising an existence error from the
engine's interior;
native storage: `native_storage_module/2`, `native_storage_functor/2`,
`ensure_native_storage_module/2` and `native_atom_clause/3`, the same doors an
ordinary atom write uses, so a library that pre-generates a space's storage
writes the one format the space reads;
effects and caching: `metta_effect_class_canonical/2`, `metta_effect_rank/2`,
`metta_effect_join/3`, `metta_effect_compose/2`, `metta_operation_effect/2`,
`metta_annotated_operation_effect/2` for the class an annotated arrow
published, `metta_operation_plan_effect/2`, `metta_effect_walk/3`,
and `metta_function_cacheable/1`, with
`support_record/2`, `support_invalidate/1` and `support_forget/1` for taking
part in the support graph whose handler seams the engine already declares,
plus `support_memo_sccs/2` and `support_memo_take_change/2` for its call-graph
SCC view and changed-edge signal;
foreign spaces: `metta_shape_route/5` for the routed view of any shape-routed
declaration kind, `foreign_pushdown_class/3` and `foreign_provides/2`, the
routing classifier and capability probe, `metta_require_events/2`, which
refuses a wait on a context that promises no change events, `match_foreign/4`
for the library that checks a provider's contract, and
`run_with_loading_marker/2` for a library that performs an import of its
own), and it
exists so a backend never reaches into
`engine/parser.pl`, the same reason SQLite hands extensions an
`sqlite3_api_routines` table instead of letting them link against internals.

`engine/support_graph.pl` owns derived-state dependencies. `support_replace/2`
publishes a complete support set, `support_record/2` adds an observation,
`support_invalidate/1` and `support_invalidate_many/1` dirty the reachable
forward subgraph once, and `support_stabilize/3` recomputes only on demand and
cuts propagation off when the value is unchanged. Nodes carry their execution
module: `function`, `function_view`, `specialization`, `memo`,
`compiled_function`, `translated_form`, `type_marker`, `dispatch_policy`, and
`derived`, which is the open kind an extension's own artifact takes.
The specializer, memo library, compiler, and language-policy registries use
these same `supports(Support, Derived)` edges.

`extensions/*/extension.pl` is read when argv carries `extensions` -- a control
file of facts declaring what each seat needs, never a script -- and a seat's
`entry(engine, _)` loads only when every need holds, so there is no backend
"mode" to select and the engine names no seat. A boot without the token reads
none of them, which is the pure kernel. `extensions/` holds every seat in one
folder, told apart by the `entry/2` roles they declare rather than by where
they sit: `entry(engine, File)` is a file the engine consults, `entry(host,
File)` one the seat's own runtime consults, and a seat may declare both. A
MORK-backed store is one such seat, supplying `&mork` and `&mork:name`; it is
present only when its shared library was built.

## Apps, from source

`metta.manifest.boot(manifest, m=None, connections=, host=, token=, authorize=,
ssl_context=)` assembles an app from `(boot ...)` forms, each sugar for exactly
one existing call, performed in source order:

```
(boot (load "rules.metta"))                m.load, manifest-relative
(boot (attach &crm "http://crm:8700"))     metta.attach
(boot (bridge &db (edge $a $b) (row ...))) metta.tables declare + bridge
(boot (serve (&self &crm) 8700))           metta.remote.serve
```

The vocabulary is closed and validated whole before anything runs; bridged names
must appear in `connections` and every connection must be claimed. Each
performed form is stored as its own atom, so the running app answers
`(match &self (boot $what) $what)` with its own topology. A manifest that fails
mid-way keeps its performed prefix's writes, closes any servers it started, and
names the failing form.

`python -m metta` has eight subcommands: `run` (files, printing each `!` answer
group), `repl` (paren-balance aware; on a terminal, TAB completes a head or a
`&space` against the live engine and history persists in `~/.metta_history`, or
wherever `METTA_HISTORY` points), `serve`, `boot`, `lint` (nonzero
exit on findings), `doc` (a name's `(@doc ...)`), `llms` (this file), and
`convert` (`program.py [-o out.metta]`, emitting the module's fresh-space
declarations as loadable MeTTa source).

`metta.remote`: `serve(m, host="127.0.0.1", port=0, spaces=, token=,
authorize=, ssl_context=, cursor_idle=300, cursor_limit=256, mutation_ttl=300,
mutation_limit=4096)`, `connect(url, timeout=30, token=,
headers=, ssl_context=)`, `RemoteSpace(transport, space="&self", batch=)` with
its `server_capabilities()`, and the root `metta.attach` to mount one.
`authorize(Request(operation, space, headers)) -> bool` can express read-only,
per-space, and tenant policy. The cursor settings bound how long an abandoned
answer cursor survives and how many the server owns at once; the mutation
settings do the same for the idempotency keys a retryable write negotiates, so
a lost reply raises `OutcomeUnknown` and its `retry()` replays the request
without repeating its effects. Credentials
require https, tokens compare in constant time, and only http/https schemes
are accepted.

`metta.events`: `m.events()` is the engine's stream of `(action, space, atom)`
changes as a first-class object, and `EventStream.fold(step=None, space=,
pattern=, on=, state=, into=, under=)` is the one way to consume it. A step is
`(state, event) -> state`, run inside the write that caused the event;
`Fold.take()` reads the accumulated state and resets it, `Fold.wait(timeout)`
is the same read blocked on a condition variable, and `Fold.cancel()` ends
it. Leave `state` alone and the fold accumulates nothing, which costs it no
serialisation. `EventStream.publish(action, space, atom)` announces a change
this process did not write, which is how a provider with its own channel
delivers. The three shipped models are that fold with three steps: subscribe
delivers, bridge writes, a declared `(on ...)` reaction evaluates.
`into=State(...)` passes the same process-shared gauge cell to every step.
Each individual store read and write is thread-safe, but compound
read-modify-write needs coordination. State has no events, history, or
transactions. With `under=algebra`, omit the step: zero initializes the fold,
merge is its step, ordinary events contribute one, and `(fact tag value)`
events contribute `tag`.
`EventStream.folds(space_name)` lists that space's live folds in registration
order, so an observability owner can inspect what is still subscribed.

`metta.subscribe`: `m.subscribe(pattern, callback, on="add", queue_max=10000)`
is the delivering fold, run INSIDE the write that matched it; without a
callback, events queue until `drain()`, and a full queue raises rather than
discarding the oldest. A callback that raises reaches the writer as
`SubscriberError`, which carries `.subscription` and says the write was
applied, so it is not a failed write and retrying it duplicates.
`bridge(...)` connects two spaces. `Subscription` is a context manager and
also a blocking event stream. A foreign space is watchable only when it
declares what its change events promise; a `RemoteSpace` declares nothing and
refuses `subscribe`, because there is no event channel on the wire.

The wire has both doors the in-process seam has. `RemoteSpace.match` is
eager, one request carrying the whole answer set, and `RemoteSpace.stream`
is the protocol's ask/next/stop lifecycle, a chunk per request, so taking
two answers of a large enumeration costs the serving engine two answers.
`metta.attach(name, metta.remote.RemoteSpace(transport, batch=1))` puts an
attached space's matching on the lazy door; `metta.remote.connect(url)`
builds the transport when it needs a token, headers or a timeout. `metta.remote.Gateway` is the same protocol with
no transport under it, for mounting on another HTTP framework.
`website/live/remote-protocol.md` is the contract every binding inherits and
`metta.testing.GatewayComplianceSuite` certifies it.

`metta.testing` ships what the suite fuzzes itself with: hypothesis strategies
(`atoms`, `expressions`, `patterns`, `names`, `numbers`, `texts`, `symbols`,
`variables`, `grounded`, `ground_atoms`, `numpy_scalars`),
`from_pattern(pattern, max_leaves=8)` for ground instances that share every
repeated named variable and draw anonymous occurrences independently, the compliance suites
(`SpaceComplianceSuite`, `GatewayComplianceSuite`, `check_space_provider`,
`check_twin`, `check_replay`, `check_minted_handles`), and the deterministic
benchmark gates (`benchmark_case`, `benchmark_counter_slope`,
`measure_counters(command, events=("instructions:u",), rounds=3,
controlled=False, timeout=60) -> CounterRuns`, `measure_instructions`,
`BenchmarkBaseline`, `count_atoms`), also exported from `metta.benchmarking`.
`CounterRuns.events` maps each requested perf event to its samples and
`.outputs` retains each measured command's stdout. Use
`BenchmarkBaseline.observe_counter` for deterministic engine counts,
`observe_measurement` for a declared noisy-counter band, and
`observe_configuration` before comparing either. `metta.pytest_plugin` gives the `metta` and
`scratch_space` fixtures; `metta.ipython` gives `%%metta` in a notebook.

These submodules and names, forty-eight of them, load on first access rather than during
`import metta`: `aio`, `algebra`, `amplitude`, `arrays`, `bag`, `bool`, `boot`,
`budget`, `casting`, `channel`, `convert`, `counting`, `derivation`, `events`,
`every`, `foreign`, `integrate`, `lint`, `manifest`, `par_map`, `parallel`,
`paths`, `prob`, `prov`, `race`, `ranked`, `remote`, `rules`, `set`, `spaces`,
`spawn`, `strategies`, `structures`, `subscribe`, `tables`, `testing`,
`tropical`, `view`, `vocabularies`, `wire`, and the
classes `Answer`, `Bindings`, `Defined`, `MeTTa`, `Space`, `SpaceProvider`,
`State`, `equation`.

Importing metta therefore never pulls in the HTTP, subscription and table
machinery boot composes over: `import metta` leaves `metta.atoms` and
`metta.errors` loaded and nothing else. `dir(metta)` still lists every one of
the forty-eight, so completion and reflection see the whole surface.

## The MeTTa language surface

Special forms are compiled by the translator rather than defined by equations,
and most answer false to "is this a function", so "no equations" does not mean
"nothing can prove it". These fifty-nine, plus the internal
`__metta_type_syntax__` the registry section below names:

```
add-atom add-atoms add-reduct add-reducts annotation call case catch
chain collapse cut elapsed eval evalc explain filter-atom foldall
foldl-atom forall get-atoms get-metatype hyperpose if inferences let
let* map-atom match metta-thread new-space noeval nop not-provable once
prog1 progn quote reduce remove-atom return sealed space-atom-count
space-contains subtract-atom super superpose switch take test
test-no-answer timeout top transaction translatePredicate unify
with-pragma! with-seed with_mutex |->
```

Eight more are written in MeTTa, as prelude equations saying what the call
expands to: `and-then`, `or-else`, `trace!`, `unique`, `alpha-unique`,
`union`, `intersection`, `subtraction`.

Each of those is an ordinary equation plus one registration, and KERNEL.md is
the ledger of which head is which, what it answers to in the minimal
instruction set the arbiter presents, and for a derived form still fused into
the compiler, the measurement that keeps it there.

The exact-integer operators are engine heads rather than library equations:
`bit-and`, `bit-or`, `bit-xor`, `bit-not`, `bit-shift-left`,
`bit-shift-right` and `floor-div`, with division by zero answering error
DATA rather than raising.

Seventy-two more engine heads the corpus exercises, by family. Numeric:
`min`, `max`, `pow-math`, `exp-math`, `log-math`, `round-math`, `trunc-math`, `ceil-math`,
`sin-math`, `cos-math`, `tan-math`, `asin-math`, `acos-math`, `atan-math`,
`isnan-math`, `isinf-math`. Atoms: `alpha-unique-atom`, `is-alpha-member`,
`is-member`, `is-var`, `is-expr`, `is-function`, `first-from-pair`,
`second-from-pair`, `reverse`, `last`, `id`, `for-each-in-atom`, `foldl`.
Logic: `xor`, `dif`. Spaces:
`get-atoms`, `space-atom-count`, `is-space`, `new-state`, `has-declared-type`,
`space-admission-verdict`. Types: `match-types`, `match-type-or`, `type-cast`.
Text, IO and files: `repr`, `println!`, `readln!`, `read-form!`, `format-args`,
`sort-strings`, `parse-command`, `sleep`, `exists_file`.
Pre-add hooks: `declare-pre-add!`, `undeclare-pre-add!`. Translator, Prolog and
modules: `add-translator-rule!`, `remove-translator-rule!`,
`import_prolog_function`, `Predicate`, `callPredicate`,
`assertaPredicate`, `git-import!`, `residual-goals`. Minimal MeTTa: `unquote`,
`noreduce-eq`, `collapse-bind`, `superpose-bind`, `return-on-error`,
`if-equal`, `repra`. Assertions beyond the four above: `assertEqualMsg`,
`assertAlphaEqualMsg`, `assertAlphaEqualToResult`, `assertEqualToResultMsg`,
`assertAlphaEqualToResultMsg`. `undocumented` reports what `doc` lacks.

Two names the corpus also exercises are LIBRARY heads and not in that count:
`file-exists`, which is `lib_file`'s spelling beside the engine's own
`exists_file`, and `import_prolog_functions_from_file`, which a library
registers.

`pragma!` accepts `max-time`, `max-inferences`, `verify-specializations`,
`verify-discharges`, `verify-cardinality`, `max-stack-depth`, `stack-limit`,
`plan-cyclic-joins`, `materialize-source-relations`, `type-check`, and
`interpreter`. The bounds, the verification modes and the two planning
switches change live engine mechanisms. `max-stack-depth` is validated exactly as the
arbiter validates it: a value that is not a non-negative integer
answers an `(Error ...)` atom while the program keeps running.
`type-check` and `interpreter` are HE spellings, accepted and not
enforced. A key outside the registry is refused rather than stored
inertly. `max-time` takes a positive number of seconds,
`max-inferences` a positive integer, and `none` explicitly disables
either bound; an invalid value leaves the previous setting unchanged.
`stack-limit` takes positive SWI combined-stack bytes and scopes the setting to
the current thread. `verify-specializations` compares the first use of each
generated higher-order call with its generic form; turning the pragma off, or
leaving a process started with `METTA_VERIFY_SPECIALIZATIONS=1`, reports the
agreed and inference-bounded counts even under `sh run.sh`'s quiet launch.
`METTA_VERIFY_BUDGET` replaces the default 200000-inference comparison bound
with a positive integer. `verify-discharges` similarly audits type checks the
compiler omitted and reports its coverage when disabled, and
`verify-cardinality` checks annotated `det` and `semidet` calls for failure or
leftover choicepoints. `plan-cyclic-joins` plans a full native cyclic
conjunction as a Generic Join instead of the retained nested loop, and
`materialize-source-relations` derives the finite function-free fragment once
at each source boundary and answers admitted ground calls from it.

`if-decons-expr` reads a held expression, unifies its head and tail with the
provided patterns, and evaluates the selected branch. Empty expressions and
incompatible patterns select the fallback.

300 builtins are registered; `m.self.builtins()` lists the live union of registered
functions and translator special forms. That live union in full, measured
2026-09-06 on a boot with this tree's extensions present, which is where the
three `mork-add-atoms`, `mork-flush` and `mm2-exec` heads come from:

`!=` `#*` `#+` `#-` `#//` `#<` `#=` `#=<` `#>` `#>=` `#\=` `#div` `#max`
`#min` `#mod` `%` `*` `+` `-` `/` `<` `<=` `=` `==` `=?` `=alpha` `>` `>=`
`Predicate` `__metta_type_syntax__` `abs-math` `acos-math` `add-atom`
`add-atoms` `add-reduct` `add-reducts` `add-translator-rule!`
`add-typing-rule!` `alpha-unique` `alpha-unique-atom` `and` `and-then`
`annotation` `append` `argv` `asin-math` `assert` `assertAlphaEqual`
`assertAlphaEqualMsg` `assertAlphaEqualToResult`
`assertAlphaEqualToResultMsg` `assertEqual` `assertEqualMsg`
`assertEqualToResult` `assertEqualToResultMsg` `assertIncludes`
`assertaPredicate` `assertzPredicate` `atan-math` `atom-subst`
`atom_chars` `atom_concat` `atomically` `bind!` `bit-and` `bit-not`
`bit-or` `bit-shift-left` `bit-shift-right` `bit-xor` `call`
`callPredicate` `car-atom` `case` `catch` `cdr-atom` `ceil-math` `chain`
`change-state!` `check_prolog_function_names` `collapse` `collapse-bind`
`cons` `cons-atom` `context-space` `copy_term` `cos-math` `current-time`
`cut` `declare-post-add!` `declare-pre-add!` `decons` `decons-atom`
`defined-name` `dif` `documented` `documented-space` `elapsed` `empty`
`error-payload` `eval` `evalc` `except` `exclude-item` `exists_file` `exp`
`exp-math` `explain` `filter-atom` `first` `first-from-pair` `floor-div`
`floor-math` `foldall` `foldl` `foldl-atom` `for-each-in-atom` `forall`
`format-args` `format-time` `function` `get-atoms` `get-doc`
`get-doc-atom` `get-doc-function` `get-doc-params` `get-doc-single-atom`
`get-doc-space` `get-metatype` `get-state` `get-type` `get-type-space`
`git-import!` `has-declared-type` `help!` `hyperpose` `id` `if`
`if-decons-expr` `if-equal` `if-equal2` `if-error` `implies` `import!`
`import_prolog_function` `import_prolog_functions` `include` `index-atom`
`inferences` `interpret` `intersection` `intersection-atom`
`is-alpha-member` `is-expr` `is-function` `is-ground` `is-member`
`is-space` `is-var` `isinf-math` `isnan-math` `lambda_1` `last` `length`
`let` `let*` `library` `list_to_set` `log-math` `map-atom` `maplist`
`match` `match-type-or` `match-types` `max` `max-atom` `member` `metta`
`metta-thread` `min` `min-atom` `mm2-exec` `mork-add-atoms` `mork-flush`
`msort` `new-space` `new-state` `noeval` `nop` `noreduce-eq` `not`
`not-provable` `once` `or` `or-else` `parse` `parse-command` `pow-math`
`pragma!` `pretty-atom` `println!` `prog1` `progn` `py-at` `py-atom`
`py-call` `py-container-kind` `py-dict` `py-dict-pairs` `py-dot` `py-eq`
`py-format` `py-global-read` `py-global-write` `py-in` `py-iter`
`py-iter-once` `py-len` `py-list` `py-operator` `py-range` `py-repr`
`py-round` `py-set` `py-set-pairs` `py-slice` `py-str` `py-str-join`
`py-truthy` `py-tuple` `quote` `random-float` `random-int` `read-form!`
`readln!` `reduce` `register-token!` `register_metta_library_path`
`remove-atom` `remove-translator-rule!` `remove-typing-rule!` `repr`
`repra` `require-extension!` `residual-goals` `retractPredicate` `return`
`return-on-error` `reverse` `round-math` `sealed` `second-from-pair`
`sin-math` `size-atom` `sleep` `sort` `sort-atom` `sort-strings`
`space-admission-verdict` `space-atom-count` `space-contains` `sqrt-math`
`sread` `subtract-atom` `subtraction` `subtraction-atom` `super`
`superpose` `superpose-bind` `switch` `take` `tan-math` `term_hash` `test`
`test-no-answer` `throw` `timeout` `top` `trace!` `transaction`
`translatePredicate` `trunc-math` `type-cast` `type-cast-holds`
`undeclare-post-add!` `undeclare-pre-add!` `undocumented`
`undocumented-space` `unify` `union` `union-atom` `unique` `unique-atom`
`unquote` `unregister-token!` `with-pragma!` `with-seed` `with_mutex`
`xor` `|->`

That roster is the whole registry: the py-* bridge, the atom algebra, the
assert family the example corpus is written in, and the CLP(FD) `#` relations
are all in it. The `#` relations RELATE rather than compute, so giving any two
of three solves the third.

The catalog also says which of those names are the language's own. A
`(visibility <name> PUBLIC|INTERNAL)` row in `&metta` classifies every one, and
seven read `INTERNAL`: `get-doc-atom`, `get-doc-function`, `get-doc-params`,
`get-doc-single-atom`, `interpret`, `match-type-or`, and
`__metta_type_syntax__`, which is the prelude casts' door for type syntax as
data. They are registered and callable, and they are implementation steps
behind public forms rather than spellings to write.

Hand a builtin an unbound variable where it needs a value and it refuses by
name: `!(car-atom $u)` is `car-atom: a value expected in argument 1, found an
unbound variable`. The guarded positions are derived from the type surface
(`guarded_input_position/3`, 82 of them over 62 names, measured 2026-09-05),
so a position declared `Expression`,
`Number`, `BigInt`, `String`, `Symbol` or `Bool` is an input to read. What stays
relational is named in the engine: `index-atom`'s index, the boolean
operations' truth table, `cons`'s open tail, `union-atom` and `member`, which
are `append/3` and `member/2` under MeTTa names, the `#` family throughout,
and every name lent to MeTTa from SWI (`msort`, `append`, `sort`, `maplist`,
`length`), which under that name IS the Prolog predicate.

Ordinary `+`, `-`, `*` and `/` are relational too, which is easy to miss
because they compute forwards. Each solves for ONE unbound slot among
integers, so `(= (double $x) (* 2 $x))` reads backwards for free and
`!(let 10 (double $x) $x)` answers `5`; a pair no integer satisfies FAILS
rather than erroring, so `(let 7 (double $x) $x)` answers nothing. Past one
unknown the rearrangement becomes a constraint: the engine posts it to CLP(FD)
and labels what propagation leaves, so `!(collapse (let 25 (* $x $x) $x))`
answers `(-5 5)`. A domain the constraint leaves unbounded is refused BY NAME,
because deciding a polynomial equation over the integers is undecidable
(Hilbert's tenth problem) and labeling needs a finite domain. Evaluation is
inside-out, so a composed backward query reaches its inner operation with two
unknowns and refuses; the `#` operators POST rather than solve and compose
across several operations, which is what they are for.
`examples/ch05-equations-and-evaluation/05-04-arithmetic-that-runs-backwards/02-relational_arithmetic.metta` runs all of it.

38 libraries load with `!(import! &self (library lib_x))`, each one line of
what it is for: `lib_builtin_types` the declared type surface of the shipped
builtins; `lib_combinatorics` range, take, choose-k, and exact independent
weighted-subset posterior marginals; `lib_conformance` proves
a foreign space provider before its users find out; `lib_constraints` CLP(Q)
over rationals and CLP(B) over booleans; `lib_csv` streams CSV rows through the foreign space seam; `lib_crypto` hashes and secure
randomness, refusing by name where OpenSSL is absent; `lib_datastructures` an
amortised O(1) functional queue and a finger tree; `lib_datetime` now,
format-date, day-of-week; `lib_derived` the derived forms the engine keeps FUSED
into its compiler, written out as equations; `lib_dict` a dictionary that IS a
space; `lib_distribution` pure finite value-distribution map, independent
product, threshold, strict win probability, exact joint conditioning, average
and Bernoulli addition; `lib_doc` keeps the old doc import path working after
its vocabulary moved; `lib_file` text files, directory creation, byte copies, queryable metadata, lexical paths and process streams;
`lib_gitimport` git-import!, Prolog-only, a module fetched from a repository;
`lib_he` Hyperon-Experimental compatibility, nearly all of it core now;
`lib_import` importing that fails LOUDLY where a missing file once answered
nothing; `lib_json` JSON, decoding into that dict-as-space; `lib_measure`
weighted superpositions: normalize, softmax, rank, top-k, sample; `lib_memo` the
resident automatic and explicit memoisation controls; `lib_mm2` notation over
&mork, loaded on demand; `lib_nars` NARS truth functions, inference rules and
bounded derivation; `lib_observe` filtered traces, source coverage and attributed error frames as queryable atoms; `lib_patrick` compose, for, iterate; `lib_pln` PLN truth
formulas, consistency and ranking; `lib_pln2` selected Beta and moment formulas
with explicit evidence scale and support-checked independence; `lib_redis` shared spaces over Redis;
`lib_reflect` the engine's own surface as data you can match; `lib_regex` PCRE2
over strings; `lib_roman` a list and fold basis, head, init, fold-flat,
foldr-flat; `lib_soft` soft structural unification, match quality as a measure;
`lib_spaces` moving atoms between spaces, with find and match-count;
`lib_strategy` a Stratego-style strategy basis whose plans are ordinary atoms;
`lib_string` text, imported when you need it; `lib_tabling` expert-only tabling
control; `lib_thread` parallel data operations, M:N futures and timers;
`lib_torch` PyTorch from plain MeTTa through py-call; `lib_vector` dot, norm,
cosine and random-normal-vector; `lib_zar` Prolog interop, consult and
use_module wrappers. Scored answers and fuzzy or regex matching
are `lib_measure` and `lib_regex` riding the general seam, not Python modules:
there is no `metta.measure` and no `metta.matching`.

## Contracts that cost real debugging

`match` evaluates its space and its body, never its pattern: patterns are
structural, so compute first and match after with `let`.
MeTTa equations ACCUMULATE. Redefining a function ADDS an alternative rather
than replacing the old one, so a second `(= (f x) ...)` gives `f` two answers.
Equations are alternatives, not sequential clauses; a literal-headed default
needs a guard or it fires too.
A typed call rejects a bad argument by answering empty, not by raising: use `cast`.
An unreduced call is a non-empty answer, so test truth with `any(a == True)`,
never "the result was non-empty".
Python `None` from an operation answers nothing.
`(empty)` yields no answer at all, which is how a branch prunes itself.
`collapse` is a special form: a helper "around" `collapse` collapses an
already-chosen answer (an unmasked argument evaluates eagerly) or answers the
held term itself (a masked argument is not re-run), so inline `collapse`.
`forall` stops its generator when the check fails (it compiles to Prolog's
`\+ (Gen, \+ Test)`), so a bounded take over an infinite producer is writable
and terminates where `collapse` cannot run at all.
`(top k ...)` pushes its bound into a foreign provider only when three
declarations hold together: `handles(pattern, "Exact")`, an ordered algebra
through `annotations`, and `emits("best-first")`. Drop one and the bound stays
here. `emits("best-first")` is therefore a CORRECTNESS promise, not a
formatting preference: a provider that declares it and yields out of order
makes `(top k ...)` answer the wrong rows, not a permutation of the right ones.
A Python `[:k]` slice of an ordered-carrier match asks the same promise of the
same provider, so `emits("best-first")` decides both. A slice that does not
meet every condition under `under=` above drains the provider and orders here,
which is correct whatever the provider promises and costs the whole store.
`py-iter` is lazy and yields one answer at a time; a Python generator is not
drained. Each enumeration gets its OWN cursor over a shared cache, so reading
the same iterator twice, or nesting two reads of it, answers the cartesian
product rather than exhausting it once. `py-iter-once` is the other rule, kept
by name: Python's own consumptive iteration, which is what a compiled `for`
statement wants. `py-atom` takes a metatype argument, `Grounded` for the live
reference and `Expression` for a snapshot.
Strings carry hyperon's five escapes (quote, backslash, `\n`, `\t`, `\r`).
Symbols containing whitespace, parentheses or quotes are refused at save and
digest rather than written unreadably.

## Measuring

Wall clock under ~100ms is bimodal on a loaded box and has produced false
results here twice. `m.stats().inferences` is deterministic (five runs of one
workload gave 1,000,601 every time, 0.0000% spread, while wall clock swung
6.86%), so gate on inferences and let wall clock advise. For pure-Python paths
where the engine does nothing, use `perf stat -e instructions:u`. Instruction
counts move with code LAYOUT, so perturb with inert clauses before believing a
regression. Check `/proc/loadavg` before trusting any timing.

## Downstream packages built on this surface

`metta-fabricpc` projects a FabricPC predictive-coding network into a space, so
settling, attention and comparison are MeTTa rather than Python. It is not a
special case in the engine: it is an ordinary user of `op`, `arrays.install`,
`integrate.facts` and the provider seam.

The file library adds `make-dir!`, `delete-dir!`, `copy-file!`, `file-metadata!`,
`temp-dir!`, `path-join`, `path-parent`, `path-name`, and `path-extension`.
`stderr!` writes and flushes standard error; `stdin-to-string!` consumes
standard input through EOF; `(stdin)`, `(stdout)` and `(stderr)` are those same
three streams as handles 0, 1 and 2, so every handle operation reaches them and
`file-close!` refuses all three. `exit!` terminates the entire process with an
integer status from 0 to 255, including an embedding host. `csv-space` returns a
read-only row space whose queries reopen and stream the CSV file;
`csv-snapshot!` reads the file once into an ordinary space of
`(row Number Field...)` atoms, so repeated queries pay one parse and the record
number can skip a header; fields remain strings either way. `trace-source`
returns a space of selected trace events; Python selects the same functions
with `m.trace(source, filter=...)` before recording bounds are applied.

`observe-source` takes an execution space, a source label and source text. Its
report space contains binary `source-coverage` rows, unchanged `source-error`
values and `source-frame` rows with exact or `generated-by` attribution.
Coordinates are one-based Unicode codepoints with exclusive ends. Unavailable
source metadata is explicit; only the observation collects diagnostic state.
