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).

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.
• 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.