Commit 9e4b500d authored by Björn Peemöller 's avatar Björn Peemöller
Browse files

Split report into separate tex files

parent 45368450
# To format the Curry report
TEXFILES = $(wildcard *.tex) $(wildcard syntax/*.tex)
.PHONY: all
all: report.pdf
report.dvi: report.tex
report.dvi: report.tex $(TEXFILES)
latex report
bibtex report
latex report
......@@ -13,7 +15,7 @@ report.dvi: report.tex report.dvi
dvips report
report.pdf: report.tex
report.pdf: report.tex $(TEXFILES)
pdflatex report
bibtex report
pdflatex report
......@@ -40,4 +42,3 @@ clean:
/bin/mv report.tex report.texx
/bin/rm -f report.?? report.???
/bin/mv report.texx report.tex
\section{Encapsulated Search}
Global search, possibly implemented by backtracking,
must be avoided in some situations (user-control of
efficiency, concurrent computations, non-backtrackable I/O).
Hence it is sometimes necessary to encapsulate search,
i.e., non-deterministic computations in parts of larger programs.
Non-deterministic computations might occur in Curry
whenever a function must be evaluated with a free variable at
a flexible argument position. In this case, the computation must follow
different branches with different bindings applied to
the current expression which has the effect that the entire
expression is split into (at least) two independent disjunctions.
To give the programmer control
on the actions taken in this situation, Curry provides
a primitive search operator which is the basis to implement
sophisticated search strategies.
This section sketches the idea of encapsulating search in Curry
and describes some predefined search strategies.
\subsection{Search Goals and Search Operators}
Since search is used to find solutions to some constraint,
search is always initiated by a constraint containing a
\emph{search variable}\index{variable!search}\index{search variable}
for which a solution should be
computed.\footnote{The generalization to more than
one search variable is straightforward by the use of tuples.}
Since the search variable may be bound to different solutions
in different disjunctive branches, it must be abstracted.
Therefore, a \emph{search goal}\index{search goal} has the type
\code{a->Success} where \code{a} is the type of the values
which we are searching for. In particular, if $c$ is a constraint
containing a variable $x$ and we are interested in solutions
for $x$, i.e., values for $x$ such that $c$ is satisfied,
then the corresponding search goal has the form \code{(\ttbs$x$->$c$)}.
However, any other expression of the same type can also be used
as a search goal.
To control the search performed to find solutions to search goals,
Curry has a predefined operator\pindex{try}
try :: (a->Success) -> [a->Success]
which takes a search goal and produces a list of search goals.
The search operator \code{try} attempts to evaluate
the search goal until the computation finishes or
performs a non-deterministic splitting. In the latter case,
the computation is stopped and the different search goals
caused by this splitting are returned as the result list.
Thus, an expression of the form \code{try (\ttbs$x$->$c$)}
can have three possible results:
An empty list. This indicates that the search goal \code{(\ttbs$x$->$c$)}
has no solution. For instance, the expression
try (\ttbs{}x -> 1=:=2)
reduces to \code{[]}.
A list containing a single element. In this case, the search goal
\code{(\ttbs$x$->$c$)} has a single solution represented by the element
of this list. For instance, the expression
try (\ttbs{}x->[x]=:=[0])
reduces to \code{[\ttbs{}x->x=:=0]}.
Note that a solution, i.e., a binding for the search variable
like the substitution $\{\code{x}\mapsto\code{0}\}$,
can always be presented by an equational constraint
like \code{x=:=0}.
Generally, a one-element list as a result of \code{try}
has always the form \code{[\ttbs$x$->$x$=:=$e$]}
(plus some local variables, see next subsection)
where $e$ is fully evaluated, i.e., $e$ does not contain defined functions.
Otherwise, this goal might not be solvable due to the definition
of equational constraints.
A list containing more than one element. In this case, the evaluation
of the search goal \code{(\ttbs$x$->$c$)} requires a non-deterministic
computation step. The different alternatives immediately after
this non-deterministic step are represented as elements of this list.
For instance, if the function \code{f} is defined by
f a = c
f b = d
then the expression
try (\ttbs{}x -> f x =:= d)
reduces to the list
\code{[\ttbs{}x->x=:=a \& f a =:= d, \ttbs{}x->x=:=b \& f b =:= d]}.
This example also shows why the search variable must be abstracted:
the alternative bindings cannot be actually performed
(since a free variable is only bound to at most one value
in each computation thread) but are represented as
equational constraints in the search goal.
Note that the search goals of the list in the last example
are not further evaluated.
This provides the possibility to determine the behavior
for non-deterministic computations. For instance,
the following function defines a depth-first search operator
which collects all solutions of a search goal in a list:
solveAll :: (a->Success) -> [a->Success]
solveAll g = collect (try g)
where collect [] = []
collect [g] = [g]
collect (g1:g2:gs) = concat (map solveAll (g1:g2:gs))
(\code{concat} concatenates a list of lists to a single list).
For instance, if \code{append} is the list concatenation, then the expression
solveAll (\ttbs{}l -> append l [1] =:= [0,1])
reduces to \code{[\ttbs{}l->l=:=[0]]}.
The value computed for the search variable in a search goal
can be easily accessed by applying it to a free variable.
For instance, the evaluation of the applicative expression
solveAll (\ttbs{}l->append l [1] =:= [0,1]) =:= [g] \& g x
binds the variable \code{g} to the search goal
\code{[\ttbs{}l->l=:=[0]]} and the variable \code{x} to the value \code{[0]}
(due to solving the constraint \code{x=:=[0]}).
Based on this idea, there is a predefined function
findall :: (a->Success) -> [a]
which takes a search goal and collects all solutions
(computed by a depth-first search like \code{solveAll})
for the search variable into a list.
Due to the laziness of the language, search goals with infinitely
many solutions cause no problems if one is interested only in finitely
many solutions. For instance, a function which computes only the
first solution w.r.t.\ a depth-first search strategy can be defined by
first g = head (findall g)
Note that \code{first} is a partial function, i.e., it is undefined
if \code{g} has no solution.
\subsection{Local Variables}
Some care is necessary if free variables occur in the search goal,
like in the goal
\ttbs{}l2 -> append l1 l2 =:= [0,1]
Here, only the variable \code{l2} is abstracted in the search goal
but \code{l1} is free. Since non-deterministic bindings
cannot be performed during encapsulated search,
\emph{free variables are never bound inside encapsulated search}.
Thus, if it is necessary to bind a free variable in order to
proceed an encapsulated search operation, the computation suspends.
For instance, the expression
first (\ttbs{}l2 -> append l1 l2 =:= [0,1])
cannot be evaluated and will be suspended until the variable \code{l1}
is bound by another part of the computation. Thus, the constraint
s =:= first (\ttbs{}l2->append l1 l2 =:= [0,1]) \& l1 =:= [0]
can be evaluated since the free variable \code{l1} in the search goal
is bound to \code{[0]}, i.e., this constraint reduces to the answer
\{l1=[0], s=[1]\}
In some cases it is reasonable to have unbound variables
in search goals, but these variables should be treated as local,
i.e., they might have different bindings in different branches
of the search. For instance, if we want to compute
the last element of the list \code{[3,4,5]}
based on \code{append}, we could try to solve
the search goal
\ttbs{}e -> append l [e] =:= [3,4,5]
However, the evaluation of this goal suspends due to the necessary
binding of the free variable \code{l}.
This can be avoided by declaring the variable \code{l}
as \emph{local} to the constraint by the use of \code{let}
(see Section~\ref{sec-freevars}), like in the following expression:
first (\ttbs{}e -> let l free in append l [e] =:= [3,4,5])
Due to the local declaration of the variable \code{l}
(which corresponds logically to an
existential quantification), the variable \code{l} is only visible
inside the constraint and, therefore, it can be bound to
different values in different branches. Hence this expression
evaluates to the result \code{5}.
In order to ensure that an encapsulated search will not be
suspended due to necessary bindings of free variables,
the search goal should be a closed expression when a search operator is
applied to it, i.e., the search variable is bound by the
lambda abstraction and all other free variables are existentially
quantified by local declarations.
\subsection{Predefined Search Operators}
There are a number of search operators which are predefined
in the prelude. All these operators are based on the primitive
\code{try} as described above.
It is also possible to define other search strategies
in a similar way. Thus, the \code{try} operator is a
a powerful primitive to define appropriate search strategies.
In the following, we list the predefined search operators.
\item[\code{solveAll :: (a->Success) -> [a->Success]}]~\pindex{solveAll}\\
Compute all solutions for a search goal via a depth-first search
strategy. If there is no solution and the search space is finite,
the result is the empty list, otherwise the list contains solved
search goals (i.e., without defined operations).
\item[\code{once :: (a->Success) -> (a->Success)}]~\pindex{once}\\
Compute the first solution for a search goal via a depth-first search
strategy. Note that \code{once} is partially defined, i.e.,
if there is no solution and the search space is finite,
the result is undefined.
\item[\code{findall :: (a->Success) -> [a]}]~\pindex{findall}\\
Compute all solutions for a search goal via a depth-first search
strategy and unpack the solution's values for the search variable
into a list.
\item[\code{best :: (a->Success) -> (a->a->Bool) -> [a->Success]}]~\pindex{best}\\
Compute the best solution via a depth-first search strategy, according to
a specified relation (the second argument)
that can always take a decision which of two solutions is better
(the relation should deliver \code{True} if the first argument
is a better solution than the second argument).
As a trivial example, consider the relation \code{shorter} defined by
shorter l1 l2 = length l1 <= length l2
Then the expression
best (\ttbs{}x -> let y free in append x y =:= [1,2,3]) shorter
computes the shortest list which can be obtained by splitting the
list \code{[1,2,3]} into this list and some other list, i.e.,
it reduces to \code{[\ttbs{}x->x=:=[]]}. Similarly, the expression
best (\ttbs{}x -> let y free in append x y =:= [1,2,3])
(\ttbs{}l1 l2 -> length l1 > length l2)
reduces to \code{[\ttbs{}x->x=:=[1,2,3]]}.
\item[\code{browse :: (a->Success) -> IO ()}]~\pindex{browse}\\
Show the solution of a \emph{solved} constraint on the standard output,
i.e., a call \code{browse g}, where \code{g} is a solved search goal,
is evaluated to an I/O action which prints the solution.
If \code{g} is not an abstraction of a solved constraint,
a call \code{browse g} produces a runtime error.
\item[\code{browseList :: [a->Success] -> IO ()}]~\pindex{browseList}\\
Similar to \code{browse} but shows a list of solutions on the standard output.
The \code{browse} operators are useful for testing search
strategies. For instance, the evaluation of the expression
browseList (solveAll (\ttbs{}x -> let y free in append x y =:= [0,1,2]))
produces the following result on the standard output:
Due to the laziness of the evaluation strategy, one can also
browse the solutions of a goal with infinitely many solutions
which are printed on the standard output until the process is stopped.
\section{Example Programs}
This section contains a few example programs together with some initial
expressions and their computed results.
\subsection{Operations on Lists}
Here are simple operations on lists.
Note that, due to the logic programming features of Curry,
\code{append} can be used to split lists. We exploit this property
to define the last element of a list in a very simple way.
-- Concatenation of two lists:
append :: [t] -> [t] -> [t]
append [] ys = ys
append (x:xs) ys = x:append xs ys
-- Naive reverse of all list elements:
rev :: [t] -> [t]
rev [] = []
rev (x:xs) = append (rev xs) [x]
-- Last element of a list:
last :: [t] -> t
last xs | append _ [x] =:= xs = x where x free
Expressions and their evaluated results:
append [0,1] [2,3] $~~\leadsto~~$ [0,1,2,3]
append L M =:= [0,1]
$~~\leadsto~~$ \{L=[],M=[0,1]\} | \{L=[0],M=[1]\} | \{L=[0,1],M=[]\}
rev [0,1,2,3] $~~\leadsto~~$ [3,2,1,0]
last (append [1,2] [3,4]) $~~\leadsto~~$ 4
\subsection{Higher-Order Functions}
Here are some ``traditional'' higher-order functions
to show that the familiar functional programming techniques
can be applied in Curry. Note that the functions \code{map}, \code{foldr},
and \code{filter} are predefined in Curry (see Appendix~\ref{app-prelude}).
-- Map a function on a list (predefined):
map :: (t1->t2) -> [t1] -> [t2]
map f [] = []
map f (x:xs) = f x : map f xs
-- Fold a list (predefined):
foldr :: (t1->t2->t2) -> t2 -> [t1] -> t2
foldr f a [] = a
foldr f a (x:xs) = f x (foldr f a xs)
-- Filter elements in a list (predefined):
filter :: (t -> Bool) -> [t] -> [t]
filter p [] = []
filter p (x:xs) = if p x then x : filter p xs
else filter p xs
-- Quicksort function:
quicksort :: [Int] -> [Int]
quicksort [] = []
quicksort (x:xs) = quicksort (filter (<= x) xs)
++ [x]
++ quicksort (filter (> x) xs)
\subsection{Relational Programming}
Here is a traditional example from logic programming:
a simple deductive database with family relationships.
We use a relational programming style, i.e., all
relationships are represented as constraints
(i.e., functions with result type \code{Success}).
-- Declaration of an enumeration type for persons:
-- (as an alternative, one could consider persons as strings)
data Person = Christine | Maria | Monica | Alice | Susan |
Antony | Bill | John | Frank | Peter | Andrew
-- Two basic relationships:
married :: Person -> Person -> Success
married Christine Antony = success
married Maria Bill = success
married Monica John = success
married Alice Frank = success
mother :: Person -> Person -> Success
mother Christine John = success
mother Christine Alice = success
mother Maria Frank = success
mother Monica Susan = success
mother Monica Peter = success
mother Alice Andrew = success
-- and here are the deduced relationships:
father :: Person -> Person -> Success
father f c = let m free in married m f \& mother m c
grandfather :: Person -> Person -> Success
grandfather g c = let f free in father g f \& father f c
grandfather g c = let m free in father g m \& mother m c
Expressions and their evaluated results:\vspace{1ex}
father John child $~~\leadsto~~$ \{child=Susan\} | \{child=Peter\}
grandfather g c $~~\leadsto~~$
\{g=Antony,c=Susan\} | \{g=Antony,c=Peter\} |
\{g=Bill,c=Andrew\} | \{g=Antony,c=Andrew\}
\subsection{Functional Logic Programming}
This is the same example as in the previous section.
However, we use here a functional logic programming style
which is more readable but provides the same goal solving
capabilities. The basic functions are \code{husband}
and \code{mother} which express the functional dependencies
between the different persons. Note that the derived
function \code{grandfather} is a non-deterministic function
which yields all grandfathers for a given person.
data Person = Christine | Maria | Monica | Alice | Susan |
Antony | Bill | John | Frank | Peter | Andrew
-- Two basic functional dependencies:
husband :: Person -> Person
husband Christine = Antony
husband Maria = Bill
husband Monica = John
husband Alice = Frank
mother :: Person -> Person
mother John = Christine
mother Alice = Christine
mother Frank = Maria
mother Susan = Monica
mother Peter = Monica
mother Andrew = Alice
-- and here are the deduced functions and relationships:
father :: Person -> Person
father c = husband (mother c)
grandfather :: Person -> Person
grandfather g = father (father g)
grandfather g = father (mother g)
Expressions and their evaluated results:
father Child =:= john $~~\leadsto~~$ \{Child=susan\} | \{Child=peter\}
grandfather c $~~\leadsto~~$
\{c=Susan\} Antony | \{c=Peter\} Antony | \{c=Andrew\} Bill | \{c=Andrew\} Antony
\subsection{Constraint Solving and Concurrent Programming}
In this example we demonstrate how Curry's concurrent features
can be used to solve constraint problems with finite domains
more efficiently than a simple generate-and-test solver.
We want to solve the classical map coloring problem.
Consider the following simple map:
\begin{tabular}{|c|@{}c@{}|c|} \hline
\mbox{Country 1} & \begin{tabular}{c} ~\\~~\mbox{Country 2}~~ \\~\\
\hline ~\\ \mbox{Country 3}\\~\\ \end{tabular} & \mbox{Country 4} \\
The problem is to assign to each of the four countries
a color (red, green, yellow, or blue) such that countries
with a common border have different colors.
To solve this problem, we have to specify
that some countries have different colors. For this purpose,
we define the following constraint which checks to elements
for incompatibility:
diff :: a -> a -> Success
diff x y = (x==y)=:=False
For instance, \code{diff $t_1\,t_2$} is satisfied if $t_1$
and $t_2$ are different constants. If one of the arguments is a variable,
the evaluation of the function is delayed by definition of \code{==}.
Now there is a straightforward solution of the map coloring problem.
We define a constraint \code{coloring} specifying the valid colors for
each country and a constraint \code{correct} specifying which countries
must have different colors:
data Color = Red | Green | Yellow | Blue
isColor :: Color -> Success
isColor Red = success
isColor Yellow = success
isColor Green = success
isColor Blue = success
coloring :: Color -> Color -> Color -> Color -> Success
coloring l1 l2 l3 l4 = isColor l1 \& isColor l2 \& isColor l3 \& isColor l4
correct :: Color -> Color -> Color -> Color -> Success
correct l1 l2 l3 l4 =
diff l1 l2 \& diff l1 l3 \& diff l2 l3 \& diff l2 l4 \& diff l3 l4
In classical logic programming, we can compute the solutions to
the map coloring problem by enumerating all potential solutions
followed by a check whether a potential solution is a correct one
(``generate and test''). This can be expressed by solving
the following goal:\footnote{We assume an implementation
that processes the concurrent conjunction $c_1 \cconj c_2$
in a ``sequential-first'' manner: first $c_1$ is solved and, if
this is not possible due to a suspended evaluation, $c_2$ is solved.}
coloring l1 l2 l3 l4 \& correct l1 l2 l3 l4
However, a much faster solution can be obtained by reversing the order
of the tester and the generator:
correct l1 l2 l3 l4 \& coloring l1 l2 l3 l4
The latter constraint is evaluated in a concurrent way. In the first steps,
the subexpression \code{correct l1 l2 l3 l4} is reduced to the constraint
diff l1 l2 \& diff l1 l3 \& diff l2 l3 \& diff l2 l4 \& diff l3 l4
which is then reduced to
(l1==l2)=:=False \& (l1==l3)=:=False \& (l2==l3)=:=False \& (l2==l4)=:=False
\& (l3==l4)=:=False
This constraint cannot be further evaluated since the arguments to \code{==} are
free variables. Therefore, it is suspended and the final equational constraint
\code{coloring l1 l2 l3 l4} is evaluated which binds the variables
to the potential colors. Since the variable binding is performed
by consecutive computation steps, the equalities are evaluated
as soon as their arguments are bound. For instance, if the variables
\code{l1} and \code{l2} are bound to the color \code{Red}, the first constraint
\code{(l1==l2)=:=False} cannot be solved (due to the unsolvability of
the equational constraint \code{True=:=False}) which causes the failure
of the entire goal. As a consequence, not all potential colorings
are computed (as in the generate-and-test approach) but only those
colorings for which the constraints \code{correct l1 l2 l3 l4} is satisfiable.
Therefore, the (dis)equality goals act as ``passive constraints''
aiming to reduce the search space.
\subsection{Concurrent Object-Oriented Programming}
The following example shows a simple method to program
in a concurrent object-oriented style in Curry.
For this purpose, an object is a process waiting for incoming
messages. The local state is a parameter of this process.
Thus, a process is a function of type
State -> [Message] -> Success
In the subsequent example, we implement a bank account
as an object waiting for messages of the form
\code{Deposit i}, \code{Withdraw i}, or \code{Balance i}.
Thus, the bank account can be defined as follows:
data Message = Deposit Int | Withdraw Int | Balance Int
account :: Int -> [Message] -> Success
account _ [] = success
account n (Deposit a : ms) = account (n+a) ms
account n (Withdraw a : ms) = account (n-a) ms
account n (Balance b : ms) = b=:=n \& account n ms
-- Install an initial account with message stream s:
make_account s = {account 0 (ensureSpine s)}
A new account object is created by the constraint \ccode{make_account s}
where \code{s} is a free variable.
The function \code{ensureSpine}\pindex{ensureSpine}
(see Section~\ref{sec-ensurenotfree}) used in the definition of
\code{make_account} ensures that the evaluation of the function call
to \code{account} suspends on uninstantiated parts of the message list
When \code{s} is instantiated with
messages, the account object starts processing these messages.
The following concurrent conjunction of constraints creates
an account and sends messages:
make_account s \& s=:=[Deposit 200, Deposit 50, Balance b]
After this goal is solved, the free variable \code{b} has been bound to
\code{250} representing the balance after the two deposits.
To show a client-server interaction, we define a client of
a bank account who is finished if his account is \code{50},
buys things for \code{30} if his account is greater than \code{50},
and works for an income of \code{70} if his account is less than \code{50}.
In order to get the client program independent of the account
processing, the client sends messages to his account.
Therefore, the client is implemented as follows: