[[Documentation]]

*Guards

**Rules with a Guard

The syntax of a rule with a guard is:
>'''Head''' :- '''Guard''' | '''Body'''

where '''Guard''' is a multiset of ''type constraints'' of the form:
'''p'''($'''p'''&size(10){1};, ..., $'''p'''&size(10){'''n'''};).
'''c'''($'''p'''&size(10){1};, ..., $'''p'''&size(10){'''n'''};).

Type constraints put constraints on the shapes of processes
Type constraints constrains the shapes of processes
(or the names of unary atoms)
with which the process contexts specified in its arguments can match.
The ''type constraint name'' '''p''' is drawn from a built-in set and specifies which kind of constraints is imposed.
received by the process contexts $'''p'''&size(10){1};, ..., $'''p'''&size(10){'''n'''};.
The ''type constraint name'' '''c''' is drawn from a built-in set and specifies which kind of constraints is imposed.

A constraint of the form ''uniq''($'''p'''&size(10){1};, ..., $'''p'''&size(10){'''n'''};) is
also allowed.  This is a control structure rather than a type constraint
and used to avoid infinite rule application (see below).

***Examples

Here is an example rule with guard:

 waitint(X), $p[X] :- int($p) | ok.

This can be abbreviated to

 waitint($p) :- int($p) | ok.

This rule can be thought of as an abbreviation
of the following infinite number of rules:
and can be thought of representing the following infinite number of rules:

 waitint(0) :- ok.
 waitint(1) :- ok.
 waitint(-1):- ok.
 waitint(2) :- ok.
   ...
 waitint(0)  :- ok.
 waitint(1)  :- ok.
 waitint(-1) :- ok.
 waitint(2)  :- ok.
 waitint(-2) :- ok.
 ...

The following list contains examples of some type constraints that can be written in '''Guard''':

- int($p) --- specifies that $p must be an integer atom.
- 4($p) --- specifies that $p must be a unary integer atom of value 4 (i.e., 4(X)).
- $p < $q --- specifies that $p and $q are integer atoms
such that the value of $p is less than that of $q.
- $r = $p +. $q --- specifies that $p, $q, and $r are floating
point number atoms
such that the sum of the values of $p and $q is equal to the value of $r. 

***Notes

Each type constraint name (such as int or <)
has its own mode of usage
that specifies which of its arguments are input arguments.
The effect of the constraint specified by a type constraint
is enabled only after the shapes (or values)
of its input arguments are all determined.
For example, $r = $p + $q proceeds only when $p and $q are determined.

The same abbreviation scheme as defined for atoms
applies to type constraints when a process context name
$'''p'''&size(10){'''k'''};
occurs exactly twice in the rule.
For example, p($n) :- $n>$z, 0($z) | ok can be abbreviated
to p($n) :- $n>0 | ok.

**Typed Process Contexts

A process context name $p constrained in '''Guard'''
is said to be ''typed'' in that rule.
As a syntactic sugar,
typed process context names can be written as link names.
For inscance, the above example can be written as:
 waitint(X) :- int(X) | ok.
// ( Res = gen(N) :- N > 0 | Res = [N|gen(N-1)] ), p(gen(10))
A process context constrained in '''Guard'''
is said to be a ''typed process context''.
// As a syntactic sugar,
// typed process context names can be written as link names.
// For inscance, the above example can be written as:
//  waitint(X) :- int(X) | ok.
// // ( Res = gen(N) :- N > 0 | Res = [N|gen(N-1)] ), p(gen(10))
// However, the original form, waitint($p) :- int($p) | ok, is preferred
// because, unlike link names, typed process context names has no constraints
// on the number of their occurrences.

**Avoiding Infinite Rule Application

A constraint of the form
''uniq''($'''p'''&size(10){1};, ..., $'''p'''&size(10){'''n'''};)
succeeds if each $'''p'''&size(10){'''k'''}; is a '''ground''' structure
(connected graph with exactly one free link; see below) 
and the rule has not
been applied to the tuple
$'''p'''&size(10){1};, ..., $'''p'''&size(10){'''n'''};
before.

As a special case of '''n'''=0,
''uniq'' succeeds if the rule in question has not been used
before.  The ''uniq''() test is a general tool for avoiding 
infinite application of rules whose right-hand side is a 
super(multi)set of the left-hand side.


**Guard Library

Currently, the following type constraints can be written in the
guard. The + specifies an input argument.
The following type constraints can be used in guards.
The + (input) sign preceding a process context name means that the name should
appear in the head, while the - (output) sign means that the name should not
appear in the head.

 '='(+U1,-U2)               - make sure that U1 and U2 are (connected to)
                              unary atoms with the same name
 '='(-U1,+U2)               - same as above
 '=='(+U1,+U2)              - check if U1 and U2 are (connected to) unary
                              atoms with the same name
 unary(+U)                  - check if U is (connected to) a unary atom
 ground(+G)                 - check if G is (connected to) a connected graph
                              with exactly one free link (which is G)
 int(+I)                    - check if I is (connected to) an integer
 float(+F)                  - check if F is (connected to) a float
 int(+Float,-Int)           - cast
 float(+Int,-Float)         - cast
 345(-Int)                  - defined for every integer (not only with 345)
 '-3.14'(-Float)            - defined for every float
 '<'(+Int,+Int)             - integer comparison; also: > =< >= =:= =\=
 '+'(+Int,+Int,-Int)        - integer operation;  also: - * / mod
 '<.'(+Float,+Float)        - float comparison;   also: >. =<. >=. =:=. =\=.
 '+.'(+Float,+Float,-Float) - float operation;    also: -. *. /.
 uniq(+G1,...,+Gn)          - uniqueness constraint; checks if the rule has
                              not been applied to the tuple G1,...,Gn (n>=0)
 '='(+$u,-$v)                  - make sure that $u[X] and $v[Y] are unary atoms
                                 with the same name
 '='(-$u,+$v)                  - same as above
 '=='(+$u,+$v)                 - check if $u[X] and $v[Y] are unary atoms with
                                 the same name
 unary(+$u)                    - check if $u[X] is a unary atom
 ground(+$g)                   - check if $g[X1,...,Xn] (n>0) is a connected
                                 graph whose free links are exactly X1,...,Xn 
 int(+$i)                      - check if $i[X] is an integer
 float(+$f)                    - check if $f[X] is a float
 int(+$float,-$int)            - cast
 float(+$int,-$float)          - cast
 345(-$int)                    - defined for every integer (not only with 345)
 '-3.14'(-$float)              - defined for every float
 '<'(+$int,+$int)              - integer comparison; also: > =< >= =:= =\=
 '+'(+$int,+$int,-$int)        - integer operation;  also: - * / mod
 '<.'(+$float,+$float)         - float comparison;   also: >. =<. >=. =:=. =\=.
 '+.'(+$float,+$float,-$float) - float operation;    also: -. *. /.
 uniq(+$g1,...,+$gn)           - uniqueness constraint; checks if the rule has
                                 not been applied to the tuple $g1[X1], ..., $gn[Xn] (n>=0)
Front page List of pages Search Recent changes Backup   Help   RSS of recent changes