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
2fd5e1eb
Commit
2fd5e1eb
authored
Mar 27, 2006
by
Michael Hanus
Browse files
eval choice removed and changes due to Wolfgang
parent
a7a8c90e
Changes
1
Hide whitespace changes
Inline
Sidebyside
Showing
1 changed file
with
140 additions
and
98 deletions
+140
98
report.tex
report.tex
+140
98
No files found.
report.tex
View file @
2fd5e1eb
...
...
@@ 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
14
, 2006
}
\\
[8ex]
{
\large
March
20
, 2006
}
\\
[8ex]
%{\large \today}\\[8ex]
\Large
Michael Hanus
$^
1
$
[editor]
\\
[3ex]
...
...
@@ 547,7 +547,7 @@ Patterns are useful to split the definition of functions into
easily comprehensible cases. Thus, a pattern denotes some
part of a structure of the actual argument. Sometimes one wants to
reuse this structure in the righthand side of the defining equation.
This can be expressed by an
\emph
{
aspattern
}
\index
{
aspattern
}
\pindex
{
@
}
This can be expressed by an
\emph
{
aspattern
}
\index
{
aspattern
}
\pindex
{
"
@
}
which allows to identify this structure by a variable.
An aspattern has the form
\code
{$
v
$
@
$
pat
$}
where the variable
$
v
$
identifies the structure matched by the pattern
$
pat
$
.
...
...
@@ 689,11 +689,10 @@ in the presence of search operators, see Section~\ref{secencapsearch},
where existential quantifiers and lambda abstractions are often
mixed). Therefore, Curry requires that
\emph
{
each free variable
$
x
$
must be explicitly declared
}
using a declaration
\index
{
declaration!free
}
\index
{
free declaration
}
using a
local
declaration
\index
{
declaration!free
}
\index
{
free declaration
}
\index
{
variable!declaration
}
of the form
\code
{$
x
$
free
}
.
\pindex
{
free
}
These declarations
can occur in
\code
{
where
}
clauses or in a
\code
{
let
}
enclosing
a constraint. The variable is then introduced as unbound
of the form
\code
{$
x
$
free
}
.
\pindex
{
free
}
The variable is then introduced as unbound
with the same scoping rules as for all other local
entities (see Section~
\ref
{
seclocaldecls
}
).
For instance, we can define
...
...
@@ 1485,14 +1484,10 @@ $
\mbox
{
~~if
$
\tau
$
is a type expression
}
\\
[
3
ex
]
\mbox
{
Existential:
}
&
\infrule
{
\Ac
[
x
/
\tau
]
\vdash
e::
\
code
{
Success
}
}
{
\Ac
\vdash
\code
{
let
\,
}
x
\code
{
\,
free
\,
in
\,
}
e::
\
code
{
Success
}
}
\infrule
{
\Ac
[
x
/
\tau
]
\vdash
e::
\
tau
'
}
{
\Ac
\vdash
\code
{
let
\,
}
x
\code
{
\,
free
\,
in
\,
}
e::
\
tau
'
}
\mbox
{
~~if
$
\tau
$
is a type expression
}
\\
[
3
ex
]
\mbox
{
Conditional:
}
&
\infrule
{
\Ac
\vdash
e
_
1
::
\code
{
Bool
}
\quad
\Ac
\vdash
e
_
2
::
\tau
\quad
\Ac
\vdash
e
_
3
::
\tau
}
{
\Ac
\vdash
\code
{
if
\,
}
e
_
1
\code
{
\,
then
\,
}
e
_
2
\code
{
\,
else
\,
}
e
_
3
::
\tau
}
\\
[
3
ex
]
\end
{
array
}
$
}
% fbox
...
...
@@ 2610,71 +2605,64 @@ which are printed on the standard output until the process is stopped.
\end{description}
\subsection
{
Choice
}
\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 the special evaluation annotation
\index
{
evaluation annotation
}
\code
{
choice
}
\pindex
{
choice
}
\index
{
committed choice
}
:
\startprog
$
f
$
eval choice
\stopprog
Intuitively, a function
$
f
$
declared as a
\code
{
choice
}
function
behaves as follows. A call to
$
f
$
is evaluated as usual
(with a fair evaluation of disjunctive alternatives, which is
important here!) but with the following differences:
\begin{enumerate}
\item
No free variable of this function call is bound
(i.e., this function call and all its subcalls are suspended in case of
an attempt to instantiate a free variable of this call).
\item
If one rule for
$
f
$
matches and its guard is entailed
(i.e., satisfiable without binding goal variables), all other
alternatives for evaluating this call are ignored.
\end{enumerate}
This means that the first applicable rule for this function call
(after pattern matching and guard checking) is taken and all
other alternatives are discarded.
As an example, consider the nondeterministic function
\code
{
merge
}
\pindex
{
merge
}
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
eval choice
merge [] l2 =
l2
merge l1 [] =
l1
merge (e:r) l2 = e : merge r
l2
merge l1 (e:r) = e
: merge l1
r
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
Due to the
\code
{
choice
}
annotation
, a call to
\code
{
merge
}
is reducible
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
{
c
hoice
}
annotation is a fair
Another application of the
\code
{
c
ommit
}
annotation is a fair
evaluation of disjunctive search goals. For instance,
the following
func
tion takes a search goal and computes
the following
opera
tion 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 eval choice
tryone g  g x = x where x free
tryone g = commit [let x free in (g x, x)]
\stopprog
%
Note that functions containing
\code
{
choice
}
expressions
may be
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
functions declared with
\code
{
c
hoice
}
only one result is computed for
calls to
\code
{
c
ommit
}
instead of all results. As a consequence, the
completeness result for Curry's operational semantics
\cite
{
Hanus97POPL
}
does not hold in the presence of
the evaluation
annotation
\code
{
c
hoice
}
. Since indeterministic functions
\cite
{
Hanus97POPL
}
does not hold in the presence of
calls
to
\code
{
c
ommit
}
. Since indeterministic functions
are mainly used in the coordination level of concurrent
applications (as in parallel functional computation models
\cite
{
BreitingerLoogenOrtega95,ChakravartyEtAl98Goffin
}
),
...
...
@@ 3531,7 +3519,7 @@ failed  1=:=2 = x where x free
~
 Boolean values
~
data Bool =
True  Fals
e
\pindex
{
Bool
}
\pindex
{
True
}
\pindex
{
False
}
data Bool =
False  Tru
e
\pindex
{
Bool
}
\pindex
{
True
}
\pindex
{
False
}
~
 Sequential conjunction
(
\&\&
) :: Bool > Bool > Bool
\pindex
{
\&\&
}
...
...
@@ 3557,10 +3545,6 @@ otherwise :: Bool \pindex{otherwise}
otherwise = True
~
~
 Ordering
\pindex
{
Ordering
}
\pindex
{
LT
}
\pindex
{
EQ
}
\pindex
{
GT
}
data Ordering = LT  EQ  GT
~
~
 Equality on finite ground data terms
(==) :: a > a > Bool
\pindex
{
==
}
~
...
...
@@ 3569,6 +3553,41 @@ data Ordering = LT  EQ  GT
x /= y = not (x==y)
~
~
 Ordering
\pindex
{
Ordering
}
\pindex
{
LT
}
\pindex
{
EQ
}
\pindex
{
GT
}
data Ordering = LT  EQ  GT
~
 Comparison of arbitrary ground data terms.
\pindex
{
compare
}
 Data constructors are compared in the order of their definition
 in the datatype declarations and recursively in the arguments.
compare :: a > a > Ordering
~
 Lessthan on ground data terms
(<) :: a > a > Bool
\pindex
{
<
}
x < y = case compare x y of LT > True
_
> False
~
 Greaterthan on ground data terms
(>) :: a > a > Bool
\pindex
{
>
}
x > y = case compare x y of GT > True
_
> False
~
 Lessorequal on ground data terms
(<=) :: a > a > Bool
\pindex
{
<=
}
x <= y = not (x > y)
~
 Greaterorequal on ground data terms
(>=) :: a > a > Bool
\pindex
{
>=
}
x >= y = not (x < y)
~
 Maximum of ground data terms
max :: a > a > a
\pindex
{
max
}
max x y = if x >= y then x else y
~
 Minimum of ground data terms
min :: a > a > a
\pindex
{
min
}
min x y = if x <= y then x else y
~
~
 Pairs
~
data (a,b) = (a,b)
\pindex
{
(
\ldots
)
}
\index
{
pair
}
\index
{
tuple
}
...
...
@@ 3851,17 +3870,13 @@ chr :: Int > Char \pindex{chr}
show :: a > String
\pindex
{
show
}
~
~
 Types of primitive arithmetic functions
and predicates
 Types of primitive arithmetic functions
~
(+) :: Int > Int > Int
\pindex
{
+
}
() :: Int > Int > Int
\pindex
{

}
(*) :: Int > Int > Int
\pindex
{
*
}
div :: Int > Int > Int
\pindex
{
div
}
mod :: Int > Int > Int
\pindex
{
mod
}
(<) :: Int > Int > Bool
\pindex
{
<
}
(>) :: Int > Int > Bool
\pindex
{
>
}
(<=) :: Int > Int > Bool
\pindex
{
<=
}
(>=) :: Int > Int > Bool
\pindex
{
>=
}
~
 Unary minus (usually written as " e")
negate :: Int > Int
\pindex
{
negate
}
...
...
@@ 4006,11 +4021,13 @@ 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 eval choice
tryone g  g x = x where x free
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
}
...
...
@@ 4092,9 +4109,9 @@ or another identifier
The following symbols are
\emph
{
keywords
}
\index
{
keywords
}
and cannot be used as an identifier:
\startprog
case
choice
data do else e
val external
free
i
f
import in
infix infixl infixr
let module
of then type where
case data do else e
xternal free if
infix
i
nfixl infixr
import in
let module
of then type where
\stopprog
%
Note that the symbols
\term
{
as
}
\pindex
{
as
}
,
\term
{
hiding
}
\pindex
{
hiding
}
,
...
...
@@ 4292,7 +4309,7 @@ end
\lexicon
{
InfixOpID
}
\production
FunctionDeclaration
Signature
$

$
EvalAnnot
$

$
Equat
Signature
$

$
Equat
end
\production
Signature FunctionNames
\term
{
::
}
TypeExpr end
...
...
@@ 4308,8 +4325,6 @@ end
\lexicon
{
FunctionID
}
\production
EvalAnnot FunctionNames
\term
{
eval
}
\term
{
choice
}
end
\production
Equat
FunLHS
\term
{
=
}
Expr
\opt
{
\term
{
where
}
LocalDefs
}
\por
FunLHS CondExprs
\opt
{
\term
{
where
}
LocalDefs
}
...
...
@@ 4663,7 +4678,7 @@ to such nodes with more than two subtrees is straightforward.}
\end
{
description
}
The
$
rigid
$
/
$
flex
$
tag in a branch will be used to specify the
suspension behavior w.r.t.
\
free variables as actual arguments.
User

defined function are always translated into definitional trees
User

defined function
s
are always translated into definitional trees
with
$
flex
$
tags, but case expressions are translated
into definitional trees with
$
rigid
$
tags.
...
...
@@ 4901,6 +4916,36 @@ $
\caption
{
Evaluation of conditional rules
\label
{
figure

condrules
}}
\end
{
figure
*
}
\paragraph
{
Ensuring instantiation
}
The semantics of the primitive
\code
{
ensureNotFree
}
to ensure
computations with instantiated expressions, as informally
described in Section~
\ref
{
sec

ensurenotfree
}
,
can be easily described by the rules in Figure~
\ref
{
figure

notfreerules
}
.
If
\code
{
ensureNotFree
}
occurs in a computation with a
constructor term as argument, it has no effect on the computation
(
first rule
)
. It behaves like the identity as long as
the argument is a function call. Otherwise
(
i.e., if the argument
is a free variable
)
, no evaluation step is possible.
\begin
{
figure
*
}
[
t
]
\begin
{
center
}
\fbox
{
$
\begin{array}
{
l@
{}}
\infrule
{
\eval
{
c(e
_
1,
\ldots
,e
_
n)
}
\To
\dexp
}
{
\eval
{
\code
{
ensureNotFree
}
(c(e
_
1,
\ldots
,e
_
n))
}
\To
\dexp
}
\\
[3ex]
\infrule
{
\eval
{
f(e
_
1,
\ldots
,e
_
n)
}
\To
\dexp
}
{
\eval
{
\code
{
ensureNotFree
}
(f(e
_
1,
\ldots
,e
_
n))
}
\To
replace(
\code
{
ensureNotFree
}
(f(e
_
1,
\ldots
,e
_
n)),1,
\dexp
)
}
\\
[3ex]
\end{array}
$
}
% fbox
\end
{
center
}
\vspace
{

3
ex
}
\caption
{
Evaluation of
\code
{
ensureNotFree
}
\label
{
figure

notfreerules
}}
\end
{
figure
*
}
\paragraph
{
Sharing and graph rewriting.
}
For the sake of simplicity,
this description of the operational semantics is based on term rewriting
...
...
@@ 4940,37 +4985,36 @@ based on heap structures to model sharing can be found in
\subsection
{
Committed Choice
}
To define the semantics of calls to functions with
the evaluation annotation
\code
{
choice
}
, we assume that all
such calls are enclosed by
$
choice(
\ldots
)
$
. Now we extend the rules
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
$
choice(f(e
_
1,
\ldots
,e
_
n))
$
is reduced as follows.
If
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
{
f
(
e
_
1
,
\ldots
,e
_
n
)
}
~
\To
^
*
~
\{\ldots
,
\sigma
\ans
\code
{
success

}
\varphi
(
r
)
,
\ldots\}
\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
$
l
\code
{
~
\,
}
c
\code
{
~=
\,
}
r
$
is a rule for
$
f
$
,
\footnote
{
An unconditional rule
$
l
\code
{
\,
=
\,
}
r
$
is considered here as an abbreviation for
$
l
\code
{
\,

\,
success
\,
=
\,
}
r
$
.
}
$
\sigma
$
does not bind any free variable
occurring in
$
f(e
_
1,
\ldots
,e
_
n)
$
, and this is the first
step in the derivation with this property, then
$
\eval
{
choice(f(e
_
1,
\ldots
,e
_
n))
}
\To
\{
id
\ans
\varphi
(r)
\}
$
.
Thus, if disjunctions occur due to the evaluation of a call
to a choice function, these disjunctions are not distributed
to the top level but are kept inside the
$
choice
$
expression.
If one rule for the choice function becomes applicable
(
without
binding of free variables in this call
)
, all
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
choice function
corresponds to
the
committed choice
(
with
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
can b
e bound.
local variables
ar
e bound.
\subsection
{
Equational Constraints
}
...
...
@@ 5145,9 +5189,7 @@ is $\{1\}$.
The
\emph
{
g
}
eneration of a definitional
\emph
{
t
}
ree for a call pattern
$
\pi
$
and a set of rules
$
R
$
(
where
$
l
$
is an instance of
$
\pi
$
for each
$
l
\code
{
\,
=
\,
}
r
\in
R
$
)
is described by the function
$
gt(
\pi
,m,R)
$
(
$
m
\in
\{
flex,rigid
\}
$
determines the mode annotation in the generated
$
branch
$
nodes
)
.
$
l
\code
{
\,
=
\,
}
r
\in
R
$
)
is described by the function
$
gt(
\pi
,R)
$
.
We distinguish the following cases for
$
gt
$
:
\begin
{
enumerate
}
\item
...
...
@@ 5158,10 +5200,10 @@ $n_1,\ldots,n_k$,
and
$
R
_
i =
\{
l
\code
{
\,
=
\,
}
r
\in
R
\mid
root(l
_
o) = c
_
i
\}
$
, then
\[
\begin
{
array
}{
l@
{
\,
}
l
}
gt
(
\pi
,
m,
R
)
=
branch
(
\pi
,o,
m
,
&
gt
(
\pi
[
c
_
1
(
x
_{
11
}
,
\ldots
,x
_{
1
n
_
1
}
)]
_
o,
m,
R
_
1
)
,
\\
gt
(
\pi
,R
)
=
branch
(
\pi
,o,
flex
,
&
gt
(
\pi
[
c
_
1
(
x
_{
11
}
,
\ldots
,x
_{
1
n
_
1
}
)]
_
o,R
_
1
)
,
\\
&
\ldots
,
\\
&
gt
(
\pi
[
c
_
k
(
x
_{
k
1
}
,
\ldots
,x
_{
kn
_
k
}
)]
_
o,
m,
R
_
k
))
&
gt
(
\pi
[
c
_
k
(
x
_{
k
1
}
,
\ldots
,x
_{
kn
_
k
}
)]
_
o,R
_
k
))
\end
{
array
}
\]
where
$
x
_{
ij
}$
are fresh variables.
...
...
@@ 5172,7 +5214,7 @@ If $IP(\pi,R) = \emptyset$, let $o$ be the leftmost position in $DP(\pi,R)$
and
$
R' =
\{
l
\code
{
\,
=
\,
}
r
\in
R
\mid
root(l
_
o)
\in
\Cc
\}
$
.
Then
\[
gt
(
\pi
,
m,
R
)
=
or
(
gt
(
\pi
,
m,
R'
)
,gt
(
\pi
,
m,
R

R'
))
gt
(
\pi
,R
)
=
or
(
gt
(
\pi
,R'
)
,gt
(
\pi
,R

R'
))
\]
I.e., we generate an
$
or
$
node if the leftmost demanded position
of the call pattern is not demanded by the left

hand sides of all rules.
...
...
@@ 5180,7 +5222,7 @@ of the call pattern is not demanded by the lefthand sides of all rules.
If
$
DP(
\pi
,R) =
\emptyset
$
and
$
l
\code
{
\,
=
\,
}
r
$
variant of some rule in
$
R
$
with
$
l =
\pi
$
, then
\[
gt
(
\pi
,
m,
R
)
=
rule
(
l
\code
{
\,
=
\,
}
r
)
gt
(
\pi
,R
)
=
rule
(
l
\code
{
\,
=
\,
}
r
)
\]
Note that all rules in
$
R
$
are variants of each other if there is no demanded
position
(
this follows from the weak orthogonality of the rewrite system
)
.
...
...
@@ 5191,7 +5233,7 @@ the different rules by $or$ nodes.
\end
{
enumerate
}
If
$
R
$
is the set of all rules defining the
$
n
$

ary function
$
f
$
,
then a definitional tree for
$
f
$
is generated by computing
$
gt(f(x
_
1,
\ldots
,x
_
n),
flex,
R)
$
.
$
gt(f(x
_
1,
\ldots
,x
_
n),R)
$
.
It is easy to see that this algorithm
computes a definitional tree for each
...
...
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