WANDA: A Higher-Order Termination Tool

User Documentation

WANDA is a command-line termination tool. Given a file describing a (higher-order) term rewriting system, she will return YES (the system is terminating), NO (the system is non-terminating) or MAYBE (termination status could not be determined).

In its most basic form, you invoke WANDA by typing: ./wanda.exe <benchmark>

File Formats:

file.afsm: An input file in applicative AFSM format, listing first function declarations, followed by an empty line, and then rules.
example afsm input file
file.xml: An input file in the format employed in the annual termination competition for the higher-order union beta category. These are Algebraic Functional Systems, so systems with both function application and application, but no meta-variables.
example xml input file
file.afs: An input file in "converted" xml format: WANDA's own human-readable variation of the competition's XML format.
example afs input file
file.atrs: A normal TRS input file in the human-readable format used in the termination competition, which represents an applicative TRS: there is only one binary function symbol; everything else has arity 0. If possible, this system is given a typing and treated as an applicative higher-order system. Note that WANDA's answer does not give information about termination of the original untyped system!
example atrs input file

Note that, internally, all these input formats are converted to the AFSM formalism, corresponding to the .afsm format.

Command-line arguments:

<filename>

The input file to analyse. If no file name is given, the user is prompted to type in a system in AFSM format. If several files are given, termination is analysed for all of them.

<time>

By default, a purely numeric input to WANDA is assumed to be the timeout. However, this number is completely ignored at this time.

--verbose, -v

Give additional comments during execution, such as describing what the tool is doing. When verbose is enabled, the proof output is printed during execution, rather than afterwards.

--silent, -s

By default WANDA prints YES/NO/MAYBE followed by an explanation (a proof, counter example or the reason why deciding was difficult). You can suppress this explanation by choosing silent mode.

--rewrite, -r

Rather than proving termination, the user is prompted to type in a term, and this term is rewritten following the rules.

--format=<format>, -f <format>

Rather than choosing the standard formalism associated with a file's extension, consider all input files in the given formalism.

--firstorder=<file>, -i <file>

WANDA uses a first-order termination prover, located in the resources/ directory, to prove termination of the first order part of the rules. With this argument you can indicate which file in the resources/ directory should be used. If none is indicated, WANDA will not attempt to use a first-order prover. If this is omitted, the file "firstorderprover" will be used (make sure that it is set as executable!).

--disable=<list>, -d <list>

You can disable certain features of WANDA; for example to disable non-termination proving and rule removal, use --disable=nt,rr or -d nt,rr (note that there is no space after the comma!). The things you can disable are:

nt: non-termination proving
rr: rule removal
dp: the dependency pair framework
static: static dependency pairs
dynamic: dynamic dependency pairs
sc: the subterm criterion
fr: formative rules
ur: usable rules
local: using tags and suchlike improvements for abstraction-simple (also sometimes called local) systems
graph: the dependency graph
poly: polynomial interpretations
pprod: polynomial interpretations with products
horpo: the recursive path ordering

--query=<property>, -q <property>

Query whether the system has the given property; outputs YES or NO and does nothing else. The property must be one of the following:

etalong
baseoutputs
local
pfp
strongpfp
leftlinear
fullyextended
algebraic (no meta-variables occur below an abstraction)
argumentfree (meta-variables do not take arguments)

--show, -w

Just show the system (possibly converting it to an AFSM first) and abort.

--debug, -D

Give additional debug information during execution. More verbose than --erbose, this is really just for debugging problems (for example, the entire formula table of HORPO is printed).

--style=<style>, -y <style>

Creates output of the given style for the proof; default is plain. Possible styles are:

html: creates a single html-page (unfinished)
plain: just ascii
ansi: just ascii, but with ansi-colour characters
utf: prints to the terminal using utf8-characters
ansiutf: prints to the terminal using utf8-characters and ansi-colour

--output=<filename>, -o <filename>

Prints only the YES/NO/MAYBE to stdout, and the rest to the given file.

Further notes

A default SAT-solver and a default first-order termination prover are supplied in the resources/ directory. Both can be replaced by other solvers, with similar input and output, provided they are given the same name. The expected input/output is that which is defined by the relevant competitions.

In addition, a non-termination prover is included in the resources/ directory. The given script is simply a placeholder which returns MAYBE. However, it can be replaced by any tool which takes a first-order TRS in standard human-readable format as input, and returns YES, NO or MAYBE, followed by a non-terminating term in the case of NO. Using this, WANDA can identify non-terminating systems if the first-order part is non-terminating. No suitable such tool is included because no open-source tools with these specifications exist at the moment.