STSYS
A semiThue system or string rewriting system (SRS) for solving the word problem by employing the KnuthBendix completion procedure.
Quick Run
The completion procedure can be run from the command line. In the installation directory run
$ node run
for usage information.
Axioms and optionally goals (i.e., word problems to be solved) are specified in a file.
Samples of such files can be found in directory samples
. Consult
in particular samples/test4.eqs
for details on the notation
used in such a file.
Usage
The index module of the package exposes the following function:
createProver (axioms, options)
Parameter axioms
is mandatory and must be either a string specifying a single axiom,
or an array of strings, each string specifying an axiom. We use the term axiom to denote a given
equation. Such an equation consists of a lefthand and righthand side separated by =
.
Lefthand and righthand
sides are strings over the lower and upper case letters of the
Latin alphabet, i.e. a
through z
and A
through Z
. Note that the empty string
is a valid lefthand or righthand side. In other words there is no special character denoting the empty string.
Leading or trailing spaces, as well as spaces surrounding the equality character, are ignored.
Examples
The following equations are all valid:
ab = ba
aaa=
=bb
Parameter options
is optional.
If it is supplied it should be an object with one or more of the following properties:

logger
: a function accepting one argument (a string) that receives all information to be logged depending on the log level. An example for such a function isconsole.log
. The default isnull
, i.e. there is no logger. 
logLevel
: the log level, a (natural) number in the range 0..6. A level 0 produces no logging output (i.e. calls tologger
), bigger numbers produce incrementally detailed logging output. The default is 0. 
ordering
: The ordering to be used. The value of this property must be one of the following strings (i.e., ordering names):lex
(lengthlexicographic ordering),lpo
(lexicographic path ordering),syll
(syllable ordering with lefttoright comparison of syllables), orsylr
(syllable ordering with righttoleft comparison of syllables). All these orderings require a preorder. Without preorder the ordering is null and void. The ordering can also be set or modified through parameteroptions
ofrerun
or a firsttimerun
(see below). 
preorder
: The preorder on the letters of the chosen alphabet, i.e. all letters occurring in the axioms. The preorder is given as an array of letters in descending (pre)order. Note that in connection with syllable orderings a letter may be augmented with directional information. For instance,['a:r','b','c:l']
triggers a righttoleft comparison of syllables ofa
, and a lefttoright comparison of syllables ofc
, regardless of whether the ordering issyll
orsylr
. Syllables ofb
, on the other hand, are compared in the direction dictated by the ordering (name). Note that providing a preorder has no effect if no ordering name is supplied. The preorder can also be set or modified through parameteroptions
ofrerun
or a firsttimerun
(see below).
Function createProver
returns an object that has the following properties, all of which
are functions:

run(options)
: Starts the completion procedure, possibly resuming from where it left off before. When called the first timerun
is equivalent torerun
. The return value is the state of the prover, which is the same as the value returned bygetState()
. Parameteroptions
is optional. If it is supplied it should be an object with one or more of the following properties:
logger
: a function accepting one argument (a string) that receives all information to be logged depending on the log level. An example for such a function isconsole.log
. A previously set logger is overwritten if a valid value (a function) is supplied. 
logLevel
: the log level, a (natural) number in the range 0..6. A level 0 produces no logging output (i.e. calls tologger
), bigger numbers produce incrementally growing logging output. A previously set level is overwritten if a valid value (a number) is supplied. 
ordering
: The ordering to be used. The value of this property must be one of the following strings (i.e., ordering names):lex
(lengthlexicographic ordering),lpo
(lexicographic path ordering),syll
(syllable ordering with lefttoright comparison of syllables), orsylr
(syllable ordering with righttoleft comparison of syllables). All these orderings require a preorder. A previously chosen preorder will be made use of unless it is overwritten. Note that the ordering can only be changed when starting from scratch, i.e. throughrerun
or a firsttimerun
. Furthermore, there is no default ordering. That is, an ordering needs to be specified here or when callingcreateProver
. 
preorder
: The preorder on the letters of the chosen alphabet, i.e. all letters occurring in the axioms. The preorder is given as an array of letters in descending (pre)order. Note that in connection with syllable orderings a letter may be augmented with directional information. For instance,['a:r','b','c:l']
triggers a righttoleft comparison of syllables ofa
, and a lefttoright comparison of syllables ofc
, regardless of whether the ordering issyll
orsylr
. Syllables ofb
, on the other hand, are compared in the direction dictated by the ordering (name). Note that the preorder can only be changed when starting from scratch, i.e. throughrerun
or a firsttimerun
. Furthermore, there is no default preorder. That is, a preorder needs to be specified here or when callingcreateProver
. 
statistics
: A flag (i.e. a Boolean valuetrue
orfalse
) that indicates whether statistical data is to be collected. The default isfalse
. Note that this flag is taken into account only if the procedure starts from scratch, i.e. throughrerun
or a firsttimerun
. The statistical data can be retrieved throughgetStatistics()
. 
timeout
: The timeout in milliseconds after which the procedure will stop. The value of this property must be a number greater than or equal to zero. Otherwise there will be no timeout. 
maxRuleGen
: The maximal number of rules generated by the completion procedure. The value of this property must be a number greater than or equal to zero. Otherwise there will be no limit on the number of rules generated. Note that the limit is imposed on the number of rules generated in the upcoming run, not on the total (aggregate) number of rules of all runs so far plus the upcoming run. 
preReduceCps
: A flag (i.e. a Boolean valuetrue
orfalse
) that indicates whether or not a critical pair is subject to reduction prior to being added to the set of critical pairs. The default isfalse
. Note that reducing a critical pair before adding it to the set of critical pairs can lower the memory consumption, but it will increase processing time. It can also alter the order in which critical pairs are selected, which may affect the course of the completion procedure. 
goals
: An equation or a list (array) of equations for which the word problem is to be solved. The format is the same as for parameteraxioms
ofcreateProver
. Note that goals are added to possibly existing goals when resuming a stopped run. Note also that the procedure will stop in the stateproved
as soon as all word problems were solved.


rerun(options)
: Starts the completion procedure from scratch, discarding any results of a previous run. For a description ofoptions
consultrun
. The return value is the state of the prover, which is the same as the value returned bygetState()
. 
getState()
: Gets the state of the completion procedure. The state isnull
if there was no run. Otherwise it is one of the following strings:
completed
: The completion procedure produced a convergent set of rules. 
proved
: The completion procedure proved the given goals (i.e., solved the respective word problems) by reducing them to trivial equations. A convergent set of rules may not (yet) have been produced. 
stopped
: The completion procedure stopped because of a timeout or reaching the value ofmaxRuleGen
.


getHrtimeElapsed()
: Gets the time consumed by the most recent run (inprocess.hrtime
format) 
getTimeElapsed()
: Gets the time consumed by the most recent run (in a humanreadable string format) 
getAxioms()
: Gets the axioms as an array of strings 
getOrdering()
: Gets the current ordering (name) 
getPreorder()
: Gets the current preorder as an array of letters in descending (pre)order 
getRulesCount()
: Gets the total number of rules 
getRules()
: Gets the rules as an array of strings 
getTotalGoalsCount()
: Gets the total number of goals 
getProvedGoalsCount()
: Gets the number of goals proved 
getGoals()
: Gets the current set of goals as an array of goal objects. Each such object has the following properties:
id
: The identifier of the goal (a natural number starting with 1) 
goal
: The original goal as it was provided 
proved
: A flag indicating whether the goal was proved 
provedBy
: The trivial equation that was produced from the original goal. This property is available only if the goal was indeed proved, i.e. the flagproved
istrue
.


clearGoals()
: Removes all goals 
getTotalCpCount()
: Gets the total number of critical pairs awaiting processing 
getStatistics()
: Gets statistical data, which is only available if optionstatistics:true
is supplied. Note that the statistical data is an aggregate of all runs since the most recent call torerun
or firsttimerun
. The returned value is an object with the following numerical properties:
rulesGenerated
: The number of rules generated, or in other words the number of critical pairs converted into rules 
rulesDemoted
: The number of rules converted back into critical pairs due to reduction of the lefthand side 
rulesDiscarded
: The number of rules discarded after having been reduced to a trivial equation (an identity) 
cpsAdded
: The number of critical pairs added to the set of critical pairs; besides the critical pairs generated through overlapping, this number includes the axioms as well as demoted rules. 
cpsGenerated
: The number of critical pairs generated (through overlapping of lefthand sides of rules) 
cpsObsolete
: The number of critical pairs that were obsolete at the time of selection due to one or both parent rules having been demoted or discarded in the meantime 
cpsTrivialImmediate
: The number of overlappings of lefthand sides of rules that immediately (without any reduction step) resulted in a trivial equation (an identity) 
cpsTrivialPrereduced
: The number of critical pairs reduced to an identity prior to being added to the set of critical pairs and hence never added. Note that this statistical value will be 0 unless optionpreReduceCps:true
is supplied. 
cpsTrivialSelected
: The number of critical pairs that were reduced to a trivial equation (an identity) after having been selected


normalize(s)
: Computes the normal form of the given string w.r.t. the current set of rules 
testEquality(s1, s2)
: Checks whether the two given stringss1
ands2
are equal w.r.t. the current set of rules. The result istrue
if the two string can be reduced to the same string (a.k.a. normal form if the set of rules is complete). The result isundefined
if the two strings cannot be reduced to the same string and the current set of rules has not been completed (i.e.,getState()
does not returncompleted
). The result isfalse
if there is a complete set of rules and the normal forms of the strings are not identical. Note that it is possible to omit the second argument and provide the first one as an equation.