.\" The version string should track the overall package version
.TH PLEBBY 1 "2022-03-15" "Version 1.0" "Language Toolkit"
.SH NAME
plebby \- Piecewise / Local Expression Builder Interpreter
.SH SYNOPSIS
.B plebby
.SH DESCRIPTION
The interactive theorem-prover reads and evaluates single-line
.BR pleb (5)
statements.
Additionally, it provides various commands that
one can use to explore and interact with languages.
.SS Interpreter Basics
.TP
.B :quit
Exit the interpreter.
.
.TP
.B :help
Print an alphabetical list of commands
with brief descriptions.
.
.SS Saving and Loading
.B :savestate
.RI < file >
.RS
Write the current state to
.RI < file >.
.RE
.
.PP
.B :writeATT
.RI < file >
.RI < file >
.RI < file >
.RI < expr >
.RS
Write an AT&T transducer representation of
.RI < expr >
to the three
.RI < file >
argmuents, which represent the transitions, input symbols, and output symbols,
respectively.
If
.B _
is given as the name of a symbol table,
then that table is not written.
The input and output tables are identical, so writing both is redundant.
.RE
.
.PP
.B :write
.RI < file >
.RI < expr >
.RS
Write a binary form of
.RI < expr >
to
.RI < file >.
.RE
.
.PP
.B :loadstate
.RI < file >
.RS
Restore a state previously written by
.B :savestate
from
.RI < file >.
.RE
.
.PP
.B :readATT
.RI < file "> <" file "> <" file >
.RS
Read an AT&T format transducer from the three
.RI < file >
arguments (transitions, input symbols, and output symbols),
and store the input-projection of the result in the special variable
.BR it .
If
.B _
is given as the name of a symbol table,
then no file is read for that table.
.RE
.
.PP
.B :readATTO
.RI < file "> <" file "> <" file >
.RS
Equivalent to
.B :readATT
except that it is the output-projection that is stored.
.RE
.
.PP
.B :readBin
.RI < file >
.RS
Read a binary format expression from
.RI < file >
and store the result in the special variable
.BR it .
.RE
.
.PP
.B :readJeff
.RI < file >
.RS
Read an automaton file in Jeff format from
.RI < file >
and store the result in the special variable
.BR it .
This will never result in an alphabet-agnostic constraint automaton.
In other words, adding to the alphabet has no effect on whether a
word is accepted by the resulting automaton,
because it is always in ground form.
.RE
.
.PP
.B :read
.RI < file >
.RS
Read
.RI < file >
as a
.BR pleb (5)
program, assimilating all bindings.
If there are any bare expressions,
the last one is assigned to the special variable
.BR it .
.RE
.
.PP
.B :import
.RI < file >
.RS
Read
.RI < file >
one line at a time as if its contents had been typed into the interpreter.
Specifically this means that each statement must be
entirely on one line,
and some lines may be interpreter commands (including
.BR :import ).
.RE
.
.SS Determining the Class of an Expression
The commands in this section determine whether a given
.I expr
is in the corresponding class
with respect to the current
.BR universe .
.
.PP
.B :isB
.RI < expr >
.RS
Band, everything is idempotent.
.RE
.
.PP
.B :isCB
.RI < expr >
.RS
Commutative band, a semilattice.
.RE
.
.PP
.B :isDef
.RI < expr >
.RS
Definite, defined by a set of permitted suffixes.
.RE
.
.PP
.B :isFinite
.RI < expr >
.RS
Finite, having an acyclic graph representation.
.RE
.
.PP
.B :isFO2
.RI < expr >
.RS
First-order logic with general precedence,
restricted to two variables.
.RE
.
.PP
.B :isFO2B
.RI < expr >
.RS
First-order logic with general precedence and betweenness,
restricted to two variables.
.RE
.
.PP
.B :isFO2S
.RI < expr >
.RS
First-order logic with general precedence and successor,
restricted to two variables.
.RE
.
.PP
.B :isGD
.RI < expr >
.RS
Generalized definite.
.RE
.
.PP
.B :isGLPT
.RI < expr >
.RS
Generalized locally J-trivial. Related to LT and PT.
.RE
.
.PP
.B :isGLT
.RI < expr >
.RS
Generalized locally testable.
.RE
.
.PP
.B :isLB
.RI < expr >
.RS
Locally a band, all local subsemigroups are idempotent.
.RE
.
.PP
.B :isLPT
.RI < expr >
.RS
Locally J-trivial. Related to LT and PT.
.RE
.
.PP
.B :isLT
.RI < expr >
.RS
Locally testable.
.RE
.
.PP
.B :isLTT
.RI < expr >
.RS
Locally threshold testable,
equivalent to first-order logic with successor
but not general precedence.
.RE
.
.PP
.B :isPT
.RI < expr >
.RS
Piecewise testable.
.RE
.
.PP
.B :isRDef
.RI < expr >
.RS
Reverse definite, defined by a set of permitted prefixes.
.RE
.
.PP
.B :isSF
.RI < expr >
.RS
Star-free, equivalent to first-order logic with general precedence.
.RE
.
.PP
.B :isSL
.RI < expr >
.RS
Strictly local.
.RE
.
.PP
.B :isSP
.RI < expr >
.RS
Strictly piecewise.
.RE
.
.PP
.B :isTDef
.RI < expr >
.RS
Tier-based definite, defined by a set of permitted tier-suffixes.
.RE
.
.PP
.B :isTGD
.RI < expr >
.RS
Tier-based generalized definite:
contains all and only the strings whose projections
to some fixed subset of the current
.B universe
lie in a generalized definite stringset.
.RE
.
.PP
.B :isTLB
.RI < expr >
.RS
Tier-based locally a band, all local subsemigroups are idempotent
after restriction to some tier.
.RE
.
.PP
.B :isTLPT
.RI < expr >
.RS
Tier-based locally J-trivial:
contains all and only the strings whose projections
to some fixed subset of the current
.B universe
lie in a locally J-trivial stringset.
.RE
.
.PP
.B :isTLT
.RI < expr >
.RS
Tier-based locally testable:
contains all and only the strings whose projections
to some fixed subset of the current
.B universe
lie in a locally testable stringset.
.RE
.
.PP
.B :isTLTT
.RI < expr >
.RS
Tier-based locally threshold testable:
contains all and only the strings whose projections
to some fixed subset of the current
.B universe
lie in a locally threshold testable stringset.
.RE
.
.PP
.B :isTRDef
.RI < expr >
.RS
Tier-based reverse definite,
defined by a set of permitted tier-prefixes.
.RE
.
.PP
.B :isTrivial
.RI < expr >
.RS
One-state.
.RE
.
.PP
.B :isTSL
.RI < expr >
.RS
Tier-based strictly local:
contains all and only the strings whose projections
to some fixed subset of the current
.B universe
lie in a strictly local stringset.
.RE
.
.SS Grammatical Inference
.B :learnSL
.RI < int >
.RI < file >
.RS
Read
.RI < file >
as a sequence of newline-terminated words
composed of space-separated symbols,
and construct an
.RI < int >-SL
automaton compatible with this data.
Symbols not in the data are always rejected.
.RE
.
.PP
.B :learnSP
.RI < int >
.RI < file >
.RS
Read
.RI < file >
as a sequence of newline-terminated words
composed of space-separated symbols,
and construct an
.RI < int >-SP
automaton compatible with this data.
Symbols not in the data are always rejected.
.RE
.
.PP
.B :learnTSL
.RI < int >
.RI < file >
.RS
Read
.RI < file >
as a sequence of newline-terminated words
composed of space-separated symbols,
and construct an
.RI < int >-TSL
automaton compatible with this data.
Symbols not in the data are always rejected.
.RE
.
.SS Comparing Expressions
.B :strict-subset
.RI < expr >
.RI < expr >
.RS
Determine whether the first
.RI < expr >
is a proper subset of the second
in the current
.BR universe .
.RE
.
.PP
.B :subset
.RI < expr >
.RI < expr >
.RS
Determine whether the first
.RI < expr >
is a (not necessarily proper) subset of the second
in the current
.BR universe .
.RE
.
.PP
.B :equal
.RI < expr >
.RI < expr >
.RS
Determine whether the first
.RI < expr >
is equal to the second
in the current
.BR universe ,
i.e. each is a subset of the other.
.RE
.
.PP
.B :implies
.RI < expr >
.RI < expr >
.RS
Determine whether the first
.RI < expr >
logically implies the second
in the current
.BR universe .
This is equivalent to
.BR :subset .
.RE
.
.SS Graphical Output
All commands that display graphical output
require the
.B dot
and
.B display
programs accessible on
.RI ${ PATH },
where
.B dot
is GraphViz-compatible and
.B display
can accept a PNG file over the standard input and display it appropriately.
ImageMagick, for example, contains such a
.B display
program.
.
.PP
.B :display
.RI < expr >
.RS
Show a normal-form automaton representation of
.RI < expr >
graphically.
.RE
.
.PP
.B :psg
.RI < expr >
.RS
Show the powerset graph of a normal-form automaton representation of
.RI < expr >
graphically.
.RE
.
.PP
.B :synmon
.RI < expr >
.RS
Show the syntactic monoid associated with a
normal-form automaton representation of
.RI < expr >
graphically.
.RE
.
.SS Generating Dot Files Without Displaying Them
.B :dot
.RI < expr >
.RS
Print a Dot file for a normal-form automaton representation of
.RI < expr >.
.RE
.
.PP
.B :dot-psg
.RI < expr >
.RS
Print a Dot file for the powerset graph of
a normal-form automaton representation of
.RI < expr >.
.RE
.
.PP
.B :dot-synmon
.RI < expr >
.RS
Print a Dot file for the syntactic monoid associated with
a normal-form automaton representation of
.RI < expr >.
.RE
.
.SS Operations on the Environment
.TP
.B :bindings
Print a list of currently-bound variables and their bindings.
Because expression variables have large representations,
these representations are omitted from this listing
but can be displayed individually with
.BR :show .
.
.PP
.B :show
.RI < var >
.RS
Print the current binding of
.RI < var >,
if any, or a message indicating that it is not bound.
.RE
.
.PP
.B :unset
.RI < var >
.RS
Remove any binding for
.RI < var >
from the current environment.
.RE
.
.TP
.B :reset
Remove all bindings from the current environment.
.
.TP
.B :restore-universe
Set the special variable
.B universe
to the symbol set that contains all and only
those symbols used in other bindings
in the current environment.
.
.TP
.B :compile
Convert all saved expressions into automata,
retaining the metadata that allows the expression
to be alphabet-agnostic.
.
.TP
.B :ground
Convert all saved expressions into automata,
discarding the metadata that allows the expression
to be alphabet-agnostic.
.
.TP
.B :restrict
Remove all symbols that are not in the current
.B universe
from all current bindings.
This may result in an empty symbol set,
which cannot be assigned directly.
Non-satisfiable factors are uniformly replaced by
.B !<>
for simplicity.
.
.SH OPTIONS
None.
.SH "EXIT STATUS"
.TP
.B 0
Successful program execution
.TP
.B ">0"
An error occurred.
.
.SH ENVIRONMENT
.TP
.B PAGER
If
.B PAGER
is set, its value is used as the program to use to display the help text.
If not, then
.B less
is used with no arguments.
.
.SH FILES
.TP
~/.haskeline
Configuration file for the line editor.
.
.SH NOTES
Most of the complexity class decision algorithms are based on
properties of the syntactic monoid that,
given the representation,
might be slow to compute.
This holds especially true for the (T)LTT test.
.
.P
The AT&T format cannot handle symbols that contain spaces.
Further, numeric symbols are treated as indices into the symbols files,
so symbol mapping files must be written
when exporting automata that actually use such symbols.
.SH BUGS
Lines that cannot be parsed are ignored,
but generally no warnings are emitted.
.SH "SEE ALSO"
.BR display (1),
.BR dot (1),
.BR fsm (5),
.BR pleb (5)
.PP
https://github.com/judah/haskeline/wiki/UserPreferences