All guards in the theory language

This chapter presents guards (operators) that may be used to write rules. Such guards may be used to constrain the domain of application of a rule, using informations related to the goal and the hypothesis. To help writing and verifying the rules, all the guards of the theory language are documented thereafter.

A guard is a special antecedent in a rule. In fact, each guard in a rule is interpreted directly before the rule being effectively applied or not. Evaluating a guard never results in the creation of a SUCCESSor. The evalution of a guard may succeed or fail. For a rule to be effectively applicable, all the associated guard must be successful .

The following table summarizes the guard constructs:

bmatch bnot

band	conjunction of two guards
bfresh	construction of a fresh variable
bgetallhyp	obtains all the hypothesis
binhyp	tests the presence of a formula in (as ???) an hypothesis
blvar	lists the quantified variables
identity by matching
negation of a guard
bnum	numerality test
bpattern	tests formula matching
bsearch	tests presence in a list
bstring	tests if is a character string
bsubfrm	finds sub-formulas
btest	numeric comparison
bvrb	variable test

band

band(g1,g2)

Parameters

• g1 : guard

• g2 : guard

Nature

guard

Summary

Combines several guards.

Evaluation

The evaluation strategy differs according to the nature of the guards g1 and g2 :

• if g1 is binhyp(H ), or binhyp(n,H ), or binhyp(m,n,H ), and if, in the last two cases, n is a wildcard, then the resulting guard succeeds if there exists an hypothesis h that matches H and that is such that g2 is successful

• if g1 is a bsubfrm, bsearch or brule guard, then the resulting guard is successful if there exists a wildcard instantiation such that g1 successful , and such that g2 is successful .

• in all other cases, the resulting guard is successful if both guards g1 and g2, evaluated in sequence are successful . If g2 fails, the evaluation does not backtrack to g1 as in the preceding cases.

Example

THEORY tentative IS
band(binhyp(aaa(x)), band(binhyp(ccc),binhyp(bbb(x))) ) &
bcall(WRITE: bwritef("x: %n",x))
=>
H;

bcall((DED~;ess):((bbb(1) => (aaa(2) & bbb(2) & ccc & aaa(1) => titi))))
=>
foobar
END

Result

x: 1

bnot

bnot(g)

Parameters

• g : guard

Nature

Guard

Summary

Used to simplify expression of guards in case of failure.

Evaluation

The evaluation of bnot(g) is successful if the evaluation of g is a failure.

Example

THEORY tentative IS
bcall(WRITE: bwritef("OK n"))
=>
aaa(n);

breade("Write ?>? (substituting the ? with numbers): ",a>b) &
bnot(btest(a>b)) &
bcall(WRITE: bwritef("Hello??? n")) &
aaa(n+1)
=>
aaa(n)/*(a,b)*/;

bcall((ARI;ess)~: aaa(1))
=>
foobar
END

Result

Write ?>? (substituting the ? with numbers): 3>5
Hello???
Write ?>? (substituting the ? with numbers): 4>9
Hello???
Write ?>? (substituting the ? with numbers): 5>1
OK

bfresh

bfresh(v, f, V)

Parameters

• v: variable or variable list

• f: formula

• V: wildcard

Nature

Guard

Summary

To create fresh variables.

Evaluation

The evaluation is always successful . The wildcard V is instantiated with as many variables as there are in v. Moreover the new variables are not free in f. If v is not free in f, then V is the same as v.

Example

THEORY tentative IS
bfresh((xx,yy,zz),aaa+xx$0-yy*zz,V) &
bcall(WRITE: bwritef("%n",V))
=>
foobar
END

Result

xx$1,yy$1,zz$1

bgethyp

bgethyp(h), bgetallhyp(h)

Parameters

• h : formula

Nature

Guard

Summary

This guard gets the hypothesis in a proof.

Evaluation

The evaluation of the guard is successful when the proof contains hypothesis and that the conjunction of these hypothesis matches with formula h. These hypothesis also depend on the type of guard:

• Guard bgethyp only yields the main hypothesis;

• Guard bgetallhyp yields the main hypothesis as well as the hypothesis derived from these main hypothesis.

In any case, all the wildcards of h are instantiated.

Example

THEORY tentative IS
bgethyp(H) &
bgetallhyp(G) &
bcall(WRITE: bwritef("Main hypothesis: %n",H)) &
bcall(WRITE: bwritef("Main and derived hypothesis: %n",G))
=>
P;

bcall((DED;ess),fwd: (aaa & bbb => ggg))
=>
foobar
END

&

THEORY fwd IS
aaa => ccc;
ccc & bbb => ddd & eee
END

Result

Main hypothesis: aaa & bbb
Main and derived hypothesis: aaa & bbb & ccc & ddd & eee

binhyp

binhyp(h)
binhyp(n, h)
binhyp(m, n, h)

Parameters

• h: formula

• n: formula

• m: number

Nature

Guard

Summary

To access an hypothesis.

Evaluation

The guard binhyp(h) is successful when there exists an hypothesis that matches h. When there are several hypothesis, the last one is picked. All wildcards of h are instantiated. The evaluation of the guard binhyp(n,h ) depends on the nature of n: When n is a number, the evaluation is successful when the hypothesis of rank n exists and matches hypothesis h. All wildcards of h are instantiated. When n is a wildcard, the evaluation is successful if there exists an hypothesis that matches hypothesis h. n is then instantiated with the rank of h. All wildcards of h are instantiated. In all other cases, the evaluation fails. The evaluation of the guard binhyp(m,n,h) is similar to that of the guard binhyp(n,h), but in the case where n is a wildcard, the selected hypothesis is the last that matches h and with rank smaller or equal to i m. Note the similarities between these last two forms of the binhyp guard and the guards brule and lemma.

Example

THEORY tentative IS
foo(i);

binhyp(i,n,H) &
bcall(WRITE: bwritef("hyp_%: %n",n,H)) &
foo(n-1)
=>
foo(i);

binhyp(n,H) &
bcall(WRITE: bwritef("hyp_%: %n",n,H)) &
foo(n-1)
=>
bar;

binhyp(1,H) &
bcall(WRITE: bwritef("hyp_1: %n",H)) &
bar
=>
baz;

binhyp(H+G) &
bcall(WRITE: bwritef("hyp: %n",H+G)) &
baz
=>
P;

bcall((DED;(ARI;ess)~):((aaa & bbb+ccc & ddd) => pp))
=>
foobar
END

Result

hyp: bbb+ccc
hyp_1: aaa
hyp_3: ddd
hyp_2: bbb+ccc
hyp_1: aaa

blvar

blvar(l)

Parameters

• l : list of variables

Nature

Guard

Summary

To get the list of quantified variables at the current rewrite position.

Evaluation

The guard is always successful . If there is at least one quantified variable at the current rewrite position, l contains the list of quantified variables. Othewise l contains ?. For instance, if the current goal is

(aa,bb,cc).0<=aa & 0<=bb & 0<=cc => 0<=aa+bb+cc

and the rule

binhyp(x=0) &
blvar(Q) &
xQ
=>
x == 0

is applied, then Q will be (aa,bb,cc).

This guard is used within rewrite rules. It provides the guarantee that one does not mix quantified with non-quantified variables. It is often used in conjunction with the absence of freedom guard bnfree x E. ? E is always true, whatever E is.

Example

THEORY tentative IS
bnot(blvar(?))
=>
qq == pp;

!qq.(qq+1>qq)
=>
%ii.(ii: NAT | uu) = oi$5;

blvar(t$i)
=>
(t$i) == ii;

blvar(Q) &
Q!yx.(yx<yx+oo) &
bcall(WRITE: bwritef("free Q is %n",Q)) &
%(tt$0).(tt$0: NAT | uu) = oi$5
=>
!yx.(yx<yx+oo);

blvar(Q) &
Q(aa+2) &
bcall(WRITE:bwritef("aa transforms into oon"))
=>
aa == oo;

blvar(Q) &
Q(yx+2) &
bcall(WRITE:bwritef("yx transforms into zan"))
=>
yx == za;

!yx.(yx<yx+aa)
=>
!(zz$0,uu,hh$9).(zz$0+uu+hh$9>0);

blvar(Q) &
bcall(WRITE:bwritef("Q is %n",Q))
=>
vv == hh;

!(zz$0,uu,vv$9).(zz$0+uu+vv$9>0)
=>
!yy.(yy<yy+1);

blvar(Q) &
bcall(WRITE:bwritef("Q is %n",Q))
=>
xx == yy;

!xx.(xx < xx+1)
=>
foobar

END

Result

Q is xx
Q is xx
Q is xx
Q is zz$0,uu,vv$9
Q is zz$0,uu,vv$9
aa transforms into oo
free Q is ?
EXECUTION ABORTED ON GOAL: !pp.(pp+1>pp)

bmatch

bmatch(x, p, q e)

Parameters

• x: variable

• p: formula

• q: formula

• e: formula

Nature

Guard

Summary

Checks if a quantified formula may be instantiated.

Evaluation

For the guard to be successful , it is first necessary that the formula p does not contain quantifiers. Then it is required that there exists a formula f such that the substitution of x by f in p is the same as formula q. Finally, formula f must match e. All wildcards in e are instantiated.

Example

THEORY tentative IS
binhyp(!x.(H=>P)) &
bmatch(x,P,Q,E) &
bcall((SUB;WRITE):
bwritef("P: %nx: %nE: %n[x:=E]P: %nQ: %n",P,x,E,[x:=E]P,Q))
=>
Q;

( !(xx$1,yy).(qq(xx$1,yy) => pp(xx$1,ff(xx$1),yy))
=>
pp(aa,ff(aa),bb)
)
=>
ccc;

bcall((ess;DED;ess):ccc)
=>
foobar
END

Result

P: pp(xx$1,ff(xx$1),yy)
x: xx$1,yy
E: aa,bb
[x:=E]P: pp(aa,ff(aa),bb)
Q: pp(aa,ff(aa),bb)

bpattern

bpattern(f, g)

Parameters

• f: formula

• g: formula

Nature

Guard

Summary

Tests if a formula matches another formula.

Evaluation

The guard is successful if formula f matches formula g. All wildcards in g are instantiated.

Example

THEORY tentative IS

bnot(bpattern(p,q)) &
bcall(WRITE: bwritef("FAILURE"))
=>
baz(p,q);

bpattern(aaa+bbb,a+b) &
bcall(WRITE: bwritef("% %n",a,b)) &
baz(aaa+bbb,k+l)
=>
foobar

END

Result

aaa bbb
FAILURE

bsearch

bsearch(p, l, r)
bsearch(p, l, r, s)

Parameters

• p: formula

• l : non-atomic formula

• r: formula

• s: formula

Nature

Guard

Summary

To search, and possibly modify an element in a list.

Evaluation

The formula l has the form l1 op … op li op … op ln where n is greater than or equal to 2 and op is a binary operator.

The guard bsearch(p,l,r ) is successful when there exists a sub-formula li that matches p, and when the formula obtained by removing li from l matches formula r.

The guard bsearch(p,l,r,s ) is successful when there exists a sub-formula li that matches p, and when the formula obtained by substituting li in l with the corresponding instance matches formula r.

All wildcards in p, r and s are instantiated.

Example

THEORY tentative IS
bsearch((a-{x}),(aaa / (bbb-{xx}) / ccc / (ddd / {xx}) / eee),r,a) &
bsearch((b/{x}),r,s,b) &
bsearch((b/{x}),(aaa / (bbb-{xx}) / ccc / (ddd / {xx}) / eee),h) &
bcall(WRITE: bwritef("r: %na: %nb: %ns: %nh: %n",r,a,b,s,h))
=>
foobar
END

Result

r: aaa/bbb/ccc/(ddd/{xx})/eee
a: bbb
b: ddd
s: aaa/bbb/ccc/ddd/eee
h: aaa/bbb-{xx}/ccc/eee

bstring

bstring(f)

Parameters

• f: formula

Nature

Guard

Summary

To test that a formula is a character string.

Evaluation

The evaluation of the guard is successful if f is a character string (i.e. a sequence in characters between double-quotes). A double-quote may be present inside the string if it is preceded by a backslash.

Example

THEORY tentative IS

bcall (WRITE: bwritef("test3: FAILUREn"))
=>
test3;

bstring(aa+bb);
bcall (WRITE: bwritef("test3: SUCCESSn"))
=>
test3;

bcall (WRITE: bwritef("test2: FAILUREn"))
test3
=>
test2;

bstring(aaa) &
bcall (WRITE: bwritef("test2: SUCCESSn")) &
test3
=>
test2;

bcall (WRITE: bwritef("test1: FAILUREn")) &
test2
=>
test1;

bstring("Hello "Sir"") &
bcall (WRITE: bwritef("test1: SUCCESSn")) &
test2
=>
test2;

bcall(ess: test1)
=>
foobar

END

Result

test1: SUCCESS
test2: FAILURE
test3: FAILURE

bsubfrm

bsubfrm(g, d, p, q)
bsubfrm(g, d, p, (q, v))

Parameters

• g: formula

• d: formula

• p: formula

• q: formula

• v: formula

Nature

Guard

Summary

Tests the presence of a sub-formula in a formula and substitute it with another one.

Evaluation

For the evaluation of the first type of guard to be successful , it is first necessary that a formula f of p matches g (not instantiated). We then consider p obtained by substitution, in p, by the instantiated sub-formula f. Such formula p must match q (not instantiated). Most of the time, q is a simple wildcard.

In the second type of guard, the list of quantified variables on which f depends is also considered. If there is no such variable, then the list contains a single element: ?. This list must match v, not instantiated. Most of the time v is also a simple wildcard. All remaining unmatched wildcards are instantiated.

Example

THEORY tentative IS
bsubfrm(x/:s,not(x:s),#(y,z).!(xxx$1,x,bbb).(x/:s => aaa),(q,v)) &
bcall((SUB;WRITE): bwritef("q: %nv: %n",q,v))
=>
foobar
END

Result

q: #(y,z).!(xxx$1,x,bbb).(not(x: s) => aaa)
v: xxx$1,x,bbb,y,z

btest

btest(m op n)

Parameters

• m: formula

• n: formula

• op: comparison operator

Nature

Guard

Summary

To compare two numeric values.

Evaluation

The evaluation of the guard is successful when m and n related by the specified operator. The comparison operators:

• Equal: =

• Different: /=

• Smaller: <

• Smaller or equal: <=

• Greater: >

• Greater or equal: >=

When the operator is equality or difference, the evaluation of the guard is also successful when m and n are both identifiers that are related by the operator

Example

THEORY tentative IS

btest(bb/=aa) &
bcall(WRITE: bwritef("test3: SUCCESSn"))
=>
test3;

bnot(btest(8=aa)) &
bcall(WRITE: bwritef("test2: FAILUREn")) &
test3
=>
test2;

btest(8=8) &
bcall(WRITE: bwritef("test1: SUCCESSn")) &
test2
=>
foobar

END

Result

test1: SUCCESS
test2: FAILURE
test3: SUCCESS

bvrb

bvrb(f)

Parameters

• f : formula

Nature

Guard

Summary

To test that a formula is a variable.

Evaluation

The evaluation is successful if f is a variable. Recall that a variable is either a letter (wildcard) or an identifier that do not start with an underscore, or one of the two previous possibilities followed by a $ and a number smaller than 10000, or a list composed of distinct elements that fall into the previous cases.

Example

THEORY tentative IS

bcall(WRITE: bwritef("test5: FAILUREn"))
=>
test5;

bvrb(a+b) &
bcall(WRITE: bwritef("test5: SUCCESSn"))
=>
test5;

bcall(WRITE: bwritef("test4: FAILUREn")) &
test5
=>
test4;

bvrb(_a) &
bcall(WRITE: bwritef("test4: SUCCESSn")) &
test5
=>
test4;

bcall(WRITE: bwritef("test3: FAILUREn")) &
test4
=>
test3;

bvrb(a$10000) &
bcall(WRITE: bwritef("test3: SUCCESSn")) & test4
=>
test3;

bcall(WRITE: bwritef("test2: FAILUREn")) &
test3
=>
test2;

bvrb(a,a,bbb) &
bcall(WRITE: bwritef("test2: SUCCESSn")) &
test3
=>
test2;

bcall(WRITE: bwritef("test1: FAILUREn")) &
test2
=>
test1;

bvrb(aaaa_3,xxx,xx$2,y) &
bcall(WRITE: bwritef("test1: SUCCESSn")) &
test2
=>
test1;

bcall(ess: test1)
=>
foobar

END

Result

test1: SUCCESS
test2: FAILURE
test3: FAILURE
test4: FAILURE
test5: FAILURE