MeTTa TS 1.1.7

Author: MesTTo

RELEASE_NOTES.md

@@ -1,3 +1,42 @@
+# MeTTa TS 1.1.7
+
+MeTTa TS 1.1.7 fixes a unification soundness bug in grounded substitution.
+
+## Substitution resolves to a fixpoint
+
+A specialized forward chainer emulating backward chaining on propositional
+calculus returned an extra spurious proof (GitHub issue #2). Applying a binding
+set as a substitution was single-pass: a variable whose value mentioned another
+still-bound variable left that inner variable unresolved, and a later scope
+restriction then dropped its binding and lost the derived constraint, so a freed
+type unified with the wrong axiom. `instantiate` now resolves to a fixpoint. The
+query returns the single proof that Hyperon 0.2.10 and PeTTa (SWI-Prolog) both
+produce.
+
+The resolution stays bounded and scalable: a variable chain is followed
+iteratively, so a four-million-link chain resolves rather than overflowing the
+stack; a name-to-value index makes a long chain linear rather than quadratic;
+binding cycles truncate deterministically; and a shared value DAG is resolved
+once by object identity, so a term with an exponential number of paths resolves
+in constant time with bounded memory.
+
+## Verification
+
+- Full test suite passes, with new fixpoint and backward-chaining regression
+  tests, each shown to fail on the single-pass version.
+- Core/ST conformance is unchanged from 1.1.6: 431 passed, 77 established
+  failures, 60 manifest expected failures, byte-identical failure set.
+- Performance is neutral against 1.1.6 on the nondeterminism benchmark suite.
+
+## Packages
+
+All public packages use version `1.1.7`:
+
+```bash
+npm install @metta-ts/core@1.1.7
+npm install -g @metta-ts/node@1.1.7
+```
+
 # MeTTa TS 1.1.6
 
 MeTTa TS 1.1.6 reduces the cold and loaded cost of compiled nondeterministic

packages/browser/package.json

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

packages/core/package.json

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

packages/core/src/backward-chaining-unification.test.ts

@@ -0,0 +1,50 @@
+// SPDX-FileCopyrightText: 2026 MesTTo
+//
+// SPDX-License-Identifier: MIT
+
+// Regression: a specialized forward chainer emulating backward chaining on propositional calculus
+// (GitHub issue #2). A triangular binding built during proof search (a rule variable constrained to a
+// ground type through a nonlinear unification) must be resolved to a fixpoint when the rule RHS is
+// instantiated. A one-pass substitution left the constraint unresolved in the accumulated type, which
+// scope restriction then dropped, admitting a spurious extra solution. The correct answer is a single
+// proof, confirmed against Hyperon 0.2.10 and PeTTa (SWI-Prolog), which both yield exactly one solution.
+import { describe, it, expect } from "vitest";
+import { runProgram } from "./runner";
+import { format } from "./parser";
+
+const solutions = (src: string): string[] => {
+  const r = runProgram(src);
+  return r[r.length - 1]!.results.map(format);
+};
+
+// The propositional-calculus chainer from the issue. `ax₁`/`ax₂` are the K/S axioms, `mpⁱ` inverse
+// modus ponens; `obfc` searches for a proof term of a target type up to a depth.
+const OFC = `
+(= (ofc $depth $hypcnt $tgt (: $x $a))
+   (if (< 0 $hypcnt)
+       (if (and (< 0 $depth) (<= $hypcnt $depth))
+           (ofc-rec (- $depth 1) (- $hypcnt 1) $tgt (: $x $a))
+           (empty))
+       (let (: $x $a) $tgt (: $x $a))))
+(= (ofc-rec $dd $hd $tgt (: $f (-> (→ $𝜑 (→ $𝜓 $𝜑)) $b)))
+   (ofc $dd $hd $tgt (: ($f ax₁) $b)))
+(= (ofc-rec $dd $hd $tgt (: $f (-> (→ (→ $𝜑 (→ $𝜓 $𝜒)) (→ (→ $𝜑 $𝜓) (→ $𝜑 $𝜒))) $b)))
+   (ofc $dd $hd $tgt (: ($f ax₂) $b)))
+(= (ofc-rec $dd $hd $tgt (: $f (-> $b $c)))
+   (ofc $dd (+ $hd 2) $tgt (: (mpⁱ $f) (-> (→ $a $b) (-> $a $c)))))
+(= (obfc $depth (: $x $a))
+   (ofc $depth 1 (: $x $a) (: I (-> $a $a))))
+`;
+
+describe("backward-chaining unification soundness", () => {
+  it("proves 𝜑 → 𝜑 with exactly one proof term (issue #2)", () => {
+    const out = solutions(`${OFC}\n!(obfc 5 (: $x (→ 𝜑 𝜑)))`);
+    expect(out).toEqual(["(: ((((mpⁱ (mpⁱ I)) ax₂) ax₁) ax₁) (→ 𝜑 𝜑))"]);
+  });
+
+  it("finds no proof below the required depth", () => {
+    for (const d of [1, 2, 3, 4]) {
+      expect(solutions(`${OFC}\n!(obfc ${d} (: $x (→ 𝜑 𝜑)))`)).toEqual([]);
+    }
+  });
+});

packages/core/src/bindings.ts

@@ -162,6 +162,11 @@ export function makeValRel(x: string, a: Atom): ValRel {
   return valRel(x, a);
 }
 
+/** Build a single variable-equality relation. */
+export function makeEqRel(x: string, y: string): EqRel {
+  return eqRel(x, y);
+}
+
 /** Build a binding set from an explicit list of relations (newest-first). */
 export function fromRelations(rels: readonly BindingRel[]): Bindings {
   return rels;

packages/core/src/instantiate.test.ts

@@ -0,0 +1,81 @@
+// SPDX-FileCopyrightText: 2026 MesTTo
+//
+// SPDX-License-Identifier: MIT
+
+// `instantiate` applies a binding set as a substitution resolved to a fixpoint. A binding set from
+// unification is triangular (a value can mention another still-bound variable), so a one-pass
+// application would leave inner variables unresolved and later lose their constraints. These tests pin
+// the transitive resolution and its termination on binding cycles.
+import { describe, it, expect } from "vitest";
+import { instantiate } from "./instantiate";
+import { fromRelations, makeValRel, makeEqRel } from "./bindings";
+import { sym, variable, expr, type Atom } from "./atom";
+import { format } from "./parser";
+
+const f = (a: Atom): string => format(a);
+
+describe("instantiate transitive (fixpoint) resolution", () => {
+  it("resolves a variable whose value mentions another bound variable", () => {
+    const b = fromRelations([
+      makeValRel("x", expr([sym("f"), variable("y")])),
+      makeValRel("y", sym("a")),
+    ]);
+    // One-pass would leave `$y`: `(out (f $y))`. The fixpoint bakes in `$y := a`.
+    expect(f(instantiate(b, expr([sym("out"), variable("x")])))).toBe("(out (f a))");
+  });
+
+  it("resolves regardless of relation order", () => {
+    const b = fromRelations([
+      makeValRel("y", sym("a")),
+      makeValRel("x", expr([sym("f"), variable("y")])),
+    ]);
+    expect(f(instantiate(b, expr([sym("out"), variable("x")])))).toBe("(out (f a))");
+  });
+
+  it("resolves through several levels of nested structure", () => {
+    const b = fromRelations([
+      makeValRel(
+        "a",
+        expr([sym("Arr"), variable("p"), expr([sym("Arr"), variable("q"), variable("p")])]),
+      ),
+      makeValRel("p", sym("P")),
+      makeValRel("q", sym("Q")),
+    ]);
+    expect(f(instantiate(b, expr([sym("t"), variable("a")])))).toBe("(t (Arr P (Arr Q P)))");
+  });
+
+  it("bakes the deep resolution into a rule RHS via the scoping suffix", () => {
+    // The reduce path instantiates a rule RHS with a per-application suffix. A value pulled from the
+    // binding set already carries final (suffixed) names and must still be resolved transitively.
+    const b = fromRelations([
+      makeValRel("b#1", expr([sym("Pair"), variable("a#0")])),
+      makeValRel("a#0", expr([sym("S"), variable("p#1")])),
+      makeValRel("p#1", sym("Z")),
+    ]);
+    expect(f(instantiate(b, expr([sym("res"), variable("b")]), "#1"))).toBe("(res (Pair (S Z)))");
+  });
+
+  it("terminates on a direct variable-alias cycle, truncating at the variable", () => {
+    const b = fromRelations([makeValRel("x", variable("y")), makeValRel("y", variable("x"))]);
+    expect(f(instantiate(b, expr([sym("out"), variable("x")])))).toBe("(out $x)");
+  });
+
+  it("terminates on a structural binding cycle", () => {
+    const b = fromRelations([
+      makeValRel("x", expr([sym("f"), variable("y")])),
+      makeValRel("y", expr([sym("g"), variable("x")])),
+    ]);
+    expect(f(instantiate(b, expr([sym("out"), variable("x")])))).toBe("(out (f (g $x)))");
+  });
+
+  it("leaves a genuinely unbound variable free", () => {
+    const b = fromRelations([makeValRel("x", expr([sym("S"), variable("y")]))]);
+    expect(f(instantiate(b, expr([sym("out"), variable("x")])))).toBe("(out (S $y))");
+  });
+
+  it("ignores eq aliases, resolving only value bindings", () => {
+    const b = fromRelations([makeEqRel("x", "y"), makeValRel("y", sym("a"))]);
+    // `instantiate` applies value bindings only (eq aliases are dropped), so `$x` stays free.
+    expect(f(instantiate(b, expr([sym("out"), variable("x")])))).toBe("(out $x)");
+  });
+});