Then and Back

Chronological Backtracking means exactly that: winding back the clock to a previous stage in the computation. It has numerous applications, particularly in complex problem-solving where the problem space must be searched.

The language supports chronological backtracking with two keywords: then and back. then behaves syntactically as a right associative binary operator. It evaluates and returns its lhs, but if backtracked to, it evaluates and returns its rhs. The keyword back causes immediate backtracking. Here's an example from the tests:

let
    fn require(condition) {
        condition or back
    }

    fn one_of {
        ([]) { back }
        ( h @ t) { h then one_of(t) }
    }
in            
    x = one_of([1, 2, 3, 4, 5]);
    require(x == 4);
    print(x); // 4

The function one_of is defined to first return the head of its argument list, then if backtracked to it recurses on the tail of the list.

The let body then defines x to be one_of the numbers 1, 2, 3, 4 or 5, then requires that x be 4 (which repeatedly backtracks into one_of until one_of returns 4) then the require succeeds and the expression prints x which is now 4.

Here's a more involved example, generating pythagorean triples where x squared plus y squared equals z squared.

fn integers_from(n) {
   n then integers_from(n + 1)
}

fn integers_between(lower, upper) {
    require(lower <= upper);
    lower then integers_between(lower + 1, upper);
}

fn pythagorean_triples() {
    z = integers_from(1);
    x = integers_between(1, z);
    y = integers_between(x, z);
    require(x ** 2 + y ** 2 == z ** 2);
    [x, y, z];
}

The first call to pythagorean_triples returns the list [3, 4, 5], but if repeatedly backtracked through will continue to produce all pythagorean triples. Note that then does not evaluate its rhs until it is backtracked through, so integers_from is not a runaway recursion.

It should be pointed out that chronological backtracking is far more than some kind of try/throw/catch. In some sense it is like try/throw/catch but unlike try/catch the then can be done at any chronologically previous point in the process, not just below some stack-based scope. A back will backtrack to the most recently executed then anywhere in the code.

require, one_of and others are pre-defined in the ambutils.fn namespace.

Under the hood this is an implementation of the construct amb from the classic SICP (Ch 4, S 3)

Next: Namespaces