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
f6417293
Commit
f6417293
authored
May 10, 2006
by
Michael Hanus
Browse files
New version 0.8.2
parent
2fd5e1eb
Changes
1
Hide whitespace changes
Inline
Sidebyside
Showing
1 changed file
with
106 additions
and
120 deletions
+106
120
report.tex
report.tex
+106
120
No files found.
report.tex
View file @
f6417293
...
...
@@ 106,7 +106,7 @@
{
\Huge\bf
Curry
}
\\
[4ex]
{
\LARGE\bf
An Integrated Functional Logic Language
}
\\
[5ex]
{
\large\bf
Version 0.8.2
}
\\
[1ex]
{
\large
March 2
0
, 2006
}
\\
[8ex]
{
\large
March 2
8
, 2006
}
\\
[8ex]
%{\large \today}\\[8ex]
\Large
Michael Hanus
$^
1
$
[editor]
\\
[3ex]
...
...
@@ 1869,7 +1869,8 @@ the name of the module followed by the keyword
\startprog
module Stack where
\ldots
\stopprog
If a module stored in file
\code
{
M.curry
}
does not contain a module head,
If a module stored in a directory in file
\code
{
M.curry
}
does not contain a module head,
the
\emph
{
standard module head
}
``
\code
{
module M where
}
'' is implicitly inserted.
\emph
{
Module names
}
\index
{
module name
}
\index
{
name!of a module
}
...
...
@@ 2567,16 +2568,16 @@ best (\ttbs{}x > let y free in append x y =:= [1,2,3])
\stopprog
reduces to
\code
{
[
\ttbs
{}
x>x=:=[1,2,3]]
}
.
\item
[\code{one :: (a>Success) > [a>Success]
}
]~
\pindex
{
one
}
\\
Compute one solution via a fair strategy.
If there is no solution and the search space is finite,
the result is the empty list, otherwise the list contains one element
(the first solution represented as a search goal).
%
\item[\code{one :: (a>Success) > [a>Success]}]~\pindex{one}\\
%
Compute one solution via a fair strategy.
%
If there is no solution and the search space is finite,
%
the result is the empty list, otherwise the list contains one element
%
(the first solution represented as a search goal).
\item
[\code{condSearch :: (a>Success) > (a>Bool) > [a>Success]
}
]~
\pindex
{
condSearch
}
\\
Compute the first solution (via a fair strategy)
that meets a specified condition.
The condition (second argument) must be a unary Boolean function.
%
\item[\code{condSearch :: (a>Success) > (a>Bool) > [a>Success]}]~\pindex{condSearch}\\
%
Compute the first solution (via a fair strategy)
%
that meets a specified condition.
%
The condition (second argument) must be a unary Boolean function.
\item
[\code{browse :: (a>Success) > IO ()}]
~
\pindex
{
browse
}
\\
Show the solution of a
\emph
{
solved
}
constraint on the standard output,
...
...
@@ 2605,69 +2606,69 @@ which are printed on the standard output until the process is stopped.
\end{description}
\subsection
{
Committed Choice
}
In order to provide a ``don't care'' selection of an element
out of different alternatives, which is necessary in concurrent
computation structures to support manytoone communication,
Curry provides primitive operation
\code
{
commit
}
\pindex
{
commit
}
\index
{
committed choice
}
:
\startprog
commit :: [(Success,a)] > a
\stopprog
Intuitively, a call to
\code
{
commit
}
has a list of constraint/expression
pairs as argument and returns one of the expressions whose constraint
is satisfied without binding variables that are not local to the
constraint/expression pair.
If more than one of the constraints is satisfied, one of the
corresponding expressions are returned and the other alternatives
are discarded. The evaluation order is not specified, i.e.,
\code
{
commit
}
implements a fair but
\emph
{
indeterministic
}
search
for solutions.
As an example, consider the indeterministic function
\code
{
merge
}
\pindex
{
merge
}
for the fair merge of two lists:
\startprog
merge :: [a] > [a] > [a]
merge l1 l2 =
commit [(l1=:=[], l2),
(l2=:=[], l1),
(not (null l1) =:= True, head l1 : merge (tail l1) l2),
(not (null l2) =:= True, head l2 : merge l1 (tail l2))]
\stopprog
Thus, a call to
\code
{
merge
}
is reducible
if one of the input lists is known to be empty or nonempty
(but it is not reducible if both inputs are unknown).
Thus,
\code
{
merge
}
can also merge partially unknown lists
which are incrementally instantiated during computation.
Another application of the
\code
{
commit
}
annotation is a fair
evaluation of disjunctive search goals. For instance,
the following operation takes a search goal and computes
one result (if it exists) for the search variable in a fair manner,
i.e., possible infinite computation branches in a disjunction do not inhibit
the computation of a solution in another branch:
\pindex
{
tryone
}
\startprog
tryone :: (a>Success) > a
tryone g = commit [let x free in (g x, x)]
\stopprog
%
Note that functions containing calls to
\code
{
commit
}
may be
indeterministic in contrast to other userdefined functions,
i.e., identical calls may lead to different answers at different times.
This is similar to nondeterministic functions which can
be given a declarative semantics
\cite
{
GonzalezEtAl99
}
.
The difference to nondeterministic functions is that
only one result is computed for calls to
\code
{
commit
}
instead of all results. As a consequence, the
completeness result for Curry's operational semantics
\cite
{
Hanus97POPL
}
does not hold in the presence of calls
to
\code
{
commit
}
. Since indeterministic functions
are mainly used in the coordination level of concurrent
applications (as in parallel functional computation models
\cite
{
BreitingerLoogenOrtega95,ChakravartyEtAl98Goffin
}
),
this is a only minor problem. A programming environment
for Curry could classify the indeterministic functions in a program.
%
\subsection{Committed Choice}
%
In order to provide a ``don't care'' selection of an element
%
out of different alternatives, which is necessary in concurrent
%
computation structures to support manytoone communication,
%
Curry provides primitive operation
%
\code{commit}\pindex{commit}\index{committed choice}:
%
\startprog
%
commit :: [(Success,a)] > a
%
\stopprog
%
Intuitively, a call to \code{commit} has a list of constraint/expression
%
pairs as argument and returns one of the expressions whose constraint
%
is satisfied without binding variables that are not local to the
%
constraint/expression pair.
%
If more than one of the constraints is satisfied, one of the
%
corresponding expressions are returned and the other alternatives
%
are discarded. The evaluation order is not specified, i.e.,
%
\code{commit} implements a fair but \emph{indeterministic} search
%
for solutions.
%
As an example, consider the indeterministic function \code{merge}\pindex{merge}
%
for the fair merge of two lists:
%
\startprog
%
merge :: [a] > [a] > [a]
%
merge l1 l2 =
%
commit [(l1=:=[], l2),
%
(l2=:=[], l1),
%
(not (null l1) =:= True, head l1 : merge (tail l1) l2),
%
(not (null l2) =:= True, head l2 : merge l1 (tail l2))]
%
\stopprog
%
Thus, a call to \code{merge} is reducible
%
if one of the input lists is known to be empty or nonempty
%
(but it is not reducible if both inputs are unknown).
%
Thus, \code{merge} can also merge partially unknown lists
%
which are incrementally instantiated during computation.
%
Another application of the \code{commit} annotation is a fair
%
evaluation of disjunctive search goals. For instance,
%
the following operation takes a search goal and computes
%
one result (if it exists) for the search variable in a fair manner,
%
i.e., possible infinite computation branches in a disjunction do not inhibit
%
the computation of a solution in another branch:\pindex{tryone}
%
\startprog
%
tryone :: (a>Success) > a
%
tryone g = commit [let x free in (g x, x)]
%
\stopprog
%
%
%
Note that functions containing calls to \code{commit} may be
%
indeterministic in contrast to other userdefined functions,
%
i.e., identical calls may lead to different answers at different times.
%
This is similar to nondeterministic functions which can
%
be given a declarative semantics \cite{GonzalezEtAl99}.
%
The difference to nondeterministic functions is that
%
only one result is computed for calls to \code{commit}
%
instead of all results. As a consequence, the
%
completeness result for Curry's operational semantics
%
\cite{Hanus97POPL} does not hold in the presence of calls
%
to \code{commit}. Since indeterministic functions
%
are mainly used in the coordination level of concurrent
%
applications (as in parallel functional computation models
%
\cite{BreitingerLoogenOrtega95,ChakravartyEtAl98Goffin}),
%
this is a only minor problem. A programming environment
%
for Curry could classify the indeterministic functions in a program.
\newpage
...
...
@@ 4021,21 +4022,6 @@ findall g = map unpack (solveAll g)
 compute best solution via branchandbound with depthfirst search
best :: (a>Success) > (a>a>Bool) > [a>Success]
\pindex
{
best
}
~
 primitive operation for committed choice
commit :: [(Success,a)] > a
\pindex
{
commit
}
~
 try to find a solution to a search goal via a fair search
 (and fail if there is no solution)
tryone :: (a>Success) > a
\pindex
{
tryone
}
tryone g = commit [let x free in (g x, x)]
~
 compute one solution with a fair search strategy
one :: (a>Success) > [a>Success]
\pindex
{
one
}
one g = solveAll (
\ttbs
{}
x > x =:= tryone g)
~
 compute one solution with a fair search satisfying a condition
condSearch :: (a>Success) > (a>Bool) > [a>Success]
\pindex
{
condSearch
}
condSearch g cond = one (
\ttbs
{}
x > g x
\&
cond x =:= True)
~
 show the solution of a solved constraint
browse :: (a>Success) > IO ()
\pindex
{
browse
}
...
...
@@ 4983,38 +4969,38 @@ based on heap structures to model sharing can be found in
\cite
{
AlbertHanusHuchOliverVidal
05
}
.
\subsection
{
Committed Choice
}
%
\subsection{Committed Choice}
To define the semantics of the committed choice primitive
\code
{
commit
}
, we extend the rules
in Figures~
\ref
{
figure

opsem
}
and~
\ref
{
figure

condrules
}
for covering such choices.
An expression
$
e =
\code
{
commit[(
$
c
_
1
$
,
$
e
_
1
$
),
\ldots
,(
$
c
_
n
$
,
$
e
_
n
$
)]
}$
is reduced as follows.
If, for some
$
i
\in
\{
1,
\ldots
,n
\}
$
,
\[
\eval
{
c
_
i
}
~
\To
^
*
~
\{\ldots
,
\sigma
\ans
\code
{
success
}
,
\ldots\}
\]
according to the operational semantics described in
Figures~
\ref
{
figure

opsem
}
and~
\ref
{
figure

condrules
}
,
where
$
\sigma
$
does not bind any free variable
occurring in
$
e
$
, then
\[
\eval
{
\code
{
commit
[(
$
c
_
1
$
,
$
e
_
1
$
)
,
\ldots
,
(
$
c
_
n
$
,
$
e
_
n
$
)]
}}
~
\To
^
*
~
\{\sigma
\ans
\code
{$
\sigma
(e
_
i)
$}
\}
\]
%
Thus, if disjunctions occur during the evaluation of a
\code
{
commit
}
,
these disjunctions are not distributed
to the top level but are kept inside the
\code
{
commit
}
expression.
If one constraints is successfully evaluated
(
without
binding free variables in this call
)
, all
other alternatives in the disjunction are discarded.
Hence, a call to a
\code
{
commit
}
corresponds to a committed choice
(
with
deep guards
)
of concurrent logic languages.
This can be implemented by evaluating this call
(
with a fair
strategy for alternatives
)
as usual but with the restriction that only
local variables are bound.
%
To define the semantics of the committed choice primitive
%
\code{commit}, we extend the rules
%
in Figures~\ref{figureopsem} and~\ref{figurecondrules}
%
for covering such choices.
%
An expression $e = \code{commit[($c_1$,$e_1$),\ldots,($c_n$,$e_n$)]}$
%
is reduced as follows.
%
If, for some $i \in \{1,\ldots,n\}$,
%
\[
%
\eval{c_i} ~\To^*~ \{\ldots,\sigma \ans \code{success},\ldots\}
%
\]
%
according to the operational semantics described in
%
Figures~\ref{figureopsem} and~\ref{figurecondrules},
%
where $\sigma$ does not bind any free variable
%
occurring in $e$, then
%
\[
%
\eval{\code{commit[($c_1$,$e_1$),\ldots,($c_n$,$e_n$)]}} ~\To^*~
%
\{\sigma \ans \code{$\sigma(e_i)$}\}
%
\]
%
%
%
Thus, if disjunctions occur during the evaluation of a \code{commit},
%
these disjunctions are not distributed
%
to the top level but are kept inside the \code{commit} expression.
%
If one constraints is successfully evaluated (without
%
binding free variables in this call), all
%
other alternatives in the disjunction are discarded.
%
Hence, a call to a \code{commit} corresponds to a committed choice (with
%
deep guards) of concurrent logic languages.
%
This can be implemented by evaluating this call (with a fair
%
strategy for alternatives) as usual but with the restriction that only
%
local variables are bound.
\subsection
{
Equational Constraints
}
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment