Add initial introduction for the term rewriting
This commit is contained in:
parent
ce5c3c8e58
commit
8358375892
@ -1,4 +1,5 @@
|
||||
\newacronym[see={[Glossary:]{gls-cbls}}]{cbls}{CBLS\glsadd{gls-cbls}}{Constraint-Based Local Search}
|
||||
\newacronym[see={[Glossary:]{gls-chr}}]{chr}{CHR\glsadd{gls-chr}}{Constraint Handling Rules}
|
||||
\newacronym[see={[Glossary:]{gls-clp}}]{clp}{CLP\glsadd{gls-clp}}{Constraint Logic Programming}
|
||||
\newacronym[see={[Glossary:]{gls-cp}}]{cp}{CP\glsadd{gls-cp}}{Constraint Programming}
|
||||
\newacronym[see={[Glossary:]{gls-cse}}]{cse}{CSE\glsadd{gls-cse}}{Common Sub-expression Elimination}
|
||||
@ -9,3 +10,4 @@
|
||||
\newacronym[see={[Glossary:]{gls-lns}}]{lns}{LNS\glsadd{gls-lns}}{Large Neighbourhood Search}
|
||||
\newacronym[see={[Glossary:]{gls-mip}}]{mip}{MIP\glsadd{gls-mip}}{Mixed Integer Programming}
|
||||
\newacronym[see={[Glossary:]{gls-sat}}]{sat}{SAT\glsadd{gls-sat}}{Boolean Satisfiability}
|
||||
\newacronym[see={[Glossary:]{gls-trs}}]{trs}{TRS\glsadd{gls-trs}}{Term Rewriting System}
|
||||
|
||||
@ -26,6 +26,15 @@
|
||||
bibsource = {dblp computer science bibliography, https://dblp.org}
|
||||
}
|
||||
|
||||
@book{baader-1998-term-rewriting,
|
||||
place = {Cambridge},
|
||||
title = {Term Rewriting and All That},
|
||||
DOI = {10.1017/CBO9781139172752},
|
||||
publisher = {Cambridge University Press},
|
||||
author = {Baader, Franz and Nipkow, Tobias},
|
||||
year = 1998
|
||||
}
|
||||
|
||||
@article{baatar-2011-radiation,
|
||||
author = {Davaatseren Baatar and Natashia Boland and Sebastian Brand
|
||||
and Peter J. Stuckey},
|
||||
@ -599,6 +608,17 @@
|
||||
bibsource = {dblp computer science bibliography, https://dblp.org}
|
||||
}
|
||||
|
||||
@phdthesis{rendl-2010-thesis,
|
||||
author = {Andrea Rendl},
|
||||
title = {Effective compilation of constraint models},
|
||||
school = {University of St Andrews, {UK}},
|
||||
year = {2010},
|
||||
url = {http://hdl.handle.net/10023/973},
|
||||
timestamp = {Thu, 25 Aug 2016 17:20:59 +0200},
|
||||
biburl = {https://dblp.org/rec/phd/ethos/Rendl10.bib},
|
||||
bibsource = {dblp computer science bibliography, https://dblp.org}
|
||||
}
|
||||
|
||||
@inproceedings{rendl-2009-enhanced-tailoring,
|
||||
author = {Andrea Rendl and Ian Miguel and Ian P. Gent and Christopher
|
||||
Jefferson},
|
||||
@ -617,17 +637,6 @@
|
||||
bibsource = {dblp computer science bibliography, https://dblp.org}
|
||||
}
|
||||
|
||||
@phdthesis{rendl-2010-thesis,
|
||||
author = {Andrea Rendl},
|
||||
title = {Effective compilation of constraint models},
|
||||
school = {University of St Andrews, {UK}},
|
||||
year = {2010},
|
||||
url = {http://hdl.handle.net/10023/973},
|
||||
timestamp = {Thu, 25 Aug 2016 17:20:59 +0200},
|
||||
biburl = {https://dblp.org/rec/phd/ethos/Rendl10.bib},
|
||||
bibsource = {dblp computer science bibliography, https://dblp.org}
|
||||
}
|
||||
|
||||
@inproceedings{rendl-2015-minisearch,
|
||||
author = {Andrea Rendl and Tias Guns and Peter J. Stuckey and Guido
|
||||
Tack},
|
||||
@ -836,6 +845,17 @@
|
||||
bibsource = {dblp computer science bibliography, https://dblp.org}
|
||||
}
|
||||
|
||||
@techreport{gamrath-2020-scip,
|
||||
author = {Gerald Gamrath and Daniel Anderson and Ksenia Bestuzheva and Wei-Kun Chen and Leon Eifler and Maxime Gasse and Patrick Gemander and Ambros Gleixner and Leona Gottwald and Katrin Halbig and Gregor Hendel and Christopher Hojny and Thorsten Koch and Le Bodic, Pierre and Stephen J. Maher and Frederic Matter and Matthias Miltenberger and Erik M{\"u}hmer and Benjamin M{\"u}ller and Marc E. Pfetsch and Franziska Schl{\"o}sser and Felipe Serrano and Yuji Shinano and Christine Tawfik and Stefan Vigerske and Fabian Wegscheider and Dieter Weninger and Jakob Witzig},
|
||||
title = {{The SCIP Optimization Suite 7.0}},
|
||||
type = {ZIB-Report},
|
||||
institution = {Zuse Institute Berlin},
|
||||
number = {20-10},
|
||||
month = {3},
|
||||
year = {2020},
|
||||
url = {http://nbn-resolving.de/urn:nbn:de:0297-zib-78023}
|
||||
}
|
||||
|
||||
@article{stuckey-2014-challenge,
|
||||
author = {Peter J. Stuckey and Thibaut Feydy and Andreas Schutt and
|
||||
Guido Tack and Julien Fischer},
|
||||
@ -852,17 +872,6 @@
|
||||
bibsource = {dblp computer science bibliography, https://dblp.org}
|
||||
}
|
||||
|
||||
@techreport{gamrath-2020-scip,
|
||||
author = {Gerald Gamrath and Daniel Anderson and Ksenia Bestuzheva and Wei-Kun Chen and Leon Eifler and Maxime Gasse and Patrick Gemander and Ambros Gleixner and Leona Gottwald and Katrin Halbig and Gregor Hendel and Christopher Hojny and Thorsten Koch and Le Bodic, Pierre and Stephen J. Maher and Frederic Matter and Matthias Miltenberger and Erik M{\"u}hmer and Benjamin M{\"u}ller and Marc E. Pfetsch and Franziska Schl{\"o}sser and Felipe Serrano and Yuji Shinano and Christine Tawfik and Stefan Vigerske and Fabian Wegscheider and Dieter Weninger and Jakob Witzig},
|
||||
title = {{The SCIP Optimization Suite 7.0}},
|
||||
type = {ZIB-Report},
|
||||
institution = {Zuse Institute Berlin},
|
||||
number = {20-10},
|
||||
month = {3},
|
||||
year = {2020},
|
||||
url = {http://nbn-resolving.de/urn:nbn:de:0297-zib-78023}
|
||||
}
|
||||
|
||||
@unpublished{van-hentenryck-1992-indexicals,
|
||||
title = {Constraint processing in cc(FD)},
|
||||
author = {Van Hentenryck, P. and Saraswat, V. and Deville, Y.},
|
||||
|
||||
@ -49,8 +49,8 @@
|
||||
description={},
|
||||
}
|
||||
|
||||
\newglossaryentry{gls-cp}{
|
||||
name={constraint programming},
|
||||
\newglossaryentry{gls-chr}{
|
||||
name={constraint handling rules},
|
||||
description={},
|
||||
}
|
||||
|
||||
@ -59,11 +59,21 @@
|
||||
description={},
|
||||
}
|
||||
|
||||
\newglossaryentry{gls-cp}{
|
||||
name={constraint programming},
|
||||
description={},
|
||||
}
|
||||
|
||||
\newglossaryentry{gls-cse}{
|
||||
name={common subexpression elimination},
|
||||
description={},
|
||||
}
|
||||
|
||||
\newglossaryentry{confluence}{
|
||||
name={confluence},
|
||||
description={},
|
||||
}
|
||||
|
||||
\newglossaryentry{gls-csp}{
|
||||
name={constraint satisfaction problem},
|
||||
description={},
|
||||
@ -150,6 +160,11 @@
|
||||
description={},
|
||||
}
|
||||
|
||||
\newglossaryentry{normal-form}{
|
||||
name={normal form},
|
||||
description={},
|
||||
}
|
||||
|
||||
\newglossaryentry{gls-mip}{
|
||||
name={Mixed Integer Programming},
|
||||
description={},
|
||||
@ -210,8 +225,18 @@
|
||||
description={},
|
||||
}
|
||||
|
||||
\newglossaryentry{term-rewriting}{
|
||||
name={term rewriting},
|
||||
\newglossaryentry{term}{
|
||||
name={term},
|
||||
description={},
|
||||
}
|
||||
|
||||
\newglossaryentry{gls-trs}{
|
||||
name={term rewriting system},
|
||||
description={},
|
||||
}
|
||||
|
||||
\newglossaryentry{termination}{
|
||||
name={termination},
|
||||
description={},
|
||||
}
|
||||
|
||||
|
||||
@ -46,30 +46,6 @@ the model.
|
||||
space left in the car, so we cannot bring all the toys. Since Audrey gets
|
||||
enjoys playing with some toys more than others, we can now try and pick the
|
||||
toys that bring Audrey the most amount of joy, but still fit in the car.
|
||||
|
||||
One way to solve this problem is to try all combinations of toys, but this is
|
||||
time intensive and quickly grows with the number of toys considered (which one
|
||||
would quickly realise trying to pack a car \(2^{|\text{toys}|}\) different
|
||||
ways).
|
||||
|
||||
An educated reader in optimisation problems might recognise that this is a
|
||||
variation on the widely known \gls{knapsack}, more specifically a \textit{0--1
|
||||
knapsack problem} \autocite[13--67]{silvano-1990-knapsack}. A commonly used
|
||||
solution to this problem is based on dynamic programming. An implementation of
|
||||
this approach is shown in \cref{lst:2-dyn-knapsack}. The use of dynamic
|
||||
programming avoids the exponential growth of the problem when increasing the
|
||||
number of toys.
|
||||
|
||||
Although expert knowledge can sometimes bring you an efficient solution to a
|
||||
known problem, it should be noted that not all problems will easily map to
|
||||
well known (and studied) problems. Even when part of a problem finds an
|
||||
equivalent in a well studied problem, the overall problem might still contain
|
||||
requirements that impair you from using known algorithms to solve the problem.
|
||||
For example, if wanted to bring toys with different colours, then the
|
||||
algorithm in \cref{lst:2-dyn-knapsack} would have to be drastically changed.
|
||||
\Gls{constraint-modelling} can offer a more flexible alternative that requires
|
||||
less expert knowledge.
|
||||
|
||||
The following set of equations describe this knapsack problem as a \gls{cop}:
|
||||
|
||||
\begin{equation*}
|
||||
@ -106,8 +82,8 @@ introduce \minizinc\ as the leading \cml\ used within this thesis.
|
||||
interpreter uses to translate a \minizinc\ model into a solver-level constraint
|
||||
model. Then, \cref{sec:back-other-languages} introduces alternative \cmls\ and
|
||||
compares their functionality to \minizinc{}. Finally, \cref{sec:back-term} and
|
||||
\cref{sec:back-clp} survey the closely related fields of \gls{term-rewriting}
|
||||
and \gls{clp}.
|
||||
\cref{sec:back-clp} survey the closely related fields of \gls{trs} and
|
||||
\gls{clp}.
|
||||
|
||||
\section{\glsentrytext{minizinc}}%
|
||||
\label{sec:back-minizinc}
|
||||
@ -585,6 +561,9 @@ following stages:
|
||||
|
||||
\jip{TODO: Description of the techniques used during the optimisation phase}
|
||||
|
||||
\subsection{Propagation}
|
||||
\label{sub:back-propagation}
|
||||
|
||||
\section{Other Constraint Modelling Languages}%
|
||||
\label{sec:back-other-languages}
|
||||
|
||||
@ -597,8 +576,52 @@ following stages:
|
||||
\subsection{Essence}%
|
||||
\label{sub:back-essence}
|
||||
|
||||
\section{ACD Term Rewriting}%
|
||||
\section{Term Rewriting}%
|
||||
\label{sec:back-term}
|
||||
|
||||
At the heart of the flattening process lies a \glsaccesslong{trs}. A \gls{trs}
|
||||
\cite{baader-1998-term-rewriting} describes a computational model the full
|
||||
process can be describe as the application of rules \(l \rightarrow r\), that
|
||||
replace a \gls{term} \(l\) with another \gls{term} \(r\). A \gls{term} is an
|
||||
expression with nested sub-expressions consisting of \emph{function} and
|
||||
\emph{constant} symbols. An example of a term is \(F(0 + 1,F(1,0))\), where
|
||||
\(F\) and \(+\) are function symbols and \(0\) and \(1\) are constant symbols.
|
||||
In a term rewriting rule, a term can also contain a \emph{term variable} which
|
||||
captures a term sub-expression. For example, the following \gls{trs} consists of
|
||||
some (well-known) rules to handle logical and:
|
||||
|
||||
\begin{align*}
|
||||
(r_{1}):& 0 \land x \rightarrow 0 \\
|
||||
(r_{2}):& 1 \land x \rightarrow x \\
|
||||
(r_{3}):& x \land y \rightarrow y \land x
|
||||
\end{align*}
|
||||
|
||||
From these rules it follows that
|
||||
|
||||
\[ 1 \land 1 \land 0 \rightarrow^{r_{1}} 1 \land 0 \rightarrow^{r_{3}} 0 \land 1 \rightarrow^{r_{2}} 0 \]
|
||||
|
||||
Notice that there can be a choice between different rules. A \gls{trs} can be
|
||||
non-deterministic. In the example we could also have applied the \(r_{1}\) twice
|
||||
and arrived at the same result. Two important properties of \gls{trs} are,
|
||||
therefore, \gls{termination} and \gls{confluence}. A \gls{trs} is said to be
|
||||
terminating if, no-matter what order the term rewriting rules are applied, you
|
||||
always arrive at a \gls{normal-form} (\ie, a term where no more rules apply). A
|
||||
\gls{trs} is confluent if, no-matter what order the term rewriting rules are
|
||||
applied, you always arrive at the same \gls{normal-form} (if you arrive at a
|
||||
\gls{normal-form}).
|
||||
|
||||
It is trivial to see that our previous example is non-terminating, since you can
|
||||
repeat rule \(r_{3}\) an infinite amount of times. The system, however, is
|
||||
confluent as, if it arrives at the same \gls{normal-form}: if the term contains
|
||||
any \(0\), then the result will be \(0\); otherwise, the result will be \(1\).
|
||||
|
||||
\subsection{Constraint Handling Rules}%
|
||||
\label{sub:back-chr}
|
||||
|
||||
|
||||
|
||||
\subsection{ACD Term Rewriting}%
|
||||
\label{subsec:back-acd}
|
||||
|
||||
\section{Constraint Logic Programming}%
|
||||
\label{sec:back-clp}
|
||||
|
||||
Reference in New Issue
Block a user