cl-banner

FORT 0.2


Description
In this document the usage of FORT is described. If you are Windows user,
replace every occurrence of "./fort" by "fort.exe". Type

    ./fort -h

for a shorter version of this document.

---------------------------------------------------------------------------

VERSION

Type

    ./fort -v

to get the version of FORT.

---------------------------------------------------------------------------

DECISION TOOL

In order to use FORT as a decision tool type

    ./fort -D  [] ""

The  specifies the property that should be tested on the TRS 
specified in . The syntax of TRSs follows the standard TPDB format. 
The optional  parameter takes a value in { 0, 1, 2 }. The higher
the number the more detailed the output will be. The default value is 0. 
The syntax of  is explained below. The quotation marks surrounding
it are essential. 

---------------------------------------------------------------------------

SYNTHESIS TOOL

There are two ways to call the synthesis tool. The first one

    ./fort -S [options] ""

specifies the formula on the command line. The search space is restricted
by the following optional parameters:

    -f 
    -v 
    -r 
    -s 
    -d 

The signature  is specified as a comma separated list of function
symbols and arities. For example, "a 0, g 1, h 1" specifies a constant a
and two unary symbols g and h. If no signature is given, FORT will
incrementally increase the signature starting from a single constant.
The other optional parameters are the maximum number  of different
variables, the maximum number  of rewrite rules, and the maximum size
 and depth  of terms in the rewrite rules. The default values are
 = 1,  = 3,  = 4, and  = 3.

The second way to call the synthesis tool

    ./fort -S [options] 

requires a  containing a line

    (FORMULA )

and optional lines

    (FUN )
    (VARIABLES )
    (RULES )
    (SIZE )
    (DEPTH )

corresponding to the optional parameters described above. 

---------------------------------------------------------------------------

SYNTAX OF FORMULAS

The syntax for  is given by the following EBNF:

     = 
              |   
              | '~'
              | (  )
              |   ()
  = '&' | '|' | '=>'
    = '->' | '->+' | '->*' | '->!' | '-||->' | '->e' | '->be' 
              | '<-' | '+<-' | '*<-' | '<-!' | '<-||-' | 'e<-' | 'be<-' 
              | '<->' | '<->*' | 'join' | 'meet' | '=' 
  = forall | exists
    = CR | WCR | SCR | SCR() | WN | UN | UN()
              | UNC | NFP | SN | diamond | diamond()
              | GCR | GWCR | WSCR | GSCR() | GUN | GUN()
              | GUNC | GNFP | Gdiamond | Gdiamond()
              | CR() | WCR() | SCR()
              | SCR(, ) | WN() | UN()
              | UN(, ) | NFP() | SN()
              | diamond() | diamond(, )
              | NF() | Fin(,)
    =  
              | '~'
              | (  )
     = '->' | '-||->'

Here  denotes any nonempty sequence of alphanumeric symbols that does
not start with a number, except the ones already used in the EBNF. Symbols
like '_', '+', '-', '*', '/' and some others are allowed as well. The
formula must be closed.

---------------------------------------------------------------------------

SEMANTICS OF FORMULAS

The meaning of the terminal symbols in the above EBNF is explained here.

    '~'    negates the formula following it
    '&'    denotes conjunction
    '|'    denoted disjunction
    '=>'   denotes implication

The usual binding precedence '~' > '&' > '|' > '=>' is adopted. The 
parentheses used for quantifiers may be omitted. Then quantification binds 
stronger than '&'. The following binary rewrite relations (and their 
inverses) can be used:

    '->'      one-step rewriting
    '->+'     transitive closure of '->'
    '->*'     transitive reflexive closure of '->'
    '->!'     rewriting to normal form
    '-||->'   parallel rewriting
    '->e'     one-step rewriting at the root
    '->be'    one-step rewriting below the root
    '<->'     one-step bidirectional rewriting
    '<->*'    conversion
    'join'    joinability
    'meet'    meetability
    '='       equality

The following properties can be used:

    CR   confluence (Church-Rosser property)
         "~exists s, t, u ((s -> t & s ->* u) & ~exists v (t ->* v & u ->* v))"

    WCR  local confluence (weak Church-Rosser property)
         "~exists s, t, u ((s -> t & s -> u) & ~exists v (t ->* v & u ->* v))"

    SCR  strong confluence
         "~exists s, t, u ((s -> t & s -> u) & ~exists v (t ->= v & u ->* v))"

    SCR()
         strong confluence with respect to 
  "~exists s, t, u ((s  t & s  u) & 
	 ~exists v (t = v & u * v))"

    WN   (weak) normalization
         "~exists s ~exists t (s ->! t)"

    UN   unique normal forms
         "~exists s, t, u ((s ->! t & s ->! u) & ~t = u)"

    UN()
         unique normal forms with respect to 
         "~exists s, t, u ((s ! t & s ! u) & ~t = u)"

    UNC  unique normal forms with respect to conversion
         "~exists s, t (((s <->* t & NF(s)) & NF(t)) & ~s = t)"

    NFP  normal form property
         "~exists s, t, u ((s -> t & s ->! u) & ~t ->! u)"

    SN   termination (strong normalization)
         "forall t Fin(->*, t) & ~exists u (u ->+ u)"

    CR()
          is confluent
 "~exists t, u (( -> t &  ->* u) & ~exists v (t ->* v & u ->* v))"

    WCR()
    SCR()
    SCR(, )
    WN() 
    UN()
    UN(, )
    NFP()
        modifying WCR, SCR, SCR(), WN, UN, UN(), 
        NFP accordingly

    SN() 
         is terminating
        "Fin(->+, ) & ~exists u ( ->* u & u ->+ u)"

    NF()
          is a normal form

    Fin(, )
         finiteness of the set of terms u such that the pair (, u)
         belongs to the binary relation 

---------------------------------------------------------------------------

To improve the performance of FORT, it is recommend to set certain OCAML
runtime options:

    export OCAMLRUNPARAM="s=16M,i=64M,o=150"
Nach oben scrollen