Disallow cyclic definitions of variables

[jacobdweightman]

This Allium program proves a blatantly false proposition:

// Peano construction of the natural numbers
type Nat {
    ctor Z;
    ctor S(Nat);
}

// equality of natural numbers
pred eq(Nat, Nat) {
    eq(Z, Z) <- true;
    eq(S(let x), S(x)) <- true;
}

pred main {
    main <- eq(let y, S(y));
}

This program corresponds to a proof of the claim "there exists a natural number y such that y = y + 1." Clearly there is no such natural number, and yet the program succeeds. The problem is that the witness it finds is not a ground term, but cyclic — it concludes that x = S(x) is a witness.

Prolog addresses this problem by making an optional "occurs check," which prevents matching a variable with any term that contains it recursively. One solution would be to implement this approach in Allium, however this can have significant performance implications for pattern matching in the general case. Another approach would be to find a semantic restriction which prevents these cyclic (non-)witnesses.

[kwalberg]

I started looking into this one with the assumption that we're implementing the occurs check now and figuring out any optimizations later.