Arithmetic rule library. Each predicate defines a relation between its operands and is reversible — given any two of three operands, the rule solves for the third.

import {rules as mathRules} from 'yopl/rules/math.js';

add(X, Y, Z) is the relation X + Y = Z. With two operands bound, the third is determined:

import {variable} from 'deep6/env.js';
import assemble from 'deep6/traverse/assemble.js';
import solve from 'yopl';
import {rules as mathRules} from 'yopl/rules/math.js';
const Z = variable('Z');
solve(mathRules, 'add', [2, 3, Z], env => console.log(assemble(Z, env))); // 5
const Y = variable('Y');
solve(mathRules, 'add', [2, Y, 5], env => console.log(assemble(Y, env))); // 3
const X = variable('X');
solve(mathRules, 'add', [X, 3, 5], env => console.log(assemble(X, env))); // 2

With all three operands bound, the predicate behaves as a check:

solve(mathRules, 'add', [2, 3, 5], () => console.log('correct')); // fires
solve(mathRules, 'add', [2, 3, 6], () => console.log('correct')); // does not fire

With fewer than two bound, the predicate fails (it cannot solve for two unknowns).

Reversible addition. Includes shortcut clauses for 0 + Y = Y and X + 0 = X so the obvious base cases don't have to go through the general arithmetic path.

Reversible subtraction. Shortcut clauses for X − 0 = X and X − X = 0.

Reversible multiplication. Shortcut clauses for 0 ×ばつ _ = 0, _ ×ばつ 0 = 0, 1 ×ばつ X = X, X ×ばつ 1 = X.

Reversible division. Shortcut clauses for 0 ÷ _ = 0, X ÷ X = 1, X ÷ 1 = X. No guard against division by zero in the general clause — guard yourself with nz from rules-comp when needed.

Reversible negation. Shortcut clause for neg(0, 0).

Evaluates an arithmetic expression on the right and unifies the result with the left. Mirrors ISO Prolog's X is Expr. Throws on insufficiently-instantiated subterms (matching Prolog's instantiation_error); returns false on type mismatches.

import {prolog} from 'yopl/compile/prolog';
import {rules as systemRules} from 'yopl/rules/system.js';
import {rules as mathRules} from 'yopl/rules/math.js';
const rules = {
 ...systemRules,
 ...mathRules,
 ...prolog`
 square(X, Y) :- Y is X * X.
`
};
solve(rules, 'square', [4, v('Y')], env => console.log(assemble(v('Y'), env))); // 16

The op-table is registered with is at priority 700 (xfx), so Y is X * X parses as is(Y, *(X, X)). Surface ops covered:

Functor form is also accepted for any of these: Y is abs(X).

Both sides are evaluated as arithmetic expressions (via the same evalExpr walker is/2 uses), then compared with ===.

prolog`q(X) :- X = 7, X =:= 3 + 4.`; // succeeds

Distinct from unification (= / eq) — X = 3 + 4 would unify X with the compound term 3 + 4, while X =:= 3 + 4 evaluates the RHS arithmetically.

Symmetric to =:=. Both sides evaluated; succeeds when the resulting numbers are not ===.

Arithmetic predicates shine when composed with each other and with the rest of the rule library. A few patterns:

Constrained arithmetic — express a relation as a chain of small reversible steps:

const rules = {
 ...systemRules,
 ...mathRules,
 // average(X, Y, A) — A is the average of X and Y
 average: (X, Y, A, S) => [head(X, Y, A), term('add', X, Y, S), term('div', S, 2, A)]
};

Search via the solver — when you don't know which operand is unknown ahead of time, the same rule serves all directions, so callers don't need separate addForward / addReverseY / addReverseX predicates.

Type discipline — every predicate refuses non-numeric arguments by failing rather than throwing, so feeding in a string or undefined leads to backtracking instead of a runtime error.

• All operands must be plain JavaScript numbers; BigInt is not supported.
• Equality uses ===, so 0 + 0.1 === 0.1 is false on some inputs due to IEEE-754 — be careful with the all-bound check form (and with =:= / =\= on non-integer arithmetic).
• The general clause commits via cut after a successful arithmetic resolution, so the shortcut clauses are unreachable when the general clause already produces a binding.
• is/2 is not reversible — the LHS may be a Variable to bind, but the RHS expression must evaluate to a concrete number. For relational arithmetic that solves any one of three operands from the other two, use add / sub / mul / div / neg.
• < / > / =< / >= (in rules-comp) compare bound numeric values via < / > JS operators directly; they do not evaluate compound expressions on either side. Wrap in is/2 first if you need that: Y is X + 1, Y > 10.