Commit c1070076 authored by Michael Hanus 's avatar Michael Hanus
Browse files

Section on lambda lifting transformation added

parent 33434637
% $Id$
% $Log$
% $Id: report.tex,v 1.1 1999/07/21 12:29:41 hanus Exp hanus $
% $Log: report.tex,v $
% Revision 1.1 1999/07/21 12:29:41 hanus
% Initial revision
%
%\documentstyle[makeidx,11pt,fleqn]{article}
\documentclass[11pt,fleqn]{article}
......@@ -86,7 +89,7 @@
\begin{center}\vspace{10ex}
{\Huge\bf Curry}\\[4ex]
{\LARGE\bf An Integrated Functional Logic Language}\\[5ex]
{\large\bf Version 0.5.1}\\[1ex]
{\large\bf Version 0.5.2}\\[1ex]
{\large \today}\\[8ex]
\Large
Michael Hanus$^1$ [editor] \\[3ex]
......@@ -639,7 +642,8 @@ g y z = k y z
\ldots
let y free in c y (f y (g y 1))
\stopprog
See Appendix~\ref{app-lifting} for more details about
the meaning and transformation of local definitions.
\subsection{Constraints and Equality}
......@@ -3348,7 +3352,8 @@ as $\varphi(e_1,\ldots,e_n)$
which is equivalent to Curry's notation $\varphi~e_1\ldots e_n$.}
The set of all expressions and data terms are denoted
by $\Tc(\Cc \cup \Fc,\Xc)$ and $\Tc(\Cc,\Xc)$, respectively.
A \emph{pattern}\index{pattern} is an expression of the form
A \emph{function pattern}\index{function pattern}\index{pattern!function}
is an expression of the form
$f(t_1,\ldots,t_n)$ where each variable occurs only once,
$f \in \Fc$ is an $n$-ary function, and $t_1,\ldots,t_n \in \Tc(\Cc,\Xc)$.
$root(e)$ denotes the symbol at the
......@@ -3382,7 +3387,7 @@ for every expression $f(e_1,\ldots,e_n)$.
A Curry program is a set of rules \pr{$l$\,=\,$r$} satisfying
some restrictions (see Section~\ref{sec-funcdecl}).
In particular, the left-hand side $l$ must be a pattern.
In particular, the left-hand side $l$ must be a function pattern.
A rewrite rule is called a \emph{variant}\index{variant} of another rule
if it is obtained by a unique replacement of variables
by other variables.
......@@ -3409,7 +3414,8 @@ by Antoy's work \cite{Antoy92ALP}, but here we use an extended form
of definitional trees.}
A definitional tree is a hierarchical structure containing
all rules of a defined function.
$\Tc$ is a \emph{definitional tree with pattern}\index{definitional tree} $\pi$
$\Tc$ is a
\emph{definitional tree with function pattern}\index{definitional tree} $\pi$
iff the depth of $\Tc$ is finite and
one of the following cases holds:
\begin{description}
......@@ -3421,21 +3427,21 @@ $r \in \{rigid,flex\}$,
$c_1,\ldots,c_k$ are different constructors of the sort
of $\pi|_o$, for some $k > 0$,
and, for all $i = 1,\ldots,k$, $\Tc_i$ is a definitional tree with
pattern $\pi[c_i(x_1,\ldots,x_n)]_o$,
function pattern $\pi[c_i(x_1,\ldots,x_n)]_o$,
where $n$ is the arity of $c_i$ and
$x_1,\ldots,x_n$ are new variables.
\item [$\Tc=or(\Tc_1,\Tc_2),$] where $\Tc_1$ and $\Tc_2$ are
definitional trees with pattern $\pi$.\footnote{For the sake of simplicity,
we consider only binary $or$ nodes. The extension
definitional trees with function pattern $\pi$.\footnote{For the sake of
simplicity, we consider only binary $or$ nodes. The extension
to such nodes with more than two subtrees is straightforward.}
\end{description}
A \emph{definitional tree of an $n$-ary function} $f$
is a definitional tree $\Tc$ with pattern $f(x_1,\ldots,x_n)$,
is a definitional tree $\Tc$ with function pattern $f(x_1,\ldots,x_n)$,
where $x_1,\ldots,x_n$ are distinct variables, such that for each rule
$l \pr{\,=\,} r$ with $l = f(t_1,\ldots,t_n)$ there is a node
$rule(l' \pr{\,=\,} r')$
in $\Tc$ with $l$ variant of $l'$.
In the following, we write $pat(\Tc)$ for the pattern
In the following, we write $pat(\Tc)$ for the function pattern
of a definitional tree $\Tc$.
It is always possible to construct a definitional tree
......@@ -3858,7 +3864,7 @@ definitional trees for a single function representing different
evaluation strategies. This demands for a default strategy
to generate definitional trees. Curry uses the following default strategy:
\begin{enumerate}
\item Pattern-matching is performed from left to right.
\item Pattern matching is performed from left to right.
\item $or$ nodes are generated in case of a conflict
between constructors and variables, i.e., if two rules
have a variable and a constructor at the same position on the left-hand side.
......@@ -3877,13 +3883,13 @@ To specify the construction algorithm, we define by
DP(\pi,R) = \{ o \mbox{ position of a variable in } \pi \mid
root(l|_o) \in \Cc \mbox{ for some } l \pr{\,=\,} r \in R \}
\]
the set of \emph{demanded positions} of a pattern $\pi$ w.r.t.\ a set of
rules $R$. For instance, the demanded positions of the pattern
the set of \emph{demanded positions} of a function pattern $\pi$ w.r.t.\ a
set of rules $R$. For instance, the demanded positions of the function pattern
\pr{leq(x,y)} w.r.t.\ the rules for the predicate \pr{leq}
(see Section~\ref{example-leq}, page~\pageref{example-leq})
are $\{1,2\}$ referring to the pattern variables \pr{x} and \pr{y}.
The \emph{g}eneration of a definitional \emph{t}ree for a pattern $\pi$
and a set of rules $R$ (where $l$ is an instance of $\pi$ for each
The \emph{g}eneration of a definitional \emph{t}ree for a function pattern
$\pi$ and a set of rules $R$ (where $l$ is an instance of $\pi$ for each
$l \pr{\,=\,} 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).
......@@ -3913,7 +3919,7 @@ $R' = \{ l \pr{\,=\,} r \in R \mid root(l|_o) \in \Cc \} \neq R$, then
gt(\pi,m,R) = or(gt(\pi,m,R'),gt(\pi,m,R-R'))
\]
I.e., we generate an $or$ node if the leftmost demanded position
of the pattern is not demanded by the left-hand sides of all rules.
of the function pattern is not demanded by the left-hand sides of all rules.
\item
If $DP(\pi,R) = \emptyset$ and $l \pr{\,=\,} r$ variant of some rule in $R$
with $l = \pi$, then
......@@ -3939,7 +3945,7 @@ It is easy to see that this algorithm
computes a definitional tree for each
function since the number of rules is reduced in each recursive call
and it keeps the invariant that the left-hand sides of the current set
of rules are always instances of the current pattern.
of rules are always instances of the current function pattern.
The algorithm $gt$ conforms to the evaluation strategy
of functional languages like Haskell or Miranda, since it generates
......@@ -4048,7 +4054,8 @@ A search goal is solved (second case) if the constraint is solvable
without bindings of global variables. In a deterministic step (third
case), we apply the \pr{try} operator again after adding the newly
introduced variables to the list of local variables. Note that the
\emph{free variables} occurring in $g$, denoted by $free(g)$, must not
\emph{free variables}\index{free variable}\index{variable!free}
occurring in $g$, denoted by $free(g)$\index{free@$free(\cdot)$}, must not
be locally declared because they can appear also outside of $g$, and
therefore they have to be removed from $\VRan(\sigma)$. In a
non-deterministic step (fourth case), we return the different
......@@ -4122,6 +4129,182 @@ Thus, different implementations of Curry can support
one or both of these definitions.
\subsection{Eliminating Local Declarations}
\label{app-lifting}
In the description of the operational semantics above,
we assumed that a Curry program is a set of rules \pr{$l$\,=\,$r$}
where the left-hand side $l$ is a function pattern and the
right-hand side $r$ is an expression containing variables,
constructors, and defined functions.
However, a Curry program can also contain local declarations
(cf.\ Section~\ref{sec-localdecls}) whose operational semantics
is not defined so far. To simplify the operational semantics,
we do not extend it to local declarations but provide in the following
a transformation of Curry programs containing local declarations into Curry
programs without local declarations (except for free variables).
The main purpose of this transformation is to provide
a precise definition of the operational semantics of the full
language. This transformation can also be performed by implementations
of Curry but it is also possible that some implementations provide
explicit support for local declarations, provided that
they satisfy the operational meaning described in the following.
The elimination of local function and pattern declarations is done
in three steps:
\begin{enumerate}
\item Eliminate multiple guards in rules
\item Transform \pr{where} declarations into \pr{let} declarations
\item Eliminate local patterns and functions
\end{enumerate}
These steps are described in the following.
For the following we assume that all name conflicts have been resolved,
i.e., the names of functions and argument variables defined
in the different declarations are pairwise different.
Furthermore, we assume that all $\lambda$-abstractions have
been eliminated by providing a new name (cf.\ Section~\ref{app-higher-order}),
i.e., each $\lambda$-abstraction \pr{(\ttbs$x_1\ldots x_n$->$e$)}
is replaced by the expression \pr{($f~y_1\ldots y_m$)}
together with the new top-level definition
\startprog
$f~x_1\ldots{}x_n~y_1\ldots{}y_m$ = $e$
\stopprog
where $f$ is a new function name and $y_1\ldots y_m$ are the free variables
occurring in $e$ and different from $x_1\ldots x_n$.
Then we perform the following steps
for each rule ``\pr{$l$\,|\,$c$\,=\,$r$~where~$decls$}'':
\begin{description}
\item[Eliminate multiple guards:]~\\
This is done according the meaning described in Section~\ref{sec-bool-guards}.
A rule of the form
\startprog
$f~t_1\ldots{}t_n$ | $b_1$ = $e_1$
\,$\vdots$
\,| $b_k$ = $e_k$
where~$decls$
\stopprog
(the \pr{where} part can also be missing),
where all guards $b_1,\ldots,b_k$ ($k>0$) are expressions of type \pr{Bool},
is transformed into the single rule
\startprog
$f~t_1\ldots{}t_n$ = if $b_1$ then $e_1$ else
\,$\vdots$
\,if $b_k$ then $e_k$ else \mbox{\it{}undefined}
where~$decls$
\stopprog
A rule of the form
\startprog
$f~t_1\ldots{}t_n$ | $c_1$ = $e_1$
\,$\vdots$
\,| $c_k$ = $e_k$
where~$decls$
\stopprog
(the \pr{where} part can also be missing),
where all guards $c_1,\ldots,c_k$ ($k>0$) are constraints,
is transformed into the $k$ rules
\startprog
$f~t_1\ldots{}t_n$ | $c_1$ = $e_1$ where~$decls$
$\vdots$
$f~t_1\ldots{}t_n$ | $c_k$ = $e_k$ where~$decls$
\stopprog
\item[Transform \pr{where} into \pr{let}:]~\\
Each unconditional rule of the form
\startprog
$l$ = $r$ where $decls$
\stopprog
is transformed into
\startprog
$l$ = let $decls$ in $r$ .
\stopprog
Each conditional rule of the form
\startprog
$l$ | $c$ = $r$ where $decls$
\stopprog
is transformed into
\startprog
$l$ = let $decls$ in ($c$|$r$)
\stopprog
where the meaning of the guarded expression \pr{($c$|$r$)}
is explained in Figure~\ref{figure-condrules}.
Note that this transformation is not really necessary
but provides for a unified treatment of the elimination
of local pattern and function declarations in \pr{let} and \pr{where}.
\item[Eliminate local patterns and functions:]~\\
All local pattern and function declarations in a rule
``\pr{$l$\,\,=\,\,let\,\,$decls$\,\,in\,\,$r$}'' are stepwise eliminated
by applying the following transformations as long as possible:\footnote{%
If the right-hand side $r$ has not a \pr{let} declaration with local
patterns or functions at the top,
then these transformations are applied to an outermost \pr{let}
declaration in $r$.}
\begin{description}
\item[Eliminate patterns:]~\\
Select a local pattern declaration which contains only
argument variables from the main function's left-hand side
in the expression, i.e., the rule has the form
\startprog
$l$ = let $decls_1$
$p$ = $e$
$decls_2$
in $r$
\stopprog
with $free(e) \subseteq free(l)$
(it is a programming error if no pattern declaration has this property,
i.e., cyclic pattern definitions are not allowed).
Then transform this rule into the rules
\startprog
$l$ = $f'~x_1\ldots{}x_k~e$
$f'~x_1\ldots{}x_k~p$ = let $decls_1$
\,$decls_2$
\,in $r$
\stopprog
where $x_1\ldots{}x_k$ are all the variables occurring in $l$
and $f'$ is a new function symbol. Repeat this step for $f'$
until all local pattern declarations are eliminated.
\item[Complete local function definitions:]~\\
If a locally declared function $f$ refers in its definition
to a variable $v$ not contained in its argument patterns,
then add the argument $v$ to all occurrences of $f$ (i.e., left-hand
sides and calls). Repeat this step until all locally defined
functions are completed. Note that this completion step must also
be applied to free variables introduced in the same \pr{let}
expression, i.e., the rule
\startprog
f x = let y free
g z = c y z
in g 0
\stopprog
is completed to
\startprog
f x = let y free
g z y = c y z
in g 0 y
\stopprog
\item[Globalize local function definitions:]~\\
If the definitions of all locally declared functions are completed,
i.e., the definitions only refer to variables in the argument
patterns, delete the locally declared functions and
define them at the top-level. For instance, the previous
rule is transformed into the definitions
\startprog
g z y = c y z
f x = let y free in g 0 y
\stopprog
Note that the entire transformation process must be applied again
to the new top-level declarations since they may also contain
local declarations.
\end{description}
\end{description}
After applying these transformation steps to all rules in the program,
we obtain a program where the local declarations contains only
free variables.
\newpage
\addcontentsline{toc}{section}{Bibliography}
\bibliography{mh}
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment