Portability | unportable |
---|---|
Stability | unstable |
Maintainer | Martin Avanzini <martin.avanzini@uibk.ac.at> |
Safe Haskell | Safe-Infered |
Tct.Interactive
Contents
Description
This section describes the interactive interface of TcT (TcT-i for short),
for usage information on the command line interface, please
refer to Tct.
Since TcT-i relies on the Interpreter ghci
from the Glasgow
Haskell Compiler (http://www.haskell.org/ghc/), the interactive
interface is only available if ghci
is present on your system.
As explained in Tct.Configuration,
TcT can be easily customized. TcT-i makes use of this by loading
the configuration file, usually located in ${HOME}/.tct/tct.hs
.
The interactive interface is invoked from the command line as follows:
>>>
tct -i
GHCi, version 7.4.1: http://www.haskell.org/ghc/ :? for help ... Loading package tct-2.0 ... linking ... done. [1 of 1] Compiling Main ( tct.hs, interpreted ) Ok, modules loaded: Main. . Welcome to the TcT ------------------ . This is version 2.0 of the Tyrolean Complexity Tool. . (c) Martin Avanzini <martin.avanzini@uibk.ac.at>, Georg Moser <georg.moser@uibk.ac.at>, and Andreas Schnabl <andreas.schnabl@uibk.ac.at>. . This software is licensed under the GNU Lesser General Public License, see <http://www.gnu.org/licenses/>. . Don't know how to start? Type 'help'. TcT>
As can be readily seen from the output,
this command starts a customized version of ghci
.
In particular all the functionality of ghci
is available, cf.
http://www.haskell.org/ghc/docs/latest/html/users_guide/ghci.html
on general usage information of ghci
.
- load :: FilePath -> IO ()
- loadRC :: FilePath -> IO ()
- loadIRC :: FilePath -> IO ()
- loadDC :: FilePath -> IO ()
- loadIDC :: FilePath -> IO ()
- apply :: Apply p => p -> IO ()
- class Apply p
- state :: IO ()
- proof :: IO ()
- writeProof :: FilePath -> IO ()
- problems :: IO [Problem]
- wdgs :: IO [DG]
- cwdgs :: IO [CDG]
- uargs :: IO [UsablePositions]
- selectedRules :: ExpressionSelector -> IO [SelectorExpression]
- class Selector i
- select :: Selector sel => sel -> IO ()
- unselect :: Selector sel => sel -> IO ()
- data SelectAll
- data SelectInv s
- setRC :: IO ()
- setIRC :: IO ()
- setDC :: IO ()
- setIDC :: IO ()
- addRuleFromString :: String -> IO ()
- deleteRuleFromString :: String -> IO ()
- modifyInitialWith :: (Problem -> Problem) -> IO ()
- reset :: IO ()
- undo :: IO ()
- setShowProofs :: Bool -> IO ()
- help :: IO ()
- welcome :: IO ()
- class Describe p where
- pprint :: PrettyPrintable a => a -> IO ()
- processor :: (ParsableArguments (ArgumentsOf p), Processor p) => p -> IO (InstanceOf (StdProcessor p))
- termFromString :: String -> Problem -> IO (Term, Problem)
- ruleFromString :: String -> Problem -> IO (Rule, Problem)
- getConfig :: IO Config
- setConfig :: Config -> IO ()
- modifyConfig :: (Config -> Config) -> IO ()
- wdgs' :: IO [DG]
- problems' :: IO [Problem]
- runTct :: StdSolverM a -> IO a
Loading Problems
A complexity problem can be loaded into TcT-i by invoking
the load
action. This action accepts a file path refering
to either a file in the old tpdb-format (cf. http://www.lri.fr/~marche/tpdb/format.html)
or in the new xml-based format (cf. http://dev.aspsimon.org/xtc.xsd).
Examples are available in the directory examples
in the software distribution,
or the current termination problem database
(http://termcomp.uibk.ac.at/status/downloads/tpdb-current-exported.tar.gz).
Loads a complexity problem from the given file.
>>>
load "examples/quot.trs"
-------------------------------------------------------------------- Selected Open Problems: ----------------------- Strict Trs: { quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) , quot(0(), s(y)) -> 0() , minus(s(x), s(y)) -> minus(x, y) , minus(x, 0()) -> x} StartTerms: basic terms Strategy: none
Loading Problems with Respect to a Complexity Category
For convenience, TcT-i provides the following modifications of load
,
matching the categories of the complexity division of
the internation termination competition
http://termination-portal.org/wiki/Complexity.
Same as load
, but overwrites strategy and start-terms
in order to match a runtime-complexity problem.
Same as load
, but overwrites strategy and start-terms
in order to match a innermost runtime-complexity problem.
Same as load
, but overwrites strategy and start-terms
in order to match a derivational-complexity problem.
Same as load
, but overwrites strategy and start-terms
in order to match a innermost derivational-complexity problem.
The Proof State
During the interactive session, TcT-i maintains a so called proof state, which is basically a list of open complexity problems together with some information on how this state was obtained. In order to prove upper bounds on complexity problem, this proof state needs to be reduced to the empty list.
To see the list of open problems, use the action state
.
To obtain a proof, use the action proof
. To simplify the state
use the action apply
as described below.
Applying Complexity Techniques
The proof state is modified by applying instance of processors. A processor is the TcT representation of a complexity technique. Processors are separated for historical reasons into standard-processors and transformers.
Processors are usually parameterised by some arguments, for instance the
dependency pair processor dependencyPairs
accepts a flag usetuples
that defines whether dependency tuples should be employed.
Processors with instantiated arguments are called instances of processors.
When applying a processor, TcT-i will prompt the user for any necessary arguments
so it can construct the corresponding instance.
Predefined processors are available in module Tct.Processors. Instances can be constructed also directly, using the functionality provided in Tct.Instances. This module defines also a wealth of combinators and is considered the preferred way for dealing with processors.
Type
for some technique apply
mm
to simplify the list of selected open problems
using m
.
The proof state is updated by replacing each open problem with the result of applying m
.
TcT-i displays the proof fragment resulting from applying m
to each selected open problem,
and finally redisplays the new proof state.
The following example demonstrates the application of dependency pairs. Note that when a processor from Tct.Processors is applied, TcT-i might ask for further flags.
>>>
apply Processor.dependencyPairs
Input arguments for dp * 'usetuples' This argument specifies whether dependency tuples instead of pairs should be used. Synopsis: On|Off Use the default value 'Off'? Enter 'yes' or 'no', default is 'yes': > Problem 1: ---------- 1) Dependency Pairs [OPEN]: --------------------------- . We consider the following problem: Strict Trs: { quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) , quot(0(), s(y)) -> 0() , minus(s(x), s(y)) -> minus(x, y) , minus(x, 0()) -> x} StartTerms: basic terms Strategy: none . We have computed the following dependency pairs . Strict DPs: { quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y)) , quot^#(0(), s(y)) -> c_2() , minus^#(s(x), s(y)) -> minus^#(x, y) , minus^#(x, 0()) -> x} . Generated New Problems: ----------------------- . * Problem 1.1) Strict DPs: { quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y)) , quot^#(0(), s(y)) -> c_2() , minus^#(s(x), s(y)) -> minus^#(x, y) , minus^#(x, 0()) -> x} Strict Trs: { quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) , quot(0(), s(y)) -> 0() , minus(s(x), s(y)) -> minus(x, y) , minus(x, 0()) -> x} StartTerms: basic terms Strategy: none . 1.1) Open Problem [OPEN]: ------------------------- We consider the following problem: Strict DPs: { quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y)) , quot^#(0(), s(y)) -> c_2() , minus^#(s(x), s(y)) -> minus^#(x, y) , minus^#(x, 0()) -> x} Strict Trs: { quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) , quot(0(), s(y)) -> 0() , minus(s(x), s(y)) -> minus(x, y) , minus(x, 0()) -> x} StartTerms: basic terms Strategy: none . ---------------------------------------------------------------------- Selected Open Problems: ----------------------- Strict DPs: { quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y)) , quot^#(0(), s(y)) -> c_2() , minus^#(s(x), s(y)) -> minus^#(x, y) , minus^#(x, 0()) -> x} Strict Trs: { quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) , quot(0(), s(y)) -> 0() , minus(s(x), s(y)) -> minus(x, y) , minus(x, 0()) -> x} StartTerms: basic terms Strategy: none ----------------------------------------------------------------------
The next example shows the application of instances, in combination with the combinators from Tct.Instances.
>>>
:module +Tct.Instances
>>>
apply $ try removeWeakSuffix >>> try usableRules
... ---------------------------------------------------------------------- Selected Open Problems: ----------------------- Strict DPs: { quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y)) , quot^#(0(), s(y)) -> c_2() , minus^#(s(x), s(y)) -> minus^#(x, y) , minus^#(x, 0()) -> x} Strict Trs: { minus(s(x), s(y)) -> minus(x, y) , minus(x, 0()) -> x} StartTerms: basic terms Strategy: none ----------------------------------------------------------------------
class Apply p
Instances
Processor p => Apply (InstanceOf p) | |
(ParsableArguments (ArgumentsOf p), Processor p) => Apply (StdProcessor p) | |
Transformer t => Apply (TheTransformer t) | |
(ParsableArguments (ArgumentsOf t), Transformer t) => Apply (Transformation t sub) |
Instance of the class apply can be used to modify
the list of (selected) open problems using the action apply
.
Values of type
and StdProcessor
p
can be found in module Tct.Processors.
Values of type Transformation
t sub
and InstanceOf
p
for
(standard) processors TheTransformer
tp
and transformations t
, i.e.,
instances of processors, are collected in Tct.Instances.
Inspecting the State
As explained above, TcT-i retains a list of open problems
and proof information. These are accessible anytime using the
actions state
and proof
.
This action prints the current proof state.
>>>
state
---------------------------------------------------------------------- Selected Open Problems: ----------------------- Strict DPs: { quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y)) , quot^#(0(), s(y)) -> c_2() , minus^#(s(x), s(y)) -> minus^#(x, y) , minus^#(x, 0()) -> x} Strict Trs: { minus(s(x), s(y)) -> minus(x, y) , minus(x, 0()) -> x} StartTerms: basic terms Strategy: none ----------------------------------------------------------------------
The output shows the example from load
, already simplified using weak dependency pairs,
and further processed by try
removeTails
>>>
try
usableRules
This action prints the current proof tree.
>>>
proof
1) Dependency Pairs [OPEN]: --------------------------- . We consider the following problem: Strict Trs: { quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) , quot(0(), s(y)) -> 0() , minus(s(x), s(y)) -> minus(x, y) , minus(x, 0()) -> x} StartTerms: basic terms Strategy: none . We have computed the following dependency pairs . Strict DPs: { quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y)) , quot^#(0(), s(y)) -> c_2() , minus^#(s(x), s(y)) -> minus^#(x, y) , minus^#(x, 0()) -> x} . Generated New Problems: ----------------------- . * Problem 1.1) Strict DPs: { quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y)) , quot^#(0(), s(y)) -> c_2() , minus^#(s(x), s(y)) -> minus^#(x, y) , minus^#(x, 0()) -> x} Strict Trs: { quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) , quot(0(), s(y)) -> 0() , minus(s(x), s(y)) -> minus(x, y) , minus(x, 0()) -> x} StartTerms: basic terms Strategy: none . 1.1) removetails >>> ... [OPEN]: -------------------------------- . We consider the following problem: Strict DPs: { quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y)) , quot^#(0(), s(y)) -> c_2() , minus^#(s(x), s(y)) -> minus^#(x, y) , minus^#(x, 0()) -> x} Strict Trs: { quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) , quot(0(), s(y)) -> 0() , minus(s(x), s(y)) -> minus(x, y) , minus(x, 0()) -> x} StartTerms: basic terms Strategy: none . The processor is inapplicable since the strict component of the input problem is not empty . We apply the transformation 'usablerules' on the resulting sub-problem(s): . We consider the problem . Strict DPs: { quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y)) , quot^#(0(), s(y)) -> c_2() , minus^#(s(x), s(y)) -> minus^#(x, y) , minus^#(x, 0()) -> x} Strict Trs: { quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) , quot(0(), s(y)) -> 0() , minus(s(x), s(y)) -> minus(x, y) , minus(x, 0()) -> x} StartTerms: basic terms Strategy: none . We replace strict/weak-rules by the corresponding usable rules: . Strict Usable Rules: { minus(s(x), s(y)) -> minus(x, y) , minus(x, 0()) -> x} . The consider problem is replaced by . 1) Strict DPs: { quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y)) , quot^#(0(), s(y)) -> c_2() , minus^#(s(x), s(y)) -> minus^#(x, y) , minus^#(x, 0()) -> x} Strict Trs: { minus(s(x), s(y)) -> minus(x, y) , minus(x, 0()) -> x} StartTerms: basic terms Strategy: none . Generated New Problems: ----------------------- . * Problem 1.1.1) Strict DPs: { quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y)) , quot^#(0(), s(y)) -> c_2() , minus^#(s(x), s(y)) -> minus^#(x, y) , minus^#(x, 0()) -> x} Strict Trs: { minus(s(x), s(y)) -> minus(x, y) , minus(x, 0()) -> x} StartTerms: basic terms Strategy: none . 1.1.1) Open Problem [OPEN]: --------------------------- . We consider the following problem: Strict DPs: { quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y)) , quot^#(0(), s(y)) -> c_2() , minus^#(s(x), s(y)) -> minus^#(x, y) , minus^#(x, 0()) -> x} Strict Trs: { minus(s(x), s(y)) -> minus(x, y) , minus(x, 0()) -> x} StartTerms: basic terms Strategy: none
The output precisely reflects how the current proof state was
obtained from the initial state. Since state
contains still open problems,
the proof also open subproblems, in this case
subproblem 1.1.1).
From the output we can also see that removeTails
is inapplicable.
The reason is that removeTails
is unsound if the strict trs
from the problem is not empty. TcT will never apply processors in an unsound
setting!
as proof
, but output to given file
writeProof :: FilePath -> IO ()
Extracting the State
Beside showing the current state and the proof constructed so far, TcT-i also defines actions for extractions.
Displays and returns the list of selected open problems.
>>>
problems
Problem 1: . Strict DPs: { quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y)) , quot^#(0(), s(y)) -> c_2() , minus^#(s(x), s(y)) -> minus^#(x, y) , minus^#(x, 0()) -> x} Strict Trs: { minus(s(x), s(y)) -> minus(x, y) , minus(x, 0()) -> x} StartTerms: basic terms Strategy: none . [Problem { startTerms = ... , strategy = ... , variables = ... , signature = ... , strictDPs = Trs {rules = ...} , strictTrs = Trs {rules = ...} , weakDPs = Trs {rules = ...} , weakTrs = Trs {rules = ...}} ]
Problems are defined in the accompanying term rewriting library
(cf. http://cl-informatik.uibk.ac.at/software/tct/projects/termlib/).
The module Repl
, collecting most of the functionality of
the term rewriting library, is imported qualified as module TR
. Cf.
http://cl-informatik.uibk.ac.at/software/tct/projects/termlib/docs/Termlib-Repl.html
for documentation of the module Repl
.
This action displays the weak dependency graphs of all selected
problems. If dot
from the GraphViz project (c.f. http://www.graphviz.org/)
is installed, then a SVG-picture is rendered in 'dg.svg' of
the current working directory.
This action displays the weak congruence dependency graphs of all
selected problems. To produce an SVG-picture, use the procedure
wdgs
that draws weak dependency graphs, but also shows
congruence classes.
uargs :: IO [UsablePositions]
This action displays the usable argument positions of the selected problems.
This action displays the application of a rule-selector.
Selecting and Unselecting Problems
Sometimes it is convenient to consider a sublist of the list
of open Problems. To restrict the list of problems considered
by apply
, use the procedures select
and unselect
,
in combination with a Selector
.
class Selector i
Instances of this class can be used in combination with
select. Note that Selector [
selects according to the
problem number as recorded in the state (c.f. procedure Int
]state
).
Select problems from the proof state according to the given Selector
.
Consider the following state that is obtained from the running example,
after applying pathAnalysis
.
>>>
state
-------------------------------------------------------------------- Selected Open Problems: ----------------------- 1) Strict DPs: {minus^#(s(x), s(y)) -> minus^#(x, y)} Strict Trs: { minus(s(x), s(y)) -> minus(x, y) , minus(x, 0()) -> x} StartTerms: basic terms Strategy: none . 2) Strict DPs: {minus^#(x, 0()) -> x} Strict Trs: { minus(s(x), s(y)) -> minus(x, y) , minus(x, 0()) -> x} Weak DPs: {minus^#(s(x), s(y)) -> minus^#(x, y)} StartTerms: basic terms Strategy: none . 3) Strict DPs: {quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y))} Strict Trs: { minus(s(x), s(y)) -> minus(x, y) , minus(x, 0()) -> x} StartTerms: basic terms Strategy: none . 4) Strict DPs: {quot^#(0(), s(y)) -> c_2()} Strict Trs: { minus(s(x), s(y)) -> minus(x, y) , minus(x, 0()) -> x} Weak DPs: {quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y))} StartTerms: basic terms Strategy: none .>>>
select [1,3]
-------------------------------------------------------------------- Unselected Open Problems: ------------------------- 2) Strict DPs: {minus^#(x, 0()) -> x} Strict Trs: { minus(s(x), s(y)) -> minus(x, y) , minus(x, 0()) -> x} Weak DPs: {minus^#(s(x), s(y)) -> minus^#(x, y)} StartTerms: basic terms Strategy: none . 4) Strict DPs: {quot^#(0(), s(y)) -> c_2()} Strict Trs: { minus(s(x), s(y)) -> minus(x, y) , minus(x, 0()) -> x} Weak DPs: {quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y))} StartTerms: basic terms Strategy: none . Selected Open Problems: ----------------------- 1) Strict DPs: {minus^#(s(x), s(y)) -> minus^#(x, y)} Strict Trs: { minus(s(x), s(y)) -> minus(x, y) , minus(x, 0()) -> x} StartTerms: basic terms Strategy: none . 3) Strict DPs: {quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y))} Strict Trs: { minus(s(x), s(y)) -> minus(x, y) , minus(x, 0()) -> x} StartTerms: basic terms Strategy: none
Special selector to select all open problems.
Special selector to inverse a selection.
Changing the Initial Problem
The following procedures change the initial problem.
Note that in order to guarantee soundness, any progress
will undone. However the procedure undo
allows to revert
a change to the initial problem.
This action overwrites strategy and start-terms in order to match a runtime-complexity problem.
This action overwrites strategy and start-terms in order to match a innermost runtime-complexity problem.
This action overwrites strategy and start-terms in order to match a derivational-complexity problem.
This action overwrites strategy and start-terms in order to match a innermost derivational-complexity problem.
addRuleFromString :: String -> IO ()
This action adds the given rule to the input problem. Terms are parsed using the simple grammar
RULE -> TERM SEP TERM
-
TERM -> SYM([TERM]*) | SYM
.
Here SEP
is either ->
or ->=
. In the former case, the parsed rule
is considered a strict rule, in the latter case a weak rule.
SYM
is either the special name COM
, or any character not matchin (),"-=
.
If the root of the left hand side has ^
as suffix, then
the rule is considered a dependency pair (these dependency pair suffixes
are stripped off by the parser).
The special symbol COM
is replaced by a fresh compound symbol.
deleteRuleFromString :: String -> IO ()
This action deletes the given rule from the input problem. See addRuleFromString
for grammar.
modifyInitialWith :: (Problem -> Problem) -> IO ()
This action modifies the initial problem according to given function.
History Functionality
TcT provides basic history functionality, in order to undo previous actions. This functionality covers all actions that modify the state.
This action resets the proof state to the initially loaded system.
Undos the last modification of the proof state
Changing the behaviour of TcTi
When set to True
, interactive mode will print
proofs after execution of commands. This can be globally configured
in your configuration by modifying interactiveShowProofs
.
setShowProofs :: Bool -> IO ()
Help and Documentation
Displays a help message.
Displays a help message.
Prints a description of the given technique. In particular,
describe
accepts processors as defined in Processors
.
>>>
describe Processor.lmpo
. Processor "lmpo": ----------------- This processor implements orientation of the input problem using 'light multiset path orders', a technique applicable for innermost runtime-complexity analysis. Light multiset path orders are a miniaturisation of 'multiset path orders', restricted so that compatibility assesses polytime computability of the functions defined. Further, it induces exponentially bounded innermost runtime-complexity. . Usage: lmpo [:ps [On|Off]] [:wsc [On|Off]] . Arguments: ps: If enabled then the scheme of parameter substitution is admitted, cf. http://cl-informatik.uibk.ac.at/~zini/publications/WST09.pdf how this is done for polynomial path orders. The default is set to 'On'. . wsc: If enabled then composition is restricted to weak safe composition. . For documentation concerning creation of instances, consult: http://cl-informatik.uibk.ac.at/software/tct/projects/tct/docs/Tct-Instances.html#v:lmpo
class Describe p where
Instances
(Processor p, ParsableArguments (ArgumentsOf p)) => Describe (ProcessorInstance p) | |
(Processor p, ParsableArguments (ArgumentsOf p)) => Describe (StdProcessor p) | |
(Transformer t, ParsableArguments (ArgumentsOf t)) => Describe (TheTransformer t) | |
(Transformer t, ParsableArguments (ArgumentsOf t)) => Describe (Transformation t AnyProcessor) |
Instances of this class can be handled by the action describe
.
Miscellaneous Utilities
pprint :: PrettyPrintable a => a -> IO ()
pretty-print objects.
processor :: (ParsableArguments (ArgumentsOf p), Processor p) => p -> IO (InstanceOf (StdProcessor p))
given a processor, construct an instance
Parses a term from a string, with respect
to the signature and variables from the given problem.
See addRuleFromString
for grammar.
Parses a rule from a string, with respect
to the signature and variables from the given problem.
See addRuleFromString
for grammar.
Accessing to the Configuration
The TcT configuration file, usually residing in ${HOME}/.tct/tct.hs
contains
a definition config ::
.
In particular, TcT-i employs the field Config
processors
when it requires the list
of available processors, for instance when parsing arguments.
The configuration is accessible throught the following actions.
Note that the configuration can be modified while running TcT-i.
Returns the current configuration.
Set the configuration.
modifyConfig :: (Config -> Config) -> IO ()
Modify the configuration according to the given function.
Silent Versions
Misc
runTct :: StdSolverM a -> IO a