MeTTa Kernel

MeTTa, implemented in Prolog and C. One engine, three surfaces: Python, TypeScript, C.

Python is the complete one and everything below is Python unless it says otherwise.

Install

sudo apt install swi-prolog          # macOS: brew install swi-prolog
                                     # Windows: winget install SWI-Prolog.SWI-Prolog
pip install 'pymetta[engine]'

pymetta installs and imports without SWI-Prolog. The engine extra adds the bridge. Without it the first engine call names the command for your platform.

Requires SWI-Prolog 9.3+ and Python 3.12+.

The representation

Everything is an atom, and there are four kinds. This is how MeTTa writes them:

Tom                  ; a symbol, a name that denotes itself
$x                   ; a variable
42                   ; a grounded value: a number, a string, a host object
(Parent Tom Bob)     ; an expression, atoms in order

Python builds the same four, without parsing anything. A symbol comes from S, a variable from V, and applying a symbol builds an expression:

from metta import S, V

term = S.Parent(S.Tom, S.Bob)
assert str(term) == "(Parent Tom Bob)"
assert str(S.f(V.x) & S.g(V.x)) == "(and (f $x) (g $x))"
assert str(S[">="](V.age, 18)) == "(>= $age 18)"

Strings are for text. A name comes from its factory, a function from its own Python name, a space from its handle.

Spaces and queries

A space holds atoms and equations. Queries join, guard, bound and explain.

from metta import S, V, space

m = space()
m.add(S.Parent(S.Tom, S.Bob), S.Parent(S.Bob, S.Ann))

assert m.match(S.Parent(S.Tom, V.child)).to_dicts() == [{"child": "Bob"}]

# A conjunction is a join.
assert m.match(S.Parent(V.x, V.y), S.Parent(V.y, V.z)).to_dicts() == [
    {"x": "Tom", "y": "Bob", "z": "Ann"}
]

m.add(S.Age(S.Tom, 62), S.Age(S.Bob, 40))
assert m.match(S.Age(V.p, V.n), where=S[">="](V.n, 60)).to_dicts() == [
    {"p": "Tom", "n": 62}
]
assert len(m.match(S.Age(V.p, V.n), limit=1)) == 1

# Facts for one block only.
with m.assuming(S.Parent(S.Ann, S.Zoe)):
    assert m.match(S.Parent(S.Ann, V.c)).to_dicts() == [{"c": "Zoe"}]

# A prepared statement: the shape and its columns build once, then every
# solve() reuses them. given= adds facts for one solve and leaves nothing.
grand = m.prepare(S.Parent(V.x, V.y), S.Parent(V.y, V.z))
assert grand.solve().to_dicts() == [{"x": "Tom", "y": "Bob", "z": "Ann"}]
assert len(grand.solve(given=[S.Parent(S.Ann, S.Zoe)])) == 2

m.eval(term) evaluates a built term and answers every answer. m.run(source) is the door for whole MeTTa programs as text, which is what source files are; prefer building the term when you have one, because a built term is knowledge already and a string has to be parsed before it is. rows.why() explains an empty match. m.derivation(atom) builds the proof tree behind an answer.

Writing MeTTa in Python

@m.define reads the function's source and lowers it into MeTTa equations. Clauses stack the way MeTTa equations do.

from metta import space

m = space()

@m.define
def fib(n=0):
    return 0

@m.define
def fib(n=1):
    return 1

@m.define
def fib(n):
    return fib(n - 1) + fib(n - 2)

assert fib(10) == [55]           # callable from Python, answers a list
assert fib.py(10) == 55          # and the Python twin stays callable

The equations are readable, so you can see exactly what your Python became:

from metta import space

m = space()

@m.define
def fact(n):
    if n == 0:
        return 1
    return n * fact(n - 1)

assert str(fact.head) == "(fact $n)"
assert str(fact.body) == "(if (py-eq $n 0) 1 (* $n (fact (- $n 1))))"
assert fact(5) == [120]

The subset is Python as Python means it: rebinding compiles through static single assignment, while and for become tail-recursive equations in constant stack, a generator compiles to nondeterminism, a lambda to |->, comprehensions to map-atom and filter-atom. Anything outside the subset is refused by name and line, never a silent fallback.

What it does that a library cannot

A function you wrote forwards runs backwards. solve takes the answer and asks for the argument:

from metta import S, V, space

m = space()

@m.define
def double(x):
    return 2 * x

assert double(5) == [10]                  # forwards, and callable from Python
assert m.solve(10, S.double(V.x)).x == 5  # backwards, no second definition
assert m.solve(5, V.p + 2).p == 3         # every operator solves for its slot
assert m.solve(12, V.q * 4).q == 3

Many answers is the normal case rather than an error:

from metta import S, space

m = space()
assert sorted(a.value for a in m.eval(S.superpose((1, 2, 3)))) == [1, 2, 3]

The program is data. An equation is an atom, so adding one at run time changes what the program means, and the equations are queryable like anything else:

from metta import S, V, space

m = space()
m.add(S["="](S.price(V.x), 10))           # an equation is an atom you add
assert m.eval(S.price(S.apple)) == [10]

m.add(S["="](S.price(S.apple), 3))        # a second one, at run time
assert sorted(a.value for a in m.eval(S.price(S.apple))) == [3, 10]

heads = {str(row.head) for row in m.match(S["="](V.head, V.body))}
assert "(price apple)" in heads           # the program can read itself

Everything below builds on those three: the space holds both the facts and the program, evaluation is matching, and nothing is closed to inspection.

Where that leads: a hypothesis nobody wrote down

In 1986 Swanson found that fish oil might treat Raynaud's syndrome. No paper said so. One literature reported that fish oil lowers blood viscosity; another, which did not cite the first, reported that raised blood viscosity aggravates Raynaud's. The conclusion followed from the two together, was stated by neither, and went unnoticed partly because the two literatures did not share vocabulary.

That problem needs both halves of a neurosymbolic system, which is why it is the example. This is extensions/python/examples/reasoning/literature_discovery.py, which the gate runs:

import torch
from metta import TRUE, G, S, V, counting, prov, space
from metta.arrays import EmbeddingStore

m = space()

# Two literatures that never cite each other, and a red herring. Each claim
# carries the paper it came from. Nothing here states a conclusion.
for paper, agent, verb, target in [
    ("p1", "omega-3", "lowers", "blood-viscosity"),
    ("p2", "blood-viscosity", "aggravates", "raynaud"),
    ("p4", "omega-3", "lowers", "platelet-aggregation"),
    ("p5", "platelet-aggregation", "aggravates", "raynaud"),
    ("p3", "aspirin", "lowers", "inflammation"),
]:
    m.add_tagged_fact(S[paper], S.reports(S[agent], S[verb], S[target]))

# Swanson's ABC rule, tagged like any other source.
m.add_tagged_rule(
    S.abc,
    S.suggests(V.agent, V.condition),
    S.reports(V.agent, S.lowers, V.factor),
    S.reports(V.factor, S.aggravates, V.condition),
)

TERMS = {"omega-3": [0.90, 0.10, 0.0], "fish-oil": [0.88, 0.16, 0.0],
         "aspirin": [0.10, 0.90, 0.0], "blood-viscosity": [0.0, 0.10, 0.90]}
store = EmbeddingStore(m, name="terms", mirror=False)
for term, vector in TERMS.items():
    store.add(S[term], torch.tensor(vector))

class Like:
    """Unifies with whatever the embedding puts within `floor`. `match_` is the
    whole interface: no registration, and it composes with `unify`."""
    def __init__(self, key, floor=0.95):
        self.key, self.floor = key, floor
    def match_(self, other):
        for key, score in store.ranked(self.key, len(TERMS)):
            if str(key) == str(other) and float(score) >= self.floor:
                yield other

near_fish_oil = S.unify(G(Like(S.fish_oil)), V.agent, TRUE, S.superpose(()))

# Symbolically there is nothing. No paper contains the phrase.
assert m.match(S.reports(S.fish_oil, S.lowers, V.factor)).to_dicts() == []

# The same corpus, asked with a term the embedding can place. The join is the
# engine's; deciding that fish-oil IS omega-3 is the tensor's.
found = m.match(S.suggests(V.agent, S.raynaud), where=near_fish_oil, under=prov).one()
assert str(found.value) == "(suggests omega-3 raynaud)"

# How much independent support? The same question under a different algebra.
assert m.match(S.suggests(S["omega-3"], S.raynaud), under=counting).one() == 2

# Which papers? A provenance polynomial: `times` is joint use, `plus` is an
# alternative derivation. Read it as "the rule with p1 and p2, or with p4 and p5".
assert str(found.annotation) == (
    "(plus (times (times abc p1) p2) (times (times abc p4) p5))"
)
assert all(name in found.why().render() for name in ("abc", "p1", "p2", "p4", "p5"))

The answer is not a plausible sentence. It is a derivation naming abc, p1 and p2, which a reader can go and check.

And the evidence is algebra rather than bookkeeping. The same question under counting says how many independent literature paths support the hypothesis; under prov it says which papers, as a polynomial. Neither costs a line of tracking code, because tags compose through the join the way the join composes [Green, Karvounarakis and Tannen, Provenance semirings, PODS 2007].

Neither half of this works alone. A language model does not do reliable multi-hop chaining and cannot show its working; a symbolic prover cannot cross a vocabulary gap where two names share nothing but their meaning. The embedding decides what unifies, the engine decides what follows, and the answer carries its own citations. The neural gate, the tagged rule and the semiring are all in that one query, and none of them is a plugin: they are the same seam.

Three axes

A crossing between Python and the engine makes three independent choices.

axis	poles	how you say it
where the body lives	CALLED, or LOWERED	@m.pure and friends, or @m.define
what the body may observe	pure, reads, writes, io	the decorator's name
what a value crosses as	transparent, or opaque	transport="encoded" or "raw"

The first two are different questions and are easy to run together. Where the body lives decides whether Python runs at all. What it may observe decides whether the engine may cache it.

from metta import space

m = space()

# CALLED: the body stays Python and the engine calls it. The decorator says
# what it may observe, which is the only thing the engine cannot see for
# itself.
@m.pure
def called(x: int) -> int:
    return x + 1

# LOWERED: the body becomes MeTTa equations. No Python at run time, and no
# effect to declare, because now the engine can read the code.
@m.define
def lowered(x):
    return x + 1

assert list(m.fn.called(41)) == [42]
assert lowered(41) == [42]
assert lowered.effect == "pureStructural"      # derived, not declared

Four decorators, ordered, each admitting everything below it. Only pure may be cached, memoised or tabled.

decorator	what it may observe or change
@m.pure	nothing but its arguments; same answer forever
@m.reads	state that can change, without changing it
@m.writes	engine or host state
@m.io	an external oracle: clock, randomness, network, file

There is no nondet: a generator IS nondeterministic, so the registration works that out from the function and lifts the class itself.

import metta
from metta import S, V, space

m = space()

@m.pure
def upto(n: int):
    yield from range(1, n + 1)

assert sorted(a.value for a in m.fn.upto(3)) == [1, 2, 3]

lifted = metta.reflection.match(S.effect(S.upto, V.e))
assert [str(row.e) for row in lifted] == ["nondeterministicReadOnly"]

transport="raw" composes with any of them and is 1.6x cheaper, at the cost of the symbol/string distinction: symbols reach a raw operation as plain strings.

Measured, per crossing: letting the engine call out costs 19,557 retired instructions against 96,771 for the host driving in, so a loop over many items belongs in MeTTa. A transparent value costs four inferences per element and an opaque one costs 12.31 whatever the size, so at a thousand elements the gap is 419x and still growing. EXTENDING.md prices all three and extensions/python/benchmarks/axes.py reproduces the numbers.

Async

import asyncio
import metta
from metta import S, V

async def main():
    async with await metta.aio.connect() as m:
        await m.add(S.edge(S.a, S.b))
        rows = await m.match(S.edge(V.x, V.y))
        return rows.to_dicts()

assert asyncio.run(main()) == [{"x": "a", "y": "b"}]

The engine runs on its own thread and every door is awaitable.

Parallel evaluation

import metta
from metta import G, S, space

m = space()

# Branches on real threads. The answers come back as a list, so `collapse` has
# nothing to do here and the order is not fixed.
assert sorted(a.value for a in m.parallel(G(1) + 1, G(2) + 2)) == [2, 4]

@m.define
def double(x):
    return 2 * x

# A parallel MAP is a different promise: it keeps the input's order, where
# the fan-out above answers in completion order.
assert str(m.eval(metta.par_map(S.double, (1, 2, 3)))[0]) == "(2 4 6)"

lib_thread also carries futures (spawn answers a space), await, channels with backpressure, pools, Linda-style waits and locks.

Across processes

serve publishes this engine's spaces over HTTP; attach registers another engine's space here as an ordinary space, so a query crosses the network the way it crosses into a database.

from metta import S, space, remote

m = space()
m.add(S.edge(S.a, S.b))

with remote.serve(m, spaces=[m.name]) as server:
    server.url          # another process attaches to this

import metta
from metta import S, V, space, remote

server_space = space()
server_space.add(S.edge(S.a, S.b), S.edge(S.b, S.c))

# In ONE process the transport is a Gateway: janus holds the GIL across a
# Prolog call, so an HTTP attach here is refused with this remedy named.
metta.attach("&warehouse", remote.RemoteSpace(
    remote.Gateway(server_space, [server_space.name]), str(server_space.name)))
edges = metta.space("&warehouse").match(S.edge(V.x, V.y))
assert edges.to_dicts() == [{"x": "a", "y": "b"}, {"x": "b", "y": "c"}]

Bearer tokens, TLS and a per-request authorization hook are arguments to serve. Answers stream a chunk at a time, so taking two answers costs two answers' work whatever the space holds.

Standing queries

A subscription is a query that stays, delivered inside the write that matched it.

from metta import S, V, space

m = space()
seen = []
m.subscribe(S.Alarm(V.what), seen.append)
m.add(S.Alarm(S.fire))

assert [str(event.atom) for event in seen] == ["(Alarm fire)"]
assert str(seen[0].bindings["what"]) == "fire"

Spaces backed by anything

A space provider puts atoms wherever they already live: a SQL table, a dataframe, a service, another engine. The engine keeps unification, so a provider may over-approximate and stay correct.

import metta
from metta import S, V
from metta.foreign import SpaceProvider

class Rows(SpaceProvider):
    def __init__(self, rows):
        self.rows = rows

    def atoms(self):
        return [S.user(i, name) for i, name in self.rows]

metta.attach("&catalogue", Rows([(1, "Ada"), (2, "Bob")]))
rows = metta.space("&catalogue").match(S.user(V.id, V.name))
assert rows.to_dicts() == [{"id": 1, "name": "Ada"}, {"id": 2, "name": "Bob"}]

Bound positions reach the provider as its WHERE clause, and a provider that declares its filtering exact is handed the caller's bound to push down. Worked instances ship for SQLite, DuckDB, Redis, C and TypeScript.

Integrating a library

MeTTa's semantics already subsume what libraries are made of, so integration is a mapping rather than machinery.

the library has	it becomes
functions, methods	grounded functions; a call is a reduction
objects with state	grounded atoms with identity
tables, frames, indexes	spaces; a query is a match
dispatch (routes, handlers)	equations over one head
generators, search, retrieval	nondeterminism; each yield one answer
schemas, records, enums	constructor expressions and (: ...) declarations

import math
from metta import space
from metta.integrate import module_ops

m = space()
module_ops(m, math, ["sqrt", "gcd"], effect="pureStructural")
assert list(m.fn.sqrt(16.0)) == [4.0]

A package advertises itself through the metta.integrations entry-point group, and m.discover() finds it.

Command line

python -m metta run program.metta        # run files, print each ! answer group
python -m metta repl                     # interactive loop
python -m metta serve kb.metta --port 8700
python -m metta lint program.metta       # nonzero exit on findings
python -m metta doc car-atom

TypeScript

extensions/node/ runs the engine inside Node over WebAssembly, so no SWI-Prolog on the machine and no socket. The same three axes, spelled the way TypeScript spells things. This is extensions/node/examples/readme-snippet.ts, which the gate runs:

import { metta, S, type Term, V } from "metta-node";

const m = await metta();
m.add(S.parent(S.tom, S.bob), S.parent(S.bob, S.ann));

// Rows are keyed by the pattern's own variable names.
for await (const { child } of m.match(S.parent(S.tom, V.child))) {
  console.log(String(child));                   // bob
}

// LOWERED: an ordinary function becomes one equation the engine holds, so the
// call crosses into no host at all.
const twice = m.define(function twice(n: number): number { return n * 2; });
console.log(String(await twice(21).one()));     // 42

// A generator body is traced into clauses; `yield*` asks, `yield` emits.
const grandparent = m.define(function* grandparent(x: Term) {
  const { y } = yield* m.match(S.parent(x, V.y));
  const { z } = yield* m.match(S.parent(y, V.z));
  return z;
});
console.log(String(await grandparent(S.tom).one()));   // ann

// CALLED: a function the engine calls back into mid-reduction, awaited when it
// answers with a promise. Its effect is read off the function, not declared.
m.op(async function fetchJson(url: string) { return (await fetch(url)).json(); });
console.log(m.effectOf("fetch-json"));          // oracleIO

m.dispose();

C

extensions/cmetta/ embeds the engine through SWI's foreign interface. It has the same two definition doors, and C reaches the lowered one through the preprocessor: Python lowers by reading a function's __code__ and Node by reading its toString(), while # is C's own access to its source. From extensions/cmetta/examples/lower.c:

#define MT_SHORTHAND
#include <cmetta.h>

/* CALLED: the engine crosses into C, so the effect class must be declared. */
mt_def(m, (mt_op){ .name = "triple", .arity = 1,
                   .effect = MT_PURE, .fn = op_triple });

/* LOWERED: C tokens the compiler already saw, installed as equations. No
   quoting, no escaped newlines, and unbalanced parentheses are a COMPILE
   error rather than a runtime one. */
mt_lower(m, (twice $x), (* 2 $x));
mt_lower(m, (fib $n), (if (< $n 2) $n
                          (+ (fib (- $n 1)) (fib (- $n 2)))));

/* One body, two languages: the operators are parameters, so the same source
   expands to C in one mode and to MeTTa tokens in the other. */
#define POLY(ADD, MUL, x)  ADD(MUL(3, x), 1)
static int64_t poly(int64_t x) { return POLY(C_ADD, C_MUL, x); }
mt_lower(m, (poly $x), POLY(M_ADD, M_MUL, $x));

examples/ beside it carries hello, ops, lower and stream, each built and run by the gate.

Backends

sh build.sh builds the MORK backend, which gives MORK-backed atom spaces over trueagi-io/MORK and Adam-Vandervorst/PathMap. FAISS atom-vector spaces come from a MeTTa library the engine fetches on request:

!(git-import! "https://github.com/patham9/faiss_ffi" "build.sh")

Conformance

The semantics are PeTTa's. Where anything disagrees with it, this engine follows PeTTa, and tests/conformance/petta/ is how that is checked rather than asserted: it holds upstream's example corpus beside the exact bytes upstream printed for each file, captured from a named commit and vendored here, so a neighbouring checkout cannot move the lane. check.sh replays every entry and gates per FILE.

Two entries carry a recorded ruling rather than agreement, each with the difference it is allowed to have written down beside it, so neither can drift further without failing. Both are cases where this engine answers and upstream does not: bind! binding a value upstream has no clause for, and a parametric apply upstream's own specializer builds and then fails to apply.

What the examples show

extensions/python/examples/language-feature-examples/ is 219 runnable programs, each the idiomatic Python for one MeTTa example, and the gate runs every one. They are the depth this page only samples:

chapter	what it demonstrates
arithmetic that runs backwards	+ - * / as relations, then CLP(FD) constraints when rearrangement runs out, then a named refusal
changing the equations	a program that specialises and removes its own definitions at run time
many answers	superposition, collapse, bounded and committed searches
types	parametric, recursive and dependent types
a reasoner you can serve	constructive negation, a dependently-typed backward chainer, PLN deduction, weak unification, the Scallop programs
performance	a million atoms across five index shapes, memoisation and tabling, four million-step kernels
transactions and worlds	a counter five threads share, state cells, arbitrary MeTTa at the write door, admission pools
events and standing queries	subscriptions delivered inside the write that matched them
spaces backed by anything	a space in C, a builtin in C, SQL and DuckDB providers
extending the engine	translator rules, MeTTa written in MeTTa, Prolog underneath

Documentation

• EXTENDING.md, nine extension points ordered by measured cost.
• KERNEL.md, which forms the translator gives meaning to, and why.
• CODEC.md, the wire every atom crosses on.
• DEVELOPING.md, gates and measurement rules.
• CONTRIBUTING.md, what a contribution has to be.
• SECURITY.md, how to report a vulnerability privately.
• CHANGELOG.md, what changed.

extensions/python/examples/ holds runnable, self-verifying integrations that the test suite runs, so they cannot drift.

Licence

MIT. See LICENSE for the notices it carries, and CITATION.cff for citation metadata.