MeTTa TS 1.1.6

Author: MesTTo

README.md

@@ -303,21 +303,23 @@ A representative slice (wall-clock, subprocess including startup; `speedup` = Pe
 
 The full per-program table is in [`RESULTS-corpus.md`](packages/node/bench/RESULTS-corpus.md).
 
-The checked nondeterminism benchmark also includes four adversarial programs reported by Patrick Hammer and the `jarr` and `loowoz` bounded backward-chaining queries reported by Nil Geisweiller. Both BFC files extract the exact `obc` definitions and target queries from [`trueagi-io/chaining@bc9beb2`](https://github.com/trueagi-io/chaining/blob/bc9beb2672953e07971b3abecc1fe67651ecddc4/experimental/backward-via-forward/bfc-xp.metta). These are 15-run subprocess medians measured on 2026-07-15 on an AMD Ryzen 9 9950X, including startup, with Node 22.22.1 and the clean PeTTa `6b7f52f` checkout on SWI-Prolog 9.3.33:
+The checked nondeterminism benchmark also includes four adversarial programs reported by Patrick Hammer and the `jarr` and `loowoz` bounded backward-chaining queries reported by Nil Geisweiller. Both BFC files extract the exact `obc` definitions and target queries from [`trueagi-io/chaining@bc9beb2`](https://github.com/trueagi-io/chaining/blob/bc9beb2672953e07971b3abecc1fe67651ecddc4/experimental/backward-via-forward/bfc-xp.metta). These are 15-run subprocess medians measured on 2026-07-15 on an AMD Ryzen 9 9950X, including startup, with Node 22.22.1 and the clean PeTTa `6f5639a` checkout on SWI-Prolog 9.2.9:
 
 | Program                          | PeTTa ms | PeTTa MiB | MeTTa TS ms | MeTTa TS MiB |   Speedup |
 | -------------------------------- | -------: | --------: | ----------: | -----------: | --------: |
-| BFC `jarr`                       |    134.6 |      16.4 |       125.6 |         86.5 | **1.07x** |
-| BFC `loowoz`                     |   2441.2 |      16.4 |       872.8 |        108.9 | **2.80x** |
-| filtered `matespacefast` matches |   6157.9 |    3334.5 |      3568.3 |        424.0 | **1.73x** |
-| 22^4 `superpose` cross product   |    357.5 |      87.9 |       147.7 |        148.8 | **2.42x** |
-| nondeterministic tabled `fib(7)` |    127.8 |      16.4 |        94.1 |         79.8 | **1.36x** |
-| duplicate-heavy `TupleConcat`    |    126.0 |      16.3 |        96.3 |         79.4 | **1.31x** |
+| BFC `jarr`                       |    136.5 |      16.4 |       113.6 |         91.4 | **1.20x** |
+| BFC `loowoz`                     |   2466.3 |      16.4 |       743.6 |        100.0 | **3.32x** |
+| filtered `matespacefast` matches |   6140.3 |    3331.0 |      3380.2 |        424.6 | **1.82x** |
+| 22^4 `superpose` cross product   |    354.5 |      87.9 |       150.3 |        146.8 | **2.36x** |
+| nondeterministic tabled `fib(7)` |    128.6 |      16.3 |        98.5 |         79.9 | **1.31x** |
+| duplicate-heavy `TupleConcat`    |    127.6 |      16.3 |        98.0 |         78.6 | **1.30x** |
 
 The MiB columns are the highest sampled process-tree RSS across the 15 runs on Linux.
 
 The benchmark validates both `jarr` proofs and all three `loowoz` proofs in exact order, all 234,256 cross-product results, all 196 distinct Fibonacci answers, the exact `TupleConcat` result, and the embedded matespace assertion. MeTTa TS uses the same default evaluator as the CLI. No benchmark, PeTTa, curry, or tabling mode is selected.
 
+Against the untouched 1.1.5 build on the same machine, alternating exact-output comparisons improved `jarr` by 1.14x cold and 1.12x loaded. `loowoz` improved by 1.18x cold and 1.31x loaded. The `jarr` cold path also improved on Node 20, 22, and 24. Ineligible programs skip the new route and retain the old generated module shape.
+
 Automatic tabling does not memoize every recursive function. Admission requires transitive purity and a recursive strongly connected component that branches back into itself at least twice. Linear recursion such as factorial stays on the compiled path. Custom host operations and space, state, file, random, time, import, and output operations are excluded.
 
 Completed and active tables share hard entry, answer, retained-cell, per-entry, and interner limits. Completed entries are LRU-evictable. Active entries cannot be evicted while their producer runs, so a call that cannot fit returns `TableResourceLimit` instead of continuing toward process exhaustion. See [Scaling to millions of atoms](website/advanced/scaling.md#automatic-tabling) for the current limits and completion policy.
@@ -336,7 +338,7 @@ That speed comes from general engine work:
 - a slot-based evaluator for closed pure `let` and `superpose` products that preserves result order and multiplicity without allocating general binding frames;
 - a native-code compiler for the pure deterministic int/bool/tuple subset, with tail-recursion compiled to loops and PeTTa-style **higher-order specialisation** so a function passed as an argument (e.g. `iterate`'s `$step`) is bound and compiled rather than interpreted;
 - a compiler for **nondeterministic `let*`-chain functions** (the backward-chainer class): a multi-equation function whose clause bodies chain space matches and recursive calls compiles to a clause-major depth-first search, the same fragment PeTTa hands to Prolog's clause alternatives;
-- dependency-sensitive dispatch for static pure search: answer-dependent recursive joins use the compiler first, while independent overlapping calls retain moded tabling; common-result-layout compilation passes only changing result fields through recursive continuations and rebuilds the full MeTTa atom once at the evaluator boundary;
+- dependency-sensitive dispatch for static pure search: answer-dependent recursive joins use the compiler first, while independent overlapping calls retain moded tabling; common-result-layout compilation omits input-projected fields from recursive continuations and constructs a proven independent output only after child searches succeed;
 - WAM-style fresh write-mode binding: when static dataflow proves that every slot in a constructed pattern subtree is introduced at that site, generated code binds the new structure directly; input and previously introduced slots retain the full occurs-checking unifier;
 - a compiler for **add-atom saturation loops**: the add-if-absent idiom becomes one exact-membership probe plus append, and a single-branch `case` over a space match becomes a snapshot-and-thread loop with Empty-pruned branches.
 

RELEASE_NOTES.md

@@ -1,3 +1,99 @@
+# MeTTa TS 1.1.6
+
+MeTTa TS 1.1.6 reduces the cold and loaded cost of compiled nondeterministic
+proof search. It also adds Hyperon-style structural inequality to the core and
+TypeScript EDSL.
+
+## Deferred proof output
+
+The nondeterministic compiler can now prove that one result field is an
+unbound output projection which does not affect clause choice, matching,
+guards, or recursive call arguments. For those relations, generated search
+code carries only the control fields. It constructs the deferred field after
+all child searches succeed. Result fields already projected from call inputs
+are recovered at the consumer instead of being passed through every recursive
+continuation.
+
+The analysis uses result and input projections from the existing compiler. It
+does not recognize `obc`, theorem names, or benchmark source. Runtime admission
+requires the projected input to be unbound and unaliased, and requires a
+natural-number descent field for the existing bounded-recursion guard. If any
+proof fails, the ordinary compiled search runs with unchanged ordered-bag
+semantics. Groups with no deferred plan retain the 1.1.5 generated module shape
+and skip the deferred attempt entirely.
+
+Large generated clause matchers are emitted as separate JavaScript functions,
+while small recurrence clauses stay inline. This reduces V8 compilation work
+for large rule groups without changing source-order dispatch.
+
+An alternating same-host A/B against the untouched 1.1.5 build compared exact
+ordered output on every run. On Node 22.22.1, `jarr` improved from 127.9 ms to
+111.9 ms over 51 cold pairs and from 3.32 ms to 2.97 ms over 401 loaded pairs.
+`loowoz` improved from 892.0 ms to 754.8 ms cold and from 922.3 ms to 705.3 ms
+loaded.
+
+The cold `jarr` comparison was also repeated on three Node majors:
+
+| Runtime      |    1.1.5 |    1.1.6 | Speedup |
+| ------------ | -------: | -------: | ------: |
+| Node 20.20.2 |  86.0 ms |  69.4 ms |   1.24x |
+| Node 22.22.1 | 127.9 ms | 111.9 ms |   1.14x |
+| Node 24.18.0 |  56.6 ms |  54.3 ms |   1.04x |
+
+The clean 15-run subprocess comparison on an AMD Ryzen 9 9950X used PeTTa
+`6f5639a` on SWI-Prolog 9.2.9. Times include process startup and use the normal
+MeTTa TS evaluator:
+
+| Program      |     PeTTa | MeTTa TS | Speedup |
+| ------------ | --------: | -------: | ------: |
+| BFC `jarr`   |  136.5 ms | 113.6 ms |   1.20x |
+| BFC `loowoz` | 2466.3 ms | 743.6 ms |   3.32x |
+
+Maximum sampled MeTTa TS process-tree RSS was 91.4 MiB for `jarr` and 100.0
+MiB for `loowoz`. The benchmark validates both `jarr` proofs and all three
+`loowoz` proofs in exact order.
+
+## Inequality
+
+MeTTa TS now provides `!=` as a core grounded operation. It is the Boolean
+complement of Hyperon's structural `==` for non-error operands, including
+integer/float promotion and NaN behavior. Both operators use the same
+`(-> $t $t Bool)` type, arity checks, argument evaluation, and error
+propagation. The TypeScript EDSL exports the matching `neq(a, b)` builder.
+
+## Verification
+
+The release candidate was checked on Linux with Node 22 and pnpm 11.
+
+- All 116 executed test files pass: 1,164 tests passed and 38 optional live
+  integration tests were skipped.
+- The checked 270-assertion oracle passes all 23 corpus files.
+- Core/ST conformance is byte-identical to 1.1.5 at 431 passed, 77 established
+  failures, 60 manifest expected failures, and zero skips.
+- The standard benchmark, all six nondeterminism cases, concurrency checks,
+  and all 33 scale cases pass.
+- The documentation site builds, and all ten package tarballs install together
+  in a clean npm project. The packed evaluator, EDSL, `jarr`, GIF renderer, and
+  TypeScript declarations pass their smoke checks.
+- Browser and grapher base entries import from a clean install without Sharp or
+  `gifenc`. The production dependency audit reports no known vulnerabilities.
+
+## Packages
+
+All public packages use version `1.1.6`:
+
+```bash
+npm install @metta-ts/core@1.1.6
+npm install -g @metta-ts/node@1.1.6
+```
+
+Optional host packages use the same version:
+
+```bash
+npm install @metta-ts/py@1.1.6 pythonia
+npm install @metta-ts/prolog@1.1.6
+```
+
 # MeTTa TS 1.1.5
 
 MeTTa TS 1.1.5 adds a programmatic reduction-GIF API for plain Node.js. It

packages/browser/package.json

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

packages/core/package.json

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

packages/core/src/builtins.ts

@@ -73,6 +73,18 @@ export type ReduceResult =
 export type GroundFn = (args: readonly Atom[]) => ReduceResult;
 export type GroundingTable = Map<string, GroundFn>;
 
+const groundedOperationTypes = new WeakMap<GroundFn, Atom>();
+
+function withGroundedOperationType(op: GroundFn, type: Atom): GroundFn {
+  groundedOperationTypes.set(op, type);
+  return op;
+}
+
+/** Return the type carried by a grounded operation, if it has one. */
+export function groundedOperationType(op: GroundFn): Atom | undefined {
+  return groundedOperationTypes.get(op);
+}
+
 // Monotonic counter for `sealed`'s fresh variable names (process-wide uniqueness, like Hyperon's make_unique).
 let sealCounter = 0;
 const ok = (...results: Atom[]): ReduceResult => ({ tag: "ok", results });
@@ -340,15 +352,23 @@ function boolBin(f: (x: boolean, y: boolean) => boolean): GroundFn {
   };
 }
 
-// `==`: error operands pass through; otherwise structural equality as a Bool.
-const eqAtom: GroundFn = (args) => {
-  if (args.length !== 2) return ierr("expected exactly two arguments");
-  const a = args[0]!;
-  const b = args[1]!;
-  if (isErrorAtom(a)) return ok(a);
-  if (isErrorAtom(b)) return ok(b);
-  return ok(gbool(atomEq(a, b)));
-};
+// Equality operators pass through error operands and compare every other atom structurally.
+function equalityCmp(expectEqual: boolean): GroundFn {
+  return (args) => {
+    if (args.length !== 2) return ierr("expected exactly two arguments");
+    const a = args[0]!;
+    const b = args[1]!;
+    if (isErrorAtom(a)) return ok(a);
+    if (isErrorAtom(b)) return ok(b);
+    return ok(gbool(atomEq(a, b) === expectEqual));
+  };
+}
+const eqAtom = equalityCmp(true);
+// Hyperon carries operation types on grounded values instead of inserting declarations into &self.
+const neqAtom = withGroundedOperationType(
+  equalityCmp(false),
+  expr([sym("->"), variable("t"), variable("t"), sym("Bool")]),
+);
 
 // --- list surgery ---
 const consAtom: GroundFn = (args) => {
@@ -474,6 +494,7 @@ const coreEntries: Array<[string, GroundFn]> = [
   [">", numCmp((c) => c > 0)],
   [">=", numCmp((c) => c >= 0)],
   ["==", eqAtom],
+  ["!=", neqAtom],
   ["and", boolBin((a, b) => a && b)],
   ["or", boolBin((a, b) => a || b)],
   ["cons-atom", consAtom],

packages/core/src/choice-plan.ts

@@ -163,18 +163,19 @@ function compileEquality(
   args: readonly Atom[],
   scope: ReadonlyMap<string, number>,
   state: CompileState,
+  expectEqual: boolean,
 ): ChoiceNode | undefined {
   const nodes = compileBinaryChoices(args, scope, state);
   if (nodes === undefined) return undefined;
   const [left, right] = nodes;
   if (left.one !== undefined && right.one !== undefined) {
-    const bool: BoolNode = (frame) => atomEq(left.one!(frame), right.one!(frame));
+    const bool: BoolNode = (frame) => atomEq(left.one!(frame), right.one!(frame)) === expectEqual;
     return oneChoice((frame) => gbool(bool(frame)), undefined, bool);
   }
   return {
     run(frame, emit) {
       left.run(frame, (leftAtom) =>
-        right.run(frame, (rightAtom) => emit(gbool(atomEq(leftAtom, rightAtom)))),
+        right.run(frame, (rightAtom) => emit(gbool(atomEq(leftAtom, rightAtom) === expectEqual))),
       );
     },
   };
@@ -329,7 +330,9 @@ function compileChoice(
     case ">=":
       return compileComparison(args, scope, state, (comparison) => comparison >= 0);
     case "==":
-      return compileEquality(args, scope, state);
+      return compileEquality(args, scope, state, true);
+    case "!=":
+      return compileEquality(args, scope, state, false);
     case "if":
       return compileIf(args, scope, state);
     case "superpose":

packages/core/src/compile-impure.test.ts

@@ -38,6 +38,18 @@ describe("compiled impure body (matespace VM de-risk)", () => {
     expect(run(g, true)).toEqual(run(g, false));
   });
 
+  it("compiles != in an impure recursive guard", () => {
+    const src = `
+      (= (g-neq $n)
+         (if (!= $n 0)
+             (let $x (add-atom &self (item-neq $n)) (g-neq (- $n 1)))
+             done))
+      !(g-neq 4)
+      !(collapse (match &self (item-neq $k) $k))`;
+    expect(compiledEnvWith(src).compiled!.get("g-neq")?.kind).toBe("imperative");
+    expect(run(src, true)).toEqual(run(src, false));
+  });
+
   // A longer completing run: every looped application must advance the fresh-variable counter in lockstep
   // with the interpreter, and the 50 add-atoms must accumulate in the same order, across 50 iterations.
   const g50 = `

packages/core/src/compile.test.ts

@@ -93,11 +93,32 @@ describe("deterministic-core compiler", () => {
     expect(runFunctional(c, "odd", [10])).toBe(false);
   });
 
+  it("compiles != as the complement of integer equality", () => {
+    const c = compileEnv(envWith("(= (different $a $b) (!= $a $b))"));
+    expect(runFunctional(c, "different", [4, 4])).toBe(false);
+    expect(runFunctional(c, "different", [4, 5])).toBe(true);
+  });
+
   it("a match-using function is outside the pure int/bool core but compiles as nondet", () => {
     const c = compileEnv(envWith("(= (q $x) (match &self ($x) $x))"));
     expect(c.get("q")?.kind).toBe("nondet");
   });
 
+  it("compiles != guards in nondeterministic recursion", () => {
+    const src = `
+      (= (walk 0) left)
+      (= (walk 0) right)
+      (= (walk $n)
+         (if (!= $n 0)
+             (let $child (walk (- $n 1)) (S $child))
+             (empty)))`;
+    const c = compileEnv(envWith(src));
+    expect(c.get("walk")?.kind).toBe("nondet");
+    expect(compareCompiledAndInterpreted(`${src}\n!(walk 2)`)).toEqual([
+      ["(S (S left))", "(S (S right))"],
+    ]);
+  });
+
   it("declines a nondeterministic group with a wrong-arity internal call", () => {
     const c = compileEnv(
       envWith(`

packages/core/src/compile.ts

@@ -189,6 +189,7 @@ const KNOWN_OPS = new Set([
   ">",
   ">=",
   "==",
+  "!=",
   "if",
   "unify",
   "let",
@@ -288,7 +289,7 @@ function compileBody(a: Atom, scope: Scope, holders: FunctionalFns): Compiled |
       type: "int",
     };
   }
-  if (op === "<" || op === "<=" || op === ">" || op === ">=" || op === "==") {
+  if (op === "<" || op === "<=" || op === ">" || op === ">=" || op === "==" || op === "!=") {
     const xy = binIntArgs(args, scope, holders);
     if (!xy) return undefined;
     const [xn, yn] = xy;
@@ -301,7 +302,9 @@ function compileBody(a: Atom, scope: Scope, holders: FunctionalFns): Compiled |
             ? (c: number) => c > 0
             : op === ">="
               ? (c: number) => c >= 0
-              : (c: number) => c === 0;
+              : op === "=="
+                ? (c: number) => c === 0
+                : (c: number) => c !== 0;
     return { node: (fr) => test(cmpIntVal(xn(fr), yn(fr))), type: "bool" };
   }
   if (op === "if") {
@@ -554,7 +557,8 @@ function inferType(
       : undefined;
   const op = (hd as { name: string }).name;
   if (op === "+" || op === "-" || op === "*" || op === "/" || op === "%") return "int";
-  if (op === "<" || op === "<=" || op === ">" || op === ">=" || op === "==") return "bool";
+  if (op === "<" || op === "<=" || op === ">" || op === ">=" || op === "==" || op === "!=")
+    return "bool";
   if (op === "if" && a.items.length === 4) {
     const tt = inferType(a.items[2]!, varTypes, holders);
     const te = inferType(a.items[3]!, varTypes, holders);
@@ -1062,7 +1066,7 @@ function nondetIsData(env: MinEnv, a: Atom): boolean {
 // comparison operators an `(if ...)` guard may test. Both evaluate at runtime through the interpreter's
 // own grounded ops (callGrounded), so the compiled result is byte-identical to the interpreted one.
 const ARITH_FOLD = new Set(["+", "-", "*"]);
-const NONDET_COMPARE = new Set(["<", "<=", ">", ">=", "=="]);
+const NONDET_COMPARE = new Set(["<", "<=", ">", ">=", "==", "!="]);
 
 /** A call argument or result template the search can build and resolve: interpreter data, but also
  *  binary arithmetic (`(- $s 2)`, `(+ (+ $fs $xs) 1)`) anywhere inside, folded to an int once its
@@ -1810,6 +1814,8 @@ function compileNondetGroup(
             return c >= 0;
           case "==":
             return c === 0;
+          case "!=":
+            return c !== 0;
           default:
             throw BAIL;
         }
@@ -1983,7 +1989,11 @@ function compileNondetGroup(
         }
       };
 
-      return attempt("direct") ?? attempt("frontier");
+      return (
+        (jg.tryDeferred === undefined ? undefined : attempt("deferred")) ??
+        attempt("direct") ??
+        attempt("frontier")
+      );
     };
 
   const holders = new Map<string, NondetHolder>();
@@ -2038,7 +2048,7 @@ type ImpNode = (
 ) => ImpEval;
 type ImperativeFns = Map<string, ImperativeHolder>;
 
-const IMP_GROUNDED = new Set(["==", "<", ">", "<=", ">=", "+", "-", "*", "%"]);
+const IMP_GROUNDED = new Set(["==", "!=", "<", ">", "<=", ">=", "+", "-", "*", "%"]);
 // Heads that are never inert data: the compiled language's own constructs, plus every evaluation
 // op (IMPURE_OPS: match, collapse, once, superpose, metta, ...). Without the latter, a body like
 // `(match &self p t)` whose head happens to have no rule and no grounding would freeze as a tuple,