The experiments on specializing the word equation interpreters by the supercompiler SCP4

• The following examples run under the supercompiler SCP4. In order to execute the examples, you have to install the supercompiler SCP4. The #1-#5 examples all together may be transformed by execution of the module all_interpreters. The #6 and #7 examples all together may be transformed by execution of the module specialization_tasks.
• A word equation is an equation of the form W1 = W2, where W1 and W2 are arbitrary strings belonging to the joint alphabet of the symbols, symbol type variables, and string type variables. As a rule the set of all solutions of a given word equation is represented/enumerated with a rooted directed graph.
• The following encoding of the equations is used.

  	'A', 'B', ... ,'H' stand for the letters (belonging to the alphabet of the terminals);
  	'x', 'y', 'z', 'v', 'w', 'u', 't', 'p' ,'q' stand for the letter type variables;
  	'xs', 'ys', 'zs', 'vs', 'ws', 'us' stand for the string type variables.

The list of the interpreters used in the experiments:

Example #1 (The basic word equation interpreter: string type variables):

The source code of the interpreter

• Given any quadratic word equation, supercompilation of an input point of the form sampled below constructs a residual program that represents a rooted directed graph enumerating the solution set of the given equation.

• The specialization task is as follows, where %Int-Base-Source stands for the interpreter source code.

  <Scp   ................................................................................  >

  <Eq #e.Path <Encode ('xs ys A B A A A B = A B A A A B xs ys') >> %Int-Base-Source  ;

• The residual program representing the graph constructed for the word equation: 'xs ys A B A A A B = A B A A A B xs ys'.
  
• See the source code of the interpreter for a number of other specialization tasks.

Example #2 (Splitting equation from the left side: string type variables):

The source code of the interpreter

• Let any quadratic word equation or any word equation of the form T W = W T', where W is a word in the mixed alphabet of the letters and string type variables, while T, T' are words of the equal lengths not containing the variables, be given. Supercompilation of an input point of the form sampled below constructs a residual program that represents a rooted directed graph enumerating the solution set of the given equation.

• The specialization task is as follows, where %Int-Split-Source stands for the interpreter source code.

  <Scp   .........................................................................  >

  <Eq #e.Path <Encode ('xs xs A B A B = A B A B xs xs') >> %Int-Split-Source  ;

• The residual program representing the graph constructed for the word equation: 'xs xs A B A B = A B A B xs xs'.
  
• See the source code of the interpreter for a number of other specialization tasks.

Example #3 (Splitting equation from the both sides: string type variables):

The source code of the interpreter

• Let any quadratic word equation, or any word equation containing the only string type variable having any number of occurrences in the equation, or any word equation of the form T W = W T', where W is a word in the mixed alphabet of the letters and string type variables, while T, T' are words of the equal lengths not containing the variables, be given. Supercompilation of an input point of the form sampled below constructs a residual program that represents a rooted directed graph enumerating the solution set of the given equation.

• The specialization task is as follows, where %Int-Split2-Source stands for the interpreter source code.

  <Scp   ..........................................................................  >

  <Eq #e.Path <Encode ('xs xs xs B A B = B xs B xs xs') >> %Int-Split2-Source  ;

• The residual program representing the graph constructed for word equation 'xs xs xs B A B = B xs B xs xs' shows that this equation has no solutions.
  
• See the source code of the interpreter for a number of other specialization tasks.

Example #4 (Splitting equation from the left side: string and letter type variables):

The source code of the interpreter

• Let any quadratic word equation or any word equation of the form T W = W T', where W is a word in the mixed alphabet of the letters, letter type variables, and string type variables, while T, T' are words of the equal lengths not containing the string type variables, be given. Supercompilation of an input point of the form sampled below constructs a residual program that represents a rooted directed graph enumerating the solution set of the given equation.

• The specialization task is as follows, where %Int-SplitS-Source stands for the interpreter source code, while t, p, q stand for three different letter type variables.

  <Scp   ......................................................................................  >

  <Eq #e.Path <Encode ('xs t t ys ys xs A A = p q xs t t ys ys xs') >> %Int-SplitS-Source  ;

• The residual program representing the graph constructed for the word equation: 'xs t t ys ys xs A A = p q xs t t ys ys xs'.
  
• See the source code of the interpreter for a number of other specialization tasks.

Example #5 (Splitting equation from the both sides: string and letter type variables):

The source code of the interpreter

• Let any word equation from the class described in Example #4 or any word equation containing the only string type variable having any number of occurrences in the equation and any number of letter type variables, be given. Supercompilation of an input point of the form sampled below constructs a residual program that represents a rooted directed graph enumerating the solution set of the given equation.

• The specialization task is as follows, where %Int-Sort-Source stands for the interpreter source code, while t and q stand for two different letter type variables.

  <Scp   ................................................................  >

  <Eq #e.Path <Encode ('xs t xs B = q A xs xs') >> %Int-Sort-Source  ;

• The residual program representing the graph constructed for the word equation: 'xs t xs B = q A xs xs'.
  
• See the source code of the interpreter for a number of other specialization tasks.

Example #6 (Specialization task: the order of computation):

The input and residual programs

• Given any quadratic word equation, supercompilation of an input point of the form sampled below constructs a residual program that represents a rooted directed graph enumerating the solution set of the given equation, provided that variable 'ys' takes its value, when the value of the variable 'xs' is still undefined.

• The specialization task is as follows, where %Int-BaseS-Source stands for the source code of a version of the interpreter used in Example #1.

  <Scp   ...................................................................................................  >

  <Eq (#e.Path ('xs -> empty')) <Encode ('xs ys A B A A A B = A B A A A B xs ys') >> %Int-BaseS-Source  ;

• The residual program shows that, using Hmelevsky's method, the required solution paths do not exist.
  
• See the source code of the interpreter for a number of other specialization tasks.

Example #7 (Specialization task: possible values of variables):

The input and residual programs

• Let any word equation from the class described in Example #4, or any word equation containing the only string type variable having any number of occurrences in the equation and any number of letter type variables, be given.

• The specialization task is as follows, where %Int-SortS-Source stands for the source code of a version of the interpreter used in Example #5, while t and q stand for two different letter type variables.
• Supercompilation of an input point below constructs a residual program that represents a rooted directed graph enumerating the solution path set of the given equation. Additionally the residual program returns values of the parameter #s.Value that are generated on those paths successfully solving the equation 'A t xs xs = xs xs q A'. The function Filter is responsible for pruning the dead-lock branches leading to no-solution variants, during the specialization.

  <Scp   .........................................................................................................  >

  <Filter <Eq (#e.Path1 ('t -> ' #s.Value) #e.Path2) <Encode ('A t xs xs = xs xs q A') >>> %Int-SortS-Source  ;

• The residual program representing the graph constructed for word equation 'A t xs xs = xs xs q A' shows that the parameter #s.Value can take only 'A' as its value.
  
• See the source code of the interpreter for a number of other specialization tasks.