rules system - uhop/yopl GitHub Wiki

rules-system

Built-in helpers and control predicates. Provides both the low-level term builders used to write rules and a rules object you can spread into your own rule database.

See Writing rules for the conceptual introduction; this page is a per-export reference.

Import

import {head, term, list, listHead, rest, call, cut, fail, halt, isBound, rules as systemRules} from 'yopl/rules/system.js';

Term builders

Helper Returns Description
head(...args) {args} Rule head with the given argument vector.
term(name, ...args) {name, args} Structured goal term.
list(...args) cons-list (or null if empty) Build a yopl cons-list. Wrap the last arg in rest() to splice in an explicit tail.
listHead(...args) cons-list Like list, but the last argument is the tail directly. Requires ≥ 2 args.
rest(value) Tail Mark a value as the tail position for list.
import {head, term, list, rest, listHead} from 'yopl/rules/system.js';

head(1, 2, 3); // → {args: [1, 2, 3]}
term('member', X, list); // → {name: 'member', args: [X, list]}
list(1, 2, 3); // → {value: 1, next: {value: 2, next: {value: 3, next: null}}}
list(1, 2, rest(tail)); // tail spliced in at the end
listHead(1, 2, tail); // {value: 1, next: {value: 2, next: tail}}

Inline-goal helpers

These are JavaScript functions you place directly in a rule body to express side effects, computations, or control flow that the unifier cannot describe on its own.

Helper Description
fail Always fails — forces backtracking.
halt Aborts the proof search by clearing the driver stack.
cut(sys) Builds a Prolog-style cut. Pass the trailing ...sys rest-args from the rule definition.
call(X) Meta-call — evaluate X (a goal name, term, or bound variable) as a goal.
isBound(...vars) Succeeds when every supplied variable is bound.

fail

Always fails. Combined with cut, it implements negation as failure: prove the negated goal, commit, then fail — leaving any alternative clauses to handle the "succeed" case.

const rules = {
  // alwaysFails(X) has no solutions, no matter the argument.
  alwaysFails: () => [head(_), fail]
};

halt

Empties the solver's choice-point stack. Use it as an exception-style abort when something has gone irrecoverably wrong inside the proof. Unlike cut, halt stops the entire search, not just the current rule. The user-visible callback for the solution that triggered halt does not fire.

const rules = {
  validate: X => [head(X), env => X.isBound(env) || (console.error('unbound'), false), halt]
};

cut(sys)

The Prolog ! cut operator. Commits to the current clause: any alternative clauses for the same predicate are pruned, as is any backtracking within the current clause that would happen below the cut. Pass the trailing ...sys rest-args from the rule definition so cut can locate the choice-point frame.

Use cut for:

  • "first match wins" — memberchk-style lookups where you only care that an element exists.
  • guarded clauses — when the head match isn't enough to disambiguate but a side-condition is.
  • negation as failure — paired with fail.
const rules = {
  // member that stops at the first match
  member: [(V, X, ...sys) => [head(list(V, rest(X)), V), cut(sys)], (V, X) => [head({next: X}, V), term('member', X, V)]]
};

call(X)

Higher-order meta-call. The argument is one of:

  • a string — interpreted as a rule name with no arguments.
  • a structured term {name, args}.
  • a logical variable that is bound to one of the above.

call is what makes higher-order predicates like map, filter, foldl, and compose possible — they receive a callable name and synthesize a call(term(F, …)) for each list element.

const rules = {
  ...systemRules,
  // Apply the predicate F to X.
  apply: (F, X) => [head(F, X), call(term(F, X))]
};

isBound(...vars)

Succeeds when every supplied variable is currently bound in the environment. Useful as a guard before code that does direct value extraction (X.get(env)), so the rule can fail cleanly when invoked with an unground argument instead of crashing on undefined.

const rules = {
  doubleNumber: (X, Y) => [
    head(X, Y),
    isBound(X), // refuse if X is still unbound
    env => (env.bindVal(Y.name, X.get(env) * 2), true)
  ]
};

The rules object

Spreadable rule database. The remainder of this section covers each predicate, why it exists, and how to use it.

Type predicates

isVar, isNonVar, isNumber, isString, isNull, isUndefined, isArray — all unary, all check the type of their single argument in the current environment. They are guards: succeed when the type matches, fail otherwise.

const X = variable('X');
solve(systemRules, 'isVar', [X], () => console.log('still unbound'));
solve(systemRules, 'isNumber', [42], () => console.log('numeric'));

Use them inside a rule body to refuse to commit when the input is the wrong shape:

const rules = {
  ...systemRules,
  greet: X => [head(X), term('isString', X), env => (console.log('hi,', X.get(env)), true)]
};

eq / unify

eq(X, Y);

Succeeds when X and Y unify. The two names are aliases — unify is provided for readability when you want to emphasize that the operation is unification, not value equality.

eq is the building block of higher-level predicates: most rules effectively call eq implicitly through head matching, but you sometimes want it as an explicit body goal — for example to force two parameters to share a value at a specific point in the body.

solve(systemRules, 'eq', [X, 42], env => {
  // X is bound to 42 here
});

notEq / notUnifiable

notEq(X, Y);

Succeeds when X and Y cannot unify. Implemented as the standard Prolog \\= idiom — try to unify, then cut + fail if successful; otherwise the second clause succeeds.

solve(systemRules, 'notEq', [1, 2], () => console.log('different')); // fires
solve(systemRules, 'notEq', [1, 1], () => console.log('different')); // does not fire

Because this is negation as failure, both arguments must be sufficiently bound at the call site for the result to be meaningful.

not(Goal)

not(Goal);

Negation as failure: succeeds when Goal (a string, structured term, or bound variable) cannot be proven. Implemented as call(Goal), cut, fail followed by a default-true clause.

solve({...systemRules}, 'not', [term('eq', 1, 2)], () => console.log('1 ≠ 2')); // fires
solve({...systemRules}, 'not', [term('eq', 1, 1)], () => console.log('1 ≠ 1')); // does not fire

isUnifiable(X, Y)

Succeeds when X and Y would unify, without actually committing to the binding. Implemented as not(not(eq(X, Y))) — the double negation tests for satisfiability and then discards the bindings.

Use it for "could these be the same?" checks where you don't want to leak the bindings into the surrounding goal chain.

true

true;

A nullary always-succeeds rule. Useful as a placeholder body or as a "no-op" in conditional constructions.

const rules = {
  ...systemRules,
  maybe: P => [head(P), term('not', term('not', P))] // "P is satisfiable"
};

once(Goal)

Run Goal, commit to its first solution, and stop. Equivalent to call(Goal), cut.

const rules = {
  ...systemRules,
  ...mathRules,
  // First positive number in a list — once we find one, stop.
  firstPositive: (L, X) => [head(L, X), term('member', L, X), term('lt', 0, X)],
  firstPositiveOnce: (L, X) => [head(L, X), term('once', term('firstPositive', L, X))]
};

conjunction(List) and disjunction(List)

conjunction succeeds when every goal in List succeeds (logical AND). disjunction succeeds when any goal in List succeeds (logical OR). Both take a yopl cons-list of goals as their single argument.

import {list, term} from 'yopl/rules/system.js';

solve({...systemRules}, 'conjunction', [list(term('eq', 1, 1), term('eq', 2, 2))], () => console.log('both held'));

These are mostly useful when you build the list of goals dynamically — for static cases you can just inline the goals as body terms.

counterExample(A, B) and implies(A, B)

counterExample(A, B) succeeds when A holds but B does not — i.e. it found a witness against the implication "A ⇒ B".

implies(A, B) succeeds when no such counterexample exists — i.e. for every solution of A, B also holds. Implemented as not(counterExample(A, B)).

These let you express simple universally-quantified properties:

// Every element in `list` is a number.
solve({...systemRules}, 'implies', [term('member', list, X), term('isNumber', X)], () => console.log('all numeric'));

Higher-order: map, filter, foldl, foldr, compose, converse

These take a predicate name (passed by name, as a string or term) and apply it to elements of a cons-list. Internally they use call(term(F, …)) to invoke the predicate on each element.

Predicate Meaning
map(F, L, R) R is the result of applying binary F(In, Out) to every element of L.
filter(P, L, R) R contains the elements of L for which the unary predicate P succeeds.
foldl(F, A, L, R) Left fold: R is the result of F(Acc, Elem, NewAcc) applied left-to-right starting from A.
foldr(F, A, L, R) Right fold: same combiner, applied right-to-left.
compose(F, G, X, Y) Y = F(G(X)). F and G are binary predicates Pred(In, Out).
converse(F, X, Y, Z) converse(F)(X, Y) = F(Y, X) — argument-swapping wrapper.
const rules = {
  ...systemRules,
  ...mathRules,
  // square(X, Y) — Y is X*X
  square: (X, Y) => [head(X, Y), term('mul', X, X, Y)]
};

const In = list(1, 2, 3, 4),
  Out = variable('Out');
solve(rules, 'map', ['square', In, Out], env => {
  console.log(assemble(Out, env)); // list of 1, 4, 9, 16
});

Composing libraries

Spread systemRules together with the topical libraries to get a single database:

import solve from 'yopl';
import {rules as systemRules} from 'yopl/rules/system.js';
import {rules as compRules} from 'yopl/rules/comp.js';
import {rules as mathRules} from 'yopl/rules/math.js';

const rules = {
  ...systemRules,
  ...compRules,
  ...mathRules,
  myRule: () => [
    /* … */
  ]
};