Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
curry
report
Commits
5ce007dc
Commit
5ce007dc
authored
Nov 16, 2015
by
Michael Hanus
Browse files
Changes for version 0.9.0
parent
ccd23fb0
Changes
20
Expand all
Hide whitespace changes
Inline
Sidebyside
Showing
20 changed files
with
1518 additions
and
1501 deletions
+1518
1501
encsearch.tex
encsearch.tex
+84
79
examples.tex
examples.tex
+128
168
expressions.tex
expressions.tex
+44
38
externals.tex
externals.tex
+2
2
fieldlabels.tex
fieldlabels.tex
+94
113
input_output.tex
input_output.tex
+27
22
interactive.tex
interactive.tex
+0
2
literate.tex
literate.tex
+14
9
long_semantics.tex
long_semantics.tex
+94
121
modules.tex
modules.tex
+52
47
prelude.tex
prelude.tex
+333
328
programs.tex
programs.tex
+249
162
report.tex
report.tex
+41
18
short_semantics.tex
short_semantics.tex
+24
19
syntax.tex
syntax.tex
+23
3
syntax/grammar.tex
syntax/grammar.tex
+175
196
syntax/layout.tex
syntax/layout.tex
+6
6
syntax/lexicon.tex
syntax/lexicon.tex
+9
4
titlepage.tex
titlepage.tex
+12
4
types.tex
types.tex
+107
160
No files found.
encsearch.tex
View file @
5ce007dc
...
...
@@ 31,51 +31,51 @@ 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
\code
{
a>
Bool
}
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
{
(
\
tt
bs
$
x
$
>
$
c
$
)
}
.
then the corresponding search goal has the form
\code
{
(
\bs
$
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
}
\
startprog
try :: (a>
Success
) > [a>
Success
]
\
stopprog
\
begin{curry}
try :: (a>
Bool
) > [a>
Bool
]
\
end{curry}
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 nondeterministic 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 (
\
tt
bs
$
x
$
>
$
c
$
)
}
Thus, an expression of the form
\code
{
try (
\bs
$
x
$
>
$
c
$
)
}
can have three possible results:
\begin{enumerate}
\item
An empty list. This indicates that the search goal
\code
{
(
\
tt
bs
$
x
$
>
$
c
$
)
}
An empty list. This indicates that the search goal
\code
{
(
\bs
$
x
$
>
$
c
$
)
}
has no solution. For instance, the expression
\
startprog
try (
\
ttbs
{}
x > 1=:=2)
\
stopprog
\
begin{curry}
try (
\x
> 1=:=2)
\
end{curry}
reduces to
\code
{
[]
}
.
\item
A list containing a single element. In this case, the search goal
\code
{
(
\
tt
bs
$
x
$
>
$
c
$
)
}
has a single solution represented by the element
\code
{
(
\bs
$
x
$
>
$
c
$
)
}
has a single solution represented by the element
of this list. For instance, the expression
\
startprog
try (
\
ttbs
{}
x>[x]=:=[0])
\
stopprog
reduces to
\code
{
[
\
tt
bs
{}
x>x=:=0]
}
.
\
begin{curry}
try (
\x
>[x]=:=[0])
\
end{curry}
reduces to
\code
{
[
\bs
{}
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 oneelement list as a result of
\code
{
try
}
has always the form
\code
{
[
\
tt
bs
$
x
$
>
$
x
$
=:=
$
e
$
]
}
has always the form
\code
{
[
\bs
$
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
...
...
@@ 83,20 +83,20 @@ of equational constraints.
\item
A list containing more than one element. In this case, the evaluation
of the search goal
\code
{
(
\
tt
bs
$
x
$
>
$
c
$
)
}
requires a nondeterministic
of the search goal
\code
{
(
\bs
$
x
$
>
$
c
$
)
}
requires a nondeterministic
computation step. The different alternatives immediately after
this nondeterministic step are represented as elements of this list.
For instance, if the function
\code
{
f
}
is defined by
\
startprog
\
begin{curry}
f a = c
f b = d
\
stopprog
\
end{curry}
then the expression
\
startprog
try (
\
ttbs
{}
x > f x =:= d)
\
stopprog
\
begin{curry}
try (
\x
> f x =:= d)
\
end{curry}
reduces to the list
\code
{
[
\
tt
bs
{}
x>x=:=a
\&
f a =:= d,
\
tt
bs
{}
x>x=:=b
\&
f b =:= d]
}
.
\code
{
[
\bs
{}
x>x=:=a
\&
f a =:= d,
\bs
{}
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
...
...
@@ 109,33 +109,33 @@ This provides the possibility to determine the behavior
for nondeterministic computations. For instance,
the following function defines a depthfirst search operator
which collects all solutions of a search goal in a list:
\
startprog
solveAll :: (a>
Success
) > [a>
Success
]
\
begin{curry}
solveAll :: (a>
Bool
) > [a>
Bool
]
solveAll g = collect (try g)
where collect [] = []
collect [g] = [g]
collect (g1:g2:gs) = concat (map solveAll (g1:g2:gs))
\
stopprog
\
end{curry}
(
\code
{
concat
}
concatenates a list of lists to a single list).
For instance, if
\code
{
append
}
is the list concatenation, then the expression
\
startprog
solveAll (
\
ttbs
{}
l > append l [1] =:= [0,1])
\
stopprog
reduces to
\code
{
[
\
tt
bs
{}
l>l=:=[0]]
}
.
\
begin{curry}
solveAll (
\l
> append l [1] =:= [0,1])
\
end{curry}
reduces to
\code
{
[
\bs
{}
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
\
startprog
solveAll (
\
ttbs
{}
l>append l [1] =:= [0,1]) =:= [g]
\
&
g x
\
stopprog
\
begin{curry}
solveAll (
\l
>append l [1] =:= [0,1]) =:= [g]
&
g x
\
end{curry}
binds the variable
\code
{
g
}
to the search goal
\code
{
[
\
tt
bs
{}
l>l=:=[0]]
}
and the variable
\code
{
x
}
to the value
\code
{
[0]
}
\code
{
[
\bs
{}
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
\
startprog
findall :: (a>
Success
) > [a]
\
stopprog
\
begin{curry}
findall :: (a>
Bool
) > [a]
\
end{curry}
which takes a search goal and collects all solutions
(computed by a depthfirst search like
\code
{
solveAll
}
)
for the search variable into a list.
...
...
@@ 144,9 +144,9 @@ 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 depthfirst search strategy can be defined by
\
startprog
\
begin{curry}
first g = head (findall g)
\
stopprog
\
end{curry}
Note that
\code
{
first
}
is a partial function, i.e., it is undefined
if
\code
{
g
}
has no solution.
...
...
@@ 156,9 +156,9 @@ if \code{g} has no solution.
Some care is necessary if free variables occur in the search goal,
like in the goal
\
startprog
\
ttbs
{}
l2 > append l1 l2 =:= [0,1]
\
stopprog
\
begin{curry}
\l
2 > append l1 l2 =:= [0,1]
\
end{curry}
Here, only the variable
\code
{
l2
}
is abstracted in the search goal
but
\code
{
l1
}
is free. Since nondeterministic bindings
cannot be performed during encapsulated search,
...
...
@@ 166,19 +166,19 @@ cannot be performed during 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
\
startprog
first (
\
ttbs
{}
l2 > append l1 l2 =:= [0,1])
\
stopprog
\
begin{curry}
first (
\l
2 > append l1 l2 =:= [0,1])
\
end{curry}
cannot be evaluated and will be suspended until the variable
\code
{
l1
}
is bound by another part of the computation. Thus, the constraint
\
startprog
s =:= first (
\
ttbs
{}
l2>append l1 l2 =:= [0,1])
\
&
l1 =:= [0]
\
stopprog
\
begin{curry}
s =:= first (
\l
2>append l1 l2 =:= [0,1])
&
l1 =:= [0]
\
end{curry}
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
\
startprog
\
{
l1=[0], s=[1]
\
}
\
stopprog
\
begin{curry}
{
l1=[0], s=[1]
}
\
end{curry}
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
...
...
@@ 186,17 +186,17 @@ 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
\
startprog
\
ttbs
{}
e > append l [e] =:= [3,4,5]
\
stopprog
\
begin{curry}
\e
> append l [e] =:= [3,4,5]
\
end{curry}
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
{
secfreevars
}
), like in the following expression:
\
startprog
first (
\
ttbs
{}
e > let l free in append l [e] =:= [3,4,5])
\
stopprog
\
begin{curry}
first (
\e
> let l free in append l [e] =:= [3,4,5])
\
end{curry}
Due to the local declaration of the variable
\code
{
l
}
(which corresponds logically to an
existential quantification), the variable
\code
{
l
}
is only visible
...
...
@@ 224,24 +224,24 @@ a powerful primitive to define appropriate search strategies.
In the following, we list the predefined search operators.
\begin{description}
\item
[\code{solveAll :: (a>
Success
) > [a>
Success
]
}
]~
\pindex
{
solveAll
}
\\
\item
[\code{solveAll :: (a>
Bool
) > [a>
Bool
]
}
]~
\pindex
{
solveAll
}
\\
Compute all solutions for a search goal via a depthfirst 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
}
\\
\item
[\code{once :: (a>
Bool
) > (a>
Bool
)}]
~
\pindex
{
once
}
\\
Compute the first solution for a search goal via a depthfirst 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
}
\\
\item
[\code{findall :: (a>
Bool
) > [a]
}
]~
\pindex
{
findall
}
\\
Compute all solutions for a search goal via a depthfirst 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
}
\\
\item
[\code{best :: (a>
Bool
) > (a>a>Bool) > [a>
Bool
]
}
]~
\pindex
{
best
}
\\
Compute the best solution via a depthfirst search strategy, according to
a specified relation (the second argument)
that can always take a decision which of two solutions is better
...
...
@@ 249,44 +249,49 @@ that can always take a decision which of two solutions is better
is a better solution than the second argument).
As a trivial example, consider the relation
\code
{
shorter
}
defined by
\
startprog
\
begin{curry}
shorter l1 l2 = length l1 <= length l2
\
stopprog
\
end{curry}
Then the expression
\
startprog
best (
\
ttbs
{}
x > let y free in append x y =:= [1,2,3]) shorter
\
stopprog
\
begin{curry}
best (
\x
> let y free in append x y =:= [1,2,3]) shorter
\
end{curry}
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
{
[
\
tt
bs
{}
x>x=:=[]]
}
. Similarly, the expression
\
startprog
best (
\
ttbs
{}
x > let y free in append x y =:= [1,2,3])
(
\
ttbs
{}
l1 l2 > length l1 > length l2)
\
stopprog
reduces to
\code
{
[
\
tt
bs
{}
x>x=:=[1,2,3]]
}
.
it reduces to
\code
{
[
\bs
{}
x>x=:=[]]
}
. Similarly, the expression
\
begin{curry}
best (
\x
> let y free in append x y =:= [1,2,3])
(
\l
1 l2 > length l1 > length l2)
\
end{curry}
reduces to
\code
{
[
\bs
{}
x>x=:=[1,2,3]]
}
.
\item
[\code{browse :: (a>
Success
) > IO ()}]
~
\pindex
{
browse
}
\\
\item
[\code{browse :: (a>
Bool
) > 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
}
\\
\item
[\code{browseList :: [a>
Bool
]
> 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
\
startprog
browseList (solveAll (
\
ttbs
{}
x > let y free in append x y =:= [0,1,2]))
\
stopprog
\
begin{curry}
browseList (solveAll (
\x
> let y free in append x y =:= [0,1,2]))
\
end{curry}
produces the following result on the standard output:
\
startprog
\
begin{curry}
[]
[0]
[0,1]
[0,1,2]
\
stopprog
\
end{curry}
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.
\end{description}
%%% Local Variables:
%%% mode: latex
%%% TeXmaster: "report"
%%% End:
examples.tex
View file @
5ce007dc
...
...
@@ 10,35 +10,35 @@ 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.
\
startprog
~
\
begin{curry}
 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
~
\
stopprog
\
end{curry}
Expressions and their evaluated results:
\
startprog
~
\
begin{curry}
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
=[]
\
}
~
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
\
stopprog
\
end{curry}
\newpage
...
...
@@ 48,32 +48,32 @@ Here are some ``traditional'' higherorder 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
{
appprelude
}
).
\
startprog
~
\
begin{curry}
 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)
~
\
stopprog
\
end{curry}
\newpage
\subsection
{
Relational Programming
}
...
...
@@ 81,48 +81,48 @@ quicksort (x:xs) = quicksort (filter (<= x) xs)
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
}
).
\
startprog
relationships are represented as
predicates.
\
begin{curry}
 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
~
married :: Person > Person >
Bool
married Christine Antony =
True
married Maria
Bill = True
married Monica
John
= True
married Alice
Frank =
True
mother :: Person > Person >
Bool
mother Christine John =
True
mother Christine Alice =
True
mother Maria
Frank
= True
mother Monica
Susan
= True
mother Monica
Peter
= True
mother Alice
Andrew
= True
 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
~
\
stopprog
father :: Person > Person >
Bool
father f c

married m f
&
mother m c
= True where m free
grandfather :: Person > Person >
Bool
grandfather g c

father g f
&
&
father f c
= True where f free
grandfather g c

father g m
&
&
mother m c
= True where m free
\
end{curry}
Expressions and their evaluated results:
\vspace
{
1ex
}
\
startprog
father John child
$
~~
\leadsto
~~
$
\
{
child=Susan
\
}

\
{
child=Peter
\
}
~
\
begin{curry}
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
\
}
\
stopprog
{
g=Antony,c=Susan
}

{
g=Antony,c=Peter
}

{
g=Bill,c=Andrew
}

{
g=Antony,c=Andrew
}
\
end{curry}
...
...
@@ 138,18 +138,18 @@ between the different persons. Note that the derived
function
\code
{
grandfather
}
is a nondeterministic function
which yields all grandfathers for a given person.
\
startprog
\
begin{curry}
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
...
...
@@ 157,23 +157,23 @@ 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
)
~
\
stopprog
grandfather
c
= father (father
c
)
grandfather
c
= father (mother
c
)
\
end{curry}
Expressions and their evaluated results:
\
startprog
\vspace
{
1ex
}
father
C
hild =
:
=
j
ohn
$
~~
\leadsto
~~
$
\{
C
hild=
s
usan
\
}

\{
C
hild=
p
eter
\
}
~
\
begin{curry}
\vspace
{
1ex
}
solve
$
\code
{
\$
}$
father
c
hild ==
J
ohn
$
~~
\leadsto
~~
$
{
c
hild=
S
usan
}

{
c
hild=
P
eter
}
grandfather c
$
~~
\leadsto
~~
$
\
{
c=Susan
\
}
Antony 
\
{
c=Peter
\
}
Antony 
\
{
c=Andrew
\
}
Bill 
\
{
c=Andrew
\
}
Antony
\
stopprog
{
c=Susan
}
Antony 
{
c=Peter
}
Antony 
{
c=Andrew
}
Bill 
{
c=Andrew
}
Antony
\
end{curry}
...
...
@@ 196,80 +196,35 @@ 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:
\startprog
diff :: a > a > Success
diff x y = (x==y)=:=False
\stopprog
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.
There is a straightforward solution to 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:
\
startprog
~
\
begin{curry}
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
~
\stopprog
In classical logic programming, we can compute the solutions to
isColor :: Color > Bool
isColor Red = True
isColor Yellow = True
isColor Green = True
isColor Blue = True
coloring :: Color > Color > Color > Color > Bool
coloring l1 l2 l3 l4 = isColor l1
&
isColor l2
&
isColor l3
&
isColor l4
correct :: Color > Color > Color > Color > Bool
correct l1 l2 l3 l4 = l1 /= l2
&
l1 /= l3
&
l2 /= l3
&
l2 /= l4
&
l3 /= l4
\end{curry}
As 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 ``sequentialfirst'' manner: first
$
c
_
1
$
is solved and, if
this is not possible due to a suspended evaluation,
$
c
_
2
$
is solved.
}
\startprog
coloring l1 l2 l3 l4
\&
correct l1 l2 l3 l4
\stopprog
However, a much faster solution can be obtained by reversing the order
of the tester and the generator:
\startprog
correct l1 l2 l3 l4
\&
coloring l1 l2 l3 l4
\stopprog
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
\startprog
diff l1 l2
\&
diff l1 l3
\&
diff l2 l3
\&
diff l2 l4
\&
diff l3 l4
\stopprog
which is then reduced to
\startprog
(l1==l2)=:=False
\&
(l1==l3)=:=False
\&
(l2==l3)=:=False
\&
(l2==l4)=:=False
\&
(l3==l4)=:=False
\stopprog
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 generateandtest 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.
the following goal:
\begin{curry}
coloring l1 l2 l3 l4
&&
correct l1 l2 l3 l4
\end{curry}
\newpage
...
...
@@ 281,41 +236,41 @@ in a concurrent objectoriented style in Curry.
For this purpose, an object is a process waiting for incoming