Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Significantly refactor and simplify flattening transformation, unify …
…handling of builtins and functional predicates (#23) ## Background ### Functional predicates I originally introduced **functional predicates** with the observation that it's pretty nice to be able to write ``` size is 3. color 1 is red. color 2 is blue. color 3 is green. color 4 is orange. a (color N) :- b N, N < size. ``` where the last rule is a shorthand for ``` a Color :- b N, size is Size, N < Size, color N is Color. ``` Expanding out this shorthand is done in a step called the _flattening transformation_. ### Built-in operatons I also originally introduced **built-in operations** in a way that had a complicated interaction with the term-matching infrastructure, so that, for example, matching the term `3` against the pattern `succ X` with `succ` registered as the `NAT_SUCC` operator would result in X being bound to 2. This introduced complexity into a pretty core part of the system, **and** it wasn't clear what should happen if you try to write things like `succ "Hello world"`. One correct, well-understood, and uniform way to handle this sort of operation is by treating the successor operator as an infinite relation of the form `succ X is Y`, with the following entries: ``` succ 0 is 1. succ 1 is 2. succ 2 is 3. ... ``` This PR unifies the way both functional predicates and built-in relations get treated by the static checker and the flattening transformation. ## Built-ins are now uniformly treated as relations Without this PR, Dusa doesn't allow you to write built-in operations as relations. The following isn't allowed, for example: ``` #builtin NAT_SUCC succ a 3. b Y :- a X, succ X is Y. ``` In Dusa 0.0.14 and below, built-ins can only be referenced in their functional form, not their relational form, even though the program was compiling everything into the relational form. This is fixed, and under this PR the program above is accepted. ## Functional predicates and builts-in are now uniformly translated to relations in the flattening transformation Functional predicates and built-ins are now turned into additional predicates by the flattening transformation, a simple recursive process that mimics instruction selection in a compiler: ``` #demand f X Y, h (plus X Y). --> #demand f X Y, plus X Y is Z, h Z ``` These effects stack: ``` #demand f X Y, g (plus (plus X X) (plus X Y)). --> #demand f X Y, plus X X is X2, plus X Y is Z, plus X2 Z is G, g G. ``` This transformation is exactly the same whether `plus` is a declared relation or the builtin `INT_PLUS`. ## Modes for functional predicates are now much more generic, but still have a special case for inequality Modes for all built-ins, including the syntactically-supported ones like equality and inequality, are now uniformly handled with a mode system. This mode system has one quirk beyond the usual "input"/"output" thing, which is that "wildcard" is allowed as an input mode to handle built-ins that work like inequaltiy. Consider the following rule: ``` a Ys :- b Xs, cons 4 Ys != Xs. ``` This rule will give the following error: > The built-in relation NOT_EQUAL was given 2 arguments, and the argument in position 1 contains variables not bound by previous premises. This builtin does not support that mode of operation. Intuitively, Dusa can't handle this, because there are always going to be countably infinite `Ys` such that `cons 4 Ys != Xs`. **However** for practical logic programming it's _really really useful_ to be able to say ``` a :- b Xs, cons 4 _ != Xs. ``` Which, logically, translates to "If b Xs, and not (Exists Ys. cons 4 Ys == Xs), then a" This is admittedly irregular with respect to everything else in the language! But computationally it's quite reasonable, implementation-wise it's not particularly complex, the logical meaning is entirely decidable, and there are many cases where you avoid a lot of sad verboseness if this doesn't exist. The "wildcard" mode exists to support this specific use-case: a "wildcard" moded argument is one that isn't grounded by its premises, but any non-ground portions are limited to wildcard variables `_`. ## Backwards incompatibility This PR simplifies the existing flattening transformation, but this means that some previously-accepted programs now must be rejected. In particular, this PR disables a common idiom _that was used in one of the default sample programs_ (the graph generation example). ``` #builtin NAT_SUCC s vertex 6. vertex N :- vertex (s N). ``` This is no longer supported, and now returns this error > Because s is the built-in relation NAT_SUCC, for it to be used like a function symbol, all the arguments must be grounded by a previous premise. If you want to use s with a different mode, write it out as a separate premise, like 's * is *'. This makes `NAT_SUCC` a lot less useful in general - you can still write the program, following the advice of the error message, like this: ``` #builtin NAT_SUCC s vertex 6. vertex N :- vertex M, s N is M. ``` A better idiom in Rob's opinion now that this functionality doesn't exist, is this one: ``` #builtin INT_MINUS minus vertex 6. vertex (minus N 1) :- vertex N, N > 0. ``` (Chris disagrees, fwiw, and still thinks the program using NAT_SUCC is better. In any case we're not losing expressivity, both are possible.) ### Rationale for backwards incompatibility I believe this backwards incompatibility is acceptable, at least in the medium term, because it lets us uniformly turn all relations and premises into *separate premises* with a very uniform translation. The uniform translation, on the now-rejected program, looks like this: ``` #builtin NAT_SUCC s vertex 6. vertex N :- s N is M, vertex M. ``` ...and that clearly doesn't work, as successor with no ground inputs has an infinite number of possible ways of matching (N = 122, M = 123, or N = 123, M = 124, or N = 124, M = 125, or N = 125, M = 126, and so on). ### Alternatives to introducing backwards compatibility This was previously supported by a significantly more complex and harder-to-motivate flattening transformation that "notices" that `(s N)` is not ground in the first argument and instead translates the problematic program above like this: ``` #builtin NAT_SUCC s vertex 6. vertex N :- vertex M, s N is M. ``` I put a fair amount of work into that kind of before-and-after translation... it was very complex. I think disabling this functionality is worthwhile in the name of simplicity.
- Loading branch information
1 parent
14ac885
commit 85f7369