
\section{Conclusion}\label{sec:conclusion}

We present \tool{EqFix}, a system for fixing compilation and typesetting errors in \LaTeX~equations.
We design a DSL for expressing fixing rules 
and propose a synthesis algorithm to learn rules from user-provided examples.
Experiment results reveal the strengths of \tool{EqFix}:
(1) it is effective to synthesize an expected rule using only 1 -- 4 provided examples;
(2) it is efficient to synthesize a set of rules within 200 ms on average;
(3) it is applicable to many other domains as well, such as repairing buggy Unix commands.

\section{Evaluation}\label{sec:eval}

To measure the performance of \tool{EqFix} on fixing erroneous \LaTeX~equations,
we conduct experiments to answer the following research questions:
\begin{enumerate}[RQ1:]
    \item (Effectiveness) How effective is \tool{EqFix} at fixing \LaTeX~equations?
    \item (Practicality) How is the practicality of \tool{EqFix} in 
        realistic usage scenarios?
    \item (Extensibility) Can \tool{EqFix} be applied to other repairing
        scenes?
\end{enumerate}

\subsection{Experimental Setup}\label{sec:eval:setup}

\paragraph*{Dataset}

We collected input-output examples from the web, including online help forums, tutorials and technical blogs.
The corpus of examples reveal common mistakes made by \LaTeX~users, such as mismatch of delimiters and misuse of commands.
In total, we collected 445 examples, and classified them into 89 error categories where each contains 5 examples.
Unlike machine learning approaches, PBE techniques usually only need a few examples.
For instance, in \tool{NoFAQ} \cite{NoFAQ}, 2 -- 5 examples are needed to synthesize one fixing rule.
The average length of erroneous equations in our dataset is 20 (maximum 167,
minimum 5).
For ease of reference,
let $S_i$ be the $i$-th example group standing for the $i$-th error category.

\paragraph*{Training \& Testing}

We first set \tool{EqFix} to training mode: for each example group $S_i$,
record the top-10 candidates of the synthesized rules in the rule library.
We then set \tool{EqFix} to applying mode: query candidate corrections for every testcase and compare the results with expert-suggested corrections.
If any candidate of a testcase is identical to the expert-suggested correction of that testcase,
then we say the testcase is ``solved'', and report the number of attempted fixing rules so far.
Otherwise, we say it is ``failed''.

\paragraph*{Comparison}

Since \tool{NoFAQ} is also a PBE application targeting at repair tasks,
it is reasonable to compare the performance of \tool{EqFix} with \tool{NoFAQ}.
Due to difference of problem domain, \tool{NoFAQ}, which aims to repair buggy Unix commands,
requires an erroneous input command to be split into a token sequence by whitespaces --
\LaTeX~equations, however, \emph{cannot} be tokenized in such a way.
Therefore, we claim a comparison to \tool{NoFAQ} must be \emph{unfair}.
Even though, we did conduct an experiment in which we simply regarded the entire erroneous equation as a single token,
and unsurprisingly, \tool{NoFAQ} failed to solve any of our benchmarks.

Instead, we use \tool{FlashFill} as our baseline tool.
\tool{FlashFill} is a state-of-the-art synthesizer for string manipulation,
in particular, for solving string transformation tasks that spreadsheet users often encounter.
An input-output example of \tool{FlashFill} comprises a columns of strings as input, and a single string as output.
However, unlike \tool{EqFix}, \tool{FlashFill} does \emph{not} distinguish equations from error messages -- regarding both as ordinary strings.
Even though, we can still regard an erroneous equation and an error message as two \emph{indistinguished} columns of input and feed them into \tool{FlashFill}.

Moreover, \tool{FlashFill} does \emph{not} maintain a rule library.
To make a fair comparison, we decided to compare them group-by-group.
More specifically, for each example group, we synthesize the top-10 rules using
\tool{EqFix} and \tool{FlashFill}, respectively,
and then apply these rules to the test case of the same group,
and check if any of these rules solves the problem.

\paragraph*{Environment}

All experiments were conducted on an Intel(R) Core(TM) laptop with i7-8850H CPU (2.60GHz) and 16 GB memory, running Mac OS Mojave 10.14.4, with .NET core version 2.2.105.

\subsection{Effectiveness (RQ1)}\label{sec:eval:exp1}

Our first experiment compares the performance of \tool{EqFix} v.s. \tool{FlashFill}.
For each example group, we leave the example with the longest erroneous equation as the test case, and regard the others as training examples.
The training set for each example group is set to contain 1, 2, 3 and 4
shortest examples (i.e., with the shortest erroneous equation).
The above training configurations are referred to as C1, C2, C3 and C4, respectively.
Since \tool{FlashFill} does not maintain a rule library,
to make a fair comparison, for each example group, 
both \tool{EqFix} and \tool{FlashFill} were trained using only the training examples of that group (under the above four configurations), 
and then tested against the test case.
There are in total 356 training runs of \tool{EqFix} (also \tool{FlashFill}).

\input{fig/expr}

\paragraph{Learning Ability}

The overall number of solved test cases is presented in \cref{fig:solved}.
Under each of the above configurations, \tool{EqFix} outperformed \tool{FlashFill}.
When training with only one example (C1), \tool{EqFix} solved over 75\% of the test cases whereas \tool{FlashFill} failed to solve any.
Both \tool{EqFix} and \tool{FlashFill} performed better when more training examples were given.
This is well-understood, as more training examples can eliminate spurious
fixing rules and lead to more general rules.
\tool{EqFix} reached the highest solved rate 80.9\% when training with three examples (C3),
whereas even with the full training set (C4), \tool{FlashFill} solved less than half of the test cases.
This result illustrates that \tool{EqFix} has a stronger learning ability.

\input{tb/exp1.tex}

\cref{tb:exp1} presents more details -- the numbers of attempted rules for solving each test case.
A cross mark ``\Failed'' indicates that no (top-10) rules can yield the expected fixing result.
Among the solved test cases by \tool{EqFix}, at most 5 rules were attempted
(\#81), and 58 -- 68 test cases were solved by the top-ranked rule.
In contrast, \tool{FlashFill} attempted at most 8 rules (\#48) and at most 33 test cases were solved by the top-ranked rule.
We also recognize that providing more training examples helps to decrease the number of attempts, e.g. in \#4 and \#82.

\paragraph{Failure Cases}

\tool{EqFix} failed on 17 test cases when the full training set is enabled (C4).
Manually inspecting these cases, we classify the cause of failure into three categories:
\begin{itemize}
    \item Inconsistent examples (7 cases).
    In these cases, the provided examples are actually \emph{inconsistent} with each other, and consequently, our synthesizer failed to give any consistent fixing rule.
    To overcome this failure, the user has to either modify these examples by hand or suggest alternative ones, so that they become consistent.
    \item Insufficient error message (6 cases).
    In these cases, the provided error messages are \emph{insufficient} and hence \tool{EqFix} could not generate a useful equation pattern.
    For example, the error message ``\verb|Missing $ inserted|'' of \#12 does not contain any problem-specific information.
    Usually, the entire input equation must be transformed and since our string transformation DSL is inadequately expressive, the learned rules are overfitting to the training examples.
    \item Restricted DSL expressiveness (4 cases).
    In these cases, the test case is deviated from the training examples of the same group and due to the \emph{restricted expressiveness} of our DSL, the learned rule could not generalize to that test case.
    For instance, in \#79, the training examples all contain an ill-formed command (\t{ldots} or \t{frac}) which should begin with a backslash:
    \begin{center}
        \begin{tabular}{ll}
            ``\verb|$1,2,ldots,n$|'' & ``\verb|$34,51,ldots,n$|'' \\
            ``\verb|$frac{a}{b}$|'' & ``\verb|$frac{m}{n}$|'' \\
        \end{tabular}
    \end{center}
    The error message template is ``\t{? is a command}''.
    However, the test case $$``\verb|$\\frac{\partial y}{partial t}$|"$$
    contains both a well-formed command ``\verb|\partial|'' and an ill-formed one ``\verb|partial|'',
    which prevents the learned rule from transforming the ill-formed command merely.
\end{itemize}

\paragraph{Generalization Ability}

Due to the dynamic generation of equation patterns, the learned rules are \emph{insensitive} to positions where errors locale.
In example \#1 of \cref{tb:motivating}, the erroneous part $``\verb|10|"$
appears in the end of the input equation,
whereas in example \#2, $``\verb|123|"$ appears before $``\verb|+x|"$ in the input equation.
Although their positions are distinct, the rule synthesized by example \#1 is general enough to fix problem \#2,
as the generated equation pattern $P_2$ (in \cref{fig:demo-eval}) replaces $``\verb|123|"$ with $v_1$.
Conversely, the rules synthesized by \tool{FlashFill} are less general and in many cases as they are position-\emph{sensitive}.
According to our results, \tool{FlashFill} failed to solve any example shown in \cref{tb:motivating}.
To conclude, the learned rules by \tool{EqFix} have higher generalization ability.

\paragraph{Efficiency}

\cref{fig:syn-time} depicts the cumulative synthesis time when the number of training example group increases, under the configuration C4.
The average synthesis time was 139 ms for \tool{EqFix} and 434 ms for \tool{FlashFill}.
In 79 of 89 runs, \tool{EqFix} spent less time.
Further profiling results revealed that the efficiency is mostly due to a simpler string transformation DSL (\cref{sec:lang:trans:string-trans}).

\paragraph{Relaxer Extension}

We also noticed that in 33 (37\%) of the 89 synthesized rules under configuration C4, relaxers exhibited as a component of the synthesized rule.
This reveals that the relaxer extension of the rule DSL is necessary and it improves the practicality of our tool.
Without relaxers, these 33 synthesis tasks will fail.

\subsection{Practicality (RQ2)}\label{sec:eval:exp2}

Our second experiment executes \tool{EqFix} to fit a more realistic scene --
we first set the training mode of \tool{EqFix} to construct a rule library by
learning from the training set examples, and then set the applying mode of
\tool{EqFix} to test if the learned rules recorded in the library can deal with the problems in the testing set.

\cref{tb:exp2} summaries the overall results.
Interestingly, \tool{EqFix} solved one more test case \#71, compared with our first experiment.
In detail, it was solved by applying the top-ranked rule synthesized using examples of group \#69.

\begin{table}[h]
    \caption{Overall results of experiment 2.}
    \label{tb:exp2}
    \begin{tabular}{c|cccc}
    \toprule
   
    & C1            & C2            & C3            & C4            \\
    \midrule
    \#Solved        & 67 (75.3\%)  & 71 (79.8\%)  & 73 (82.0\%)  & 73 (82.0\%)   \\
    \zap{Training} Time (ms)       & 8478      & 9506      & 12060     & 14593 \\ 
    \bottomrule
    \end{tabular}
\end{table}

\tool{EqFix} allows users to enlarge the rule library in an incremental way.
Consider the following erroneous equation $eq^{*}$:
\begin{center}\verb|$\mu = \theta \cdot \^{r}$|.\end{center}
\LaTeX~engine prompts a compilation error that is never appeared in the above rule library (synthesized from 89 groups of examples), referred as $err^{*}$:
\begin{center}\verb|Please use \mathaccent for accents in math mode.|\end{center}
\begin{center}\verb|Command \^ invalid in math mode.|\end{center}
When feeding $eq^{*}$ to \tool{EqFix}, no applicable rules are found and therefore it fails to repair.
The user now may ask an expert for help. The expert may provide the following fixed equation $fix^{*}$:
\verb|$\mu = \theta \cdot \hat{r}$|.
So far, we have a new example $(eq^{*}, err^{*}, fix^{*})$.
Feeding this to \tool{EqFix}, a set of new fixing rules are synthesized (synthesis time: 425.2789 ms).
Using the top-ranked rule, we are able to solve the following two erroneous equations with the same type of error:
\begin{itemize}
    \item \verb|$\vec{x}_1=r_1\^{r}_1$|
    \item \verb|$E(w) = \frac{1}{2}*\sum\limits_{i=1}\^{N} ...$|
\end{itemize}

\subsection{Extensibility (RQ3)}\label{sec:eval:exp3}

In our last experiment, we evaluated \tool{EqFix} on the benchmark suite of
\tool{NoFAQ}\footnote{\url{https://github.com/MichaelBVaughn/NoFAQ}}, in the domain of repairing erroneous Unix commands.
The benchmark suite consists of 80 benchmarks, each of which consists of 3 examples.
We learn rules using the first two examples and leave the last one as the test case (totally 80 test cases).

In the 80 test cases of \tool{NoFAQ},
we identified that \tool{EqFix} successfully solved 68 (86.2\%) of them,
among which 67 were solved with the top-ranked rule.
\tool{EqFix} exceeded time limit 60 s on 3 cases;
it failed to synthesize rules for 8 cases;
the expected rule was not ranked in top-60 for only 1 case.

Although \tool{EqFix} is originally intended to repair \LaTeX~equations,
it is also applicable to the domain of repairing buggy Unix commands.
From our perspective, these two problems share a few common features:
(1) the erroneous target (an equation or a command) can be interpreted as a string;
(2) a message that reveals some information about the error is available.





\section{The EqFix System}\label{sec:impl}

We prototyped the proposed approach as a tool \tool{EqFix}, written in a combination of F\# and C\#, running on .NET core platform.
Rule application, synthesis algorithms and relaxer extensions were built from scratch 
following the approaches proposed in the paper.
We developed the synthesizer for the string transformation language $\mathcal{L}_\text{ST}$ under PROSE\footnote{https://github.com/Microsoft/prose} framework (proposed in \cite{flash-meta}),
in which we specified the syntax and semantic of our DSL,
a set of witness functions for guiding PROSE's synthesis engine,
and a set of scoring functions for ranking candidate programs.

\tool{EqFix} maintains all fixing rules learned so far in a \emph{rule library}.
This is indeed necessary, as we need different rules to solve a variety of different repairing tasks in practice.
\tool{EqFix} supports two running modes -- \emph{training mode} and \emph{applying mode}.
In the training mode, \tool{EqFix} learns a set of rules from user-provided examples,
and record them in the rule library.
For implementation reason, it is impractical and inefficient to store all candidate fixing rules.
Instead, we only store the top-ranked rules, using a user-specified rank $k$ (default 10), indicating the top-$k$ rules will be stored.

In the applying mode, an end user requests to repair an erroneous equation.
\tool{EqFix} searches in its rule library for all applicable rules, i.e. those whose error patterns can match against the error message, and attempts to apply them to the input equation.
If the fixing result is approved, then we are done.
Otherwise, \tool{EqFix} attempts the next applicable rule and the above interaction repeats.
It fails if (1) no applicable rules are found, or (2) all suggested results are rejected by the end user.
In either case, we expect an expert user to figure out a correction, which,
in association with the erroneous equation and the error message,
form a new example.
This new example can then be fed to \tool{EqFix} for incrementally learning a new rule to enlarge the rule library, by which several new equation repair problems (belonging to the same type) may be solved in future.

Error patterns are allowed to be incrementally inserted into the rule library, which makes it possible for users to extend their own keywords if a new error type is yet not covered by the rule library.
To achieve this, they simply prepare a set of examples, where they specify the error messages directly using the new keywords, and feed them to \tool{EqFix} for training.
The error pattern of the synthesized rules can match the new keywords.

Furthermore, we believe that \tool{EqFix} can gain benefit from \emph{source-crowded learning},
a technique that has been adopted in many synthesis applications such as \cite{error-messages,Crowd-Sourcing,Code-Feedback,NoFAQ},
where unsolved problems are published on the web and expert users are invited to post their solutions.
Combining \tool{EqFix}'s incremental rule library design with source-crowded learning,
a large rule library would be established and the power of \tool{EqFix} at solving equation repair problems would be significantly augmented.

\section{Introduction}

\LaTeX~is a plain text-based document preparation system,
and has been widely used in academia for publication and communication of scientific documents.
The powerful typesetting of mathematical equations makes it more and more popular in not only academia, but also industry.
\LaTeX-style equations have been integrated in both text-based document
editing languages like
Markdown\footnote{\url{https://daringfireball.net/projects/markdown/}},
and WYSIWYG (i.e., ``What you see is what you get'') document processors like
MS Word\footnote{\url{https://products.office.com/en-us/word}}.
Web plugins such as MathJax\footnote{\url{https://www.mathjax.org}} enable pretty display of \LaTeX~equations on webpages.
For ease of copying \LaTeX~equations from existing PDF documents, OCR-like
equation recognition tools such as
Detexify\footnote{\url{http://detexify.kirelabs.org/classify.html}} have been invented.
Nowadays, \LaTeX~has actually become a universal format for expressing mathematical equations.

Since the syntax of \LaTeX~equations is quite \emph{complex}, \emph{non-expert} users
may find it challenging to use.
For example, one may expect ``$x^{10}$'' by typing  
``\verb|$x^10$|''. This equation indeed compiles, however, its actual output
is ``$x^10$'', which goes against the user's expectation. 
When such an error happens, one may resort to online help-forums.
However, this process is never trivial.
First, the user has to provide several keywords (for searching) that well describe the error. 
Then, if the user is fortunate to obtain possible solutions, they may not necessarily work exactly for the user's problem -- he/she still has to adapt the solutions to that specific problem. 
The whole process (especially, the adaption of the solutions to one's own problem) requires not only intelligence but also patience. 


\emph{Programming by examples} (PBE) is believed to be a revolutionary technique for end-user programming
\cite{pbe,flash-fill,flash-normalize,flash-extract,ringer}.
It rescues users from repetitive and error-prone programming labors, by
automatically synthesizing useful programs from input-output examples, typically via search-based methods.
In recent decades, PBE has been adopted to the area of \emph{program repair},
such as patch generation \cite{PatchGen}, high-quality bug repair synthesis
\cite{S3}, etc. 
\zap{
To enable automated repair of \LaTeX~equations, we propose to express the
repair strategies 
by a sort of \emph{fixing rule}.
Since an end user may encounter a variety of errors, we need maintain a \emph{rule library} comprising a large set of fixing rules.
To establish a rule library, PBE techniques come into rescue --
every fixing rule can be synthesized from a set of \emph{input-output examples}, provided by experts, that demonstrate the underlying repairing strategy.
In this way, a fixing rule saved in the rule library may be applicable to an erroneous equation provided by an end user.
}%
\zap{
Observing that equations can be regarded as strings, one may suggest to
reduce the equation repair problem to the well-known string transformation problem and tackle it with, for example, \tool{FlashFill} \cite{flash-fill}.
This approach, however, is practically \emph{infeasible} and \emph{inefficient}.
For the equation repair problem, \emph{error messages} are always available,
either given by \LaTeX~engine,
or instantiated by end users (typesetting errors). 
The error messages usually tell us why an equation is erroneous, \tbd{or what's the
users' expectation}.
Such information is crucial for identifying which parts of the equation are \emph{relevant} to the repairing task and which are \emph{useless}.
Nonetheless, a general string transformation synthesizer does \emph{not} know about this.
Instead, it attempts to generate candidate transformers by analyzing the \emph{entire} input/output string, including the actual useless parts,
which are likely to bring about a large search space, and consequently prevent the synthesizer from generating any candidate within a reasonable time.
}%
\tool{NoFAQ}~\cite{NoFAQ} is an emerging technique that employs \emph{error messages} to assist the PBE-based repairing.
This tool aims to fix common errors in Unix commands, from an input-output example that consists of an erroneous Unix command, an error message prompted by Shell, and a rectified command specified by experts.
Note that the error messages prompted by Unix Shell are usually instantiated from
some predefined templates;
the stored information in the messages can thus be easily extracted (using a fixed pattern).

Inspired by \tool{NoFAQ} and other PBE techniques, we present \tool{EqFix}, a system for automatically fixing erroneous \LaTeX~equations by examples.
Note that \tool{NoFAQ} cannot be applied to our problem setting:
First, an equation error is not necessarily a compilation error. 
For instance, ``\verb|$x^10$|'' compiles but produces an unexpected result. 
For such errors, one needs to specify the error message by his/her own.
As a result, we cannot assume this message has a fixed structure (or, is instantiated from a template) as in
\tool{NoFAQ} (\cref{sec:error-pattern}). 
Second, the Unix command can be directly \emph{tokenized} into a sequence of
strings (using whitespaces as the delimiters). As a result, it is rather
straightforward (by comparing the tokenized strings in turn) to localize the
error position in the text of the Unix command. 
However, it is not the same case for equation text.
Instead, we have to collaborate the corresponding \emph{error message} to
tokenize an equation (\cref{sec:lang:core:pattern}). 

To the best of our knowledge, \tool{EqFix} is the \emph{first} attempt on equation repair using PBE techniques.
It can be used by novice users for automatically fixing common errors in
\LaTeX~equations; and also by expert users who contribute corrections for
erroneous equations.
We design a DSL for formally defining the fixing rules for erroneous \LaTeX~equations 
(\cref{sec:lang}).
Intuitively, a fixing rule consists of 
an \emph{error pattern}, which specifies what error messages this rule is
applicable, and a \emph{transformer} which performs the actual fixing via string transformation. 
We propose an algorithm for synthesizing fixing rules expressed by our DSL
from input-output examples (\cref{sec:syn}).

In real-world scenarios, error messages may be \emph{inadequately} informative to localize the error parts of an erroneous equation, and thus we are unable to synthesize a fixing rule.
We introduce \emph{relaxers} to describe 
the \emph{generalization} of equation patterns, with which the search space relating to the erroneous parts are expanded
and the synthesis problem will eventually be possible.
Moreover, we present a \emph{lazy} relaxer synthesis algorithm that avoids
\emph{over-generalization} (\cref{sec:relaxers}).
This is necessary because we wish to retain the underlying string transformer synthesis problem as simple as possible.

We evaluated \tool{EqFix} on a data set containing 445 real-world examples. 
Note that \tool{NoFAQ} is limited to the repairing of buggy Unix
commands, and cannot be applied to our problem settings. We thus
took the state-of-the-art PBE tool \tool{FlashFill} for comparison.
We found that \tool{EqFix} solved 72 (80.9\%) of them, whereas
\tool{FlashFill} solved only 39 (43.82\%).
Measuring execution time, \tool{EqFix} outperformed \tool{FlashFill} --
approximately twice faster.
We recognized that \tool{EqFix} is also applicable to other domains such as repairing buggy Unix commands (\tool{NoFAQ}).

The main technical contributions of this paper are summarized as follows:
\begin{itemize}
    \item We present \tool{EqFix}, a PBE-based system for automatically fixing erroneous \LaTeX~equations.
   
    \item We design a DSL for expressing fixing rules.
    We rely on equation patterns to extract and transfer relevant information between error messages
    and equations.
    \item We introduce relaxers to handle error messages that are inadequately
        informative and propose a lazy relaxer synthesis algorithm to avoid over-generalization.
    \item We conduct experiments on real-world examples.
    Results show great effectiveness and applicability of our approach.
\end{itemize}

\zap{
The remainder of this paper is organized as follows:
In \cref{sec:motivating}, we use real-world examples to illustrate our using scenarios and motivate our approach.
In \cref{sec:lang}, we present the formulation of a fixing rule.
In \cref{sec:syn}, we propose the key synthesis algorithm.
In \cref{sec:relaxers}, we propose relaxers and discuss pattern generalization process.
In \cref{sec:impl}, we provide implementation outlines of \tool{EqFix}.
In \cref{sec:eval}, we describe our evaluation method and discuss results and findings.
In \cref{sec:related}, we compare our work with existing techniques on program repair and program synthesis.
Finally, we conclude the paper in \cref{sec:conclusion}.
}

\section{Overview}\label{sec:motivating}

\input{tb/motivating}

We use several real-world examples (in \cref{tb:motivating}) to illustrate the
repairing of \LaTeX~equations. All of them were extracted from an online
\LaTeX~forum\footnote{\url{https://tex.stackexchange.com}}.
To be clear and short, we neglect the unchanged substrings of long equations.
Each example consists of three components -- the input equation $eq$, the
error message $err$ and the fixed equation $fix$. 
For convenience of reference, we number these examples from 1 to 8 and refer their components as $eq_i$, $err_i$, $fix_i$, for $1 \le i \le 8$, respectively.
The \LaTeX~output on each equation (if it compiles) is displayed after the
equation text.

\begin{table}
    \caption{Supported keywords (subset) by \tool{EqFix}.}
    \label{tb:keywords}
    \begin{tabular}{ll}
        \toprule
        Keywords  & Interpretations               \\ 
        \midrule
        superscript & expected as a superscript \\
        subscript   & expected as a subscript   \\
        set         & expected as a set \\
        function    & expected as a math function/operator \\
        greek letter    & expected as a greek letter \\
        fraction numerator   & expected as numerator of a fraction \\
        fraction denominator & expected as denominator of a fraction \\
        operator sum         & expected as a sum operator \\
        operator product     & expected as a product operator \\
        long arrow           & expected as a long arrow \\
        \bottomrule
    \end{tabular}
\end{table}

Examples \#1 -- \#4 present a scene where a user expects a superscript but forgets to parenthesize the entire superscript expression.
As shown in \#1, given the input equation ``\verb|$x^10$|'' ($eq_1$),
\LaTeX~engine treats only ``\verb|1|'' but not the entire number ``\verb|10|'' as the superscript.
In this way, it outputs ``$x^10$'', which is obviously against the user's intent.
Note that the input equation $eq_1$ itself is syntactically correct, indicating the \LaTeX~engine will not report any error.
However, the output goes against the user's intent.
In this way, the user is required to specify an error message by hand to express his/her intent.
To express the error type conveniently, a set of predefined \emph{keywords} (\cref{tb:keywords} presents a subset supported by our system) are provided for selection.
Then, the user needs to point out a substring of the input erroneous equation to show the error location.
The error message is a combination of the keywords and substring of the input equation.
Here, in $err_1$, ``\verb|superscript|'' is a predefined keyword indicating a certain substring of the input equation is expected to be the superscript, and ``\verb|10|'' gives the error location.
Then, an expert may fix\footnote{Alternatively, we may get the fix by search online.} the input equation as ``\verb|$x^{10}$|'', i.e. surrounding ``\verb|10|'' with a pair of curly brackets.
The three components, i.e, $eq_1, err_1, fix_1$, compose an input-output
example, with which we can synthesize a fixing rule.
Intuitively, the underlying fixing strategy of this rule would be ``surrounding the superscript with a pair of curly brackets''.

\tool{EqFix} maintains a \emph{rule library} that contains all synthesized rules. When a new
example is added, \tool{EqFix} first searches in its rule
library to obtain a rule that can be \emph{refined} to be \emph{consistent} with
this new example. 
For instance, the example \#2 can be added by refining the fixing rule 
synthesized merely by \#1. 
If it is not the case (for instance, consider the examples \#5 to \#8), a new rule is
synthesized and added to the system.
One may also provide examples \#1 and \#2 at once,
and \tool{EqFix} will synthesize a rule that is consistent with both of them.
When more examples are provided, the ambiguity of the user's intent is mitigated,
and thus the synthesized rule becomes more precise and effective.

Given an \emph{equation repair problem}, 
i.e., an erroneous equation together with an error message, 
\tool{EqFix} will use the existing rules to automatically produce a correction. 
For instance, the rule synthesized by examples \#1 and \#2 is applicable to
equation repair problems \#3 and \#4, i.e.
applying this rule on $(eq_3, err_3)$ and $(eq_4, err_4)$ gives $fix_3$ and $fix_4$ respectively.

Examples \#5 -- \#6 exhibit an error of unmatched brackets.
In \#5, a right curly bracket (`\verb|}|') is missing in the input equation ``\verb|${1,2,3$|''.
This equation cannot be compiled, and the \LaTeX~engine will prompt an error
message ``\verb|Missing } inserted|'', instantiated from a predefined
message template.
A possible correction suggested by an expert (or a searched result) may be 
``\verb|${1,2,3}$|'',
which inserts the missing right curly bracket at the end of the equation.

In examples \#7 -- \#8, a user regards the superscript operator ``\verb|^|''
as a command by mistake and writes ``\verb|\^|''. Again, neither of these two equations
can be compiled, and 
an error message ``\verb|Command \^| \verb| invalid in math mode|'' is prompted.
A possible correction is to use ``\verb|^|'' instead.
Observe that the equation in example \#8 is much more complicated than that of \#7, while
it can be automatically fixed using the rule synthesized from \#7. 

In summary, \tool{EqFix} facilitates an automated approach for fixing common errors
in editing \LaTeX~equations.
Our approach is rule-based (\cref{sec:lang}) and the fixing rules are automatically
synthesized from a set of input-output examples (\cref{sec:syn}).
One benefit of our system is that we may collect in advance many examples and train a
set of fixing rules from them. This training process is transparent (i.e. a black box) to the end users. 
Another benefit is that the manual efforts of
adapting the searched correction to his/her own cases, which might be the most challenging part to end users, are saved.
\section*{Acknowledgments}
  This work was supported in part by 
  the NSF of China (No. 61672310 and No. 61527812),
  the National Key R\&D Program of China (No. 2018YFB1308601),
  and the Guangdong Science and Technology Department (No. 2018B010107004). 


\section{Related Work}\label{sec:related}

\paragraph*{Program Repair}
Automated program repair aims to automatically correct programs 
so that they satisfy a desired specification \cite{Challenges-Repair}.
Heuristic-based repair tools such as \tool{GenProg}
\cite{GenProg-GP,GenProg,GenProg-Study}
employs an extended form of genetic programming with heuristics\zap{and evolves program variants until the correct one is found}.
However, it is shown that these techniques produce patches that 
overfit to the test suite \cite{Overfitting}.
Ranking techniques have been studied to address the problem.
\tool{ACS} \cite{ACS} produces precise patches\zap{that have a relatively high probability to be correct}
with a refined ranking technique for condition synthesis.
\tool{PAR} \cite{PAR} mines bug fix patterns from the history
and gives frequently occurring fixes high priority\zap{in the random search process}.
\tool{Prophet} \cite{PatchGen} outperforms the previous works by
learning a probabilistic model for ranking the candidate patches.

Semantics-based repair techniques generate repairs via symbolic execution \cite{SemFix, Angelix}
and program synthesis \cite{SPR}.
Such techniques, however, are also suspected to overfit to the test suite.
Recently, a new repair synthesis engine called \tool{S3} is proposed \cite{S3}.
It leverages \emph{Programming by Examples} (PBE) methodology 
to synthesize high-quality bug repairs, with elaborating a number of ranking features.

Technically, \tool{EqFix} belongs to the semantics-based family.
To avoid overfitting, we also rely on the a ranking technique for promoting rules with a high generality.
Furthermore, syntactic errors are common and must be tackled in equation repair, while it is usually neglected in program repair,
as people concern more about bugs \cite{Repair-Survey}.
\tool{HelpMeOut} \cite{error-messages} aids developers to debug compilation
and run-time error messages by suggesting past solutions.
Unlike \tool{EqFix}, it only provides related examples and cannot create repairs for new problems.

\tool{NoFAQ} \cite{NoFAQ} is a system for fixing buggy Unix commands using PBE.
Although the problem domain is similar to ours, due to its lazy synthesis algorithm,
it only can synthesize a practical fixing rule when at least two examples are provided,
whereas in many cases, one example is sufficient for \tool{EqFix}.
Apart from that, the DSL of \tool{NoFAQ} can only accept tokenized strings (separated by spaces) as its input.
However, in our problem domain, there is no direct way to tokenize an erroneous equation.
We thus introduce the equation patterns and propose a mechanism for synthesizing them.
These equation patterns help to pattern match against an equation and extract the variant parts, which need be transformed later.

\paragraph*{Text Transformation}
\tool{FlashFill} \cite{flash-fill} pioneered in text transformation via program synthesis
and was later extended for semantic transformation \cite{Semantic-String}.
A similar technique is put into a live programming environment by \tool{StriSynth} \cite{StriSynth}.
\tool{FlashExtract} \cite{flash-extract} automates data extraction 
by highlighting texts on web pages.
String transformation is performed at a high level in these techniques,
but it is not suitable for repairing equations.
We realize that error messages guide the repairing process.
By pattern matching the error messages, we only perform transformation on a few variables
instead of the entire equation, which is simpler and takes less time.

\paragraph*{VSA-based Program Synthesis}
\emph{Version space algebra} (VSA) has been widely adopted in PBE applications \cite{VSA-PBD, flash-normalize, flash-meta, ringer, transformation, prog-trans}.
In those applications, VSA is critical as the set of candidate programs is possibly very large.
In \tool{EqFix}, the synthesized rules are represented compactly with VSA.

VSA-based program synthesis has also been applied in program transformation.
\tool{Refazer} \cite{prog-trans} is a framework that automatically learns program transformations
at an abstract syntax tree level.
\citet{data-structure} propose a method for example-guided synthesis of
recursive data structure transformations in functional programming languages.
\citet{graph-based} present a graph-based technique that guides developers in adapting API usages.
\section{Rules Extension: Relaxers}\label{sec:relaxers}

If the generated equation pattern does not match against the corrected equation,
the synthesis algorithm we proposed in \cref{sec:syn:transformer} will fail.
In this section, we tackle this issue by introducing \emph{relaxers} on equation patterns.

\subsection{Lazy Relaxation}



\begin{example}\label{case:relaxer:mot-1}
Consider example \#5 of \cref{tb:motivating}, where
\begin{itemize}
    \item \(eq_5 = ``\verb|${1,2,3$|"\),
    \item \(fix_5=``\verb|${1,2,3}$|"\), and
    \item \(err_5 = ``\verb|Missing } inserted|"\).
\end{itemize}
Let $EP_2 \defas [``\verb|Missing|", v_1, ``\verb|inserted|"]$ be the error pattern.
Matching $EP_2$ against $err_5$ gives $\sigma_5=\{ v_1 \mapsto ``\verb|}|" \}$.
From $eq_5$ and $\sigma_5$, an equation pattern \( P_5=[``\verb|${1,2,3$|"] \) is generated.
We see that $P_5$ cannot be matched by $fix_5$.
However, a more general pattern such as $[v]$ where $v$ is a fresh variable, is matched with $fix_5$.
\end{example}

\begin{example}\label{case:relaxer:mot-2}
Consider
    $eq = s_1 \concat s_2 \concat s_3 \concat s_4$, 
    $fix = s_1 \concat s_2' \concat s_3' \concat s_4'$, 
and $\sigma = \{ v_1 \mapsto s_2, v_2 \mapsto s_4 \}$.
Note that $s_2$, $s_3$ and $s_4$ are all modified in $fix$ compared to
$eq$, however $s_3$ is not bound to a variable in $\sigma$.
From $eq$ and $\sigma$, an equation pattern $[s_1, v_1, s_3, v_2]$ is generated,
which apparently does not match against $fix$.
However, a more general pattern like $[s_1, v]$ ($v$ is a fresh variable)
can match $fix$, where $v$ is matched against $s_2' \concat s_3' \concat s_4'$.
\end{example}

In general, if the generated equation pattern cannot match the output equation,
we can always replace several string matchers with fresh variables, until it matches against the output equation -- we call this process \emph{pattern relaxation}.
As the relaxation goes on, the pattern becomes more and more general.
In the worst case, it gives $P_\top=[v]$ that consists of a single variable $v$ and can be matched by any string (as in \cref{case:relaxer:mot-1}).
To find a relaxed pattern that is as strict as possible, we propose a \emph{lazy relaxation process}.

\paragraph*{Lazy Relaxation Process}

Let $P$ be an equation pattern, and $s$ be a string (i.e. the output equation).
First of all, the process terminates as soon as $P$ already matches against $s$.
As a special case, if $P$ is a constant (i.e. contains no variables), $P_\top$ is the only possible relaxed pattern.
In general, since $P$ cannot match against $s$, there must be some string $s'$ in $P$
that is not a substring of $s$.
Three kinds of relaxations are performed on $P$ depending on the relative position (i.e. left, right, or binary) of $s'$ in $P$:
\begin{itemize}
    \item (left) If $s'$ appears at the beginning of $P$,
    we replace the subpattern that consists of $s'$ and the variable $V$ followed by it,
    with a fresh variable $\tk{LVar}(V)$.
    \item (right) If $s'$ appears in the end of $P$,
    we replace the subpattern that consists of $s'$ and the variable $V$ before it,
    with a fresh variable $\tk{RVar}(V)$.
    \item (binary) If $s'$ appears in the middle of $P$,
    we replace the subpattern that consists of $s'$ and the adjacent variables $V_1$ and $V_2$,
    with a fresh variable $\tk{BVar}(V_1,V_2)$.
\end{itemize}
It can be concluded that for any of the above cases,
the relaxed pattern is always a valid equation pattern, i.e.,
variable and string matchers appear alternatively.
The relaxation continues until the relaxed pattern matches against $s$.

\begin{example}\label{ex:relax:special}
   
    Pattern $P_5$ in \cref{case:relaxer:mot-1} is relaxed to $P_\top$. 
   
\end{example}
\begin{example}\label{ex:relax:easy}
   
    Pattern $[s_1$, $v_1, s_3$, $v_2]$ in \cref{case:relaxer:mot-2}
    is relaxed to $[s_1, \tk{BVar}(v_1, v_2)]$.
\end{example}

\begin{example}\label{ex:relax:hard}
    Consider a pattern
    $[s_1, v_2, s_3, v_4, s_5, v_6, s_7]$
    and an output equation 
    $s_1' \concat s_2 \concat s_3 \concat s_4 \concat s_5' \concat s_6 \concat s_7'$.
    It takes several steps to obtain the relaxed result. In the
    following, we use an underline to highlight the relaxed subpattern,
    and a star to highlight the unmatched string:
    \begin{align*}
        [\underline{s_1^{*}, v_2}, s_3, v_4, s_5, v_6, s_7]
        &\to [\tk{LVar}(v_2), s_3, \underline{v_4, s_5^{*}, v_6}, s_7] \\
        &\to [\tk{LVar}(v_2), s_3, \underline{\tk{BVar}(v_4, v_6), s_7^{*}}] \\
        &\to [\tk{LVar}(v_2), s_3, \tk{RVar}(\tk{BVar}(v_4, v_6))]
    \end{align*}
\end{example}



\begin{figure}[t]
    \centering
    \begin{align*}
        \text{Rule}~\mathcal{R} &::= \pair{EP, \{r_1, \ldots, r_k\}, \mathcal{T}} \\
        \text{Relaxer}~r &::= \tk{id}(v) \mid \tk{LRelax}(r) \mid \tk{RRelax}(r) \mid 
            \tk{BRelax}(r_1, r_2) \\
        \text{Variable}~V &::= v \mid \tk{LVar}(V) \mid \tk{RVar}(V) \mid \tk{BVar}(V_1, V_2)
    \end{align*}
    \caption{Syntax of the extended rule DSL.}
    \label{fig:core-lang-ext}
\end{figure}

\paragraph*{DSL Extension}

The fixing rule DSL needs to be extended (\cref{fig:core-lang-ext}) with \emph{relaxers}
\tk{LRelax} (for left), \tk{RRelax} (for right) and \tk{BRelax} (for binary) to distinguish relaxation positions.
The identity relaxer \tk{id} stands for no relaxation.
Moreover, variables are extended to include the fresh variables introduced by the relaxation process.
In applying a rule with relaxers, one or more subpatterns of the generated equation pattern will be substituted with fresh variables according to the relaxers.




\subsection{Relaxer Synthesis}\label{sec:relaxers:syn}

To synthesize a rule with relaxers,
we need an extra step that generates the relaxers after we have synthesized the equation pattern $P$ for some input-output example $(eq, err, fix)$.
Suppose that $P$ already matches against $fix$,
then no relaxation is needed and an empty set of relaxers is returned.
Otherwise, we follow the lazy relaxation process to generate a relaxed pattern $\hat{P}$.
Note that in $P$, \tk{LVar}, \tk{RVar} and \tk{BVar} variables can be used to trace the relaxation process,
we can ``reproduce'' the relaxing process by directly translating them into relaxers:

\begin{itemize}
    \item For \cref{ex:relax:special}, $r_\top$ is the synthesized relaxer.
    \item For \cref{ex:relax:easy}, $\tk{BRelax}(\tk{id}(v_1), \tk{id}(v_2))$ is synthesized from $\tk{BVar}(v_1, v_2)$.
    \item For \cref{ex:relax:hard}, the synthesized relaxers are $\{r_1, r_2\}$, where $r_1=\tk{LRelax}(\tk{id}(v_2))$ is translated from $\tk{LVar}(v_2)$,
        and $r_2=\tk{RRelax}(\tk{BRelax}(\tk{id}(v_4), \tk{id}(v_6)))$ is
        from $\tk{RVar}(\tk{BVar}(v_4, v_6))$.
\end{itemize}

Suppose multiple examples are provided, the synthesized relaxers will be updated in each iteration.
In the first iteration, the first example is processed as above, yielding a set of relaxers $R_1$.
When processing the $i$-th ($i \ge 2$) example $(eq_i,err_i,fix_i)$,
the previously synthesized relaxers $R_{i-1}$ are inherited and applied on the equation pattern $P_i$, generating $P_i'$.
The relaxation is then performed on $P_i'$ instead of $P_i$.
The relaxed pattern $\hat{P_i}$
is then translated into $R_i$.
The algorithm terminates when all examples have been processed.



\section{Rules in EqFix}\label{sec:lang}

\tool{EqFix} is a rule-based system.
Rules in \tool{EqFix} are defined by a \emph{domain-specific language} (DSL) as presented in \cref{fig:core-lang}.
Each \emph{rule} $\mathcal{R}$ is a pair $\pair{EP, \mathcal{T}}$, where 
(1) $EP$ is an error pattern, specifying what kinds of erroneous
        equations can be fixed by this rule, and
(2) $\mathcal{T}$ is a transformer, specifying how to fix the equations.

\begin{figure}[t]
    \begin{align*}
        \text{(Fixing) rule}~\mathcal{R} &::= \pair{EP, \mathcal{T}} \\
        \text{Transformer}~\mathcal{T} &::= \{v_1 \mapsto \tau_1, \ldots, v_k \mapsto \tau_k\} \\
        \text{Error pattern}~EP &::= [M_1, \ldots, M_k] \\
        \text{Matcher}~M &::= s \mid v \\
        \text{Equation pattern}~P &::= [M_1, \ldots, M_k]
    \end{align*}
    \caption{Syntax of fixing rules.
   
    }
    \label{fig:core-lang}
\end{figure}

Given an input equation $eq$ and an error message $err$, we first test if
$err$ matches the error pattern $EP$ or not. If it does, the rule will be applicable to
this equation: we proceed to apply $\mathcal{T}$ to generate the fixed
equation $fix$. Otherwise, the rule is not applicable: \tool{EqFix} 
continues to test another rule and the above process repeats. 

\subsection{Error Pattern}\label{sec:error-pattern}

An error message is either prompted by the \LaTeX~engine (e.g. \#5 -- \#8 of \cref{tb:motivating}),
or specified by the user if the generated output goes against the user's expectation (e.g. \#1 -- \#4 of \cref{tb:motivating}).
For the latter case, we assume the error message start with one or more predefined \emph{keywords} that mention the error type, and then followed by a substring of the erroneous equation which locates the error.
In either case, we represent the error message as a natural language sentence that can be split into a list of \emph{tokens} $[e_1, \ldots, e_k]$ by delimiters (whitespaces, commas, etc.).
\tool{EqFix} is unaware of the resource of the error messages and employs a unified \emph{error pattern} to match against them.
In this way, users are allowed to invent their own keywords because \tool{EqFix} will regard them as normal tokens.

An \emph{error pattern} $EP = [EM_1, \ldots, EM_k]$ contains a list of \emph{matchers}, where each of them is either:
(1) a \emph{string matcher} $s$ that only matches against $s$ itself, or
(2) a \emph{variable matcher} $v$ that matches against any token and binds the matched token to $v$.
An error message $[e_1, \ldots, e_{k'}]$ matches $EP$ if
(1) they have the same length ($k = k'$), and
(2) every token $e_i$ ($1\le i\le k$) matches the corresponding matcher $M_i$.
The matching result (if succeeds) is a mapping from variables to the bound string values $\{v_1\mapsto s_1, \ldots, v_k\mapsto s_k\}$.

\zap{
Let $\mathcal{V}$ be the set of \emph{variables} appeared in a certain error pattern.
The \emph{environment} $\sigma$ (of type \t{env}) is a set of variable bindings, represented by
$\{v_1\mapsto s_1, \ldots, v_k\mapsto s_k\}$, indicating that $s_i$ is bound to $v_i$ ($1 \le i \le k$).
We denote an empty environment by $\emptymap$.
We obtain the string bound to a variable $v$ by $\sigma(v)$.
An \emph{update} to $\sigma$, written $\sigma|_{v\mapsto s}$,
is a new environment $\sigma'$ where $v$ is now bound to $s$, and all other bindings remain unchanged.

We use $\emptystr$ to denote the empty string,
and $s_1\concat s_2$ to denote the concatenation of two strings $s_1$ and $s_2$. 
The operator $\concat$ is also used to denote the concatenation of two lists.

During the matching process, all variable bindings (in case the matcher is a variable) are
collected into an environment $\sigma$.
The matching process is defined as a function $\sem{EP} :: \t{string} \to \t{env}?$ ($\t{env}?$ indicates the union of $\t{env}$ and failure $\fail$),
which takes an error message $err$ as input,
and returns an environment $\sigma$ that contains all variable bindings if the match succeeds,
and $\fail$ if fails.
}

\begin{example}\label{ex:err-pattern}
    Consider $err_2 = [``\verb|superscript|", ``\verb|123|"]$ from \cref{tb:motivating}.
    Let $EP_1 \defas [``\verb|superscript|", v_1]$ be an error pattern.
    Matching $err_2$ against $EP_1$ succeeds with $\{v_1 \mapsto ``\verb|123|"\}$, i.e.,
    $``\verb|123|"$ is bound to $v_1$.
\end{example}

\subsection{Equation Pattern}\label{sec:lang:core:pattern}

Unlike an error message, an equation text usually involves complicated syntax and thus cannot be directly tokenized by commonly seen delimiters.
To extract the problem-specific information from an equation (e.g., to find the cause of the error),
we propose the notion of an \emph{equation pattern}.

An \emph{equation pattern} $P = [M_1, \cdots, M_k]$ consists of a list of matchers.
Especially, the string and variable matchers in $P$ must appear \emph{alternatively},
that is, if $M_i$ is a string, then $M_{i+1}$ must be a variable, and vice versa.
Intuitively, the string matchers in an equation pattern are indeed used as
``delimiters'' to tokenize the equation into a list of ``tokens''. 
Each ``token'' of the equation matches a variable matcher and may convey some
\emph{problem-specific} information which may be useful later in generating a corrected equation.
Oppositely, if we allow consecutive variable matchers to appear in an equation pattern, the split would be \emph{ambiguous}.
For instance, consider a string $``\verb|alpha|"$ and an equation pattern $[v_1,v_2]$,
we could either let $v_1$ match against ``\verb|a|'' (and $v_2$ match against ``\verb|lpha|''),
or let $v_1$ match against ``\verb|al|'' (and $v_2$ match against ``\verb|pha|''), etc.

\paragraph*{Pattern Matching}

Given that string and variable matchers appear alternatively, we can pattern match an equation pattern $P$ against an equation $s$ in an unambiguous way:
(1) when a string matcher $s$ is encountered, we expect $s$ to be a prefix of the equation and this is exactly what $s$ matches against, or else the matching fails;
(2) when a variable matcher $v$ is encountered, we let $s$ be the consecutive string matcher and expect the equation to contain $s$ as a substring --
if so, we regard the prefix precedes $s$ as what $v$ matches against;
if not, the matching fails.

\zap{
The above process is formally defined as a recursive function $\msem{P}:: \t{string}\to\t{env}\to\t{env}?$,
which takes an environment $\sigma$ (initial empty) with an equation $s$ as inputs,
and returns the updated environment if the process succeeds, or $\fail$ otherwise:
\begin{align*}
    \msem{\tk{Nil}}~s~\sigma &= \kword{if}~s=\emptystr~\kword{then}~\sigma~\kword{else}\fail \\
    \msem{[v] \concat P}~s~\sigma &=
    \!\begin{aligned}[t]
        & \kword{if}~s=s_1\concat s_2~\text{s.t.}~s_2~\text{matches}~P \\
        & \kword{then}~\msem{P}~s_2~\sigma|_{v\mapsto s_1}~\kword{else}\fail
    \end{aligned}\\
    \msem{[s_1] \concat P}~s~\sigma &= \kword{if}~s=s_1\concat s_2~\kword{then}~\msem{P}~s_2~\sigma~\kword{else}\fail
\end{align*}
}

For example, consider the equation ``$\{x_1\}$''
and the equation pattern $[v_1$, ``$x_1$'', $v_2]$.
Since ``$x_1$'' is a substring of the equation (as a string), we can split
the equation string into three parts as ``$\{$'' $\concat$ ``$x_1$'' $\concat$
``$\}$''.
Pattern matching succeeds with $\{v_1 \mapsto$ ``$\{$'', $v_2 \mapsto$ ``$\}$'' $\}$.

\paragraph*{Pattern Instantiation}

We could regard equation pattern as a sort of ``abstraction'' of the string representation of an equation,
where variable matchers behave like ``placeholders''.
Once given the bound strings of these variables, we can \emph{instantiate} an equation pattern by replacing them with the bound strings, and we obtain a constant string without any ``placeholder''.
\zap{
We call such a process \emph{pattern instantiation}.
We formulate it as a recursive function $\asem{P}:\t{env}\to\t{string}$,
which takes an environment $\sigma$ as input, and returns the instantiation of $P$ by $\sigma$.
\begin{align*}
    \asem{\tk{Nil}}~\sigma &= \emptystr \\
    \asem{[v] \concat P}~\sigma &= \sigma(v) \concat \asem{P}~\sigma \\
    \asem{[s] \concat P}~\sigma &= s \concat \asem{P}~\sigma
\end{align*}

We see pattern instantiation is a reverse process to pattern matching:
\begin{proposition}\label{thm:msem-asem}
    For every equation pattern $P$, let $\sigma$ be an environment which contains all the variables
    appeared in $P$.
    If $\asem{P}~\sigma=f$, then $\msem{P}~f~\emptymap=\sigma'$ and $\sigma'\supseteq\sigma$.
\end{proposition}
}
In fact, pattern instantiation is a reverse process to pattern matching.
\begin{example}\label{ex:matcher}
    Consider example \#2 of \cref{tb:motivating}, where \( eq_2=``\verb|$y^123+x$|" \).
    Let \( P_2 \defas [``\verb|$y^|", v_1, ``\verb|+x$|"] \) be an equation pattern.
    Matching $eq_2$ against $P_2$ gives $\sigma=\{v_1 \mapsto ``\verb|123|"\}$.
    Further, instantiating $P_2$ with $\sigma$ gives back $eq_2$.
\end{example}

\paragraph*{Pattern Generation}

In \tool{EqFix}, equation patterns are not explicitly presented in the rule.
In fact, they are only \emph{intermediate} results generated when applying a rule.
To obtain an equation pattern $P$ from an erroneous equation $eq$ with the matching result $\sigma=\{v_1 \mapsto s_1, \ldots, v_k \mapsto s_k\}$ by an error pattern, 
we substitute all the occurrences of $s_1, \ldots, s_k$ in $eq$ with $v_1, \ldots, v_k$, respectively.

\begin{example}\label{ex:pattern-gen}
    Given $\sigma=\{v_1 \mapsto ``\verb|123|"\}$ and \( eq_2=``\verb|$y^123+x$|" \),
    applying the above process yields
    \( [``\verb|$y^|", v_1, ``\verb|+x$|"] \).
\end{example}

\zap{
We summarize the relationship among the three operations defined on an equation pattern as follows:

\begin{center}
    \begin{tabular}{llll}
        operation & equation pattern & equation (string) & environment \\ \hline
        pattern matching & input & input & output \\
        pattern instantiation & input & output & input \\
        pattern generation & output & input & input \\
    \end{tabular}
\end{center}
}

\zap{
We note that $\sigma_1=\sigma^{err}_1$.
Generally speaking,
$\msem{\t{genPattern}~s~\sigma}~s~\emptymap=\sigma$ holds for any string $s$ and environment $\sigma$.

There are conditions where \t{genPattern} can generate invalid patterns.
For instance, given the input string $s=s_1 \concat s_2 \concat s_3$,
the environment $\sigma=\{v_1 \mapsto s_2, v_2\mapsto s_3\}$,
$\t{genPattern}~s~\sigma$ generates $[s_1, v_1, v_2]$, which is invalid.
To fix this problem, we can insert a string with a single white space (\textvisiblespace)
between $v_1$ and $v_2$ and have the valid pattern
$[s_1, v_1, \textvisiblespace, v_2]$ as the result.
}

\subsection{Transformer}\label{sec:transformer}

Our DSL achieves an underlying repairing strategy via string transformation.
A \emph{string transformer} is a function that maps a string into a new one.
In \tool{EqFix}, we apply a string transformer to a substring extracted from an input erroneous equation,
and regard the obtained new string as a substring of the corrected equation.
Given an equation pattern, only the substrings that match variable matchers need be transformed.
Thus, we define a \emph{transformer} as a mapping from the variables into the (underlying) string transformers,
denoted by $\{v_1 \mapsto \tau_1, \ldots, v_k \mapsto \tau_k\}$, where each
$v_i$ is a variable and each $\tau_i$ is an string transformer (will be explained in \cref{sec:lang:trans:string-trans}).

\zap{
A transformer $\mathcal{T} = \{v_1 \mapsto \tau_1, \ldots, v_k \mapsto \tau_k\}$ is regarded as a sequence of updates to an environment $\sigma$.
We define the operation as a function $\sem{\mathcal{T}}::\t{env}\to\t{env}$, where
$$\sem{\{v_1 \mapsto \tau_1, \ldots, v_k \mapsto \tau_k\}}~\sigma =
    ((\sigma|_{v_1\mapsto \tau_1(\sigma(v_1))})_{\ldots})|_{v_k\mapsto\tau_k(\sigma(v_k))}$$
}

\begin{example}\label{ex:transformer}
    Let $\tau_1$ be a string transformer that inserts a pair of curly parentheses surrounding the input.
    Let $\mathcal{T}_1 \defas\{v_1 \mapsto \tau_1\}$ be a transformer.
    Applying $\mathcal{T}_1$ to $\sigma=\{v_1 \mapsto ``\verb|123|"\}$ yields
    $\sigma'=\{v_1 \mapsto ``\verb|{123}|"\}$.
\end{example}

\paragraph*{String Transformer}\label{sec:lang:trans:string-trans}

We now present $\mathcal{L}_\text{ST}$, a DSL for expressing the underlying string transformation.
We first define notions for manipulating substrings.
Let $s$ be a string, we denote $s[k_1..k_2]$ the substring of $s$ that
starts from the index $k_1$ (inclusive) until the index $k_2$ (inclusive).
We assume the indexes start from $0$, and we use a negative index $-k (k>0)$ to count from the end of the string.
For simplicity, we write $s[..k]$ for $s[0..k]$, and $s[k..]$ for $s[k..-1]$.

\begin{figure}
    \begin{align*}
        \tau &::= \t{fun}~x \Rightarrow S \\
        S &::= F \mid \tk{Concat}(F, S) \\
        F &::= \tk{ConstStr}(s) \mid \tk{SubStr}(x, p_1, p_2) \\
        p &::= \tk{AbsPos}(x, k) \mid \tk{RelPos}(x, t, j, k)
    \end{align*}
    \caption{Syntax of the string transformer language $\mathcal{L}_\text{ST}$.
   
    }
    \label{fig:st-lang}
\end{figure}

The syntax of $\mathcal{L}_\text{ST}$ is described in \cref{fig:st-lang}.
A string transformer is a function that takes a string $x$ as input and produces a new string as output.
The function body is defined by a string expression $S$ that evaluates to a string.
A string expression is either an atomic expression $F$, in which no concatenation is allowed,
or a concatenation of an atomic expression with another string expression.
An atomic expression $F$ is either of the form $\tk{ConstStr}(s)$ denoting a constant string $s$,
or $\tk{SubStr}(x, p_1, p_2)$ denoting the substring $x[i_1..i_2]$, given that the two position expressions $p_1$ and $p_2$ are evaluated to indexes $i_1$ and $i_2$ respectively.

A position expression $p$ evaluates to an index of a string $x$.
It is either of the form $\tk{AbsPos}(x, k)$ denoting the absolute index $k$,
or $\tk{RelPos}(x, t, j, k)$ denoting a relative index of the $j$-th occurrence of the regular expression token $t$ in $x$ plus an offset $k$.
We allow $j$ to be a negative value, say $-i(i>0)$, indicating the last $i$-th occurrence.
The same case also applies to the offset $k$.
An regular expression token can be customized to employ the domain knowledge of mathematical equations,
such as commonly-seen special characters
$``\verb|{|"$, $``\verb|}|"$, $``\verb|(|"$, $``\verb|)|"$, $``\verb|^|"$, $``\verb|_|"$ and numbers.



\subsubsection{Comparison with Other String Transformers}

Our string transformation DSL $\mathcal{L}_{\text{st}}$ is inspired by \tool{FlashFill} and possesses a more restricted syntax:
it only allows a regular token to appear in the relative position,
whereas in \tool{FlashFill}, a number of regular expressions are allowed.
Apparently, $\mathcal{L}_{\text{st}}$ is less expressive than \tool{FlashFill}.
However, it is sufficient for expressing the string
transformations for equation repairing problems, where
the error parts have already be located by matchers.

Another simplified example of \tool{FlashFill} is \tool{NoFAQ}, which does not allow the concatenation of two substring expressions.
However, we find that the string concatenation is a useful and necessary operation for
equation repair, and thus keep this operation in $\mathcal{L}_{\text{st}}$.
To sum up, $\mathcal{L}_{\text{st}}$ can be considered as an adaption of the \tool{FlashFill}'s DSL to the
equation repair problem:
it is restricted for efficient searching, but
remains expressive for the equation repair problem.

\subsection{Rule Application}

Finally, with the above operations, we are ready to present how a fixing rule is applied to an equation repair problem in \tool{EqFix}.
Rule application eventually produces a corrected equation of the given problem.
Recall that the application process is only invoked when the rule is applicable to that problem.
Otherwise, the process may fail without producing any result.

Given a rule $\mathcal{R} = \pair{EP, \mathcal{T}}$:
\zap{
the application is formally defined as a function $\sem{\mathcal{R}}$ on an equation repair problem $(eq,err)$:
\begin{lstlisting}
$\sem{\pair{EP, \mathcal{T}}}~(eq, err)=\phantom{}\SP\kword{let}~\sigma=\sem{EP}~err~\kword{in}$
$\UP\kword{let}~P=\t{genPattern}~eq~\sigma~\kword{in}$
$\UP\kword{let}~\sigma'=\sem{\mathcal{T}}~\sigma~\kword{in}$
$\UP\asem{P}~\sigma'$
\end{lstlisting}
}
we first match $EP$ against $err$ and extract problem-specific information recorded in a mapping $\sigma$.
Then, we generate an equation pattern $P$ regarded as an ``abstraction'' of $eq$.
We will later generate a corrected equation based on $P$.
Next, we perform the underlying repairing strategy expressed by a set of string transformers,
say applying $\mathcal{T}$ on $\sigma$, and we obtain a new $\sigma'$.
So far, all necessary substrings of the corrected equation are known.
Finally, we obtain the fixed result by instantiating $P$ with the variable bindings declared in $\sigma'$.

\input{fig/demos}

\begin{example}
    Let rule $\mathcal{R}_1 \defas \pair{EP_1, \mathcal{T}_1}$,
    where $EP_1$ is defined in \cref{ex:err-pattern} 
    and $\mathcal{T}_1$ is defined in \cref{ex:transformer}.
    \cref{fig:demo-eval} shows how $\mathcal{R}_1$ is applied to the input \#2 of \cref{tb:motivating}.
    The steps are as follows:
    \begin{enumerate}
        \item matching $EP_1$ against $err_2$ gives $\sigma$ (as in \cref{ex:err-pattern});
        \item generate $P_2$ from $eq_2$ and $\sigma$ (as in \cref{ex:pattern-gen});
        \item transform $\sigma$ into $\sigma'$ by $\mathcal{T}_1$ (as in \cref{ex:transformer});
        \item instantiate $P$ with $\sigma'$ gives $fix_2$ (as in \cref{ex:matcher}).
    \end{enumerate}
\end{example}

\zap{
\cref{fig:demo-eval} shows how $\mathcal{R}_1$ is applied to the input \#2.
\begin{enumerate}[Step 1:]
    \item matching $EP_1$ on $err_2$ gives $\sigma_2=\{v_1 \mapsto ``\verb|123|"\}$;
    \item generate equation pattern \( P_2=[``\verb|$y^|", v_1, ``\verb|+x$|"] \);
    \item transform $\sigma_2$ into $\sigma_2'=\{v_1 \mapsto ``\verb|{123}|"\}$ 
    with $\mathcal{T}_1$;
    \item applying $P_2$ on $\sigma_2'$ gives the output \( ``\verb|$y^{123}+x$|" \),
    which is exactly $fix_2$.
\end{enumerate}
}


\section{Motivating Examples}

\begin{example}\label{ex:superscript}
    The user expects superscripts.

    \begin{tabular}{|l|l|l|l|}
        \hline
        \# & $eq$ & $err$ & $fix$ \\ 
        \hline
        \multirow{2}{*}{1} & \verb|$x^10$| 
                           & \multirow{2}{*}{10 is a superscript} 
                           & \verb|$x^{10}$| \\
        & $x^10$ & & $x^{10}$ \\
        \hline
        \multirow{2}{*}{2} & \verb|$y^123+x$|
                           & \multirow{2}{*}{123 is a superscript} 
                           & \verb|$y^{123}+x$| \\
        & $y^123+x$ & & $y^{123}+x$ \\
        \hline
        \multirow{2}{*}{3} & \verb|$f^(k)$|
                           & \multirow{2}{*}{(k) is a superscript} 
                           & \verb|$f^{(k)}$| \\
        & $f^(k)$ & & $f^{(k)}$ \\
        \hline
        \multirow{2}{*}{4} & \verb|$y=x+x^2+\ldots+x^10$|
                           & \multirow{2}{*}{10 is a superscript} 
                           & \verb|$y=x+x^2+\ldots+x^{10}$| \\
        & $y=x+x^2+\ldots+x^10$ & & $y=x+x^2+\ldots+x^{10}$ \\
        \hline
    \end{tabular}
\end{example}

\begin{example}\label{ex:parenthesis}
    Syntax error on mismatched parenthesis.

    \begin{tabular}{|l|l|l|l|}
        \hline
        \# & $eq$ & $err$ & $fix$ \\ 
        \hline
        \multirow{2}{*}{5} & \verb|${1,2,3$| 
                           & \multirow{2}{*}{Missing \} inserted}
                           & \verb|${1,2,3}$| \\
        & & & ${1,2,3}$ \\
        \hline
        
    \end{tabular}
\end{example}

\section{String Transformer}

$$\begin{array}{rcl}
    \text{String Transformer}~\tau &::=& \lambda v.S \\
    \text{Output}~S &::=& F \mid \t{Concat}(F, S) \\
    \text{Atomic}~F &::=& \t{ConstStr}(s) \mid \kword{let}~x = v_i~\kword{in}~\t{SubStr}(x, p_1, p_2) \\
    \text{Position}~p &::=& \t{AbsPos}(x, k) \mid \t{RelPos}(x, t, j, k) \\
\end{array}$$
where $s$ is a string literal, $i$ is an index (nonnegative integer),
$j$ is a non-zero integer ($j$-th occurence),
$k$ is an integer (absolute position index),
$t$ is a token of some regular expression.
Input is an array of string $v=[v_0, v_1, \ldots, v_n]$.

\section{Matcher}

\subsection{Simple Version}

$$\begin{array}{rcl}
    \text{Rule}~\mathcal{R} &::=& \pair{EP, \mathcal{T}} \\
    \text{Transformer}~\mathcal{T} &::=& \emptyset \mid (\mathbb{S} \mapsto \tau)\mathcal{T} \\
    \text{Schema}~\mathbb{S} &::=& (v, v_1, \cdots, v_k) \\
    \text{Err-Pattern}~EP &::=& \t{Nil} \mid \t{Cons}(M, EP) \\
    \text{Matcher}~M &::=& \t{MatchStr}(s) \mid \t{MatchVar}(v) \\
    \text{Pattern}~P &::=& VP \mid SP \\
    \text{V-Pattern}~VP &::=& \t{VNil} \mid \t{VCons}(v, SP) \\
    \text{S-Pattern}~SP &::=& \t{SNil} \mid \t{SCons}(s, VP) \\
\end{array}$$

\paragraph{Matching rules for Err-Pattern}

Let $M \matches s$ denote that a matcher $M$ matches with string $s$.

\inference[M-Str]{s=s_1}{\t{MatchStr}(s_1) \matches s}
\inference[M-Var]{}{\t{MatchVar}(v) \matches s}

Let $P \matches err$ denote that an err-pattern $P$ matches with the tokenized error message $err$.

\inference[M-Nil]{}{\t{Nil} \matches []}
\inference[M-Cons]{err = s :: err' & M \matches s & EP \matches err'}{\t{Cons}(M,EP) \matches err}

\paragraph{Matching Semantics for Err-Pattern}

$\sem{M}: \t{string}\to\t{env}\to\t{env}$, $\sem{M}~s~\sigma$ returns the updated environment after
trying to match $M$ with string $s$. 

\begin{align*}
    \sem{\t{MatchStr}(s_1)}~s~\sigma &= \kword{if}~s=s_1~\kword{then}~\sigma~\kword{else}\fail \\
    \sem{\t{MatchVar}(v)}~s~\sigma &= \t{insert}~v~s~\sigma
\end{align*}

$\sem{EP}: \t{string list}\to\t{env}\to\t{env}$, $\sem{EP}~err~\sigma$ returns the updated environment after
trying to match $EP$ with err message $err$.

\begin{align*}
    \sem{\t{Nil}}~err~\sigma &= \kword{if}~err=[]~\kword{then}~\sigma~\kword{else}\fail \\
    \sem{\t{Cons}(M, EP)}~[]~\sigma &=~\fail \\
    \sem{\t{Cons}(M, EP)}~s::err'~\sigma &= \kword{let}~\sigma'=\sem{M}~s~\sigma~\kword{in}~\sem{EP}~err'~\sigma'
\end{align*}

\begin{example}\label{ex:err-pattern}
    Considering the err pattern $$EP_1=[\t{MatchVar}(v_1), \t{MatchStr}(is), \t{MatchStr}(a), \t{MatchStr}(superscript)],$$
    after matching it with the err message $err$ of \#1 in \cref{ex:superscript},
    we extract the first token and have the output environment $\sigma^{err}_1=\{v_1 \mapsto 10\}$.
\end{example}

\paragraph{Pattern Generation}

$\t{genPattern}: \t{string}\to\t{env}\to\text{Pattern}$

\begin{example}\label{ex:pattern-gen}
    Let $eq_1, eq_2$ denote the input $eq$ of \#1, \#2 respectively in \cref{ex:superscript}.
    Given the environment $\sigma^{err}_1=\{v_1 \mapsto 10\}$, we abstract it as a pattern 
    $P_1=$\verb|$x^|$\concat v_1\concat$\verb|$|.
    Formally, $P_1=\t{genPattern}~eq_1~\sigma_1$.
\end{example}

\paragraph{Matching Semantics for Pattern}

$\msem{P}: \t{string}\to\t{env}\to\t{env}$, $\msem{P}~s~\sigma$ returns the updated environment after
trying to match pattern $P$ with a string $s$.

\begin{align*}
    \msem{\t{VNil}}~s~\sigma &= \kword{if}~s=\emptystr~\kword{then}~\sigma~\kword{else}\fail \\
    \msem{\t{VCons}(v, SP)}~s~\sigma &= \kword{if}~s=s_1\concat s_2~\And~SP \matches s_2~
        \kword{then}~\msem{SP}~s_2~(\t{insert}~v~\sigma)~\kword{else}\fail \\
    \msem{\t{SNil}}~s~\sigma &= \kword{if}~s=\emptystr~\kword{then}~\sigma~\kword{else}\fail \\
    \msem{\t{SCons}(s_1, VP)}~s~\sigma &= \kword{if}~s=s_1\concat s_2~\And~VP \matches s_2~
        \kword{then}~\msem{VP}~s_2~\sigma~\kword{else}\fail \\
\end{align*}

\paragraph{Applying Semantics for Pattern}

$\asem{P}: \t{env}\to\t{string}$, $\asem{P}~\sigma~$ returns the string after applying the environment $\sigma$ on pattern $P$, say instantiating a pattern $P$ with the values in the environment $\sigma$.

\begin{align*}
    \asem{\t{VNil}}~\sigma &= \emptystr \\
    \asem{\t{VCons}(v, SP)}~\sigma &= \kword{let}~s=\t{find}~v~\sigma~\kword{in}~s \concat \asem{SP}~\sigma \\
    \asem{\t{SNil}}~\sigma &= \emptystr \\
    \asem{\t{SCons}(s, VP)}~\sigma &= s \concat \asem{VP}~\sigma
\end{align*}

\begin{example}\label{ex:matcher}
    Considering the pattern $P_1$ defined in \cref{ex:pattern-gen}.
    Suppose that we only know the input equation $eq_1$,
    by matching $P_1$ with $eq_1$ we obtain the environments $\sigma_1=\{v_1 \mapsto \t{10}\}$.
    Formally, $\msem{P_1}~eq_1~\emptymap=\sigma_1$.
    Applying $\sigma_1'=\{v_1 \mapsto \t{\{10\}}\}$ on pattern $P_1$,
    we obtain the string \verb|$y^{10}+x$|, which is exactly $fix_1$.
\end{example}

We note that $\sigma_1=\sigma^{err}_1$.
Generally speaking,
$\msem{\t{genPattern}~s~\sigma}~s=\sigma$ holds for any string $s$ and environment $\sigma$.
Suppose that the pattern $P_1$ is known, it is unnessary to introduce the err-pattern
and the \t{genPattern} function.
However, synthesizing a pattern like $P_1$ given $eq_1$ is usually difficult.
The difficult thing is that we cannot always find a good splition for $eq_1$.
On the contrary, error messages are easily tokenized because they are usually reported by the compiler.
Starting from the error message, we can then generate $P_1$ with \t{genPattern} function.

\paragraph{Semantics for Transformer}

A transformer $\mathcal{T}$ takes an environment $\sigma$ as input, and generate a new environment
$\sigma'$ containing the transformed values. $\sem{\mathcal{T}}: \t{env}\to\t{env}$.

\begin{align*}
    \sem{\emptyset}~\sigma &= \sigma \\
    \sem{(\mathbb{S} \mapsto \tau)\mathcal{T}}~\sigma &= 
        \kword{let}~(v, v_1, \cdots, v_k)=\mathbb{S}~\kword{in} \\
        &~\kword{let}~s=\sigma(v), s_1=\sigma(v_1), \ldots, s_k=\sigma(v_k)~\kword{in} \\
        &~\kword{let}~s'=\tau(s, s_1, \ldots, s_k)~\kword{in} \\
        &~\kword{let}~\sigma'=\t{insert}~v~s'~\sigma~\kword{in}~\sem{\mathcal{T}}~\sigma'
\end{align*}

\begin{example}\label{ex:transformer}
    Considering a transformer for \cref{ex:superscript}: $\mathcal{T}_1=\{v_1 \mapsto \tau_1\}$,
    where $\tau_1$ is a string transformer that insert a pair of parenthesis for the input $v_1$.
    Formally, .
    For \#1, $\sigma_1=\{v_1 \mapsto 10\}$, applying $\tau_1$ on 10 yields \{10\}.
   
    Formally, $\sem{\mathcal{T}_1}~\sigma_1=\{v_1 \mapsto \t{\{10\}}\} \defas \sigma_1'$.
   
\end{example}

\paragraph{Semantics for Rule}

A rule $\mathcal{R}$ takes an equation $eq$ and a tokenized error message $err$ as input,
and generate a fix $fix$ for the input equation $eq$.

\begin{align*}
    \sem{\pair{EP, \mathcal{T}}}~eq~err
        &= \kword{let}~\sigma=\msem{EP}~err~\kword{in} \\
        &~ \kword{let}~P=\t{genPattern}~eq~\sigma~\kword{in} \\
        &~ \kword{let}~\sigma'=\sem{\mathcal{T}}~\sigma~\kword{in}~\asem{P}~\sigma'
\end{align*}

\begin{example}
    A possible rule for \cref{ex:superscript} is $\mathcal{R}_1=\pair{EP_1, \mathcal{T}_1}$.
    The definition for $EP_1$ is seen in \cref{ex:err-pattern}.
    The definition for $\mathcal{T}_1$ is seen in \cref{ex:ex:transformer}.
    We apply this rule on the input equation $eq_1$ and err message $err_1$.
    The steps have already been illstrated by the previous examples.
    \begin{enumerate}
        \item Compute the environment $\sigma^{err}_1$ as shown in \cref{ex:err-pattern}, 
        which is exactly $\sigma_1$ defined in \cref{ex:}.
        \item Compute the pattern $P_1$ as shown in \cref{ex:pattern-gen}.
        \item Compute the transformed environment $\sigma_1'$ as shown in \cref{ex:transformer},
        applying $P_1$ on $\sigma_1'$ yields the output, which is exactly $fix_1$, 
        as shown in \cref{ex:matcher}.
    \end{enumerate}
\end{example}

We evaluate the rule on \#2. See figure.

\subsection{Relaxer Version}

$$\begin{array}{rcl}
    \text{Rule}~\mathcal{R} &::=& \pair{EP, \{R_i\}_i, \mathcal{T}} \\
    \text{Transformer}~\mathcal{T} &::=& \emptyset \mid (\mathbb{S} \mapsto \tau)\mathcal{T} \\
    \text{Schema}~\mathbb{S} &::=& V * v_1 * \cdots * v_k \to V' \\
    \text{PVar}~V &::=& v \mid \t{LVar}(V) \mid \t{RVar}(V) \mid \t{BVar}(V_1, V_2) \\
    \text{V-Pattern}~VP &::=& \t{VNil} \mid \t{VCons}(V, SP) \\
    \text{Relaxer}~r &::=& \t{id}(v) \mid \t{LRelax}(r) \mid \t{RRelax}(r) \mid \t{BRelax}(r_1, r_2)
\end{array}$$

\paragraph{Relaxer Semantics}

A relaxer substitutes a sub pattern into a pattern variable. 
$P \relaxto_r V$ denotes the relaxer $r$ substitutes the sub pattern $P$ into a pattern variable $V$.

\inference[Relax-ID]{}{v \relaxto_{\t{id}(v)} v}
\inference[Relax-L]{P \relaxto_r V}{s \concat P \relaxto_{\t{LRelax}(r)} \t{LVar}(V)}
\inference[Relax-R]{P \relaxto_r V}{P \concat s \relaxto_{\t{RRelax}(r)} \t{RVar}(V)}
\inference[Relax-B]{P_1 \relaxto_{r_1} V_1 & P_2 \relaxto_{r_2} V_2}
    {P_1 \concat s \concat P_2 \relaxto_{\t{BRelax}(r_1, r_2)} \t{BVar}(V_1, V_2)}

$$\sem{r} : \text{Pattern} \to \text{Pattern}$$

\inference[Relax-ID]{P=P_1 \concat v \concat P_2}{\sem{\t{id}(v)}~P=P}
\inference[Relax-L]{P=s \concat P_1 \concat P_2 & P_1 \relaxto_r V}
    {\sem{\t{LRelax}(r)}~P=\t{LVar}(V) \concat P_2}
\inference[Relax-R]{P=P_1 \concat P_2 \concat s & P_2 \relaxto_r V}
    {\sem{\t{RRelax}(r)}~P=P_1 \concat \t{RVar}(V)}
\inference[Relax-B]{P=P_1 \concat P_2 \concat s \concat P_3 \concat P_4 
    & P_2 \relaxto_{r_1} V_1 & P_3 \relaxto_{r_2} V_2}
    {\sem{\t{BRelax}(r_1, r_2)}~P=P_1 \concat \t{BVar}(V_1, V_2) \concat P_4}

Relaxers can be composible:

$$\sem{\{r_1, \ldots, r_{k-1}, r_k\}}~P=\sem{r_k}~(\sem{r_{k-1}}~\cdots~(\sem{r_1}~P))$$

In case the pattern $P$ contains no variables, say it is a pattern with a single constant string $s$, i.e. $P=s$.
A special relaxer $\t{RelaxAll} \defas \t{id}(\t{self})$ is introduced to relax the entire pattern
as a V-pattern that contains a single variable $\t{self}$.
In the environment, we always let the special variable $\t{self}$ maps to the input equation.
This is an implict mapping and thus we only show it explictly in the examples if necessary.

\inference[Relax-ALL]{P=s}{\sem{\t{id}(\t{self})}~P=\t{self}}

\begin{example}\label{ex:relaxer:special}
    Considering \#5 in \cref{ex:parenthesis}.
    Applying the special relaxer on the pattern $P_5$ yields the relaxed pattern 
    $\hat{P_5}=\t{self}$. In the environment, $\t{self}$ maps to $eq_5$.
\end{example}

See figure for a more complex relaxer.
This example is constructed to illustrate the ideas,
but such complicated relaxers are rarely seen in real-world examples.

\paragraph{Semantics for Rule}

\begin{align*}
    \sem{\pair{EP, \{r_1, \ldots, r_k\}, \mathcal{T}}}~eq~err
        &= \kword{let}~\sigma=\msem{EP}~err~\kword{in} \\
        &~ \kword{let}~P=\t{genPattern}~eq~\sigma~\kword{in} \\
        &~ \kword{let}~\hat{P}=\sem{\{r_1, \ldots, r_k\}}~P~\kword{in} \\
        &~ \kword{let}~\hat{\sigma}=\msem{\hat{P}}~eq~\kword{in} \\
        &~ \kword{let}~\hat{\sigma'}=\sem{\mathcal{T}}~(\t{extend}~\hat\sigma~\sigma)~\kword{in}
         ~ \asem{\hat{P}}~\hat{\sigma'}
\end{align*}

\subsection{Synthesis}

Given a specification $\varphi=\{\varphi_1, \ldots, \varphi_n\}$,
where each $\varphi_i=(eq_i, err_i, fix_i)$ denotes an input-output example,
we want to synthesize a rule $\mathcal{R}$ s.t. $\mathcal{R}\models\varphi$.

Pattern Consistency: Two patterns $P_1$ and $P_2$ are consistent, if they are exactly the same excluding the constant strings.

\paragraph{Synthesizing Err-Patterns}

For each input-output example $(eq_i, err_i, fix_i)$, we generate the err-pattern by comparing each of the token with $eq_i$ and $fix_i$. 
If any token is contained in either $eq_i$ or $fix_i$, this token is substituted with a variable.
Otherwise, it remains a const string.

Suppose that more than one input-output example is provided, 
we require the error messages to have the same length and thus we can first generate an err-pattern for each example with the previous mechanism.
In most cases, the generated error patterns are exactly the same.
In case they are different, 
we define a unify operation on err-patterns so that we can find a
a single pattern that can match all the err-messages in the provided examples.

Given two err patterns $EP_1$ and $EP_2$, we define $\t{unify}~EP_1~EP_2$ to be the unified
err pattern. The rule is straight-forward, we unify each of the tokens.
$$\t{unify}~[M_1, \ldots, M_k]~[M_1', \ldots, M_k'] 
    = [\t{unify}~M_1~M_1', \ldots, \t{unify}~M_k~M_k']$$
The unify operation can be extented to many err patterns straightforwardly.

The unify operation for matchers:
\begin{align*}
    \t{unify}~\t{MatchStr}(s)~\t{MatchStr}(s) &= \t{MatchStr}(s) \\
    \t{unify}~\t{MatchVar}(v)~\t{MatchVar}(v) &= \t{MatchVar}(v) \\
    \t{unify}~\t{MatchStr}(s)~\t{MatchVar(v)} &= \t{MatchVar(v)} \\
    \t{unify}~\_~\_ &= \t{MatchAny}
\end{align*}

\begin{lemma}
    Let $EP_1, EP_2$ be two err patterns, 
    $EP_1$ matches with $err_1$ and $EP_2$ matches with $err_2$.
    If $EP=\t{unify}~EP_1~EP_2$, then $EP$ matches with $err_1$ and $err_2$.
\end{lemma}

\paragraph{Synthesizing Relaxers}

Assume that only one input-output example is provided in the specification 
$\varphi=\{(eq, err, fix)\}$, and $EP$ is the err pattern we have synthesized.
We can now generate a pattern $P$ for $eq$ given the environment by matching $EP$ on $err$, 
as we did in evaluating the rule:
$$P = \kword{let}~\sigma=\msem{EP}~err~\kword{in}~\t{genPattern}~eq~\sigma$$

If this pattern $P$ already matches with $fix$, then no relaxer is needed.
Otherwise, there must be some changes that are not captured by $EP$ and thus we have to introduce fresh variables so that the relaxed pattern can match with $fix$.


\begin{align*}
    \t{relax}~P~fix &= \kword{if}~P~\text{matches with}~fix~\kword{then}~P \\
    &~ \kword{else}~\text{let}~s~\text{be the unmatched string} \\
    &~ \kword{let}~P'=\kword{if}~P=s \concat V \concat P_1~\kword{then}~\t{LVar}(V) \concat P_1 \\
    &~ \kword{else}~\kword{if}~P=P_1 \concat V \concat s~\kword{then}~P_1 \concat \t{RVar}(V) \\
    &~ \kword{else}~\kword{if}~P=P_1 \concat s \concat V_1 \concat s \concat V_2 \concat P_2~
       \kword{then}~P_1 \concat \t{BVar}(V_1, V_2) \concat P_2 \\
    &~ \kword{in}~\t{relax}~P'~fix
\end{align*}

We follow a lazy relaxation manner, say we generate as least relaxers as possible,
until the relaxed pattern matches with $fix$.

\begin{lemma}
    Given a pattern $P$ and a string $f$, $\t{relax}~P~f$ always terminates and the returned
    pattern $P'$ matches with $f$.
\end{lemma}

When multiple input-output examples are provided, say $\varphi=\{(eq_i, err_i, fix_i)\}_{i=1}^n$,
we first generate the pattern $P_i$ for each $eq_i$ by 
$P_i = \kword{let}~\sigma=\msem{EP}~err~\kword{in}~\t{genPattern}~eq_i~\sigma$.
We require the patterns to be consistent with each other.
Relaxation is processed in the order of the examples.
The first example is relaxed with the mechanism mentioned above and we generate some relaxers (possibly empty) $R$.
Before we relax the second example, we first pass the generated relaxers $R$ to the example,
say applying $R$ on $P_2$ to generate $P_2'$, and then $\t{relax}~P_2'~fix_2$.
The new relaxers $R'$ is now updated and inherited $R$.
We repeat it until the last example is processed. 


\paragraph{Synthesizing Transformer}

A \emph{ST Example} is a pair $((s, s_1, \ldots, s_k), s')$, 
where $(s, s_1, \ldots, s_k)$ are $(k+1)$ input strings and $s'$ is the output string.
We call $s$ the \emph{primary input}, and $s_1, \ldots, s_k$ the \emph{auxiliary inputs}.

Once we have synthesized an err pattern $EP$ and relaxers $R$, we can now synthesize the transformer. To synthesize a string transformer $\tau$, we have to provided ST-examples for it.
The extraction of ST-examples are processed for each example $(eq_i, err_i, fix_i)$.
We first compute the relaxed pattern for $eq_i$ by
$\hat{P_i} = \kword{let}~\sigma=\msem{EP}~err~\kword{in}~\kword{let}~P=\t{genPattern}~eq_i~\sigma~\kword{in}~\sem{R}~P$.
By lemma, we see that $\hat{P_i}$ must also match with $fix_i$.
Therefore, we can match $\hat{P_i}$ on $eq_i$ and $fix_i$ respectively and we get
two environments $\hat{\sigma_{eq}}$ and $\hat{\sigma_{fix}}$.
These two maps have the same key set and thus for each key $V$,
we can create a mapping from $\hat{\sigma_{eq}}(V)$ to $\hat{\sigma_{fix}}(V)$,
indicating that the string $\hat{\sigma_{eq}}(V)$ is transformed to $\hat{\sigma_{fix}}(V)$.

Some extra informations from the error message may be useful.
In fact, these variables and their values are included in the examples.

\begin{align*}
    \t{ExtractSTExample}~(eq, fix)~\hat{P}~\mathbb{S}~
        &= \kword{let}~\hat{\sigma}=\msem{\hat{P}}~eq~\kword{in} \\
        &~ \kword{let}~\hat{\sigma'}=\msem{\hat{P}}~fix~\kword{in} \\
        &~ \kword{let}~s=\hat{\sigma}(v), s_1=\hat{\sigma}(v_1), \ldots, s_k=\hat{\sigma}(v_k)~\kword{in} \\
        &~ \kword{let}~s'=\hat{\sigma'}(v)~\kword{in} \\
        &~ ((s, s_1, \ldots, s_k), s')
\end{align*}

\end{document}
\section{Rule Synthesis}\label{sec:syn}

The rule synthesis algorithm takes a set of input-output examples $\mathcal{E}$
as the specification, and generates a fixing rule $\mathcal{R} = \pair{EP,
\mathcal{T}}$ that is consistent with the examples.
It consists of two passes:
(1) an error pattern $EP$ is synthesized from the examples $\mathcal{E}$, and 
(2) a transformer $\mathcal{T}$ is synthesized from $\mathcal{E}$ and $EP$.








\subsection{Synthesizing Error Patterns}\label{sec:syn:err-pattern}

Given an error message $err=[e_1, \ldots, e_k]$,
the error pattern synthesis problem is to generate an error pattern $EP=[M_1, \ldots, M_{k'}]$, such that $EP$ matches against $err$

To achieve this goal, a naive pattern $EP_{\bot} = [e_1, \ldots, e_k]$, the error message itself, is apparently a solution.
However, it is so \emph{restricted} that only this error message can match it.
Oppositely, another naive pattern $EP_{\top} = [v_1, \ldots, v_k]$ is too \emph{general} and can be matched with any error message with $k$ tokens.

To synthesize an error pattern that is neither too restricted nor too general,
we start with $EP_{\bot}$ and for each string in $EP_{\bot}$, replace it with
a fresh variable, if it also occurs in either the input equation $eq$ or the
output equation $fix$. Such replacement makes the error pattern more general.
Realizing that the error message is usually related to either the input equation by telling why it is erroneous,
or to the output equation by explaining how to repair it,
the introduced variables, in either case, will capture such important information.




\subsection{Synthesizing Transformers}\label{sec:syn:transformer}

Recall that the pattern generalization process (\cref{sec:lang:core:pattern}) produces an equation pattern $P$ from the input equation $eq$.
It is trivial that $P$ matches against $eq$, however, $P$ may not match against the output equation $fix$.
The latter case will be discussed later in \cref{sec:relaxers} as the solution requires an extension to our rule DSL.
In this section, we focus on the former case, where $P$ matches against $fix$ as well.

Given equations
    $eq = s_1 \concat s \concat s_2$,
    $fix = s_1' \concat s \concat s_2'$
and an equation pattern $P = [v_1, s, v_2]$.
Apparently, the differences between $eq$ and $fix$ are $s_1$ v.s. $s_1'$ and $s_2$ v.s. $s_2'$,
captured by $v_1$ and $v_2$ in $P$ respectively.
Thus, the expected transformer must be in the form of $\{v_1 \mapsto \tau_1, v_2 \mapsto \tau_2\}$,
where $\tau_1$, $\tau_2$ are two string transformers.
To synthesize these two string transformers, 
we need to provide input-output string examples as their specifications.
An \emph{input-output string example} for a string transformer is simply a mapping $s \to s'$,
where $s$ is the input string and $s'$ the expected output string. 
Observing the matched values of $v_1$ in $eq$ and $fix$, respectively,
we construct an input-output string example $s_1 \to s_1'$ for $\tau_1$.
Similarly, we construct $s_2 \to s_2'$ for $\tau_2$.

In general, the transformer synthesis algorithm consists of two steps: extract
a set of input-output string examples as the specification, and then invoke a
string transformer synthesizer to eventually generate the consistent string transformers.

\paragraph*{Specification Extraction}

Every string transformer $\tau_i$ is synthesized from the input-output string example 
$\sigma(v_i) \to \sigma'(v_i)$, where 
$\sigma$ is the result of matching $P$ against $eq$, and
$\sigma'$ is the result of matching $P$ against $fix$.
If more than one example is provided, we need to synthesize a transformer $\mathcal{T}$ that is consistent with them all.
Therefore, the union of the examples extracted from each $\tau_i$ gives a
complete specification for $\mathcal{T}$.

\begin{example}\label{ex:syn:st-examples}
    Given examples \#1 and \#2 in \cref{tb:motivating} as
    the input-output string examples,
    to synthesize a transformer $\tau_1$,
    we extract $``\verb|10|" \to ``\verb|{10}|"$ from example \#1, and
    $``\verb|123|" \to ``\verb|{123}|"$ from example \#2.
    The complete specification for synthesizing $\tau_1$ is thus
    $\varphi_1 = \{ ``\verb|10|" \to ``\verb|{10}|", ``\verb|123|" \to ``\verb|{123}|" \}$.
\end{example}

\paragraph*{String Transformer Synthesis}

The string transformer synthesis problem has been well-studied in previous literatures, e.g. \tool{FlashFill} \cite{flash-fill}.
Here, we follow \tool{FlashFill}'s approach to customize a synthesis algorithm for our string transformation DSL $\mathcal{L}_\text{ST}$.
Noticing that this synthesis algorithm produces a set of (instead of one) candidate programs consistent with the input-output string examples, the entire rule synthesis algorithm will produce a set of consistent candidate rules as well.
Heuristics have been built to rank between candidate rules, using the ideas from previous studies \cite{flash-fill,flash-meta}.

\zap{
We rely on an underlying synthesizer to generate string transformers expressed by $\mathcal{L}_\text{ST}$ under the given specifications.
To represent a possibly large set of candidate programs succinctly, VSA comes into rescue.
We denote a set of string transformers by $\tilde{\tau}$.
Meanwhile, for fast convergence, we specify a group of domain-specific ranking functions.

At a high level, the string transformer synthesis algorithm takes a set of input-output string examples as input,
and generate a set of candidate string transformers represented by a VSA $\tilde{\tau}$ as output.
The basic idea of VSA-based synthesis is to divide the problem into several sub-problems, each for a nonterminal appeared in the DSL.
In our situation, we must propose algorithms to find the set of subprograms expressed by string expressions ($S$),
atomic expressions ($F$), and position expressions ($p$), respectively, that satisfies the input specification.
For the string expression case, the specification is simply the input of the entire synthesis algorithm.
For the other two cases, we need manually specify so-called \emph{witness functions} to obtain the corresponding specification.

Like \tool{FlashFill}, a program expressed by $\mathcal{L}_\text{ST}$ with ``simpler'' structure is preferred.
For instance, we give an string expression concatenated with fewer atomic expressions a higher rank than another one with more atomic expressions.
We also give a relative position expression a higher rank than an absolute position expression because the former is considered to be more general and fit more problems.

We lift our rule language to the VSA representation in the following way:
\begin{align*}
    \tilde{\mathcal{R}} &::= \pair{EP, \tilde{\mathcal{T}}} \\
    \tilde{\mathcal{T}} &::= \{v_1 \mapsto \tilde{\tau_1}, \ldots, v_k \mapsto \tilde{\tau_k}\}
\end{align*}
where $\tilde{\tau}$ represents the VSA for string transformers. 
The set of concrete programs are defined as:
\begin{align*}
    \sem{\pair{EP, \tilde{\mathcal{T}}}} &=
        \{ \pair{EP, \mathcal{T}} \mid \mathcal{T} \in \sem{\tilde{\mathcal{T}}} \} \\
    \sem{\{v_1 \mapsto \tilde{\tau_1}, \ldots, v_k \mapsto \tilde{\tau_k}\}} &=
        \{\{v_1 \mapsto \tau_1, \ldots, v_k \mapsto \tau_k\} \mid \tau_1 \in \sem{\tilde{\tau_1}}, \ldots, \tau_k \in \sem{\tilde{\tau_k}} \}
\end{align*}
where $\tilde{\mathcal{T}}$ is a join node.

\begin{example}\label{ex:syn:transformer}
    Given the specification $\varphi_1$, 
    let $\tilde{\tau_1}$ be the VSA returned by the underlying synthesizer.
    Then, the transformer VSA is
    $\tilde{\mathcal{T}_1}=\{ v_1 \mapsto \tilde{\tau_1} \}$,
    and the rule VSA is
    $\tilde{\mathcal{R}_1}=\pair{EP_1, \tilde{\mathcal{T}_1}}$.
    Furthermore,
    we observe that the string transformer $\tau_1$ defined in \cref{ex:st:1} 
    is consistent with $\varphi_1$, and $\tau_1 \in \sem{\tilde{\tau_1}}$.
    Thus, the rule $\mathcal{R}_1=\pair{EP_1, \mathcal{T}_1} \in \sem{\tilde{\mathcal{R}_1}}$
    is consistent with the examples \#1 and \#2 in \cref{tb:motivating}.
\end{example}
}

\input{fig/demos-2}

\paragraph*{Summary}

Finally, we summarize the main steps of our rule synthesis algorithm using example \#1 of \cref{tb:motivating} as the specification.
The steps are also illustrated in \cref{fig:demo-syn}:
\begin{enumerate}
    \item synthesize an error pattern $EP_1$ by comparing $err_1$ with $eq_1$
        and $fix_1$, respectively, 
        $\sigma_1=\{v_1 \mapsto ``\verb|10|"\}$ records the values of the matched variable;
    \item generate the equation pattern $P_1$;
    \item match $P_1$ on $fix_1$, yielding $\sigma_1'=\{v_1 \mapsto ``\verb|{10}|"\}$;
    \item synthesize $\mathcal{T}_1$ such that $\sigma_1$ is transformed into $\sigma_1'$.
\end{enumerate}

\zap{
\subsection{Synthesizing Underlying String Transformers}\label{sec:syn:st}

We lift the string transformation language $\mathcal{L}_\text{ST}$
to be with the VSA representation:
$$\begin{array}{rcl}
    \tilde{\tau} &::=& \t{fun}~\gamma\Rightarrow\tilde{S} \\
    \tilde{S} &::=& \tilde{F} \mid \tk{Concat}_{\join}(\tilde{F}, \tilde{S}) \\
    \tilde{F} &::=& \tk{ConstStr}(s) \mid 
                    \kword{let}~x=\gamma_i~\kword{in}~\tk{SubStr}_{\join}(x, \tilde{p_1}, \tilde{p_2})
\end{array}$$
where the position VSA $\tilde{p}$ uses explicit representation.
The set of concrete programs are defined as:

\begin{align*}
    \sem{\t{fun}~\gamma\Rightarrow\tilde{S}} &= \{ \t{fun}~\gamma\Rightarrow S \mid S \in \sem{\tilde{S}} \} \\
    \sem{\tk{Concat}_{\join}(\tilde{F}, \tilde{S})} &= 
        \{ \tk{Concat}(F, S) \mid F \in \sem{\tilde{F}}, S \in \sem{\tilde{S}} \} \\
    \sem{\tk{ConstStr}(s)} &= \{ \tk{ConstStr}(s) \} \\
    \sem{\tk{SubStr}_{\join}(x, \tilde{p_1}, \tilde{p_2})} &=
        \{ \tk{SubStr}(x, p_1, p_2) \mid p_1 \in \sem{\tilde{p_1}}, p_2 \in \sem{\tilde{p_2}} \}
\end{align*}

\cref{fig:st-syn-algo} describes our synthesis algorithm for
$\mathcal{L}_{\text{st}}$.
The entry function $\t{genString}$ takes the inputs $\gamma$ and an output string $s$
as the specification, and generates all string expressions 
that are consistent with the specification, 
in terms of either an atomic expression or a \tk{Concat},
say the string expression evaluates to $s$, given $\gamma$.
These expressions form a VSA and can be classified into two groups:
(1) an atomic expression that evaluates to $s$, which is computed by \t{genAtomic};
(2) an atomic expression $F$ which evaluates to $f$, 
concatenate another string expression $S$ which evaluates to $s'$,
such that $s = f \concat s'$.

Similarly, we interpret the other generation function as follows:
\begin{itemize}
    \item $\t{genAtomic}~\gamma~s$ generates all atomic expressions that evaluates to $s$
    given the input $\gamma$;
    \item $\t{genSubStr}~x~s$ generates all substring expressions that evaluates to $s$
    given the input string $x$;
    \item $\t{genPos}~x~k$ generates all position expressions that evaluates to $k$
    given the input string $x$.
\end{itemize}

When multiple string examples are provided, we could generate a VSA for each
string example,
and then intersect all these VSAs to produce a VSA that is consistent with all the examples.
Following a similar approach proposed by \citet{flash-fill}, we can show that
our synthesis algorithm for $\mathcal{L}_{\text{st}}$ is sound and complete:

\begin{lemma}{(Soundness)}
    \label{thm:st:soundness}
    Given a specification $\varphi$,
    for every program $\tau$ returned by the algorithm in
    \cref{fig:st-syn-algo},
    and every example $s \to s'$ taken from $\varphi$, $\tau(s) = s'$.
\end{lemma}
\begin{lemma}{(Completeness)}
    \label{thm:st:completeness}
    Given a specification $\varphi$ and
    let $\tilde{\tau}$ be the program set returned by the algorithm in
    \cref{fig:st-syn-algo}.
    For every program $\tau$ (expressed in the DSL) that is consistent with $\varphi$,
    $\tau \in \sem{\tilde{\tau}}$.
\end{lemma}

\begin{figure}
    {\footnotesize
    \begin{align*}
        \t{genString}~(\gamma:\t{string list})~(s:\t{string}) &=
            \t{genAtomic}~\gamma~s \\
            &\cup \{\tk{Concat}_{\join}
            (\t{genAtomic}~\gamma~s[..i], \t{genString}~\gamma~s[i+1..]) \mid 1<i<\t{len}~s \} \\
        \t{genAtomic}~(\gamma:\t{string list})~(s:\t{string}) &=
            \{\tk{ConstStr}(s)\} \cup \{ \t{genSubStr}~x~s \mid x \in\gamma \} \\
        \t{genSubStr}~(x:\t{string})~(s:\t{string}) &=
            \{\tk{SubStr}_{\join}(x, \t{genPos}~x~k, \t{genPos}~x~(k+\t{len}~s-1)) \mid k \in K\} \\
            & \text{where}~K = \{k \mid s = x[k..k+\t{len}~s-1]\} \\
        \t{genPos}~(x:\t{string})~(k:\t{int}) &=
            \{\tk{AbsPos}(x, k), \tk{AbsPos}(x, k - \t{len}~s)\} \cup \t{genRelPos}~x~k
    \end{align*}
    }
    \caption{Synthesis algorithm for $\mathcal{L}_\text{ST}$.
    Function $\t{len}~s$ givens the length of string $s$.
    The implementation of $\t{genPos}~x~k$,
    which generates all position expressions in terms of \tk{RelPos}
    that evaluates to $k$ given the input string $x$,
    depends on the selection of regular tokens
    and thus we leave it abstract here.}
    \label{fig:st-syn-algo}
\end{figure}
}










