MeTTa TS 1.0.7

Author: MesTTo

RELEASE_NOTES.md

@@ -1,34 +1,56 @@
-# MeTTa TS 1.0.0
+# MeTTa TS 1.0.7
 
-The first public release of MeTTa TS, a pure-TypeScript implementation of [MeTTa](https://metta-lang.dev) (Meta Type Talk), the OpenCog Hyperon language. It runs anywhere TypeScript runs: the browser, Node, Deno, Bun, and edge or serverless functions. No native addons, no WASM, no Rust.
+A pure-TypeScript implementation of [MeTTa](https://metta-lang.dev) (Meta Type Talk), the OpenCog Hyperon language. It runs anywhere TypeScript runs: the browser, Node, Deno, Bun, and edge or serverless functions. No native addons, no WASM, no Rust.
 
 ## Tested on Linux
 
 This release is tested on Linux (Node 20, the CI matrix): lint, format, typecheck, the full test suite, and the build all run there. Because the engine is pure TypeScript with no native addon and no WASM, it is meant to be cross-platform and should run unchanged on any JavaScript runtime. Other operating systems are not yet part of the tested matrix.
 
-## Major performance gains
+## What's new: the proof-size-bounded backward chainer, from losing to winning
 
-MeTTa TS is fast, from pure TypeScript. A reproducible black-box benchmark runs the PeTTa example corpus through both engines as subprocesses and checks each program's embedded `(test ...)` assertions. On the Hyperon-faithful shared subset, MeTTa TS passes 95 programs and is faster than PeTTa on 92 of them, median 2.18x and up to 6.2x (`fib`), even though PeTTa runs on SWI-Prolog's GMP-backed integers.
+Nil Geisweiller's [`bfc-xp`](https://github.com/ngeiswei/chaining) benchmark searches a Łukasiewicz propositional calculus for a proof of a target formula under a fixed size bound, backtracking through modus ponens and three axiom schemes. It is a real nondeterministic search, not a lookup, and it was the one place PeTTa still beat MeTTa TS. This release closes that gap by compiling the search itself, not just the terms it searches over.
+
+A match-free nondeterministic group (no clause queries a space, only recursion, `if`-guards, and integer arithmetic) now compiles in two steps. First, every clause becomes a skeleton: a tree of constant subtrees, clause-variable slots, and structured nodes, computed once per group rather than copied per call. Second, the skeleton compiles to specialized JavaScript, one function per functor, generated once via `new Function` and shared by every run: head unification becomes read/write-mode code that fails at the first mismatch with no allocation, and body arguments and templates become direct constructor expressions with integer arithmetic unboxed. Underneath both steps, search variables are cell variables: a binding lives in a mutable slot on the variable itself, so dereferencing is pointer-chasing and undoing a failed branch is popping a trail array, no string-keyed map anywhere. Every bind carries an occurs check, so a would-be cyclic binding fails the search instead of looping, exactly the discipline `hasLoop` enforces on the interpreter's own immutable bindings and SWI-Prolog enforces under `occurs_check(true)`. A model in [`spec/loop_reject.als`](spec/loop_reject.als) proves the two mechanisms reject exactly the same binding sets, in every possible bind order. An environment that forbids dynamic code (a CSP without `unsafe-eval`) falls back to running the skeleton directly, still far faster than the plain interpreter; a group that does query a space (like `nilbc`, MeTTa TS's dependently-typed backward chainer) is unaffected and keeps running on the original interpreter-backed search.
+
+The result, measured with `hyperfine` (mean ± σ, wall clock, engine startup included, each row from one `hyperfine` invocation so the two columns are directly comparable):
+
+| benchmark                                           |           MeTTa TS |              PeTTa |
+| --------------------------------------------------- | -----------------: | -----------------: |
+| `jarr` (size 13)                                    |  124.8 ms ± 4.2 ms | 182.9 ms ± 10.6 ms |
+| `pm2.27` (size 13)                                  |  121.6 ms ± 1.3 ms |  183.0 ms ± 8.3 ms |
+| `imim1` (size 15)                                   |  152.2 ms ± 4.1 ms |  212.3 ms ± 3.9 ms |
+| `jarr` (size 17), PeTTa with `occurs_check(true)`   | 455.5 ms ± 69.5 ms | 476.0 ms ± 11.8 ms |
+| `loowoz` (size 19), PeTTa with `occurs_check(true)` |  2.092 s ± 0.063 s |  2.501 s ± 0.003 s |
+
+The last two rows run PeTTa with `occurs_check(true)`, which its SWI-Prolog translation does not set (the flag defaults to off). At these two deeper searches that gap is not just a speed difference: PeTTa as shipped finds 94 answers for `jarr` at size 17 where only 91 exist, and 44 for `loowoz` at size 19 where only 3 exist, the surplus being cyclic-binding artifacts that `occurs_check` is exactly the guard against (the same requirement `bfc-xp`'s own SWI harness documents). Run correctly, PeTTa is a little slower here too. Every MeTTa TS answer above is checked byte-identical to the plain interpreter by a differential oracle that runs the search both ways (`packages/core/src/moded-tabling.test.ts`), and the compiled and interpreted engines' outputs are additionally diffed directly at sizes 17 and 19.
+
+## Corpus benchmark
+
+The existing PeTTa-corpus benchmark (107 shared programs, 97 both engines pass, median 2.01x, geomean 2.06x) is unaffected by this release: none of those programs exercise a match-free nondeterministic group, so they run the same code as before. See [`packages/node/bench/RESULTS-corpus.md`](packages/node/bench/RESULTS-corpus.md) for the full per-program table.
+
+## Major performance gains (since 1.0.0)
 
 The speed comes from general engine work:
 
 - an O(1)-stack reduce-loop trampoline and worklist, so deep recursion does not grow the JS stack;
 - deferred rule-RHS freshening with a head-shape candidate pre-filter;
 - Prolog-style clause indexing by head functor and by every ground-leaf argument, so a keyed query over a 1,000,000-atom space resolves in about 0.2 to 1.4 ms;
 - ground-atom type memoisation and an exact-match ground-fact index;
-- automatic tabling of pure functions, including ones defined at runtime;
+- automatic tabling of pure functions, including ones defined at runtime, and moded (variant) tabling for non-ground pure calls;
 - a native-code compiler for the pure deterministic int/bool/tuple subset, with tail-recursion compiled to loops and higher-order specialisation;
-- worker-thread parallelism: `(once (hyperpose ...))` races branches across CPU cores on Node, and a `SharedArrayBuffer` flat matcher scans large knowledge bases in parallel.
+- worker-thread parallelism: `(once (hyperpose ...))` races branches across CPU cores on Node, and a `SharedArrayBuffer` flat matcher scans large knowledge bases in parallel;
+- the compiled clause-skeleton and JavaScript-codegen search described above, for match-free nondeterministic groups.
 
-Every optimisation is verified byte-identical against the 270-assertion Hyperon oracle. See [`packages/node/bench/RESULTS-corpus.md`](packages/node/bench/RESULTS-corpus.md) for the full per-program table.
+Every optimisation is verified byte-identical against the 270-assertion Hyperon oracle.
 
 ## What is in this release
 
-- `@metta-ts/core` is the interpreter, parser, type system, pattern matching, and standard library, as a single ESM bundle (~23 KB gzipped). It passes all 270 assertions of Hyperon's oracle corpus (the full dependent-type tier, spaces and mutable state, nondeterminism, grounded operations, and documentation), cross-checked against [LeaTTa](https://github.com/MesTTo/LeaTTa), the machine-checked (Lean 4) MeTTa semantics pinned to the same commit.
+- `@metta-ts/core` is the interpreter, parser, type system, pattern matching, and standard library, as a single ESM bundle. It passes all 270 assertions of Hyperon's oracle corpus (the full dependent-type tier, spaces and mutable state, nondeterminism, grounded operations, and documentation), cross-checked against [LeaTTa](https://github.com/MesTTo/LeaTTa), the machine-checked (Lean 4) MeTTa semantics pinned to the same commit.
 - `@metta-ts/hyperon` is a TypeScript class API modeled on Python's `hyperon`, with a JavaScript interop layer (`js-atom`, `js-dot`, `js-list`, `js-dict`) that calls into the host runtime directly.
 - `@metta-ts/edsl` is a typed eDSL with term builders, special-form combinators, and a tagged-template surface.
 - `@metta-ts/node` has the `metta-ts` CLI, file `import!`, and the worker-thread parallel matcher.
 - `@metta-ts/browser` is a browser entry with an in-memory virtual file system for `import!`.
+- `@metta-ts/grapher` renders a MeTTa reduction as a node graph or a nested-block view, as static SVGs or an animated GIF, with a data-driven stylesheet for node size and colour.
 - `@metta-ts/das-client` and `@metta-ts/das-gateway` are an optional client to SingularityNET's Distributed AtomSpace, run end to end against a live cluster, with atom handles matching the AtomDB byte for byte.
 
 ## Install
@@ -42,4 +64,5 @@ npm install -g @metta-ts/node     # the metta-ts CLI
 
 - Semantics: [hyperon-experimental](https://github.com/trueagi-io/hyperon-experimental), pinned to commit `3f76dc4`.
 - Verified spec and differential oracle: [LeaTTa](https://github.com/MesTTo/LeaTTa) (Lean 4).
+- Formal models: [Alloy](https://alloytools.org) specs in [`spec/`](spec/) for the matcher's deep loop rejection and the compiled search's occurs check.
 - License: [MIT](LICENSE).

packages/browser/package.json

@@ -1,6 +1,6 @@
 {
   "name": "@metta-ts/browser",
-  "version": "1.0.6",
+  "version": "1.0.7",
   "license": "MIT",
   "type": "module",
   "main": "./dist/index.js",

packages/core/package.json

@@ -1,6 +1,6 @@
 {
   "name": "@metta-ts/core",
-  "version": "1.0.6",
+  "version": "1.0.7",
   "license": "MIT",
   "type": "module",
   "main": "./dist/index.js",

packages/core/src/alpha.ts

@@ -4,9 +4,19 @@
 
 // Alpha-equivalence (LeaTTa `Core/Alpha.lean`): two atoms are alpha-equal when canonicalising
 // their variables to first-occurrence order makes them structurally equal.
-import { type Atom, variable, expr, atomEq } from "./atom";
+import { type Atom, type ExprAtom, variable, expr, atomEq } from "./atom";
 
-function canonicalize(a: Atom, map: Map<string, string>): Atom {
+/** Rename every variable in `a` to `%N`, N assigned in first-occurrence order per `map` (shared across a
+ *  whole `canonicalize` call so repeat occurrences of the same variable get the same placeholder). Exported
+ *  for tabling's moded (non-ground) cache keys: two calls that are the same up to which concrete variable
+ *  names they happen to use canonicalize to the same atom, and `map`'s insertion order (`[...map.keys()]`)
+ *  recovers which original name became which `%N`, needed to freshen a cached answer back to a new call's
+ *  actual names. `memo` is a per-call cache (fresh map, so per-call use only): within one canonicalize
+ *  call, a variable already in `map` always renames the same way, so a shared expr node (instantiate
+ *  shares unchanged subterms by reference) needs walking only once, not once per incoming path — the same
+ *  DAG-vs-tree reasoning as instantiate/occursThrough/atomEq elsewhere in this package. */
+export function canonicalize(a: Atom, map: Map<string, string>, memo?: Map<Atom, Atom>): Atom {
+  if (a.ground) return a;
   switch (a.kind) {
     case "var": {
       let c = map.get(a.name);
@@ -16,13 +26,34 @@ function canonicalize(a: Atom, map: Map<string, string>): Atom {
       }
       return variable(c);
     }
-    case "expr":
-      return expr(a.items.map((x) => canonicalize(x, map)));
+    case "expr": {
+      if (memo === undefined) return canonicalizeExpr(a, map, new Map());
+      return canonicalizeExpr(a, map, memo);
+    }
     default:
       return a;
   }
 }
 
+function canonicalizeExpr(a: ExprAtom, map: Map<string, string>, memo: Map<Atom, Atom>): Atom {
+  const cached = memo.get(a);
+  if (cached !== undefined) return cached;
+  const its = a.items;
+  let items: Atom[] | null = null;
+  for (let i = 0; i < its.length; i++) {
+    const it = its[i]!;
+    const r = canonicalize(it, map, memo);
+    if (items !== null) items.push(r);
+    else if (r !== it) {
+      items = its.slice(0, i);
+      items.push(r);
+    }
+  }
+  const result = items === null ? a : expr(items);
+  memo.set(a, result);
+  return result;
+}
+
 export function alphaEq(a: Atom, b: Atom): boolean {
   return atomEq(canonicalize(a, new Map()), canonicalize(b, new Map()));
 }

packages/core/src/atom.ts

@@ -405,23 +405,48 @@ export function atomVars(a: Atom, out: string[] = []): string[] {
   return out;
 }
 
+const noVars: readonly string[] = [];
+
+/** Which distinct variable names occur in an expression, first-seen order, cached by object identity.
+ *  Sound forever (not just for one call), unlike a per-call memo: an atom is immutable, so "which vars
+ *  occur in me" cannot change after construction — the same reasoning that already justifies the
+ *  precomputed `ground` flag. `instantiate` shares unchanged subterms by reference, so a rewrite-heavy
+ *  search walks a DAG, not a tree: the same expression object recurs as a stack/continuation is threaded
+ *  through many interpreter steps (scopeVars/chainLiveVars below). Without this cache, `collectVars` re-walks
+ *  a shared node once per occurrence instead of once ever, the same exponential-paths-vs-linear-nodes
+ *  blowup as the (now-fixed) unmemoized `occursThrough` and `instantiate` — this was the dominant cost left
+ *  after fixing those two (77% of CPU on a backward-chaining search that should run in well under a second). */
+const exprVarsCache = new WeakMap<ExprAtom, readonly string[]>();
+
+function atomVarsOf(a: Atom): readonly string[] {
+  if (a.ground) return noVars;
+  if (a.kind === "var") return [a.name];
+  if (a.kind !== "expr") return noVars;
+  const cached = exprVarsCache.get(a);
+  if (cached !== undefined) return cached;
+  const out: string[] = [];
+  const seen = new Set<string>();
+  for (const it of a.items) {
+    for (const v of atomVarsOf(it)) {
+      if (!seen.has(v)) {
+        seen.add(v);
+        out.push(v);
+      }
+    }
+  }
+  exprVarsCache.set(a, out);
+  return out;
+}
+
 /** Collect an atom's variable names into `out`, deduping via the shared `seen` set (O(1) membership instead
  *  of a linear `out.includes`). Hot accumulation loops (scopeVars/frameVars) reuse one `seen` across many
  *  atoms so the whole walk stays linear; `atomVars` is the one-shot wrapper that seeds `seen` from `out`. */
 export function collectVars(a: Atom, out: string[], seen: Set<string>): void {
-  if (a.ground) return; // closed term: no variables (ground short-circuit)
-  switch (a.kind) {
-    case "var":
-      if (!seen.has(a.name)) {
-        seen.add(a.name);
-        out.push(a.name);
-      }
-      break;
-    case "expr":
-      for (const it of a.items) collectVars(it, out, seen);
-      break;
-    default:
-      break;
+  for (const v of atomVarsOf(a)) {
+    if (!seen.has(v)) {
+      seen.add(v);
+      out.push(v);
+    }
   }
 }
 
@@ -443,6 +468,17 @@ export const isVar = (a: Atom): a is VarAtom => a.kind === "var";
 export const isSym = (a: Atom): a is SymAtom => a.kind === "sym";
 export const isGnd = (a: Atom): a is GndAtom => a.kind === "gnd";
 
+// Cached by the pair's object identity, permanently: `atomEq` is a pure structural comparison of two
+// immutable atoms with no external context, so the answer for a given (a, b) pair can never change once
+// computed — the same reasoning that already justifies the precomputed `ground` flag and `exprVarsCache`
+// above. Without this, comparing two large expressions built independently (so `a === b` never
+// short-circuits the top-level call, e.g. `addVarBinding`'s `atomEq(prev, v)` on a rebind) walks the full
+// pair every single time they're compared, anywhere in the program. A rewrite-heavy search that keeps
+// re-deriving structurally-similar terms (backward chaining over recursive rules) calls `atomEq` on
+// overlapping large pairs repeatedly; this was 92-95% of CPU on such a search after the DAG-sharing fixes
+// above stopped it from also exhausting memory.
+const eqCache = new WeakMap<Atom, WeakMap<Atom, boolean>>();
+
 /** Structural equality. Interned symbols short-circuit to reference identity. */
 export function atomEq(a: Atom, b: Atom): boolean {
   if (a === b) return true;
@@ -457,12 +493,21 @@ export function atomEq(a: Atom, b: Atom): boolean {
     case "expr": {
       const bi = (b as ExprAtom).items;
       if (a.items.length !== bi.length) return false;
+      const inner = eqCache.get(a);
+      const cached = inner?.get(b);
+      if (cached !== undefined) return cached;
+      let result = true;
       for (let i = 0; i < a.items.length; i++) {
         const ai = a.items[i] as Atom;
         const bii = bi[i] as Atom;
-        if (!atomEq(ai, bii)) return false;
+        if (!atomEq(ai, bii)) {
+          result = false;
+          break;
+        }
       }
-      return true;
+      if (inner === undefined) eqCache.set(a, new WeakMap([[b, result]]));
+      else inner.set(b, result);
+      return result;
     }
   }
 }