diff --git a/docs/content/language.md b/docs/content/language.md index 235e57f0..dd6e86e9 100644 --- a/docs/content/language.md +++ b/docs/content/language.md @@ -32,7 +32,7 @@ The following table contains root concepts that belong to code rules definition. The aim of rules defined by handlers is again twofold: firstly, they may serve as regular “checking” rules, and also, most importantly, they contribute constraint productions. These are created with a DSL that allows mixing of productions and Java code, and can also include constraint fragments inside a production template. -The following example is from experimental *control flow* aspect for baseLanguage. It demonstrates how a production is constructed using a template. A template is enclosed into a pair of `%% … %%` symbols and yields constraints wrapped into special `<% … %>` brackets. In this particular case `write/2` constraint is optional and is only added to the body of production in case the condition is satisfied (a location corresponding to a local variable is written to only if it has an initialiser). +The following example is from the experimental *control flow* aspect for baseLanguage. It demonstrates how a production is constructed using a template. A template is enclosed into a pair of `%% … %%` symbols and yields constraints wrapped into special `<% … %>` brackets. In this particular case `write/2` constraint is optional and is only added to the body of production in case the condition is satisfied (a location corresponding to a local variable is written to only if it has an initialiser). ![](img/language-writelocal-750.png) _(example of rule with production template)_ @@ -63,21 +63,39 @@ Rules may affect the scope of model locations that are processed during an evalu ![](img/language-recoverct-700.png) _(example of using `require` statement)_ -#### Productions +#### Production templates -*Productions* can be created at any place within rule body. A production has three main parts called *head*, *guard*, and *body*. Head defines what constraints trigger this production, and it can only contain constraints defined by the handler or one of the handlers it extends. Body can contain any visible constraints, as well as *predicates*. A production must include either the body or the head, no production can omit both. Guard is optional, and it can only contain predicates. +Constraint productions are discussed in details in the section on Constraint Processing System, and here we briefly enumerate the main concepts and their usage. + +*Productions* can be created at any place within a rule’s body, which amounts to creating a production *template*. This means, a production within a loop generates a runtime constraint production on every iteration of this loop. + +A production template has three parts called *head*, *guard*, and *body*. Their meanings correspond precisely to those defined for the constraint productions. + +There is a certain limitation as to what *constraints* can be used in head: it can only contain constraints defined by this handler, or one of the handlers it extends. This limitation has its origin in the way productions are chosen when an active constraint is being processed. Namely, productions to match an active constraint are selected from the handler declaring this constraint, and handlers that are its extensions. The order of productions within the handler matters, the ones declared on top are matched first. Productions from extending handlers are prepended to the list of productions of the handler they extend. + +Production’s body can contain any visible constraints, as well as *predicates*. A production must include either the body or the head, no production can omit both. Guard is optional, and it can only contain predicates. + +A production with an empty head, not declaring any constraints to serve as its input, is considered an *automatic* production and is triggered automatically on start of constraints program execution. + +Constraints in a production’s head can be declared as either *kept* or *replaced*. Replaced constraints are marked with a tilde `~`. + +Predicates, also known otherwise as “built-in constraints”, are represented either as binary operators, such as `=` for unification or `==` for equality, or they are boolean-valued functions. Unification or equality if used in guard, only tests that its arguments can be unified, otherwise if called from body, it invokes the actual unification or assigns the value to a logical variable. + +![](img/language-unify-300.png) +_(`unifies` predicate used in the guard and in the body)_ + +There are also predicates that can only be queries, such as `isFree/1` or `isBound/1`, testing if a logical variable is free or has value assigned. Such predicates can only be used in guard. + +Arbitrary Java code can be called with `eval/1` predicate. It accepts either an expression of `boolean` type, in which case it can be used in guard, or expression of any type when called from body. In the latter case the value expression evaluates to is ignored. + +![](img/language-recover-500.png) +_(example of using `eval/1` predicate)_ Both head and body can declare *logical variables*. By default a logical variable ranges over *terms*, although any POJO[^pojo] may be serve as a value. ![](img/language-compatibleWith-300.png) _(production declaring logical variables)_ -A production with an empty head, not declaring any constraints to serve as its input, is considered an *automatic* production and is triggered automatically on start of constraints program execution. - -In a production’s head constraints can be declared as either *kept* or *replaced*. Briefly put, the constraints that are *kept* are left alone after a production is fired, whereas the *replaced* ones are discarded after the production’s head has been matched. Replaced constraints are marked with a tilde `~`. - -Productions to match a particular constraint are selected from a handler that declares this constraint, and handlers that are its extensions. The order of productions within the handler matters, the ones declared on top are matched first. Productions from extending handlers are prepended to the list of productions of the handler they extend. - When a constraint with logical variable as one of its arguments is matched, that variable becomes bound to the corresponding argument of the matching occurrence. The scope of such binding is this production’s guard and body. There is support for pattern matching, using terms as patterns, which may optionally contain logical variables. For this to work, a logical variable that serves as a constraint argument should have a pattern attached. @@ -90,22 +108,9 @@ Everywhere locations in the source code (model) must be referenced, node referen ![](img/language-typeof-550.png) _(example of constraint argument referring to a model location)_ -Whereas the production’s head can only contain constraints, there are also other logical clauses that are used in guard and body. - -A *predicate* is a built-in construct that serves two purposes: when used in guard, it acts to query if the condition is satisfied, and when invoked from body, it asserts the condition. An example is `unifies` predicate, displayed as `=`, which, if used in guard, only tests that its arguments can be unified, otherwise if called from body, it invokes the actual unification. There are also predicates that can only be queries, such as `isFree/1` or `isBound/1`, testing if a logical variable is free or has value assigned. - -Production’s guard can only contain predicates, and the body can contain both constraints and predicates. - -![](img/language-unify-300.png) -_(`unifies` predicate used in the guard and in the body)_ - -Arbitrary Java code can be called with `eval/1` predicate. It accepts either an expression of `boolean` type, in which case it can be used in guard, or expression of any type when called from body. In the latter case the value expression evaluates to is ignored. - -![](img/language-recover-500.png) -_(example of using `eval/1` predicate)_ - In order to make use of macro definitions, which are essentially parameterised production templates extracted to a separate root, one of the two pseudo predicates can be used: `expand` and `call`. The former accepts a node, whereas the second expects the arguments that are substituted as macro parameters. + ***Examples of expand/call pseudo predicates*** ***Substitution — passing parameters via context*** diff --git a/docs/content/processing.md b/docs/content/processing.md index d6c8b68a..1e1af919 100644 --- a/docs/content/processing.md +++ b/docs/content/processing.md @@ -24,19 +24,29 @@ _(examples of terms)_ The unique feature of terms is that they support unification. Unification of two terms is possible with or without *variables* being used as subterms of either participant, but in the latter case the two terms must be equal. -A term variable ranges over terms. A substitution is a mapping of variables to terms. Unification searches for a substitution $\sigma$, such that for two terms being unified, $f$ and $g$, the following holds: $\sigma f = \sigma g$. +A term variable ranges over terms. A substitution is a mapping of variables to terms. Unification searches for a substitution $\sigma$, such that for two terms being unified, $f$ and $g$, the following holds: $\sigma f = \sigma g$. For example: ``` [X -> g()] unifies f(X, h(X)) and f(g(), h(g())) - - f(X, h(X)) and f(g(), h(k())) can't be unified + + [X -> Z, Y -> g(X)] unifies f(X, g(X)) and f(Z, Y) ``` -Pattern matching is possible when variables are only used by one of the terms, which is then serves as pattern. To test if a pattern matches a given term can be implemented by a linear time algorithm, whereas full unification is slightly more complicated. +The latter unifier is the most general one, since other substitutions that also unify the two terms are all subsumed by it: -***MGU*** +``` + [X -> g(X), Y -> g(g(X)), Z -> g(X)] + [X -> g(g(X)), Y -> g(g(g(X))), Z -> g(g(X))] +``` + +Unification may fail because the arity or the symbols of the two terms mismatch. Also, since *infinite terms* are not supported, unification may fail because of *occurs check*, which means a variable can’t be unified with a term, that itself or through its descendants has this variable as one of its arguments. -***Occurrs check*** +``` + f(X, h(X)) and f(g(), h(k())) can't be unified because g != k + f(X, g(X)) and f(g(X), g(h()) can't be unified because of failed occurs check +``` + +Pattern matching is possible when variables are only used by one of the terms, which then serves as a pattern. To test if a pattern matches a given term can be implemented by a linear time algorithm, whereas full unification is slightly more complicated. ### Logical variables @@ -117,12 +127,6 @@ There is some terminology inherited from CHR that can be useful when discussing Essentially, a production with only “kept” constraints in its head is a “propagation”, the one with only “replaced” constraints is a “simplification”, and the one that has both “kept” and “replaced” constraints is a combination of the two. In addition, we define a fourth kind of production, an “auto” production with an empty head. As the name implies, such production is triggered automatically on start of constraints program execution. -To illustrate the idea of using *stored* constraints to fill vacant positions when matching a production, let’s consider an example — a production resolving `containedIn/2` constraint, which corresponds to *type parameter containment* relation of BaseLanguage types. - -![](img/process-containedin-350.png) -_(example of a multi-head production)_ - -When `containedIn/2` constraint is activated, the production above matches, but two slots in its head must be filled in order for production to fire. The processor looks in the *store* for all *different* occurrences of constraint `hasBound/2` that could be matched, and substitutes them in these slots. The production will be fired for every matching triple of constraints. #### Guard @@ -132,12 +136,71 @@ Guard is a conjunction of predicates, which are checked before a production is f Body is a conjunction of predicates and constraint activations. When triggered, each body clause is evaluated in order, with predicates serving as *assertions* and constraint activations producing new constraints. Each newly activated constraint is checked against any productions that can be fired, and so on. +### Triggering a production + +The procedure `processActive()` accepts a constraint occurrence that has been activated and proceeds as follows until this constraint is either discarded or suspended (moved to store). This procedure calls itself recursively on every constraint activation, so there might be many active constraints at any given moment, organised into a stack, which matches exactly the call stack of `processActive()`. + +First, the procedure searches for “relevant” productions that declare a constraint in their heads matching the active constraint occurrence currently being processed. These productions form a FIFO queue, corresponding to the order of productions within a handler. + +For each “relevant” production, which at least partially matches the currently active constraint occurrence, the vacant slots in production’s head are filled with matching constraints from the store, which were previously suspended. Once a full match with production’s head is established, the guard is checked. + +A production together with a set of constraints matching the ones declared by its head, one of which must be the active constraint, is considered to have been triggered after the guard check returns true. Otherwise this production is skipped. + +After a production is triggered, first the constraints marked by production’s head as *replaced* are deactivated, and the logical variables defined by patterns are assigned appropriate values by asserting equality through *equals* predicate. Then the constraints and predicates defined in production’s body are activated one-by-one. Every activation of a constraint is a recursive call to `processActive()`. + +If after having processed all items in production’s body the constraint occurrence currently being processed is still “alive”, meaning it has not being discarded during one of the recursive calls to this procedure, the process of matching and triggering productions continues with the next production from the queue. + +When there are no more productions that can be matched, or the active constraint has been discarded, the procedure `processActive()` finishes. If, when the procedure is finished the active constraint is still “alive”, it is suspended and moved to the store. ***Alternative body*** +#### Example of executing a program + +Consider the following example of the Euclid algorithm taken from the CHR book[^chr]: + +``` +gcd(0) <=> true +gcd(N) \ gcd(M) <=> 0 < N, N =< M | gcd(M - N) +``` + +To illustrate the idea of using *stored* constraints to fill vacant slots when matching a production, let’s see what happens when this program is evaluated with 4 and 6 as arguments to `gcd/1` constraint. + +| Constraints store | Active constraint | Match | Result | +|:--|:--|:--|:--| +| `{}` | `gcd(4)` | no productions matched | suspend `gcd(4)` | + +On activating `gcd(4)` there are no matching productions, so the constraint is suspended. + +| Constraints store | Active constraint | Match | Result | +|:--|:--|:--|:--| +| `{gcd(4)}` | `gcd(6)` | `gcd(6) \ gcd(4)` | guard condition fails | +| `{gcd(4)}` | `gcd(6)` | `gcd(4) \ gcd(6)` | discard `gcd(6)`, activate `gcd(2)` | + +Notice how both combinations of `gcd(4)` and `gcd(6)` constraints are tested. In general, if there are $n$ usages of constraint `foo` in a given production’s head, there will be $n!$ potential matches to be evaluated, so that all permutations are covered. + +The last activation above is a recursive call to `processActive()`, so the cycle repeats. The active constraint has been deactivated, but contents of the store is unchanged. + +| Constraints store | Active constraint | Match | Result | +|:--|:--|:--|:--| +| `{gcd(4)}` | `gcd(2)` | `gcd(2) \ gcd(4)` | discard `gcd(4)`, activate `gcd(0)` | +| `{}` | `gcd(0)` | `gcd(0)` | discard `gcd(0)` | + +There are no more productions to match for `gcd(2)` as the active constraint, so it is suspended. But the constraint `gcd(6)` has been already discarded, so there are no more active constraints and the process stops. Here is the full trace of this program execution. + +| Constraints store | Active constraint | Match | Result | +|:--|:--|:--|:--| +| `{}` | `gcd(4)` | no productions matched | suspend `gcd(4)` | +| `{gcd(4)}` | `gcd(6)` | `gcd(6) \ gcd(4)` | guard condition fails | +| `{gcd(4)}` | `gcd(6)` | `gcd(4) \ gcd(6)` | discard `gcd(6)`, activate `gcd(2)` | +| `{gcd(4)}` | `gcd(2)` | `gcd(2) \ gcd(4)` | discard `gcd(4)`, activate `gcd(0)` | +| `{}` | `gcd(0)` | `gcd(0)` | discard `gcd(0)` | +| `{}` | `gcd(2)` | no productions matched | suspend `gcd(2)` | + +After the program has finished, the constraint store consists of only one constraint `gcd(2)`, which is the *GCD* of 4 and 6. + ## Semantics of constraints program -The paper by Betz and Frühwirth[^lls] gives an excellent tretise on semantics of CHR using *linear logic*. Since our constraints processing system is based on CHR, this semantics is valid for it also. +The paper by Betz and Frühwirth[^lls] gives an excellent treatise on semantics of CHR using *linear logic*. Since this constraints processing system is based on CHR, this semantics is valid for it also. Linear logic abandons boolean values and replaces them with consumable resources. Consequently, it introduces its own set of connectives, from which we are interested only in the following: $!,\otimes,\multimap$. The *multiplicative conjunction* $\otimes$ combines two or more resources that are all available at the same time. The symbol $!$ (*of course*) marks a resource that can’t be exhausted. And instead of implication $\rightarrow$ one uses $\multimap$ symbol, the meaning of which is a transformation of one resource to another. The formula $A \multimap B$ is read: “consuming $A$, produce $B$ ”, that is given a resource $A$, we can assume $B$, but $A$ can no longer be used. @@ -157,4 +220,5 @@ Propagation is different from simplification in that the set of constraints $E$, [^jchr]: K.U.Leuven JCHR System [https://dtai.cs.kuleuven.be/CHR/JCHR/](https://dtai.cs.kuleuven.be/CHR/JCHR/) [^uf]: [https://en.wikipedia.org/wiki/Disjoint-set_data_structure](https://en.wikipedia.org/wiki/Disjoint-set_data_structure) [^pred]: a.k.a. “built-in constraints” in CHR literature +[^chr]: Constraint Handling Rules [http://www.informatik.uni-ulm.de/pm/fileadmin/pm/home/fruehwirth/constraint-handling-rules-book.html](http://www.informatik.uni-ulm.de/pm/fileadmin/pm/home/fruehwirth/constraint-handling-rules-book.html) [^lls]: Betz, H. and Frühwirth, T., 2005, October. A linear-logic semantics for constraint handling rules. In International Conference on Principles and Practice of Constraint Programming (pp. 137-151). Springer, Berlin, Heidelberg.