rules math - uhop/yopl GitHub Wiki

rules-math

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

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

Reversibility, in one example

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

Predicates

add(X, Y, Z) โ€” X + Y = Z

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.

sub(X, Y, Z) โ€” X โˆ’ Y = Z

Reversible subtraction. Shortcut clauses for X โˆ’ 0 = X and X โˆ’ X = 0.

mul(X, Y, Z) โ€” X ร— Y = Z

Reversible multiplication. Shortcut clauses for 0 ร— _ = 0, _ ร— 0 = 0, 1 ร— X = X, X ร— 1 = X.

div(X, Y, Z) โ€” X รท Y = Z

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.

neg(X, Y) โ€” Y = โˆ’X

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

Use cases

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.

Limitations

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