This is a playground
to test code. It runs a full Node.js
environment and already has all of npm
’s 400,000 packages pre-installed, including stsys
with all npm
packages installed. Try it out:
require()
any package directly from npmawait
any promise instead of using callbacks (example)This service is provided by RunKit and is not affiliated with npm, Inc or the package authors.
A semi-Thue system or string rewriting system (SRS) for solving the word problem by employing the Knuth-Bendix completion procedure.
$ npm install stsys
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.
The package exposes the following function:
The 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 left-hand and right-hand side separated by =
.
Left-hand and right-hand
sides are strings over an alphabet that is a subset of the lower and upper case characters of the
Latin alphabet, i.e. a
through z
and A
through Z
. Note that the empty string
is a valid left-hand or right-hand side. Leading or trailing spaces, as well as spaces surrounding the
equality character, are ignored.
The following equations are all valid:
ab = ba
aaa=
=bb
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 time run
is equivalent to rerun
. The return value is the state
of the prover, which is the same as returned by getState()
.
The parameter options
may or may
not be supplied. If it is supplied it should be an object with one or more of the following properties:
logging
: An object with two properties logger
and level
. logger
must be a
function accepting one argument (a string). level
must be a (natural) number in the range 0..6.
A level 0 produces no logging output (i.e. calls to logger
), bigger numbers produce incrementally
growing logging output.
ordering
: The ordering to be used. The value of this property must be one of the following strings
(i.e., ordering names): lex
(length-lexicographic ordering), lpo
(lexicographic path ordering),
syl-l
(syllable ordering with left-to-right comparison of syllables), or syl-r
(syllable ordering with right-to-left comparison of syllables). All these orderings require a preorder.
Note that the order can only be changed when starting from scratch, i.e. through rerun
or
a first-time run
.
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 characters (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 right-to-left comparison of syllables of a
, and a left-to-right
comparison of syllables of c
, regardless of whether the ordering is syl-l
or syl-r
.
Syllables of b
, 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. through rerun
or
a first-time run
.
statistics
: A flag (i.e. a Boolean value true
or false
)
that indicates whether statistical data is to be collected. The default is false
. Note that
this flag is taken into account only if the procedure starts from scratch, i.e. through rerun
or
a first-time run
. The statistical data can be retrieved through getStatistics()
.
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 the rules 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 value true
or false
) that indicates whether or not
a critical pair is subject to reduction prior to being added to the set of critical pairs. The default is
false
.
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 parameter axioms
of createProver
. Note that goals are added to possibly existing goals
when resuming a stopped run. Note also that the procedure will stop in the state proved
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 of options
consult run
. The return value is the state
of the prover, which is the same as returned by getState()
.
getState()
: Gets the state of the procedure. The state is undefined 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 procedure proved the given goals (i.e., solved the respective word problems)
by reducing them to trivial equations.
stopped
: The procedure stopped because of a timeout or reaching the value of maxRuleGen
.
getHrtimeElapsed()
: The time consumed by the most recent run (in process.hrtime
format).
getTimeElapsed()
: The time consumed by the most recent run (in a human-readable string format).
getAxioms()
: Gets the axioms as an array of strings.
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 flag proved
is true
.
getTotalCpCount()
: Gets the total number of critical pairs awaiting processing.
getStatistics()
: Gets statistical data, which is only available if option statistics:true
is supplied.
Note that the statistical data is an aggregate of all runs since the most recent call to rerun
or first-time run
. 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 left-hand 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 left-hand 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 left-hand 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 option
preReduceCps: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 strings s1
and s2
are equal w.r.t. the current set of rules.
The result is true
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 is undefined
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 return completed
).
The result is false
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.