Goto Chapter: Top 1 2 3 4 Bib Ind
 [Top of Book]  [Contents]   [Previous Chapter]   [Next Chapter] 

3 Parsing first-order formulas
 3.1 PredicataFormula – strings representing first-order formulas
 3.2 PredicataTree – converting first-order formulas into trees
 3.3 PredicataRepresentation – Predicata assigned with names and arities
 3.4 Converting PredicataFormulas via PredicataTrees into Predicata

3 Parsing first-order formulas

3.1 PredicataFormula – strings representing first-order formulas

3.1-1 PredicataFormulaSymbols
‣ PredicataFormulaSymbols( global variable )

The variable PredicataFormulaSymbols stores all inbuilt function symbols.

gap> PredicataFormulaSymbols;
[ "*", "+", "-", "=", "gr", "geq", "less", "leq", "and", "or", "equiv", 
"equivalent", "implies", "not", "(", ")", "[", "]", ",", ":", "A", "E" ]

3.1-2 PredicataIsStringType
‣ PredicataIsStringType( S, T )( function )

The function PredicataIsStringType checks if the string S represents one types T="variable", "integer" (greater equal 0), "negativeinteger", "boolean", "predicate", "internalpredicate", "quantifier", "symbol", "binarysymbol", "unarysymbol". PredicataFormulaSymbols (3.1-1).

gap> PredicataIsStringType("x1", "variable");
true
gap> PredicataIsStringType("1", "integer");
true
gap> PredicataIsStringType("-1", "negativeinteger");
true
gap> PredicataIsStringType("true", "boolean");
true
gap> PredicataIsStringType("A", "quantifier");
true
gap> PredicataIsStringType("+", "symbol");
true

3.1-3 PredicataGrammarVerification
‣ PredicataGrammarVerification( S[, P] )( function )

The function PredicataGrammarVerification checks if the string S, with the optional argument PredicataRepresentation (3.3-10) P, is a well-formed formula in the Presburger arithmetic. First a lexical analysis is performed, checking if all symbols are correct. Then it is checked if the formula can be produced from the predefined grammar (see PredicataGrammar (4.1-1)). Finally, the range of the quantified variables is checked, as well as if all bounded variables doesn't also occur as free ones. Additionally, if the amount of opening and closing parenthesis differs, a corresponding message is returned.

gap> PredicataGrammarVerification("4+x=2*y");
true
gap> PredicataGrammarVerification("(E x:3+x=2*y)");
true
gap> PredicataGrammarVerification("= , 2 + <= x 4");
false

3.1-4 PredicataFormula
‣ PredicataFormula( S[, P] )( function )

The function PredicataFormula takes a string S, checks if it's a formula in the language of Presburger arithmetic (using with PredicataGrammarVerification (3.1-3)) and returns a PredicataFormula (use PredicataGrammar (4.1-1) for an overview of the rules). The optional input P is explained at PredicataRepresentation (3.3-10), however on default the predefined variable PredicataList (3.3-23) is used.

gap> PredicataFormula("(E y: x + y = z)");
< PredicataFormula: ( E y : x + y = z ) >

3.1-5 IsPredicataFormula
‣ IsPredicataFormula( f )( function )

The function IsPredicataFormula checks if f is a PredicataFormula.

gap> f:=PredicataFormula("(E y: x + y = z)");
< PredicataFormula: ( E y : x + y = z ) >
gap> IsPredicataFormula(f);
true

3.1-6 Display
‣ Display( f )( method )

The method Display displays the PredicataFormula f.

gap> f:=PredicataFormula("(A x: (E y: x = y))");
< PredicataFormula: ( A x : ( E y : x = y ) ) >
gap> Display(f);
PredicataFormula: ( A x : ( E y : x = y ) ).

3.1-7 View
‣ View( f )( method )

The method View applied on a PredicataFormula f returns the object text.

gap> f:=PredicataFormula("x + y = z");;
gap> View(f);
< PredicataFormula: x + y = z >

3.1-8 Print
‣ Print( f )( method )

The method Print prints the PredicataFormula f as a string.

gap> f:=PredicataFormula("x = 4 and not x = 5");
< PredicataFormula: x = 4 and not x = 5 >
gap> Print(f);
PredicataFormula("x = 4 and not x = 5");
gap> String(f);
"PredicataFormula(\"x = 4 and not x = 5\");"

3.1-9 FreeVariablesOfPredicataFormula
‣ FreeVariablesOfPredicataFormula( f )( function )

The function FreeVariablesOfPredicataFormula returns the free variables of the PredicataFormula f as a list of strings.

gap> f:=PredicataFormula("(E n: 3*n = x) or (E m: 4*m = x)");
< PredicataFormula: ( E n : 3 * n = x ) or ( E m : 4 * m = x ) >
gap> FreeVariablesOfPredicataFormula(f);
[ "x" ]

3.1-10 BoundedVariablesOfPredicataFormula
‣ BoundedVariablesOfPredicataFormula( f )( function )

The function BoundedVariablesOfPredicataFormula returns the bounded variables of the PredicataFormula f as a list of strings.

gap> f:=PredicataFormula("(E n: 3*n = x) or (E m: 4*m = x)");
< PredicataFormula: ( E n : 3 * n = x ) or ( E m : 4 * m = x ) >
gap> BoundedVariablesOfPredicataFormula(f);
[ "n", "m" ]

3.1-11 PredicataFormulaFormatted
‣ PredicataFormulaFormatted( f[, P] )( function )

The function PredicataFormulaFormatted adds missing parenthesis to the PredicataFormula f for unambiguous parsing in PredicataFormulaFormattedToTree (3.2-14).

gap> f:=PredicataFormula("(E y: x + y = z)");
< PredicataFormula: ( E y : x + y = z ) >
gap> F:=PredicataFormulaFormatted(f);
< PredicataFormulaFormatted: ( E y : ( ( x + y ) = z ) ) >

3.1-12 IsPredicataFormulaFormatted
‣ IsPredicataFormulaFormatted( f )( function )

The function IsPredicataFormulaFormatted checks if f is a PredicataFormula.

gap> f:=PredicataFormula("(E y: x + y = z)");
< PredicataFormula: ( E y : x + y = z ) >
gap> F:=PredicataFormulaFormatted(f);
< PredicataFormulaFormatted: ( E y : ( ( x + y ) = z ) ) >
gap> IsPredicataFormulaFormatted(F);
true

3.1-13 Display
‣ Display( F )( method )

The method Display displays the PredicataFormulaFormatted F.

gap> F:=PredicataFormulaFormatted(PredicataFormula("(E y: x + y = z)"));
< PredicataFormulaFormatted: ( E y : ( ( x + y ) = z ) ) >
gap> Display(F);
PredicataFormulaFormatted: [ "(", "E", "y", ":", "(", "(", "x", "+", "y", ")", 
"=", "z", ")", ")" ].
Concatenation: (Ey:((x+y)=z)).

3.1-14 View
‣ View( f )( method )

The method View applied on a PredicataFormulaFormatted F returns the object text.

gap> f:=PredicataFormula("x + y = z");;
gap> F:=PredicataFormulaFormatted(f);;
gap> View(F);
< PredicataFormulaFormatted: ( ( x + y ) = z ) >

3.1-15 Print
‣ Print( F )( method )

The method Print prints the PredicataFormulaFormatted F as a string.

gap> F:=PredicataFormulaFormatted(PredicataFormula("x = 4 and not x = 5"));
< PredicataFormulaFormatted: ( ( x = 4 ) and ( not ( x = 5 ) ) ) >
gap> Print(F);
PredicataFormulaFormatted(PredicataFormula(s"((x=4)and(not(x=5)))"));
gap> String(F);
"PredicataFormulaFormatted(PredicataFormula(\"((x=4)and(not(x=5)))\"));"

3.2 PredicataTree – converting first-order formulas into trees

3.2-1 PredicataTree
‣ PredicataTree( [r] )( function )

The function PredicataTree creates the a tree with root r, which may be empty.

gap> PredicataTree("root");
< PredicataTree: [ "root" ] >
gap> PredicataTree();
< PredicataTree: [ "" ] >

3.2-2 IsPredicataTree
‣ IsPredicataTree( t )( function )

The function IsPredicataTree checks if t is a PredicataTree.

gap> f:=PredicataFormula("(E y: x + y = z)");
< PredicataFormula: ( E y : x + y = z ) >
gap> IsPredicataFormula(f);
true

3.2-3 Display
‣ Display( t )( method )

The method Display prints the PredicataTree t as a nested list, i.e. it's internal structure.

gap> t:=PredicataTree("only one element");
< PredicataTree: [ "only one element" ] >
gap> Display(t);
PredicataTree: [ "only one element" ].

3.2-4 View
‣ View( t )( method )

The method View applied on a PredicataTree t returns the object text.

gap> t:=PredicataTree("root");;
gap> View(t);
< PredicataTree: [ "root" ] >

3.2-5 Print
‣ Print( t )( method )

The method Print prints the PredicataTree t as a string.

gap> t:=PredicataTree("root");;
gap> Print(t);
PredicataTree: [ "root" ]

3.2-6 IsEmptyPredicataTree
‣ IsEmptyPredicataTree( t )( function )

The function IsEmptyPredicataTree checks if a given PredicataTree t is empty.

gap> t:=PredicataTree("root");
< PredicataTree: [ "root" ] >
gap> IsEmptyPredicataTree(t);
false

3.2-7 RootOfPredicataTree
‣ RootOfPredicataTree( t )( function )

The function RootOfPredicataTree returns the current root of the PredicataTree t.

gap> t:=PredicataTree("current root");
< PredicataTree: [ "current root" ] >
gap> RootOfPredicataTree(t);
"current root"

3.2-8 SetRootOfPredicataTree
‣ SetRootOfPredicataTree( t, n )( function )

The function SetRootOfPredicataTree changes the current root of the PredicataTree t to the input n.

gap> SetRootOfPredicataTree(t, "element #2");
gap> t:=PredicataTree("element #1");
< PredicataTree: [ "element #1" ] >
gap> SetRootOfPredicataTree(t, "element #2");
gap> Display(t);
PredicataTree: [ "element #2" ].

3.2-9 InsertChildToPredicataTree
‣ InsertChildToPredicataTree( t )( function )

The function InsertChildToPredicataTree inserts a child to the current PredicataTree t.

gap> t:=PredicataTree("root");
< PredicataTree: [ "root" ] >
gap> InsertChildToPredicataTree(t);
gap> Display(t);
PredicataTree: [ "root", [ ] ].
gap> InsertChildToPredicataTree(t);
gap> Display(t);
PredicataTree: [ "root", [ ], [ ] ].

3.2-10 ChildOfPredicataTree
‣ ChildOfPredicataTree( t, i )( function )

The function ChildOfPredicataTree" enters the i-th child of the current PredicataTree t.

gap> t:=PredicataTree("root");
< PredicataTree: [ "root" ] >
gap> InsertChildToPredicataTree(t);
gap> ChildOfPredicataTree(t, 1);
< PredicataTree: [ "root", [ ] ] >
gap> SetRootOfPredicataTree(t, "child 1");
gap> Display(t);
PredicataTree: [ "root", [ "child 1" ] ].

3.2-11 NumberOfChildrenOfPredicataTree
‣ NumberOfChildrenOfPredicataTree( t )( function )

The function NumberOfChildrenOfPredicataTree returns the number of children of the current PredicataTree t.

gap> t:=PredicataTree("root");
< PredicataTree: [ "root" ] >
gap> NumberOfChildrenOfPredicataTree(t);
0
gap> InsertChildToPredicataTree(t);
gap> InsertChildToPredicataTree(t);
gap> NumberOfChildrenOfPredicataTree(t);
2
gap> ChildOfPredicataTree(t, 1);
< PredicataTree: [ "root", [ ], [ ] ] >
gap> SetRootOfPredicataTree(t, "child 1");
gap> Display(t);
PredicataTree: [ "root", [ "child 1" ], [ ] ].
gap> NumberOfChildrenOfPredicataTree(t);
0
gap> InsertChildToPredicataTree(t);
gap> InsertChildToPredicataTree(t);
gap> NumberOfChildrenOfPredicataTree(t);
2
gap> Display(t);
PredicataTree: [ "root", [ "child 1", [ ], [ ] ], [ ] ].

3.2-12 ParentOfPredicataTree
‣ ParentOfPredicataTree( t )( function )

The function ParentOfPredicataTree goes back to the parent of the current PredicataTree t.

gap> t:=PredicataTree("root");
< PredicataTree: [ "root" ] >
gap> InsertChildToPredicataTree(t);
gap> InsertChildToPredicataTree(t);
gap> Display(t);
PredicataTree: [ "root", [ ], [ ] ].
gap> ChildOfPredicataTree(t, 1);
< PredicataTree: [ "root", [ ], [ ] ] >
gap> SetRootOfPredicataTree(t, "child 1");     
gap> ParentOfPredicataTree(t);
< PredicataTree: [ "root", [ "child 1" ], [ ] ] >
gap> ChildOfPredicataTree(t, 2);
< PredicataTree: [ "root", [ "child 1" ], [ ] ] >
gap> SetRootOfPredicataTree(t, "child 2");
gap> Display(t);
PredicataTree: [ "root", [ "child 1" ], [ "child 2" ] ].

3.2-13 ReturnedChildOfPredicataTree
‣ ReturnedChildOfPredicataTree( t, i )( function )

The function ReturnedChildOfPredicataTree returns the i-th child of the current PredicataTree t as a new tree.

gap> t:=PredicataTree("root");
< PredicataTree: [ "root" ] >
gap> InsertChildToPredicataTree(t);
gap> ChildOfPredicataTree(t, 1);
< PredicataTree: [ "root", [ ], [ ] ] >
gap> SetRootOfPredicataTree(t, "child 1");     
gap> ParentOfPredicataTree(t);
gap> r:=ReturnedChildOfPredicataTree(t, 1);
< PredicataTree: [ "child 1" ] >

3.2-14 PredicataFormulaFormattedToTree
‣ PredicataFormulaFormattedToTree( F )( function )

The function converts a PredicataFormulaFormatted (3.1-11) F to a PredicataTree.

gap> f:=PredicataFormula("(E y: x+y=z and y = x)");
< PredicataFormula: ( E y : x + y = z and y = x ) >
gap> F:=PredicataFormulaFormatted(f);
< PredicataFormulaFormatted: ( E y : ( ( ( x + y ) = z ) and ( y = x ) ) ) >
gap> t:=PredicataFormulaFormattedToTree(F);
< PredicataTree: [ "E", [ "y" ], [ "and", 
[ "=", [ "+", [ "x" ], [ "y" ] ], [ "z" ] ], [ "=", [ "y" ], [ "x" ] ] ] ] >

3.2-15 FreeVariablesOfPredicataTree
‣ FreeVariablesOfPredicataTree( t )( function )

The function FreeVariablesOfPredicataTree returns the free variables of the PredicataTree t, which have been carried over from the PredicataFormula (3.1-4) and the PredicataFormulaFormatted (3.1-11).

gap> f:=PredicataFormula("(E y: x+y=z and y = x)");
< PredicataFormula: ( E y : x + y = z and y = x ) >
gap> F:=PredicataFormulaFormatted(f);
< PredicataFormulaFormatted: ( E y : ( ( ( x + y ) = z ) and ( y = x ) ) ) >
gap> t:=PredicataFormulaFormattedToTree(F);
< PredicataTree: [ "E", [ "y" ], [ "and", [ "=", [ "+", [ "x" ], [ "y" ] ],
[ "z" ] ], [ "=", [ "y" ], [ "x" ] ] ] ] >
gap> FreeVariablesOfPredicataTree(t);
[ "x", "z" ]

3.2-16 BoundedVariablesOfPredicataTree
‣ BoundedVariablesOfPredicataTree( t )( function )

The function BoundedVariablesOfPredicataTree returns the bounded variables of the PredicataTree t, which have been carried over from the PredicataFormula (3.1-4) and the PredicataFormulaFormatted (3.1-11).

gap> f:=PredicataFormula("(E y: x+y=z and y = x)"); 
< PredicataFormula: ( E y : x + y = z and y = x ) >
gap> F:=PredicataFormulaFormatted(f);
< PredicataFormulaFormatted: ( E y : ( ( ( x + y ) = z ) and ( y = x ) ) ) >
gap> t:=PredicataFormulaFormattedToTree(F);
< PredicataTree: [ "E", [ "y" ], [ "and", [ "=", [ "+", [ "x" ], [ "y" ] ], 
[ "z" ] ], [ "=", [ "y" ], [ "x" ] ] ] ] >
gap> BoundedVariablesOfPredicataTree(t);
[ "y" ]

3.2-17 PredicataTreeToPredicaton
‣ PredicataTreeToPredicaton( t[, V] )( function )

The function PredicataTreeToPredicaton calls PredicataTreeToPredicatonRecursive (3.2-18) to turn a PredicataTree (3.2-1) t into a Predicaton (2.1-1). The optional argument V allows to specify an order for the free variables in the tree.

gap> f:=PredicataFormula("(E y: x+y=z and y = x)");   
< PredicataFormula: ( E y : x + y = z and y = x ) >
gap> F:=PredicataFormulaFormatted(f);
< PredicataFormulaFormatted: ( E y : ( ( ( x + y ) = z ) and ( y = x ) ) ) >
gap> t:=PredicataFormulaFormattedToTree(F);
< PredicataTree: [ "E", [ "y" ], [ "and", [ "=", [ "+", [ "x" ], [ "y" ] ], 
[ "z" ] ], [ "=", [ "y" ], [ "x" ] ] ] ] >
gap> P:=PredicataTreeToPredicaton(t);
[ "Pred", < Predicata: deterministic finite automaton on 4 letters with 3 states 
and the variable position list [ 1, 2 ]. > ]
gap> Display(P[2]);
Predicata: deterministic finite automaton on 4 letters with 3 states, 
the variable position list [ 1, 2 ] and the following transitions:
            |  1  2  3  
------------------------
  [ 0, 0 ]  |  3  2  3  
  [ 1, 0 ]  |  3  1  3  
  [ 0, 1 ]  |  2  3  3  
  [ 1, 1 ]  |  1  3  3  
 Initial states: [ 2 ]
 Final states:   [ 2 ]

 The alphabet corresponds to the following variable list: [ "x", "z" ].

3.2-18 PredicataTreeToPredicatonRecursive
‣ PredicataTreeToPredicatonRecursive( t, V )( function )

The function PredicataTreeToPredicatonRecursive is called by PredicataTreeToPredicaton (3.2-17) in order to convert a PredicataTree t into a Predicata. The list V contains as first entry a list of free variables (not necessarily occurring) and as second entry a list containing the previous variables together with all bounded variables. This function goes down into the tree recursively until it reaches its leaves. Upon going up it creates the automaton of the Predicaton with relation to the variable position list.

gap> F:=PredicataFormulaFormatted(PredicataFormula("(E y: x+y=z and y = x)"));;
gap> t:=PredicataFormulaFormattedToTree(F);;
gap> P:=PredicataTreeToPredicatonRecursive(t, [[ "x", "z" ], [ "x", "y", "z" ]]);;
gap> Display(P[2]);
Predicata: deterministic finite automaton on 4 letters with 3 states, 
the variable position list [ 1, 3 ] and the following transitions:
            |  1  2  3  
------------------------
  [ 0, 0 ]  |  3  2  3  
  [ 1, 0 ]  |  3  1  3  
  [ 0, 1 ]  |  2  3  3  
  [ 1, 1 ]  |  1  3  3  
 Initial states: [ 2 ]
 Final states:   [ 2 ]

3.2-19 PredicataRepresentationOfPredicataTree
‣ PredicataRepresentationOfPredicataTree( t )( function )

The function PredicataRepresentationOfPredicataTree returns the PredicataRepresentation of a PredicataTree t. For more details see PredicataRepresentation (3.3-10).

gap> t:=PredicataTree("root");;
gap> PredicataRepresentationOfPredicataTree(t);
< PredicataRepresentation containing the following predicates: [ ]. >

3.3 PredicataRepresentation – Predicata assigned with names and arities

This section explains how to assign a name and an arity to a Predicata such that it can be reused in a PredicataFormula (3.1-4). The idea is to create elements containing the name, arity and the Predicata and combining them in a PredicataRepresentation (3.3-10). Additionally, there is a predefined variable PredicataList (3.3-23), which is called by the PredicataFormula on default, trying to simplify these quite lengthy construction.

3.3-1 PredicatonRepresentation
‣ PredicatonRepresentation( name, arity, automaton )( function )

The function PredicatonRepresentation creates the representation of a Predicaton, assigned with a name, an arity and an automaton (input may also be a Predicaton), allowing it to be called in a PredicataFormula (3.1-4) with Name[x1,...xN] (where N is the arity).

gap> A:=Predicaton(Automaton("det", 3, [ [ 0, 0, 0 ], [ 1, 0, 0 ], [ 0, 1, 0 ], 
> [ 1, 1, 0 ], [ 0, 0, 1 ], [ 1, 0, 1 ], [ 0, 1, 1 ], [ 1, 1, 1 ] ], 
> [ [ 1, 3, 3 ], [ 3, 2, 3 ], [ 3, 2, 3 ], [ 2, 3, 3 ], [ 3, 1, 3 ], 
> [ 1, 3, 3 ], [ 1, 3, 3 ], [ 3, 2, 3 ] ], [ 1 ], [ 1 ]), [ 1, 2, 3 ]);;
gap> p:=PredicatonRepresentation("MyAdd", 3, A);
< Predicaton represented with the name: "MyAdd", the arity: 3 
and the deterministic automaton on 8 letters and 3 states. >

3.3-2 IsPredicatonRepresentation
‣ IsPredicatonRepresentation( p )( function )

The function IsPredicatonRepresentation checks if the argument p is a PredicatonRepresentation.

gap> A:=Predicaton(Automaton("det", 2, [ [ 0 ], [ 1 ] ], [ [ 1, 2 ], [ 2, 2 ] ],
> [ 1 ], [ 1 ]), [ 1 ]);;
gap> p:=PredicatonRepresentation("EqualZero", 1, A);
< Predicaton represented with the name "EqualZero", the arity 1 and 
the deterministic automaton on 2 letters and 2 states. >
gap> IsPredicatonRepresentation(p);
true

3.3-3 Display
‣ Display( p )( method )

The method Display prints the PredicatonRepresentation p.

gap> A:=Predicaton(Automaton("det", 2, [ [ 0 ], [ 1 ] ], [ [ 1, 2 ], [ 2, 2 ] ], 
> [ 1 ], [ 1 ]), [ 1 ]);;
gap> p:=PredicatonRepresentation("EqualZero", 1, A);;
gap> Display(p);
Predicata represented with the name: EqualZero, the arity: 1 and 
the following automaton: 
deterministic finite automaton on 2 letters with 2 states and 
the following transitions:
         |  1  2  
------------------
  [ 0 ]  |  1  2  
  [ 1 ]  |  2  2  
 Initial states: [ 1 ]
 Final states:   [ 1 ]

3.3-4 View
‣ View( p )( method )

The method View applied on a PredicatonRepresentation p returns the object text.

gap> A:=Automaton("det", 4, [ [ 0, 0 ], [ 1, 0 ], [ 0, 1 ], [ 1, 1 ] ],
> [ [ 1, 2, 2, 3 ], [ 2, 2, 4, 2 ], [ 2, 2, 1, 2 ], [ 3, 2, 2, 4 ] ],
> [ 1 ], [ 1 ]);;
gap> p:=PredicatonRepresentation("MultipleOfThree", 2, A);;
gap> View(p);
< Predicaton represented with the name "MultipleOfThree", the arity 2 and 
the deterministic automaton on 4 letters and 4 states. >

3.3-5 Print
‣ Print( p )( method )

The method Print prints the PredicatonRepresentation p as a string.

gap> A:=Predicaton(Automaton("det", 2, [ [ 0 ], [ 1 ] ], [ [ 1, 2 ], [ 2, 2 ] ],
> [ 1 ], [ 2 ]), [ 1 ]);;
gap> p:=PredicatonRepresentation("GreaterZero", 1, A);;
gap> Print(p);
PredicatonRepresentation("GreaterZero", 1, Automaton("det", 2,\
[ [ 0 ], [ 1 ] ], [ [ 1, 2 ], [ 2, 2 ] ], [ 1 ], [ 2 ]))
gap> String(p);
"PredicatonRepresentation(\"GreaterZero\", 1, Automaton(\"det\", 2,\
[ [ 0 ], [ 1 ] ], [ [ 1, 2 ], [ 2, 2 ] ], [ 1 ], [ 2 ]))"

3.3-6 NameOfPredicatonRepresentation
‣ NameOfPredicatonRepresentation( p )( function )

The function NameOfPredicatonRepresentation returns the name of p.

gap> A:=Predicaton(Automaton("det", 4, [ [ 0 ], [ 1 ] ], [ [ 4, 2, 3, 3 ],
> [ 3, 3, 3, 2 ] ], [ 1 ], [ 3, 4, 1 ]), [ 1 ]);;
gap> p:=PredicatonRepresentation("NotTwo", 1, A);;
gap> NameOfPredicatonRepresentation(p);
"NotTwo"

3.3-7 ArityOfPredicatonRepresentation
‣ ArityOfPredicatonRepresentation( p )( function )

The function ArityOfPredicatonRepresentation returns the arity of p.

gap> A:=Predicaton(Automaton("det", 4, [ [ 0 ], [ 1 ] ], [ [ 4, 2, 3, 3 ],
> [ 3, 3, 3, 2 ] ], [ 1 ], [ 3, 4, 1 ]), [ 1 ]);;
gap> p:=PredicatonRepresentation("NotTwo", 1, A);;
gap> ArityOfPredicatonRepresentation(p);
1

3.3-8 AutOfPredicatonRepresentation
‣ AutOfPredicatonRepresentation( p )( function )

The function AutOfPredicatonRepresentation returns the automaton of p.

gap> A:=Predicaton(Automaton("det", 4, [ [ 0 ], [ 1 ] ], [ [ 4, 2, 3, 3 ],
> [ 3, 3, 3, 2 ] ], [ 1 ], [ 3, 4, 1 ]), [ 1 ]);;
gap> p:=PredicatonRepresentation("NotTwo", 1, A);;
gap> AutOfPredicatonRepresentation(p);
< deterministic automaton on 2 letters with 4 states >

3.3-9 CopyPredicatonRepresentation
‣ CopyPredicatonRepresentation( p )( function )

The function CopyPredicatonRepresentation copies p.

gap> A:=Automaton("det", 3, [ [ 0, 0 ], [ 1, 0 ], [ 0, 1 ], [ 1, 1 ] ],
> [ [ 1, 3, 3 ], [ 2, 3, 3 ], [ 3, 1, 3 ], [ 3, 2, 3 ] ], [ 1 ], [ 1 ]);;
gap> p:=PredicatonRepresentation("CopyPred", 2, A);;
gap> q:=CopyPredicatonRepresentation(p);
< Predicaton represented with the name "CopyPred", the arity 2 and 
the deterministic automaton on 4 letters and 3 states. >

3.3-10 PredicataRepresentation
‣ PredicataRepresentation( [l] )( function )

The function PredicataRepresentation creates a collection of elements (PredicatonRepresentation (3.3-1)), where the list l may contain arbitrary many of them. The PredicataRepresentation is an optional input for the function PredicataFormula (3.1-4) (On default it uses the predefined variable PredicataList (3.3-23)). Note that the variables must be unique within one predicate call.

gap> A1:=Predicaton(Automaton("det", 3, [ [ 0, 0, 0 ], [ 1, 0, 0 ], [ 0, 1, 0 ], 
> [ 1, 1, 0 ], [ 0, 0, 1 ], [ 1, 0, 1 ], [ 0, 1, 1 ], [ 1, 1, 1 ] ], 
> [ [ 1, 3, 3 ], [ 3, 2, 3 ], [ 3, 2, 3 ], [ 2, 3, 3 ], [ 3, 1, 3 ], 
> [ 1, 3, 3 ], [ 1, 3, 3 ], [ 3, 2, 3 ] ], [ 1 ], [ 1 ]), [ 1, 2, 3 ]);;
gap> p1:=PredicatonRepresentation("MyAdd", 3, A1);
< Predicaton represented with the name "MyAdd", the arity 3 and 
the deterministic automaton on 8 letters and 3 states. >
gap> A2:=Predicaton(Automaton("det", 2, [ [ 0, 0 ], [ 1, 0 ], [ 0, 1 ], [ 1, 1 ] ],
> [ [ 1, 2 ], [ 2, 2 ], [ 2, 2 ], [ 1, 2 ] ], [ 1 ], [ 1 ]), [ 1, 2 ]);;
gap> p2:=PredicatonRepresentation("MyEqual", 2, A2);;
gap> P:=PredicataRepresentation(p1, p2);
< PredicataRepresentation containing the following predicates: 
[ "MyEqual", "MyAdd"]. >
gap> f:=PredicataFormula("MyAdd[x,y,z] and MyEqual[x,y]", P);
< PredicataFormula: MyAdd [ x , y , z ] and MyEqual [ x , y ] >

3.3-11 IsPredicataRepresentation
‣ IsPredicataRepresentation( P )( function )

The function IsPredicataRepresentation checks if the argument P is a PredicataRepresentation.

gap> # Continued example: PredicataRepresentation
gap> IsPredicataRepresentation(P);
true

3.3-12 Display
‣ Display( p )( method )

The method Display prints the PredicataRepresentation P.

gap> # Continued example: PredicataRepresentation
gap> Display(P);
Predicata representation containing the following PredicatonRepresentations:
Predicata represented with the name: MyEqual, the arity: 2 and 
the following automaton:
deterministic finite automaton on 4 letters with 2 states and 
the following transitions:
            |  1  2  
---------------------
  [ 0, 0 ]  |  1  2  
  [ 1, 0 ]  |  2  2  
  [ 0, 1 ]  |  2  2  
  [ 1, 1 ]  |  1  2  
 Initial states: [ 1 ]
 Final states:   [ 1 ]
Predicata represented with the name: MyAdd, the arity: 3 and 
the following automaton:
deterministic finite automaton on 8 letters with 3 states and 
the following transitions:
               |  1  2  3  
---------------------------
  [ 0, 0, 0 ]  |  1  3  3  
  [ 1, 0, 0 ]  |  3  2  3  
  [ 0, 1, 0 ]  |  3  2  3  
  [ 1, 1, 0 ]  |  2  3  3  
  [ 0, 0, 1 ]  |  3  1  3  
  [ 1, 0, 1 ]  |  1  3  3  
  [ 0, 1, 1 ]  |  1  3  3  
  [ 1, 1, 1 ]  |  3  2  3  
 Initial states: [ 1 ]
 Final states:   [ 1 ]

3.3-13 View
‣ View( P )( method )

The method View applied on a PredicataRepresentation P returns the object text.

gap> P:=PredicataRepresentation();;
gap> View(P);
< PredicataRepresentation containing the following predicates: [ ]. >

3.3-14 Print
‣ Print( P )( method )

The method Print prints the PredicataRepresentation P as a string.

gap> # Continued example: PredicataRepresentation
gap> Print(P);
PredicataRepresentation(PredicatonRepresentation("MyEqual", 2, Automaton\
("det", 2, [ [ 0, 0 ], [ 1, 0 ], [ 0, 1 ], [ 1, 1 ] ], [ [ 1, 2 ], [ 2, 2 ], [\
 2, 2 ], [ 1, 2 ] ], [ 1 ], [ 1 ])), PredicatonRepresentation("MyAdd", 3\
, Automaton("det", 3, [ [ 0, 0, 0 ], [ 1, 0, 0 ], [ 0, 1, 0 ], [ 1, 1, 0 ], [ \
0, 0, 1 ], [ 1, 0, 1 ], [ 0, 1, 1 ], [ 1, 1, 1 ] ], [ [ 1, 3, 3 ], [ 3, 2, 3 ]\
, [ 3, 2, 3 ], [ 2, 3, 3 ], [ 3, 1, 3 ], [ 1, 3, 3 ], [ 1, 3, 3 ], [ 3, 2, 3 ]\
 ], [ 1 ], [ 1 ])))
gap> String(P);
"PredicataRepresentation(PredicatonRepresentation(\"MyEqual\", 2, Automa\
ton(\"det\", 2, [ [ 0, 0 ], [ 1, 0 ], [ 0, 1 ], [ 1, 1 ] ], [ [ 1, 2 ], [ 2, 2\
 ], [ 2, 2 ], [ 1, 2 ] ], [ 1 ], [ 1 ])), PredicatonRepresentation(\"MyA\
dd\", 3, Automaton(\"det\", 3, [ [ 0, 0, 0 ], [ 1, 0, 0 ], [ 0, 1, 0 ], [ 1, 1\
, 0 ], [ 0, 0, 1 ], [ 1, 0, 1 ], [ 0, 1, 1 ], [ 1, 1, 1 ] ], [ [ 1, 3, 3 ], [ \
3, 2, 3 ], [ 3, 2, 3 ], [ 2, 3, 3 ], [ 3, 1, 3 ], [ 1, 3, 3 ], [ 1, 3, 3 ], [ \
3, 2, 3 ] ], [ 1 ], [ 1 ])), PredicatonRepresentation(\"GreaterZero\", 1\
, Automaton(\"det\", 2, [ [ 0 ], [ 1 ] ], [ [ 1, 2 ], [ 2, 2 ] ], [ 1 ], [ 2 ]\
)))"

3.3-15 NamesOfPredicataRepresentation
‣ NamesOfPredicataRepresentation( P )( function )

The function NamesOfPredicataRepresentation returns the names of P.

gap> # Continued example: PredicataRepresentation
gap> NamesOfPredicataRepresentation(P);
[ "MyEqual", "MyAdd" ]

3.3-16 AritiesOfPredicatonRepresentation
‣ AritiesOfPredicatonRepresentation( P )( function )

The function AritiesOfPredicatonRepresentation returns the arities of P.

gap> # Continued example: PredicataRepresentation
gap> AritiesOfPredicataRepresentation(P);
[ 2, 3 ]

3.3-17 AutsOfPredicataRepresentation
‣ AutsOfPredicataRepresentation( P )( function )

The function AutOfPredicataRepresentation returns the automaton of P.

gap> # Continued example: PredicataRepresentation
gap> AutsOfPredicataRepresentation(P);
[ < deterministic automaton on 4 letters with 2 states >, 
  < deterministic automaton on 8 letters with 3 states > ]

3.3-18 ElementOfPredicataRepresentation
‣ ElementOfPredicataRepresentation( P, i )( function )

The function ElementOfPredicataRepresentation returns the i-th element as a PredicatonRepresentation (3.3-1).

gap> # Continued example: PredicataRepresentation
gap> ElementOfPredicataRepresentation(P, 1);
< Predicaton represented with the name "MyEqual", the arity 2 and 
the deterministic automaton on 4 letters and 2 states. >

3.3-19 Add
‣ Add( P, p )( method )

The method Add adds the PredicatonRepresentation p to P.

gap> # Continued example: PredicataRepresentation
gap> A3:=Predicaton(Automaton("det", 2, [ [ 0 ], [ 1 ] ], [ [ 1, 2 ], [ 2, 2 ] ], 
> [ 1 ], [ 2 ]), [ 1 ]);;
gap> p3:=PredicatonRepresentation("GreaterZero", 1, A3);;
gap> Add(P, p3);
gap> P;
< PredicataRepresentation containing the following predicates: 
[ "MyEqual", "MyAdd", "GreaterZero" ]. >

3.3-20 Add
‣ Add( P, name, arity, automaton )( method )

The method Add adds the PredicatonRepresentation created from name, arity and automaton to P.

gap> # Continued example: PredicataRepresentation
gap> A4:=Predicaton(Automaton("det", 2, [ [ 0 ], [ 1 ] ], [ [ 1, 2 ], [ 2, 2 ] ], 
> [ 1 ], [ 1 ]), [ 1 ]);;
gap> Add(P, "EqualZero", 1, A4);
gap> P;
< PredicataRepresentation containing the following predicates: 
[ "MyEqual", "MyAdd", "GreaterZero", "EqualZero" ]. >

3.3-21 Remove
‣ Remove( P, i )( method )

The method Remove removes the i-th element of P.

gap> A5:=Predicaton(Automaton("det", 4, [ [ 0 ], [ 1 ] ], [ [ 4, 2, 3, 3 ],
> [ 3, 3, 3, 2 ] ], [ 1 ], [ 3, 4, 1 ]), [ 1 ]);;
gap> p5:=PredicatonRepresentation("NotTwo", 1, A5);;
gap> Add(P, p5);
gap> P;
< PredicataRepresentation containing the following predicates: 
[ "NotTwo", "MyEqual", "MyAdd", "GreaterZero", "EqualZero" ]. >
gap> Remove(P, 1);
< Predicaton represented with the name "NotTwo", the arity 1 and 
the deterministic automaton on 2 letters and 4 states. >
gap> P;
< PredicataRepresentation containing the following predicates: 
[ "MyEqual", "MyAdd", "GreaterZero", "EqualZero" ]. >

3.3-22 CopyPredicataRepresentation
‣ CopyPredicataRepresentation( P )( function )

The function CopyPredicataRepresentation copies the PredicataRepresentation P.

gap> A:=Automaton("det", 3, [ [ 0, 0 ], [ 1, 0 ], [ 0, 1 ], [ 1, 1 ] ],
> [ [ 1, 3, 3 ], [ 2, 3, 3 ], [ 3, 1, 3 ], [ 3, 2, 3 ] ], [ 1 ], [ 1 ]);;
gap> p:=PredicatonRepresentation("CopyPred", 2, A);;
gap> P:=PredicataRepresentation(p);
< PredicataRepresentation containing the following predicates: [ "CopyPred" ]. >
gap> Q:=CopyPredicataRepresentation(P);
< PredicataRepresentation containing the following predicates: [ "CopyPred" ]. >

3.3-23 PredicataList
‣ PredicataList( global variable )

The variable PredicataList is a PredicataRepresentation (3.3-10) which is called on default by the PredicataFormula (3.1-4). Together with the functions AddToPredicataList (3.3-24) and RemoveFromPredicataList (3.3-26) the intention is to be able to use own predicates without specifying to much.

gap> PredicataList;
< PredicataRepresentation containing the following predicates: [  ]. >
gap> A1:=Predicaton(Automaton("det", 3, [ [ 0, 0, 0 ], [ 1, 0, 0 ], [ 0, 1, 0 ], 
> [ 1, 1, 0 ], [ 0, 0, 1 ], [ 1, 0, 1 ], [ 0, 1, 1 ], [ 1, 1, 1 ] ], 
> [ [ 1, 3, 3 ], [ 3, 2, 3 ], [ 3, 2, 3 ], [ 2, 3, 3 ], [ 3, 1, 3 ], 
> [ 1, 3, 3 ], [ 1, 3, 3 ], [ 3, 2, 3 ] ], [ 1 ], [ 1 ]), [ 1, 2, 3 ]);;
gap> p1:=PredicatonRepresentation("MyAdd", 3, A1);;
gap> Add(PredicataList, p1);
gap> PredicataList;
< PredicataRepresentation containing the following predicates: [ "MyAdd" ]. >
gap> f:=PredicataFormula("MyAdd[x,y,z]");
< PredicataFormula: MyAdd [ x , y , z ] >

3.3-24 AddToPredicataList
‣ AddToPredicataList( p[, arity, automaton] )( function )

The function AddToPredicataList adds either a PredicatonRepresentation p or the created one with p being a string (name) as well as the arity and the automaton to PredicataList.

gap> # Continued example: PredicataList
gap> A2:=Predicaton(Automaton("det", 2, [ [ 0, 0 ], [ 1, 0 ], [ 0, 1 ], [ 1, 1 ] ],
> [ [ 1, 2 ], [ 2, 2 ], [ 2, 2 ], [ 1, 2 ] ], [ 1 ], [ 1 ]), [ 1, 2 ]);;
gap> p2:=PredicatonRepresentation("MyEqual", 2, A2);;
gap> AddToPredicataList(p2);
gap> A3:=Predicaton(Automaton("det", 2, [ [ 0 ], [ 1 ] ], [ [ 1, 2 ], [ 2, 2 ] ], 
> [ 1 ], [ 2 ]), [ 1 ]);;
gap> AddToPredicataList("GreaterZero", 1, A3);
gap> PredicataList;
gap> f:=PredicataFormula("MyAdd[x,y,z] and MyEqual[x,y]");
< PredicataFormula: MyAdd [ x , y , z ] and MyEqual [ x , y ] >

3.3-25 ClearPredicataList
‣ ClearPredicataList( )( function )

The function ClearPredicataList clears the PredicataList.

gap> # Continued example: PredicataList
gap> ClearPredicataList();
gap> PredicataList;
< PredicataRepresentation containing the following predicates: [ ]. >

3.3-26 RemoveFromPredicataList
‣ RemoveFromPredicataList( i )( function )

The function RemoveFromPredicataList removes the i-th element of the PredicataList.

gap> A:=Predicaton(Automaton("det", 4, [ [ 0 ], [ 1 ] ], [ [ 4, 2, 3, 3 ],
> [ 3, 3, 3, 2 ] ], [ 1 ], [ 3, 4, 1 ]), [ 1 ]);;
gap> AddToPredicataList("NotTwo", 1, A);
gap> PredicataList;
< PredicataRepresentation containing the following predicates: [ "NotTwo" ]. >
gap> RemoveFromPredicataList(1);
gap> PredicataList;
< PredicataRepresentation containing the following predicates: [ ]. >

3.4 Converting PredicataFormulas via PredicataTrees into Predicata

3.4-1 PredicataFormulaToPredicaton
‣ PredicataFormulaToPredicaton( f[, V] )( function )

The function PredicataFormulaToPredicaton takes a PredicataFormula (3.1-4) f and returns a Predicata which language recognizes the solutions of formula f. The input f must be a first-order formula containing the operations addition+ and the constant multiplication * (as a shortcut), see PredicataGrammar (4.1-1). The optional parameter V (list containing strings) allows to set an order of the free variables occurring in f. Note that the variables must not necessarily occur in the formula (for example x = 4 and V:=["x","y"]).

gap> f:=PredicataFormula("x = 4");
< PredicataFormula: x = 4 >
gap> A:=PredicataFormulaToPredicaton(f);
Predicata: deterministic finite automaton on 2 letters with 5 states, 
the variable position list [ 1 ] and the following transitions:
         |  1  2  3  4  5  
---------------------------
  [ 0 ]  |  4  2  2  3  5  
  [ 1 ]  |  2  2  5  2  2  
 Initial states: [ 1 ]
 Final states:   [ 5 ]

 The alphabet corresponds to the following variable list: [ "x" ].

 Regular expression of the automaton:
   [ 0 ][ 0 ][ 1 ][ 0 ]*

 Output:
< Predicata: deterministic finite automaton on 2 letters with 5 states 
and the variable position list [ 1 ]. >

3.4-2 StringToPredicaton
‣ StringToPredicaton( f[, V] )( function )

The function StringToPredicaton is the simpler version of PredicataFormulaToPredicaton (3.4-1), it takes an String f, converts it to a PredicataFormula and returns a Predicata. The optional parameter V allows to set an order for the variables.

gap> A:=StringToPredicaton("x+y = z");
Predicata: deterministic finite automaton on 8 letters with 3 states, 
the variable position list [ 1, 2, 3 ] and the following transitions:
               |  1  2  3  
---------------------------
  [ 0, 0, 0 ]  |  1  3  3  
  [ 1, 0, 0 ]  |  3  2  3  
  [ 0, 1, 0 ]  |  3  2  3  
  [ 1, 1, 0 ]  |  2  3  3  
  [ 0, 0, 1 ]  |  3  1  3  
  [ 1, 0, 1 ]  |  1  3  3  
  [ 0, 1, 1 ]  |  1  3  3  
  [ 1, 1, 1 ]  |  3  2  3  
 Initial states: [ 1 ]
 Final states:   [ 1 ]

 The alphabet corresponds to the following variable list: [ "x", "y", "z" ].

 Regular expression of the automaton:
   ([ 1, 1, 0 ]([ 1, 0, 0 ]U[ 0, 1, 0 ]U[ 1, 1, 1 ])*
   [ 0, 0, 1 ]U[ 0, 0, 0 ]U[ 1, 0, 1 ]U[ 0, 1, 1 ])*

 Output:
< Predicata: deterministic finite automaton on 8 letters with 3 states 
and the variable position list [ 1, 2, 3 ]. >
 [Top of Book]  [Contents]   [Previous Chapter]   [Next Chapter] 
Goto Chapter: Top 1 2 3 4 Bib Ind

generated by GAPDoc2HTML