- List of Backups
- View the diff.
- View the source.
- View the backup.
- Go to Guards.
- 1 (2004-02-01 (Sun) 13:13:23)
- 2 (2004-02-02 (Mon) 12:52:33)
*3 (2004-04-06 (Tue) 11:45:47)*- 4 (2004-04-21 (Wed) 13:48:35)
- 5 (2004-10-15 (Fri) 10:59:26)
- 6 (2004-10-22 (Fri) 09:52:20)
- 7 (2006-01-08 (Sun) 15:18:09)
- 8 (2006-03-14 (Tue) 14:33:50)
- 9 (2006-11-02 (Thu) 10:36:50)
- 10 (2006-11-02 (Thu) 10:36:50)
- 11 (2010-06-13 (Sun) 15:51:59)
- 12 (2015-05-17 (Sun) 20:34:13)
- 13 (2015-05-18 (Mon) 21:07:14)
- 14 (2017-03-02 (Thu) 03:32:49)
- 15 (2017-03-02 (Thu) 07:49:19)
- 16 (2019-04-29 (Mon) 10:31:19)
- 17 (2019-04-29 (Mon) 16:49:44)

- The added line is THIS COLOR.
- The deleted line is THIS COLOR.

[[Documentation]] #author("2019-05-02T21:06:54+09:00","default:LMNtal","LMNtal") //[[Documentation]] *Guards #mathjax **Rules with a Guard *Guards [#v398323a] The full syntax of a rule is: ( '''Head''' :- ['''Guard''' | ] '''Body''' ) **Rules with a Guard [#x7373323] '''Guard''' must be a multiset of ''type constraints'' of the form: &math(p(\$p_1,\ldots,\$p_n));. The same abbreviation scheme as defined for atoms applies to type constraints when a process context name &math(\$p_i); occurs exactly two times in the rule. Guards specify applicability conditions of rewrite rules. The syntax of a rule with a guard is: >\( \textit{Head}\ \texttt{:-}\ \textit{Guard}\ \texttt{|}\ \textit{Body} \) Type constraints put constraints on the shapes of processes with which the process contexts specified in the arguments can match. The type constraint name &math(p); specifies the content of the constraints. where \( \textit{Guard} \) is a multiset of ''type constraints'' of the form \( c(\texttt{\$}p_1, \dots, \texttt{\$}p_n) \). For example, the following type constraints can be used in '''Guard''': Type constraints constrains the shapes of processes (or the names of unary atoms) received by the process contexts \( \texttt{\$}p_1, \dots, \texttt{\$}p_n \). The ''type constraint name'' \( c \) is drawn from a built-in set and specifies which kind of constraints is imposed. -int($p) specifies that $p must be an integer atom. -$p < $q specifies that $p and $q are integer atoms A constraint of the form ''uniq''(\( \texttt{\$}p_1, \dots, \texttt{\$}p_n \)) is also allowed. This is a control structure rather than a type constraint and used to avoid infinite rule application (see below). ***Examples [#oc28c486] Here is an example rule with guard: waitint(X), $p[X] :- int($p) | ok. This can be abbreviated to waitint($p) :- int($p) | ok. 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(-2) :- ok. ... The following are examples of some type constraints that can be written in '''Guard''': -&color(#8B4513){int($p)}; ... specifies that $p must be an integer atom. -&color(#8B4513){4($p)}; ... specifies that $p must be a unary integer atom of value 4 (i.e., 4(X)). -&color(#8B4513){$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. -&color(#8B4513){$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. In reality, each type constraint name (such as int or <) ***Notes [#z6515d94] 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 of its input arguments are all determined. 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. **Typed Process Contexts 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 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 as follows: // **Typed Process Contexts [#z5d7f69f] ( 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. **Guard Library **Guard Library [#udf848a7] Currently, the following type constraints can be used in the guard. 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. '='(+Unary,-Unary) - equivalence '='(-Unary,+Unary) - equivalence '=='(+Unary,+Unary) - equivalence unary(+Unary) int(+Int) float(+Float) int(+Float,-Int) - cast float(+Int,-Float) - cast 345(-Int) - for every integer, not only with 345 '-3.14'(-Float) - for every floating, not only with -3.14 '<'(+Int,+Int) - integer comparison, as well as: > =< >= =:= =\= '+'(+Int,+Int,-Int) - integer operation, as well as: - * / mod '<.'(+Float,+Float) - floating comparison, as well as: >. =<. >=. =:=. =\=. '+.'(+Float,+Float,-Float) - floating operation, as well as: -. *. /. ***Type checking [#l78e805c] :int(+$i)|check if $i[X] is an integer. :float(+$f)|check if $f[X] is a floating-point number. :unary(+$u)|check if $u[X] is a unary atom. Note that ''int'' and ''float'' are subtypes of ''unary''. :ground(+$g)|check if $g[X1,...,Xn] (n>0) is a connected graph whose free links are exactly X1,...,Xn. Note that ''unary'' is a subtype of ''ground''. ***Comparison [#r7825264] :'='(+$u,+$v)|check if $u[X1,...,Xn] and $v[Y1,...,Yn] are connected graphs with the same structure. :'\='(+$u,+$v)|check if $u[X1,...,Xn] and $v[Y1,...,Ym] are connected graphs with different structures. :'=='(+$u,+$v)|check if $u[X] and $v[Y] are unary atoms with the same name. :'\=='(+$u,+$v)|check if $u[X] and $v[Y] are unary atoms with different names (if either of them are not unary, the check fails.) :'<.'(+$float,+$float)|float comparison; also: ''&color(#8B4513){'>.'};'', ''&color(#8B4513){'=<.'};'', ''&color(#8B4513){'>=.'};'', ''&color(#8B4513){'=:=.'};'', ''&color(#8B4513){'=\=.'};''. :'<'(+$int,+$int)|integer comparison; also: ''&color(#8B4513){'>'};'', ''&color(#8B4513){'=<'};'', ''&color(#8B4513){'>='};'', ''&color(#8B4513){'=:='};'', ''&color(#8B4513){'=\='};''. ***Assignment [#ne364170] :'='(+$u,-$v)|make sure that $u[X] and $v[Y] are unary atoms with the same name. :'='(-$u,+$v)|same as above. :int(+$float,-$int)|cast to int. :float(+$int,-$float)|cast to float. :345(-$int)|defined for every integer (not only with 345). :'-3.14'(-$float)|defined for every float. :'+'(+$int,+$int,-$int)|integer operation; also: ''&color(#8B4513){'-'};'', ''&color(#8B4513){'*'};'', ''&color(#8B4513){'/'};'', ''&color(#8B4513){mod};''. :'+.'(+$float,+$float,-$float)|float operation; also: ''&color(#8B4513){'-.'};'', ''&color(#8B4513){'*.'};'', ''&color(#8B4513){'/.'};''. **Avoiding Infinite Rule Application [#w149d3ab] 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. //***Others [#i37c8a7c] :uniq(+$g1,...,+$gn)|uniqueness constraint; checks if the rule has not been applied to the tuple $g1[X1], ..., $gn[Xn] (n>=0).