Version: May 5, 2018
       IMPORTANT INSTRUCTIONS ON THE USAGE OF THE  wpflCzG  PROGRAM

       Content

(1) What is this program
(2) How to run the program
(3) How to create an input file
(4) Basic commands
(5) Suffix commands
(6) Two examples
(7) Further notes on input files



(1) What is this program 

This program is for the Word Problem of Free Lattices by CZedli, Gabor
(the acronym wpflCzG comes from the capitalized letters). Given
two n-ary lattice terms p and q (up to a certain complexity, depending
on the computer we are using), the program can decide whether the
inequality  p <= q   (p less than or equal to q) holds in all lattices,
equivalently, if it holds in the free lattice FL(n).
  Also, for given n-ary lattice terms p1, p2, ..., pk, the program
can decide whether the subset {p1, p2, ..., pk} generates freely
a sublattice or not.
  As opposed to most "modern" programs in which we are given a nice
interface with decorative icons and possibilities of various mouse clicks,
etc., this program takes its input from a text file. That is, from a 
file named, say,  ourdata.txt  ; there are various word processors
that can produce such a file. Warning: the file should be (saved as)
UNFORMATTED !   The advantage of this sort of input
is that we can use a lot of features of our word processor to create
an input file in an economic way; we can copy, past, and substitute with
our usual word processor. The program also contains some features
that can be used to create an input file even more conveniently;
for example, we can easily dualize a lattice term. (See the 
suffix commands later.) In addition to saving time, the automatism 
provided by our word processor and the program  helps in avoiding 
typos.
  The disadvantage of using the input technique mentioned above is
that the reader should  spend a few minutes on reading this file
before using the program. Like in case of TeX or LaTeX, the 
fastest (but not the safest) way is to modify one of the several
sample input files that come with the program.
  The program has been written in Pascal, and it has been developed and
translated in Dev-Pascal 1.9.2, a freely donwloadable fully integrated
development environment.



(2) How to run the program

You need a computer with Windows on it. Windows 10 is surely appropriate,
and I strongly believe that many earlier Windows version are also fine,
but this has not been tested. 
   The first step is that you have to put an executable version of 
the program on your hard drive. There are several ways; however, it is 
recommended that you take care of the threat by computer viruses.
   The safest but most complicated way is to deploy Dev-Pascal 1.9.2 on 
your computer and translate wpflCzG.pas to an executable file with it. 
This method might work with other versions of (Dev-)Pascal and possibly even
under operations systems distinct from Windows, but this has not been checked.
   The easiest way is to copy the wpflCzG.exe to your computer but what
I can really suggest is the following.
   Copy the wpflCzG.e&! file to your computer, check its size (see the table
below), and if the size is OK, then rename the file to wpflCzG.exe . 
(Viruses, hopefully, do not attack files with the meaningless extension
"e&!" and even if they do, then, hopefully again, they will change the
size of the file.)  
   Some parameters in the program can be modified. Hence, in fact, the 
following two versions are downloadable, and their sizes are:
   wpflCzG.e&! = wpflCzG.exe  (small) :  84 992  bytes ,
   wpflCzGXL.e&! : 84 992 bytes also.
(The second one is for really large input files and large computers;
rename it to  wpflCzGXL.exe  .)

Once wpflCzG.exe (or  wpflCzGXL.exet) is available on your 
computer, you have to create an input file. It should be an 
unformatted ASCII  *.txt file.  Important: the 
number of keystrokes used to produce this file should be the same as the 
length of the file in bytes. (Formatting will surely and unicode would 
possibly cause troubles. Hence, I suggest not to use symbols that are not 
available in English keyboards.)  

To run the program, you can simply drag-and-drop the input file on wpflCzG.exe .
Also, you can (double) click on wpflCzG.exe and type the name of the input file
when the program asks for it.  You can experiment with one of the input files
that come with the program. (These files have extension ".txt"; even if your 
Windows is set not to show filename extensions, the ".txt" extension of
the name of your input file should be typed if the program asks for the file name.)



(3) How to create an input file

As already mentioned, an input file has to be UNFORMATTED. 
An input file contains variables and lattice terms, and it also 
contains some commands that tell the program what to do. 
Improper use of commands lead to runtime errors!
   Warning: this is not a professional program that gives
proper explanation on every possible runtime error. 
Even if some loose checking is built in the program, not every runtime
error is prevented!  If you do not know what sort of error happened,
in particular, if no output is displayed,  then
run the program again with the "Save partial computational details" option or,
if this does not help, with the "Save all computational details" option.
Or run the program without an input file and type "help" instead of 
entering a file nam.
   A command in the input file is always of the form
<backslash><certain_string> . Here <backslash> refers to the single
character called "backslash". A backslash is always the first character of
a command and it CANNOT OCCUR elsewhere. (Not even in this file, which
can also be used as an input file.)
There are    "basic commands"   and   "suffix commands". For example,
<backslash>name   and <backslash>end    are basic commands while <backslash>dual
is a suffix command.  The meaning of a basic command is more or less
clear even from any of the sample input files. Suffix commands are a bit 
more sophisticated.    
(Note that you can use the program without  suffix commands but
then you may spend more time on inputting the data.) 
Highly important: do not use a suffix command unless you have carefully read the 
instruction about it!   Improper use of suffix commands can easily lead 
to runtime errors!!! 



(4) Basic commands

A BASIC COMMAND must start at the beginning of its line and
this line cannot contain anything else. The scope of a basic command starts
in the next line and terminates at the next basic command. With the exception
of the <backslash>end command, the range of a basic command cannot be empty,
so it should be followed by at least one data line. The order of the basic
commands must be either the one described in (4/a) below, or the one
described in (4/b) below; concrete examples will be given in (6/a) and (6/b).

(4/a) The basic commands needed when we want to decide whether an inequality holds
in all lattices are as follows: 
<backslash>name
   Give here some nonempty name; the scope of the command is only a single line. 
<backslash>variables
   List the variables, at least three, separated by spaces. (And/or by commas.)
   Use alphanumerical names (which will be referenced here as TOKENS): 
   like  var1, x2, or y15; their lengths cannot exceed five characters. 
   The character "@" is forbidden to use.  Note that every data line should 
   be shorter than 255 characters, and it is read only before the first % character. 
   However, no empty line is allowed between the <backslash>name line and 
   the <backslash>end line, whence  even if % is used to introduce a comment, some 
   real data should precede it in the same line.
<backslash>subterms
   Every line of the scope of this command is of the form
   <token> = a {+,*}-term of EARLIER tokens 
   Spaces (but not within tokens and command names) make
   no effect on the program. For example, we can write
   p = ((((w + x) * y) +z)* w)   +   (x * (y+z))  + (y*z) 
   as a line in the scope of the <backslash>subterms command, provided that
   w, x, y, z  have previously occurred (as variables or terms). Again, the line 
   above cannot exceed 255 characters.
<backslash>inequality
   <token1> < <token2> 
   Both tokens should have previously occurred; the meaning is that we ask whether
   the <token1> <= <token2> holds in all lattices or not. The scope of this
   command is exactly one line, and this line should be followed by:
<backslash>end
   The program disregards the lines that follow the <backslash>end command; 
   so we can write comments there without %.

(4/b) The basic commands needed when we want to decide wheter a subset of 
the free lattice FL(n) generates freely a sublattice:
   the same as above, but instead of the <backslash>inequality command
   and the line following it, we have to use the following command and the 
   line following it:
<backslash>DoTheFollowingGenerateFreely
<token1> <token2> ... <token<k>
   Note at this point that the command names are case sensitive.         


(5) Suffix commands

 The SUFFIX COMMANDS are as follows; they are allowed only in the
  scope of the   <backslash>subterms    command. 
 If you use a suffix command, then it is strongly recommended to choose the 
 "Save partial computational details" option to see the action of the command!

(5/a)  <backslash>subs    % We use this command in the form
   <token> = a {+,*}-term of earlier tokens  <backslash>subs <token1> ... <token k> <backslash>by <token1'> ... <token k'>
   For example, we can have the following line:
g2 = ((((w + x) * y) + z) * w) + (x * (y + z))  \subs w x y z  \by   x w z y
   The action of this command is that the program replaces w by x, x by w, etc., and 
   parses this line only AFTER the substitution.

(5/b)  <backslash>sym3j   % We use this command in the form
   <token> = a {+,*}-term of earlier tokens  <backslash>sym3j <token1> <token2> <token3> 
   The action is that the program permutes <token1> <token2> <token3> in the term
   in all the six ways, and forms the join of these permuted  {+,*}-terms. E.g., you can write that 
g=x*(y+z) <backslash>sym3j x y z  %(here x, y, z are variables or earlier subterms)
   and then this input line is processed as if it was
g=(x*(y+z))+(x*(z+y))+(y*(x+z))+(y*(z+x))+(z*(x+y))+(z*(y+x))
   Since   <token> = <above-mentioned join> should be shorter than 255 characters,
   this command can be used only for sufficiently short lines!    

(5/c)  <backslash>sym3m
   Almost the same as the previous suffix command but now with 
   "forms the meet of" rather then "forms the join of".

(5/d)  <backslash>dual
   This suffix command instructs the program to change +,*,a,b,...,z,A,B,...,Z
   to *,+,A,B,...,Z,a,b,...,z  , respectively, in the input line BEFORE the first
   <backslash>,   except for variable names and parentheses.
   Explanation: variables are the same as their duals. This command names the dual of 
   a term by interchanging upcase characters with the corresponding lowercase ones.
   For example, if a term is called "ThiStR", then <backslash>dual will call its dual
   "tHIsTr". (If we do not use the <backslash>dual command, we do not have to insist
   to this convention on upper case and lower case letters.)
   WARNING: all terms AND their duals after the "=" sign in the line in question should 
   have previously been defined!!!    For example, we can write
<backslash>variables
      x  y
<backslash>subterms
      m=x
      M=x
      u=(x+m)*y <backslash>dual   % (refno n1)
  but we get a runtime error if the line "M=x" is missing. (The error message
  will complain about a not yet specified token and will display "U=(x*" )
 Note that the token before the = sign is also dualized, so the
   (refno n1) line above defines U as U=(x*M)+y  but u remains undefined. 
 Note also that the <backslash>dual command can be combined with any of the 
 previous two; in this case, this command comes after the other one in the line 
 but it is performed first.

(5/e)   <backslash>dualall
  This suffix command forces the <backslash>dual action to the current line
  AND to ALL subsequent lines until the <backslash>inequality or the 
  <backslash>DoTheFollowingGenerateFreely  line, regardles if  
  <backslash>dual does or does not occur later. So the action of the 
  <backslash>dualall  suffix command cannot be invalidated later. Note that 
  <backslash>dualall and <backslash>dual cannot occur in the same line.



(6) Two examples

(6/a) An example for an inequqlity
\name
Is  g_1 <= g_2+...+g_6; see Czédli: "A selfdual embedding of the free lattice ...", Lemma 3.1
\variables
w, x, y, z 
\subterms 
g1 = ((((w + x) * y) + z) * w) + (x * (y + z))  % Use copy-paste for what comes below!    
g2 = ((((w + x) * y) + z) * w) + (x * (y + z))  \subs w x y z  \by   x w z y  \dual
g3 = ((((w + x) * y) + z) * w) + (x * (y + z))  \subs w x y z  \by   x y z w
g4 = ((((w + x) * y) + z) * w) + (x * (y + z))  \subs w x y z  \by   w z y x  \dual
g5 = ((((w + x) * y) + z) * w) + (x * (y + z))  \subs w x y z  \by   y z w x
g6 = ((((w + x) * y) + z) * w) + (x * (y + z))  \subs w x y z  \by   z y x w  \dual 
q = G2 +g3 + G4+ g5+ G6
\inequality 
g1 < q    %Spaces make no effect on the program
\end
%Note the technique above: instead of modifying g1 by hand and risking typos in this way,
%we simply copy-pasted it and applied the \subs command to each of its copies.

(6/b) And example for free generation
\name
The proof (of the lion's share) of Lemma 3.1 in Czédli: "A selfdual embedding of the free lattice ..."
\variables
 w, x, y  z % To see how the program works for this data, copy this example into a separate file
\subterms 
g1 = ((((w + x) * y) + z) * w) + (x * (y + z))  % Use copy-paste for what comes below!    
g2 = ((((w + x) * y) + z) * w) + (x * (y + z))  \subs w x y z  \by   x w z y  \dual
g3 = ((((w + x) * y) + z) * w) + (x * (y + z))  \subs w x y z  \by   x y z w
g4 = ((((w + x) * y) + z) * w) + (x * (y + z))  \subs w x y z  \by   w z y x  \dual
g5 = ((((w + x) * y) + z) * w) + (x * (y + z))  \subs w x y z  \by   y z w x
g6 = ((((w + x) * y) + z) * w) + (x * (y + z))  \subs w x y z  \by   z y x w  \dual 
q = G2 +g3 + G4+ g5+ G6   
\DoTheFollowingGenerateFreely 
g1  G2
g3 G4   g5  G6
\end



(7) Further notes on input files

   The operations + (join) and * (meet) are not necessarily binary; terms
like (x+y+z)*(a+b)*c*(y+z+w+d)    are allowed (and highly recommended). 
Superfluous parentheses are allowed; however, while 
(((x+y+z)))*(a+b)*c*((y+z+w+d))  is practically the same as above,
(x+(y+z))*(a+b)*c*(((y+z)+w)+d)  slows the program a little.  
The program verifies the syntax of the data (but it is not guaranteed
that the reports on  errors are are always self-explanatory).
   The program does not recognize if a subterm like ((x+w)*(y+z))+x
occurs elsewhere. Hence, to accelerate the program, it
is a good idea to put a   <token1>=((x+w)*(y+z))+x     in the 
<backslash>subterms   part, and use the <token1> later. But
there is a warning here: the suffix commands work only at
text-editor-level; they are not recursive! So the 
<token1>=((x+w)*(y+z))+x  is recommended only if we do not
apply suffix commands in lines containing <token1> (or if we
are REALLY aware of what we are doing).
   Although every line can consist of at most 255 characters, the, say, 
<token1>=((x+w)*(y+z))+x    technique enables us to analyze
longer terms with the help of the program.