1: \documentclass{tlp}
2:
3: \usepackage{aopmath}
4: \usepackage{latexsym}
5: \usepackage{amssymb}
6:
7: \newtheorem{definition}{Definition} % [section]
8: \newtheorem{example}{Example} % [section]
9:
10: \long\def\comment#1{}
11:
12: %% macros
13: \newcommand{\foo}[1]{#1}
14: \newcommand{\toppos}{\mbox{\footnotesize$\Lambda$}} % top position
15: \newcommand{\nat}{\mbox{$I\!\!N$}}
16: \newcommand{\nil}{[\:]}
17: \newcommand{\ol}[1]{\overline{#1}} % sequence of objects
18: \newcommand{\sleq}{\leqslant}
19: \newcommand{\pr}[1]{\mbox{\tt #1}} % program text in normal text
20: \newcommand{\Control}{\foo{Expr}}
21: \newcommand{\caseof}[1]{\foo{case}\;#1\;\foo{of}\;}
22: \newcommand{\fcaseof}[1]{\foo{fcase}\;#1\;\foo{of}\;}
23: \newcommand{\To}{\Longrightarrow}
24: \newcommand{\Var}{{\cal V}ar} % variables in an object
25:
26: \let\l=\langle
27: \let\r=\rangle
28: \def \tuple#1{\langle #1 \rangle}
29:
30: \newcommand{\sql}{\mbox{$[\![$}}
31: \newcommand{\sqr}{\mbox{$]\!]$}}
32:
33: %% letters
34: \def\defemb#1#2{\expandafter\def\csname #1\endcsname
35: {\relax\ifmmode #2\else\hbox{$#2$}\fi}}
36: \defemb{cC}{{\cal C}} %% constructors
37: \defemb{cE}{{\cal E}} %% expressions
38: \defemb{cF}{{\cal F}} %% functions
39: \defemb{cM}{{\cal M}} %% complexities
40: \defemb{cR}{{\cal R}} %% programs
41: \defemb{cS}{{\cal S}} %% states
42: \defemb{cT}{{\cal T}} %% terms
43: \defemb{cV}{{\cal V}} %% values
44: \defemb{cX}{{\cal X}} %% variables
45:
46: %% environment for typing program texts:
47: \makeatletter
48: \newenvironment{prog}{\vspace{1.0ex}\par
49: \setlength{\parindent}{2ex}
50: \setlength{\parskip}{0.0ex}
51: \obeylines\@vobeyspaces\tt}{\vspace{1.0ex}\noindent
52: }
53: \makeatother
54: \newcommand{\startprog}{\begin{prog}}
55: \newcommand{\stopprog}{\end{prog}\noindent}
56: \newcommand{\ttbs}{\mbox{\tt\char92}}
57: \newcommand{\emptyline}{\vspace{1.0ex}} % an empty line in a program text
58:
59: %\pagestyle{empty}
60:
61: \begin{document}
62: \bibliographystyle{acmtrans}
63:
64: \title[Forward Slicing by Partial Evaluation]
65: {Forward Slicing of Functional Logic Programs\\ by Partial Evaluation\thanks{%
66: A preliminary short version of this paper appeared in the
67: Proceedings of the \emph{12th International Workshop on Logic
68: Based Program
69: Synthesis and Transformation} (LOPSTR 2002).\protect\\
70: This work has been partially supported by the EU (FEDER) and the
71: Spanish MEC under grants TIN2004-00231 and TIN2005-09207-C03-02,
72: and by the ICT for EU-India Cross-Cultural Dissemination Project
73: ALA/95/23/2003/077-054. }}
74:
75: \author[Josep Silva and Germ\'an Vidal]
76: {
77: JOSEP SILVA and GERM\'AN VIDAL\\
78: DSIC, Technical University of Valencia\\
79: Camino de Vera s/n, E-46022 Valencia, Spain\\
80: \email{$\{$jsilva,gvidal$\}$@dsic.upv.es}
81: }
82:
83: \submitted{5 January 2004}
84: \revised{20 February 2005}
85: \accepted{5 January 2006}
86:
87: \maketitle
88:
89: \begin{abstract}
90: Program slicing has been mainly studied in the context of imperative
91: languages, where it has been applied to a wide variety of software
92: engineering tasks, like program understanding, maintenance,
93: debugging, testing, code reuse, etc. This work introduces the first
94: forward slicing technique for declarative multi-paradigm programs
95: which integrate features from functional and logic programming.
96: Basically, given a program and a \emph{slicing criterion} (a
97: function call in our setting), the computed forward slice contains
98: those parts of the original program which are \emph{reachable} from
99: the slicing criterion. Our approach to program slicing is based on
100: an extension of (online) partial evaluation. Therefore, it provides
101: a simple way to develop program slicing tools from existing partial
102: evaluators and helps to clarify the relation between both
103: methodologies. A slicing tool for the multi-paradigm language Curry,
104: which demonstrates the usefulness of our approach, has been
105: implemented in Curry itself.
106: \end{abstract}
107:
108: \begin{keywords}
109: forward slicing, partial evaluation, functional logic programming.
110: \end{keywords}
111:
112: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
113: \section{Introduction}
114:
115: Essentially, program slicing is a method for decomposing programs by
116: analyzing their data and control flow. It was first proposed as a
117: debugging tool to allow a better understanding of the portion of code
118: which revealed an error. Since this concept was originally introduced
119: by Weiser \citeyear{Wei79,Wei84}|in the context of imperative
120: programs|it has been successfully applied to a wide variety of
121: software engineering tasks (e.g., program understanding, maintenance,
122: debugging, merging, testing, code reuse). Surprisingly, there are
123: very few approaches to program slicing in the context of
124: \emph{declarative} programming (see Section~\ref{related}).
125:
126: Roughly speaking, a \emph{program slice} consists of those program
127: statements which are (potentially) related with the values computed at
128: some program point and/or variable, often given by a pair
129: \texttt{(line number, variable)}, referred to as a \emph{slicing
130: criterion}. Program slices are usually computed from a
131: \emph{program dependence graph} \cite{FOW87,KKPLW81} that makes
132: explicit both the data and control dependences for each operation in a
133: program. Program dependences can be traversed backwards and
134: forwards|from the slicing criterion|giving rise to so-called
135: \emph{backward} and \emph{forward} slicing, respectively.
136:
137: \begin{figure}
138: \fbox{
139: \begin{minipage}{91ex}
140: \begin{tabular}{lll}
141: \tt (1) read(n); & \tt (1) read(n); & \tt (1) \\
142: \tt (2) i := 1; & \tt (2) i := 1; & \tt (2) \\
143: \tt (3) sum := 0; & \tt (3) & \tt (3) sum := 0; \\
144: \tt (4) prod := 1; & \tt (4) prod := 1; & \tt (4) \\
145: \tt (5) while i <= n do & \tt (5) while i <= n do & \tt (5) \\
146: \tt (6)\hspace{3ex} sum := sum + i; & \tt (6) & \tt (6)\hspace{3ex} sum := sum + i; \\
147: \tt (7)\hspace{3ex} prod := prod * i;
148: & \tt (7)\hspace{3ex} prod := prod * i; & \tt (7)\\
149: \tt (8)\hspace{3ex} i := i + 1; & \tt (8)\hspace{3ex} i := i + 1;
150: & \tt (8) \\
151: \tt (9) write(sum); & \tt (9) & \tt (9) write(sum); \\
152: \tt (10)write(prod); & \tt (10)write(prod); & \tt (10) \\[2ex]
153: \hspace{8ex}(a) & \hspace{8ex}(b) & \hspace{8ex}(c) \\
154: \end{tabular}
155: \end{minipage}}
156: \caption{Forward and backward slicing ---an example} \label{fbslice}
157: \end{figure}
158:
159: Essentially, a backward slice consists of the parts of the program
160: that (potentially) affect the values computed at the slicing
161: criterion. In contrast, a forward slice consists of the statements
162: which are dependent on the slicing criterion, a statement being
163: \emph{dependent} on the slicing criterion if the values computed at
164: that statement depend on the values computed at the slicing criterion
165: or if the values computed at the slicing criterion determine if the
166: statement under consideration is executed \cite{Tip95}. Consider,
167: e.g., the example \cite{Tip95} depicted in Fig.~\ref{fbslice}~(a) for
168: computing the sum and the product of the sequence of numbers
169: \texttt{1,2,\ldots,n}. Fig.~\ref{fbslice}~(b) shows a backward slice
170: of the program w.r.t.\ the slicing criterion \texttt{(10,prod)} while
171: Fig.~\ref{fbslice}~(c) shows a forward slice w.r.t.\ the slicing
172: criterion \texttt{(3,sum)}.
173:
174: Additionally, slices can be \emph{dynamic} or \emph{static}, depending
175: on whether a concrete program's input is provided or not. \emph{Quasi}
176: static slicing was the first attempt to define a hybrid method ranging
177: between static and dynamic slicing \cite{Ven91}. It becomes useful
178: when only the value of some parameters is known. This notion is
179: closely related to partial evaluation \cite{JGS93}, a well-known
180: technique to specialize programs w.r.t.\ part of their input data.
181: For instance, quasi static slicing has been applied to program
182: understanding by Harman et al.\ \citeyear{HDS95}; similarly, Blazy and
183: Facon \citeyear{BF98} use partial evaluation for the same purpose.
184:
185: All approaches to slicing mentioned so far are \emph{syntax
186: preserving}, i.e., they are mainly obtained from the original
187: program by statement deletion. In contrast, \emph{amorphous} slicing
188: \cite{HD97} exploits different program transformations in order to
189: simplify the program while preserving its semantics w.r.t.\ the
190: slicing criterion. From this perspective, partial evaluation could
191: straightforwardly be seen as an amorphous slicing technique.
192: %
193: More detailed information on program slicing can be found in the
194: surveys of Harman and Hierons \citeyear{HH01} and Tip
195: \citeyear{Tip95}.
196:
197: The aim of this work is the definition of a forward slicing technique
198: for a multi-paradigm declarative language which integrates features
199: from functional and logic programming, like, e.g., Curry
200: \cite{CurryTR} or Toy \cite{LS99}. Similarly to in \cite{RT96}, where
201: a first-order functional language is considered, given a program $p$
202: and a projection function $\pi$, backward slicing should extract a
203: program that behaves like $\pi(p)$ (e.g., by symbolically pushing
204: $\pi$ backwards through the body of $p$). For instance, it can be used
205: to extract a program slice for computing the number of lines in a
206: string from a more general program that returns a tuple with both the
207: number of lines and the number of characters of the string; this is
208: the example that illustrates the backward slicing technique of Reps
209: and Turnidge \citeyear{RT96}. Such a slicing technique is considered
210: \emph{backward} because the algorithm proceeds from (part of) the
211: result backwards to the initial function call, i.e., in the inverse
212: direction of the standard operational semantics. In contrast, here we
213: consider the definition of a forward slicing technique that, given a
214: program and a function call, extracts a program containing all the
215: statements which are \emph{reachable} from the slicing criterion. Our
216: slicing technique is considered \emph{forward} because it proceeds
217: from a given function call to its result, i.e., we follow the control
218: flow of the standard operational semantics.
219:
220: Furthermore, rather than defining a new technique from scratch, we
221: exploit the similarities between slicing and \emph{partial evaluation}
222: \cite{JGS93}. Since a partial evaluator for the considered language
223: already exists, our approach provides a simple way to develop a
224: program slicing tool. The main purpose of partial evaluation is to
225: specialize a program w.r.t.\ part of its input data and, hence, it is
226: also known as \emph{program specialization}. The partially evaluated
227: program will be (hopefully) executed more efficiently since those
228: computations that depend only on the known data are performed|at
229: partial evaluation time|once and for all. Many (\emph{online})
230: partial evaluation schemes follow a common pattern: given a program
231: and a function call (possibly containing partial data structures by
232: means of free variables), the partial evaluator builds a \emph{finite}
233: representation|generally a graph|of the possible executions of the
234: initial call and, then, systematically extracts a \emph{residual}
235: program|the partially evaluated program|from this graph.
236:
237: The essence of our approach can be summarized as follows. First, we
238: consider that, in our functional logic context, a function
239: call|possibly containing free variables|may also play the role of
240: \emph{slicing criterion}. Since such a call may have an infinite
241: computation space, a primary task of both slicing and partial
242: evaluation is the construction of a finite representation of its
243: possible program executions. Here, the same algorithm which is used in
244: partial evaluation can be applied for computing this finite
245: representation, which will be later used to identify the program
246: statements that are reachable from the slicing criterion. Then, we
247: only need to replace the construction of a residual program in partial
248: evaluation by a simpler post-processing stage that extracts an
249: executable program which includes the reachable program statements.
250:
251: While partial evaluation usually achieves its effects by compressing
252: paths in the graph and by renaming expressions in order to remove
253: unnecessary function symbols,
254: slicing should preserve the structure of the original program (here,
255: we do not consider amorphous slicing): statements can be|totally or
256: partially|deleted but no new statements can be introduced. In order to
257: further clarify the relation between partial evaluation and slicing,
258: let us recall the following classification of partial evaluators
259: introduced by Gl\"uck and S{\o}rensen \citeyear{GS96}. According to
260: this classification, a partial evaluator is
261: \begin{itemize}
262: \item \emph{Monovariant}: if each function of the original program
263: gives rise to (at most) one residual function;
264: \item \emph{Polyvariant}: if each function of the original program may
265: give rise to one or more residual functions;
266: \item \emph{Monogenetic}: if each residual function stems from one
267: function of the original program;
268: \item \emph{Polygenetic}: if each residual function may stem from one
269: or more functions of the original program.
270: \end{itemize}
271: %
272: The main contribution of this work is to demonstrate that a forward
273: slicing technique for functional logic programs can be obtained by
274: slightly extending a \emph{monovariant} and \emph{monogenetic} partial
275: evaluation scheme.
276: %%
277: Unfortunately, this kind of monovariant/monogenetic partial evaluation
278: could be rather imprecise, thus resulting in unnecessarily large
279: residual programs (i.e., slices). In order to overcome this drawback,
280: we consider the definition of an extended operational semantics to
281: perform partial evaluations, which helps us to preserve as much
282: information as possible while maintaining the monovariant/monogenetic
283: nature of the process.
284:
285: The main contributions of this work can be summarized as follows:
286: \begin{itemize}
287: \item We define the first forward slicing technique for functional
288: logic programs. Furthermore, the application of our developments to
289: (first-order) lazy functional programs would be straightforward,
290: since either the syntax and the underlying (online) partial
291: evaluators---e.g., positive supercompilation \cite{SGJ93}---share
292: many similarities.
293:
294: \item We do not need to consider separately static and dynamic
295: slicing, since the underlying partial evaluation scheme naturally
296: accepts partial input data.
297:
298: \item Our method is defined in terms of an existing partial evaluation
299: scheme and, thus, it is easy to implement by adapting current
300: partial evaluators.
301:
302: \item Finally, our approach helps to clarify the relation between
303: forward slicing and (online) partial evaluation.
304: \end{itemize}
305: %
306: This paper is organized as follows. In the next section we recall some
307: foundations for understanding the subsequent developments.
308: Section~\ref{pe} introduces a notion of forward slicing in the context
309: of functional logic programming. We then recall, in Section~\ref{pe1},
310: the narrowing-driven approach to partial evaluation.
311: Section~\ref{depen} defines an algorithm for computing program
312: dependences by partial evaluation, while Section~\ref{extract} uses
313: these dependences to extract program slices.
314: Section~\ref{exp} presents a prototype implementation of the program
315: slicing tool and show some selected experiments. Several related
316: works are discussed in Section~\ref{related} before we conclude in
317: Section~\ref{sec-concl}. Proofs of technical results can be found in
318: \ref{proofs}.
319:
320:
321: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
322: \section{Foundations}
323: \label{sec-foundations}
324:
325: We recall in this section some basic notions of term rewriting
326: \cite{BN98,Klo91,Ter03} and functional logic programming
327: \cite{Han94JLP}.
328:
329: \subsection{Preliminaries}
330:
331: Throughout this paper, we consider a (\emph{many-sorted})
332: \emph{signature} $\Sigma$ partitioned into a set $\cC$ of
333: \emph{constructors} and a set $\cF$ of (defined) \emph{functions} or
334: \emph{operations}. We write $c/n \in \cC$ and $f/n \in \cF$ for
335: $n$-ary constructor and operation symbols, respectively. There is at
336: least one sort $Bool$ containing the constructors \pr{True} and
337: \pr{False}. The set of \emph{terms} and \emph{constructor terms} with
338: \emph{variables} (e.g., $x,y,z$) from $\cX$ are denoted by $\cT(\cC
339: \cup \cF,\cX)$ and $\cT(\cC,\cX)$, respectively. A term is
340: \emph{linear} if it does not contain multiple occurrences of one
341: variable. The set of variables occurring in a term $t$ is denoted by
342: $\Var(t)$. A term $t$ is \emph{ground} if $\Var(t) = \emptyset$.
343:
344: A \emph{pattern} is a term of the form $f(d_{1},\ldots,d_{n})$ where
345: $f/n \in \cF$ and $d_1,\ldots,d_n \in \cT(\cC,\cX)$. A term is
346: \emph{operation-rooted} (constructor-rooted) if it has an operation
347: (constructor) symbol at the root. A \emph{position} $p$ in a term $t$
348: is represented by a sequence of natural numbers ($\toppos$ denotes the
349: empty sequence, i.e., the root position). $t|_p$ denotes the
350: \emph{subterm} of $t$ at position $p$, and $t[s]_p$ denotes the result
351: of \emph{replacing the subterm} $t|_p$ by the term $s$. We denote a
352: \emph{substitution} $\sigma$ by $\{x_1 \mapsto t_1,\ldots, x_n \mapsto
353: t_n\}$ where $\sigma(x_i) = t_i$ for $i=1,\ldots,n$ (with $x_{i}\neq
354: x_{j}$ if $i\neq j$), and $\sigma(x) = x$ for all other variables $x$.
355: A substitution $\sigma$ is \emph{constructor}, if $\sigma(x)$ is a
356: constructor term for all $x$. The identity substitution is denoted by
357: $id$. A substitution $\theta$ is more general than $\sigma$, in
358: symbols $\theta \leq \sigma$, iff there exists a substitution $\gamma$
359: such that $\gamma\circ\theta = \sigma$ (``$\circ$'' denotes the
360: composition operator). Term $t'$ is a (constructor) \emph{instance}
361: of term $t$ if there is a (constructor) substitution $\sigma$ with $t'
362: = \sigma(t)$.
363:
364: A set of rewrite rules (or oriented equations) $l = r$ such that $l
365: \not\in \cX$, and $\Var(r)\subseteq\Var(l)$ is called a \emph{term
366: rewriting system} (TRS). Terms $l$ and $r$ are called the
367: \emph{left-hand side} and the \emph{right-hand side} of the rule,
368: respectively. A TRS $\cR$ is \emph{left-linear} if $l$ is linear for
369: all $l = r\in\cR$. A TRS is \emph{constructor-based} if each
370: left-hand side $l$ is a pattern. In the following, a functional logic
371: \emph{program} is a left-linear constructor-based TRS.
372: %
373: A \emph{rewrite step} is an application of a rewrite rule to a term,
374: i.e., $t \to_{p,R} s$ if there exists a position $p$ in $t$, a rewrite
375: rule $R= (l = r)$ and a substitution $\sigma$ with $t|_p = \sigma(l)$
376: and $s = t[\sigma(r)]_p$. The instantiated left-hand side $\sigma(l)$
377: of a rule $l = r$ is called a \emph{redex} (\emph{red}ucible
378: \emph{ex}pression). Given a relation $\to$, we denote by $\to^\ast$
379: its transitive and reflexive closure.
380:
381: \begin{example} \label{ex1}
382: Consider the following TRS that defines the addition on natural
383: numbers represented by terms built from \pr{Zero} and
384: \pr{Succ}:\footnote{In the examples, we write constructor symbols
385: starting with upper case (except for the list constructors,
386: ``\pr{$\nil$}'' and ``\pr{:}'', which are a shorthand for \pr{Nil}
387: and \pr{Cons}, respectively).}
388: \[
389: \begin{array}{r@{~~=~~}l@{~~~~}l}
390: \tt Zero + y & \tt y & \tt (R_1) \\
391: \tt Succ(x) + y & \tt Succ(x+y) & \tt (R_2) \\
392: \end{array}
393: \]
394: Given the term $\tt Succ(Zero)+Succ(Zero)$, we have the following
395: sequence of rewrite steps:
396: \[
397: \begin{array}{lll}
398: \tt Succ(Zero)+Succ(Zero) & \tt \to_{\toppos,R_2} & \tt Succ(Zero + Succ(Zero) \\
399: & \tt \to_{1,R_1} & \tt Succ(Succ(Zero))
400: \end{array}
401: \]
402: \end{example}
403:
404:
405: \subsection{Narrowing}
406:
407: Functional \emph{logic} programs mainly differ from purely functional
408: programs in that function calls may contain \emph{free} variables. In
409: order to evaluate terms containing free variables, \emph{narrowing}
410: non-deterministically instantiates these variables so that a rewrite
411: step is possible. Formally, $t \leadsto_{(p,R,\sigma)} t'$ is a
412: \emph{narrowing step} if $p$ is a non-variable position of $t$ and
413: $\sigma(t) \to_{p,R} t'$. We often write $t \leadsto_{\sigma} t'$
414: when the position and the rule are clear from the context. We denote
415: by $t_0 \leadsto^{n}_\sigma t_n$ a sequence of $n$ narrowing steps
416: $t_0 \leadsto_{\sigma_1} \ldots \leadsto_{\sigma_n} t_n$ with $\sigma
417: = \sigma_n \circ \cdots \circ \sigma_1$ (if $n = 0$ then $\sigma =
418: id$), usually restricted to the variables of $t_0$.
419: %
420: Due to the presence of free variables, a term may be reduced to
421: different values after instantiating these variables to different
422: terms. Given a narrowing derivation $t_0 \leadsto^{\ast}_\sigma t_n$,
423: we say that $t_{n}$ is a computed \emph{value} and $\sigma$ is a
424: computed \emph{answer} for $t_{0}$.
425:
426: \begin{example}
427: Consider again the definition of function ``\pr{+}'' in
428: Example~\ref{ex1}. Given the term $\tt x+Succ(Zero)$, narrowing
429: non-deterministically performs the following derivations:
430: \[
431: \begin{array}{lll}
432: \tt x + Succ(Zero) & \tt \leadsto_{\toppos,R_1,\{x \mapsto Zero\}}
433: & \tt Succ(Zero) \\[1ex]
434: \tt x + Succ(Zero) & \tt \leadsto_{\toppos,R_2,\{x \mapsto Succ(y_1)\}}
435: & \tt Succ(y_1 + Succ(Zero)) \\
436: & \tt \leadsto_{1,R_1,\{y_1 \mapsto Zero \}} & \tt Succ(Succ(Zero))\\[1ex]
437: \tt x + Succ(Zero) & \tt \leadsto_{\toppos,R_2,\{x \mapsto Succ(y_1)\}}
438: & \tt Succ(y_1 + Succ(Zero)) \\
439: & \tt \leadsto_{1,R_2,\{y_1 \mapsto Succ(y_2) \}}
440: & \tt Succ(Succ(y_2 + Succ(Zero)))\\
441: & \tt \leadsto_{1.1,R_1,\{y_2 \mapsto Zero\}}
442: & \tt Succ(Succ(Succ(Zero))) \\
443: \tt \ldots
444: \end{array}
445: \]
446: Therefore, $\tt x + Succ(Zero)$ non-deterministically computes the
447: values
448: \begin{itemize}
449: \item $\tt Succ(Zero)$ with answer $\tt \{x \mapsto Zero\}$,
450: \item $\tt Succ(Succ(Zero))$ with answer $\tt \{ x \mapsto
451: Succ(Zero)\}$,
452: \item $\tt Succ(Succ(Succ(Zero)))$ with answer $\tt \{ x \mapsto
453: Succ(Succ(Succ(Zero)))\}$, etc.
454: \end{itemize}
455: \end{example}
456: %
457: As in logic programming, narrowing derivations can be represented by a
458: (possibly infinite) finitely branching \emph{tree}. Formally, given a
459: program $\cR$ and an operation-rooted term $t$, a \emph{narrowing
460: tree} for $t$ in $\cR$ is a tree satisfying the following
461: conditions: (a) each node of the tree is a term, (b) the root node is
462: $t$, (c) if $s$ is a node of the tree then, for each narrowing step $s
463: \leadsto_{p,R,\sigma} s'$, the node has a child $s'$ and the
464: corresponding arc is labeled with $(p,R,\sigma)$, and (d) nodes which
465: are constructor terms have no children.
466:
467: In order to avoid unnecessary computations and to deal with infinite
468: data structures, demand-driven generation of the search space has been
469: advocated by a number \emph{lazy} narrowing strategies
470: \cite{GLMP91,LLR93,MR92}. Due to its optimality properties w.r.t.\ the
471: length of derivations and the number of computed solutions,
472: \emph{needed narrowing} \cite{AEH00} is currently the best lazy
473: narrowing strategy.
474:
475: \subsection{Needed Narrowing}
476:
477: Needed narrowing \cite{AEH00} is defined on \emph{inductively
478: sequential} TRSs \cite{Ant92}, a subclass of left-linear
479: constructor-based TRSs. Essentially, a TRS is \emph{inductively
480: sequential} when all its operations are defined by rewrite rules
481: that, recursively, make on their arguments a case distinction
482: analogous to a data type (or structural) induction. Inductive
483: sequentiality is not a limiting condition for programming. In fact,
484: the first-order components of many functional (logic) programs written
485: in, e.g., Haskell, ML or Curry, are inductively sequential.
486:
487: We say that $s \leadsto_{p,R,\sigma} t$ is a \emph{needed narrowing
488: step} iff $\sigma(s) \to_{p,R} t$ is a \emph{needed rewrite} step in
489: the sense of Huet and L\'evy \citeyear{HL92}, i.e., in every
490: computation from $\sigma(s)$ to a normal form, either $\sigma(s)|_p$
491: or one of its \emph{descendants} must be reduced. Here, we are
492: interested in a particular needed narrowing strategy, denoted by
493: $\lambda$ in \cite[Def.\ 13]{AEH00} which is based on the notion of a
494: \emph{definitional tree} \cite{Ant92}, a hierarchical structure
495: containing the rules of a function definition, which is used to guide
496: the needed narrowing steps. This strategy is basically equivalent to
497: \emph{lazy narrowing} \cite{MR92} where narrowing steps are applied to
498: the outermost function, if possible, and inner functions are only
499: narrowed if their evaluation is \emph{demanded} by a constructor
500: symbol in the left-hand side of some rule (i.e., a typical outermost
501: strategy).
502:
503: \begin{example} \label{ex-leq}
504: Consider following rules which define the less-or-equal function on
505: natural numbers:
506: \[
507: \begin{array}{r@{~\sleq~}l@{~~=~~}l}
508: \tt Zero & \tt y & \tt True \\
509: \tt Succ(x) & \tt Zero & \tt False \\
510: \tt Succ(x) & \tt Succ(y) & \tt x \;\sleq\; y
511: \end{array}
512: \]
513: In a term like $t_1 \sleq t_2$, it is always necessary to evaluate
514: $t_1$ to some \emph{head normal form} (i.e., a variable or a
515: constructor-rooted term) since all three rules defining ``$\sleq$''
516: have a non-variable first argument. On the other hand, the
517: evaluation of $t_2$ is only \emph{needed} if $t_1$ is of the form
518: \pr{Succ($t$)}. Thus, if $t_1$ is a free variable, needed narrowing
519: instantiates it to a constructor, here \pr{Zero} or \pr{Succ(x)}.
520: Depending on this instantiation, either the first rule is applied or
521: the second argument $t_2$ is evaluated.
522: \end{example}
523: %
524:
525:
526: \subsection{Declarative Multi-Paradigm Languages}
527:
528: Functional logic languages have recently evolved to so called
529: declarative \emph{multi-paradigm} languages like, e.g., Curry
530: \cite{CurryTR}, Toy \cite{HU01} and Escher \cite{Llo94}. In order to
531: make things concrete, we consider in this work the language Curry, a
532: modern multi-paradigm language which integrates features from logic
533: programming (partial data structures, built-in search), functional
534: programming (higher-order functions, demand-driven evaluation) and
535: concurrent programming (concurrent evaluation of constraints with
536: synchronization on logical variables). Curry follows a Haskell-like
537: syntax, i.e., variables and function names start with lowercase
538: letters and data constructors start with an uppercase letter. The
539: application of function $f$ to an argument $e$ is denoted by
540: juxtaposition, i.e., $(f\;e)$.
541:
542: The basic operational semantics of Curry is based on a combination of
543: needed narrowing and residuation \cite{Han97b}. The
544: \emph{residuation} principle is based on the idea of delaying function
545: calls until they are ready for a deterministic evaluation.
546: Residuation preserves the deterministic nature of functions and
547: naturally supports concurrent computations. The precise
548: mechanism---narrowing or residuation---for each function is specified
549: by \emph{evaluation annotations}. The annotation of a function as
550: \emph{rigid} forces the delayed evaluation by rewriting, while
551: functions annotated as \emph{flexible} can be evaluated in a
552: non-deterministic manner by narrowing.
553:
554:
555: In actual implementations, e.g., the PAKCS environment \cite{PAKCS00}
556: for Curry, programs may also include a number of additional features:
557: calls to external (built-in) functions, concurrent constraints,
558: higher-order functions, overlapping left-hand sides, guarded
559: expressions, etc. In order to ease the compilation of programs as well
560: as to provide a common interface for connecting different tools
561: working on source programs, a \emph{flat representation} for programs
562: has recently been introduced. This representation is based on the
563: formulation of Hanus and Prehofer \citeyear{HP99} to express
564: pattern-matching by case expressions. The complete flat
565: representation is called FlatCurry \cite{PAKCS00} and is used as an
566: intermediate language during the compilation of source programs.
567:
568: In order to simplify the presentation, we will only consider the
569: \emph{core} of the flat representation. Extending the developments in
570: this work to the remaining features is not difficult and, indeed, the
571: implementation reported in Section~\ref{exp} covers many of these
572: features. The syntax of flat programs is summarized in
573: Fig.~\ref{flat}, where $\ol{o_n}$ stands for the \emph{sequence} of
574: objects $o_1,\ldots,o_n$.
575: %
576: \begin{figure}[t]
577: \rule{\linewidth}{.01in}
578: \[
579: \hspace{-5ex}
580: \begin{array}{lcl@{~~}l@{~~~~}lcl@{~~}l}
581: \cR & ::= & D_1 \ldots D_m & \mbox{ (program) }
582: & t & ::= & x & \mbox{ (variable) } \\
583: D & ::= & f(\ol{x_{n}}) = e & \mbox{ (rule) }
584: & & | & c(\ol{t_{n}}) & \mbox{ (constructor call) } \\
585: e & ::= & t & \mbox{ (term) }
586: & & | & f(\ol{t_{n}}) & \mbox{ (function call) } \\
587: & | & \caseof{x} \{\ol{p_{m}\to e_{m}}\} & \mbox{ (rigid case) }
588: & p & ::= & c(\ol{x_{n}}) & \mbox{ (flat pattern) } \\
589: & | & \fcaseof{x} \{\ol{p_{m}\to e_{m}}\} & \mbox{ (flexible case) } \\
590: \end{array}
591: \]
592: \rule{\linewidth}{.01in}
593: \caption{Syntax of Flat Programs}
594: \label{flat}
595: \end{figure}
596: %
597: We consider the following domains:
598: \[
599: \begin{array}{l@{~~}l@{~~}l@{~~~}l@{~~~}l@{~~}l@{~~}l@{~~~}l}
600: x,y,z & \in & \cX & \mbox{\sf (variables)} &
601: a,b,c & \in & \cC & \mbox{\sf (constructor symbols)} \\
602: f,g,h & \in & \cF & \mbox{\sf (defined functions)} &
603: e_{1},e_{2},\ldots & \in & \cE & \mbox{\sf (expressions)} \\
604: t_{1},t_{2},\ldots & \in & \cT & \mbox{\sf (terms)} &
605: v_{1},v_{2},\ldots & \in & \cV & \mbox{\sf (values)}
606: \end{array}
607: \]
608: The only difference between \emph{terms} and \emph{expressions} is
609: that the latter may contain case expressions.
610: \emph{Values} are terms in head normal form, i.e., variables or
611: constructor-rooted terms. A program $\cR$ consists of a sequence of
612: function definitions; each function is defined by a single rule whose
613: left-hand side contains only different variables as parameters. The
614: right-hand side is an expression $e$ composed by variables,
615: constructors, function calls, and case expressions for
616: pattern-matching. The general form of a case expression is:\footnote{
617: We write $\foo{(f)case}$ for either $\foo{fcase}$ or $\foo{case}$.}
618: \[
619: \foo{(f)case}\;x\;\foo{of}\;\{c_1(\ol{x_{n_1}}) \to
620: e_1;\ldots;c_m(\ol{x_{n_m}}) \to e_m\}
621: \]
622: where $x$ is a variable, $c_1,\ldots,c_m$ are different constructors
623: of the type of $x$, and $e_1,\ldots, e_m$ are expressions (possibly
624: containing nested $\foo{(f)case}$'s). The variables $\ol{x_{n_i}}$
625: are local variables which occur only in the corresponding
626: subexpression $e_i$. The difference between $\foo{case}$ and
627: $\foo{fcase}$ only shows up when the argument, $x$, is a free
628: variable (within a particular computation): $\foo{case}$
629: suspends---which corresponds to \emph{residuation}, i.e., pure
630: functional reduction---whereas $\foo{fcase}$ nondeterministically
631: binds this variable to a pattern in a branch of the case
632: expression---which corresponds to either narrowing \cite{AEH00} and
633: driving \cite{Tur86b}. Note that our functional logic language mainly
634: differs from typical (lazy) functional languages in the presence of
635: flexible case expressions.
636:
637: \begin{example} \label{app-ex}
638: Consider again the rules defining functions ``\pr{$+$}''
639: (Example~\ref{ex1}) and ``\pr{$\sleq$}'' (Example~\ref{ex-leq}).
640: These functions can be defined in the flat representation as
641: follows:\footnote{ Although we consider in this work a first-order
642: representation---the flat language---we use a curried notation in
643: concrete examples (as in Curry). }
644: \startprog
645: x $+$ y = fcase x of $\{$ Zero $\to$ y;
646: $\:$Succ n $\to$ Succ (n $+$ y) $\}$\\[-1ex]
647:
648: x $\sleq$ y = fcase x of $\{$ Zero $\to$ True;
649: $\:$Succ n $\to$ fcase y of $\{$ Zero $\to$ False;
650: $\:$Succ m $\to$ n $\sleq$ m $\}$ $\}$
651: \stopprog
652: \end{example}
653: %
654: An automatic transformation from source (inductively sequential)
655: programs to flat programs has been introduced by Hanus and Prehofer
656: \citeyear{HP99}. Translated programs always fulfill the following
657: restrictions: case expressions in the right-hand sides of program
658: rules appear always in the outermost positions (i.e., there is no case
659: expression inside a function or constructor call) and all case
660: arguments are variables, thus the syntax of Fig.~\ref{flat} is general
661: enough for our purposes. We shall assume these restrictions on flat
662: programs in the following.
663:
664: The operational semantics of flat programs is shown in
665: Fig.~\ref{standard-lnt}. It is based on the LNT---for Lazy Narrowing
666: with definitional Trees---calculus of Hanus and Prehofer
667: \citeyear{HP99}. The one-step transition relation $\To_\sigma$ is
668: labeled with the substitution $\sigma$ computed in the step. Let us
669: briefly describe the LNT rules:
670:
671: The {\sf select} rule selects the appropriate branch of a case
672: expression and continues with the evaluation of this branch. This
673: rule implements \emph{pattern matching}.
674:
675: \begin{figure}[t]
676: \centering\small
677: \rule{\linewidth}{.01in}
678: \[
679: \mbox{}\hspace{-5ex}\begin{array}{l@{~~~~~}rcl}
680: \mbox{\sf (select)} & \foo{(f)case}\;c(\ol{t_n})\;of\;\{\ol{p_m \to
681: e_m}\} & \To_{\id} & \sigma(e_i) \\
682: & \multicolumn{3}{r}{\mbox{if $p_i = c(\ol{x_n})$, $c\in \cC$,
683: and $\sigma = \{\ol{x_n \mapsto t_n}\}$}}\\[1ex]
684: \mbox{\sf (guess)} & \foo{fcase}\;x\;of\;\{\ol{p_m \to e_m}\}
685: & \To_{\sigma} & \sigma(e_i) \\
686: & \multicolumn{3}{r}{\mbox{if $\sigma = \{x \mapsto p_i\}$
687: and $i \in \{1,\ldots,m\}$}}\\[1ex]
688: \mbox{\sf (case eval)} & \foo{(f)case}\;e\;of\;\{\ol{p_m \to e_m}\}
689: & \To_\sigma & \sigma((f)case\;e'\;of\;\{\ol{p_m \to e_m}\}) \\
690: & \multicolumn{3}{r}{\mbox{if $e$ is not in head normal form and $e \To_{\sigma} e'$}}\\[1ex]
691: \mbox{\sf (fun)} & f(\ol{t_n}) & \To_{\id} & \sigma(e) \\
692: & \multicolumn{3}{r}{\mbox{if $f(\ol{x_n}) = e \in \cR$
693: and $\sigma = \{\ol{x_n \mapsto t_n}\}$}}
694: \end{array}
695: \]
696: \rule{\linewidth}{.01in}
697: \caption{Standard Operational Semantics (LNT calculus)}
698: \label{standard-lnt}
699: \end{figure}
700:
701: The {\sf guess} rule applies when the argument of a \emph{flexible}
702: case expression is a variable. Then, this rule non-deterministically
703: binds this variable to a pattern in a branch of the case expression.
704: The step is labeled with the computed binding. Observe that there is
705: no rule to evaluate a rigid case expression with a variable argument.
706: This situation produces a \emph{suspension} of the evaluation.
707:
708: The {\sf case eval} rule can be applied when the argument of the case
709: construct is not in head normal form (i.e., it is either a function
710: call or another case construct). Then, it tries to evaluate this
711: expression recursively.
712:
713: Finally, the {\sf fun} rule performs the unfolding of a function call.
714: As in proof procedures for logic programming, we assume that we take a
715: program rule with fresh variables in each such evaluation step.
716:
717: Note that there is no rule to evaluate terms in head normal form; in
718: this case, the computation stops \emph{successfully}. An LNT
719: \emph{derivation} is denoted by $e_0 \To^\ast_\sigma e_n$, which is a
720: shorthand for the sequence $e_0 \To_{\sigma_1} \ldots \To_{\sigma_n}
721: e_n$ with $\sigma = \sigma_n \circ \cdots \circ \sigma_1$ (if $n=0$
722: then $\sigma = id$). An LNT derivation $e \To^\ast_\sigma e'$ is
723: \emph{successful} when $e'$ is in head normal form. Then, we say that
724: $e$ \emph{evaluates} to $e'$ with \emph{computed answer} $\sigma$.
725:
726: \begin{example} \label{app-der}
727: Consider the function ``\pr{$\sleq$}'' of Example~\ref{app-ex}.
728: Given the initial call ``\pr{(Succ x) $\sleq$ y}'', the LNT calculus
729: computes, among others, the following successful derivation:\\[1ex]
730: $
731: \begin{array}{l}
732: \tt (Succ\;x) \;\sleq\; y \\
733: \begin{array}{llr}
734: \To_{id} & \tt \!\!fcase\;(Succ\;x)\;of\; & ({\sf fun})\\
735: & \begin{array}{lll}
736: \tt \{ Z & \!\!\!\!\to\!\!\!\! & \tt True; \\
737: \tt (Succ\;n) & \!\!\!\!\to\!\!\!\! & \tt fcase\;y\;of\;\{ Z \to False;\;(Succ\;m) \to n \sleq m \}\}
738: \end{array}\\
739: \To_{id} & \tt \!\!fcase\;y\;of\;\{ Z \to \tt False;\; (Succ\;m) \to \tt x \sleq m \}& ({\sf select})\\
740: \To_{\tt \{y \mapsto Z\}} & \tt \!\!False & ({\sf guess})\\
741: \end{array}
742: \end{array}
743: $\\[1ex]
744: Therefore, \pr{(Succ x) $\sleq$ y} evaluates to \pr{False} with
745: computed answer \pr{$\{$y $\mapsto$ Z$\}$}.
746: \end{example}
747:
748:
749: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
750: \section{Forward Slicing}
751: \label{pe}
752:
753: In this section, we formalize our notion of \emph{forward slice} in
754: the context of functional logic programs. As mentioned before, in our
755: setting any function call may play the role of \emph{slicing
756: criterion}. Essentially, given a program $\cR$ and a (partially
757: instantiated) call $t$|the slicing criterion|an associated forward
758: slice is a \emph{fragment} of $\cR$ which contains all the statements
759: which are necessary for executing the call $t$, i.e., which are
760: \emph{needed} to evaluate the slicing criterion. This relation between
761: neededness|in the sense of Huet and L\'evy \citeyear{HL92}|and slicing
762: is not new; indeed, there exist several approaches to slicing of
763: functional programs which rely on the computation of neededness
764: information \cite{Bis97,FT98}. Clearly, $t$ must compute the same
765: value in $\cR$ and in the computed slice. In particular, the original
766: program is always a correct slice w.r.t.\ any slicing criterion. Our
767: aim is thus to find smaller slices.\footnote{Weiser proved that
768: computing the \emph{minimal} slice is generally undecidable
769: \cite{Wei84}.} Furthermore, we do not distinguish between dynamic
770: and static slicing, since it only depends on the degree of
771: instantiation of the slicing criterion; in order words, we consider a
772: sort of quasi static slicing \cite{Ven91}.
773:
774: As mentioned before, we do not consider the construction of amorphous
775: slices;
776: otherwise, partial evaluation could straightforwardly be seen as a
777: slicing technique. Here, we only allow the deletion of some elements
778: of the original program:
779: \begin{description}
780: \item[\sf Term deletion:] This is the simplest kind of deletion. It
781: consists of the removal of subterms which are not needed to perform
782: computations with the slicing criterion.
783:
784: \item[\sf Branch deletion:] By using the partially known data in the
785: slicing criterion, some case branches become useless and can be
786: deleted.
787:
788: \item[\sf Function deletion:] Finally, those functions which are not
789: necessary to evaluate the slicing criterion can be completely
790: deleted from the slice.
791: \end{description}
792: %
793: Analogously to Schoening and Ducass\'e \citeyear{SD96}, our notion of
794: \emph{program slice} is formalized in terms of an abstraction
795: relation. In the following, we consider that program signatures are
796: implicitly augmented with the 0-ary constructor $\top$, a special
797: symbol which is used to denote that some code fragment is missing.
798:
799: \begin{definition}[term abstraction]
800: A term $t'$ is an abstraction of term $t$, in symbols $t' \succeq
801: t$, iff $t' = \top$ or $t' = t$.
802: \end{definition}
803: %
804:
805: \begin{definition}[expression abstraction]
806: An expression $e'$ is an abstraction of an expression $e$, in
807: symbols $e' \succeq e$, iff one of the following conditions holds:
808: \begin{itemize}
809: \item $e' = \top$ (i.e., a case structure is completely deleted);
810: \item $e' = e$;
811: \item $e' = \foo{(f)case}\;x\;\foo{of}\;\{\ol{p'_n \to
812: e'_n}\}$, $e = \foo{(f)case}\;x\;\foo{of}\;\{\ol{p_n \to
813: e_n}\}$, and $e'_i \succeq e_i$ for all $i = 1,\ldots,n$.
814: \end{itemize}
815: \end{definition}
816:
817: \begin{definition}[program slice] \label{prog-abs}
818: A program $\cR' = (D'_1,\ldots,D'_m)$ is a slice of a program $\cR =
819: (D_1,\ldots,D_m)$, in symbols $\cR' \succeq \cR$, iff for all $i =
820: 1,\ldots,m$, $D'_i = (f(\ol{x_n}) = e')$, $D_i = (f(\ol{x_n}) = e)$,
821: and $e' \succeq e$.
822: \end{definition}
823: %
824: Roughly speaking, a program $\cR'$ is a slice of program $\cR$ if it
825: can be obtained by replacing some subterms, case branches, and
826: right-hand sides of function definitions by $\top$. Trivially, program
827: slices are steadily executable (and fulfill the syntax of
828: Fig.~\ref{flat}) by just considering $\top$ as an arbitrary constant
829: of the program's signature. The interest in producing
830: \emph{executable} slices comes from the fact that it facilitates
831: program reuse and, more importantly, it allows us to apply a number of
832: existing techniques to the computed slice (e.g., debugging, program
833: analysis, verification, program transformation).
834:
835: So far, we have only considered the \emph{shape} of a slice. Now, we
836: consider the \emph{semantics} of the slicing process:
837:
838: \begin{definition}[correct slice] \label{slice-def}
839: Let $\cR$ be a program and $t$ a term. We say that $\cR'$ is a
840: correct slice of $\cR$ w.r.t.\ $t$ iff
841: \begin{itemize}
842: \item $\cR'$ is a program slice of $\cR$ (i.e., $\cR' \succeq \cR$),
843: and
844: \item $t \To^\ast_{\sigma_1} t_1$ in $\cR$ iff $t
845: \To^\ast_{\sigma_2} t_2$ in $\cR'$, where $t_1,t_2$ are values
846: (different from $\top$), $t_2 \succeq t_1$, and $\sigma_1 =
847: \sigma_2$ (modulo variable renaming).
848: \end{itemize}
849: \end{definition}
850: %
851: Observe that evaluations in the slice may produce values with some
852: occurrences of $\top$ at inner positions, which is safe in our context
853: since only the outermost symbol is \emph{observable} in the LNT
854: semantics. On the other hand, no abstraction is needed for
855: substitutions, since the computed bindings can only map variables to
856: patterns of the form $c(\ol{x_n})$ with no occurrences of $\top$ (see
857: rule {\sf guess} in Fig.~\ref{standard-lnt}).
858:
859: \begin{figure}[t]
860: \rule{\linewidth}{.01in}
861: \begin{flushleft}
862: \vspace{-3ex}
863: \startprog
864: main op xs = fcase op of $\{$ Len $\to$ fst (lenmax xs);
865: $\:$Max $\to$ snd (lenmax xs) $\}$
866:
867: lenmax xs = (len xs, max xs)
868:
869: len xs = fcase xs of $\{$ [] $\to$ Zero;
870: (x:xs) $\to$ Succ (len xs) $\}$
871:
872: max xs = fcase xs of $\{$ (y:ys) $\to$ fcase ys of
873: $\{$ [] $\to$ y;
874: (z:zs) $\to$ if (y $\sleq$ z) then max (z:zs)
875: $\!$else max (y:zs) $\}$ $\}$
876:
877: x $\sleq$ y = fcase x of $\{$ Zero $\to$ True;
878: $\:$Succ n $\to$ fcase y of $\{$ Zero $\to$ False;
879: $\:$Succ m $\to$ n $\sleq$ m $\}$ $\}$
880:
881: fst x = fcase x of $\{$ (a,b) $\to$ a $\}$
882:
883: snd x = fcase x of $\{$ (a,b) $\to$ b $\}$
884: \stopprog
885: \end{flushleft}
886: \vspace{-3ex}
887: \rule{\linewidth}{.01in}
888: \caption{Example \pr{lenmax}}
889: \label{ex-lenmax}
890: \end{figure}
891:
892: \begin{example} \label{lenapp}
893: Consider the program excerpt shown in Fig.~\ref{ex-lenmax} for
894: computing the length or the maximum of a list, depending on the
895: value of the first parameter of \pr{main}. Standard functions
896: ``\pr{len}'', ``\pr{max}'', ``\pr{fst}'', and ``\pr{snd}'' return
897: the length of a list, the maximum of a list, the first element of a
898: tuple, and the second element of a tuple, respectively. Given the
899: slicing criterion ``\pr{main Len xs}'', the following slice can be
900: obtained:
901: %
902: \startprog
903: main op xs = fcase op of $\{$ Len $\to$ fst (lenmax xs);
904: Max $\to$ $\top$ $\}$
905:
906: lenmax xs = (len xs, $\top$)
907:
908: len xs = fcase xs of $\{$ [] $\to$ Zero;
909: (x:xs) $\to$ Succ (len xs) $\}$
910:
911: max xs = $\top$
912:
913: x $\sleq$ y = $\top$
914:
915: fst x = fcase x of $\{$ (a,b) $\to$ a $\}$
916:
917: snd x = $\top$
918: \stopprog
919: %
920: Here, we have performed three different kinds of code deletion:
921: \begin{description}
922: \item[\sf Term deletion:] The evaluation of the call to function
923: ``\pr{max}'' in the right-hand side of ``\pr{lenmax}'' is not
924: needed|since function ``\pr{fst}'' only demands the evaluation of
925: the first component of the tuple|and, thus, it has been replaced by
926: $\top$.
927:
928: \item[\sf Branch deletion:] In the definition of function
929: ``\pr{main}'', the second branch of the case expression is not
930: needed to execute the slicing criterion; therefore, it has also been
931: replaced by $\top$.
932:
933: \item[\sf Function deletion:] Since functions ``\pr{max}'',
934: ``\pr{$\sleq$}'', and ``\pr{snd}'' are no longer necessary to
935: evaluate the slicing criterion, their definitions have been replaced
936: by $\top$.
937: \end{description}
938: Note that this slice could not be constructed by using a simple graph
939: of functional dependencies (e.g., functions ``\pr{snd}'',
940: ``\pr{lenmax}'', and ``\pr{$\sleq$}'' depend on function ``\pr{main}''
941: but they do not appear in the computed slice).
942: \end{example}
943: %
944: In order to simplify the representation of program slices, in the
945: following we adopt the following conventions:
946: \begin{itemize}
947: \item case branches of the form $p \to \top$ are deleted and
948: %% \item case expressions with no branches, and
949: \item function definitions of the form $f(\ol{x_n}) = \top$ are
950: removed from the slice.
951: \end{itemize}
952: Therefore, the slice of Example~\ref{lenapp} is simply written as
953: follows:
954: %
955: \startprog
956: main op xs = fcase op of $\{$ Len $\to$ fst (lenmax xs) $\}$
957:
958: lenmax xs = (len xs, $\top$)
959:
960: len xs = fcase xs of $\{$ [] $\to$ Zero;
961: (x:xs) $\to$ Succ (len xs) $\}$
962:
963: fst x = fcase x of $\{$ (a,b) $\to$ a $\}$
964: \stopprog
965:
966:
967: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
968: \section{Monovariant/Monogenetic Partial Evaluation} \label{pe1}
969:
970: As discussed in the introduction, our developments rely on the fact
971: that forward slicing can be regarded as a form of
972: monovariant/monogenetic partial evaluation. This requirement is
973: necessary in order to ensure that there is a one-to-one relation
974: between the functions of the original and residual programs, which is
975: crucial to produce a fragment of the original program rather than a
976: specialized version.
977:
978: In this section, we first recall the basic narrowing-driven partial
979: evaluation (NPE) scheme \cite{AV02} and, then, modify it in order to
980: obtain a monovariant and monogenetic partial evaluator.
981:
982: Essentially, NPE proceeds by iteratively unfolding a set of function
983: calls, testing the \emph{closedness} of the unfolded expressions, and
984: adding to the current set those calls (in the derived expressions)
985: which are not closed. This process is repeated until all the unfolded
986: expressions are closed, which guarantees the correctness of the
987: transformation process \cite{AFV98}, i.e., that the resulting set of
988: expressions covers all the possible computations for the initial call.
989: This iterative style of performing partial evaluation was first
990: described by Gallagher \citeyear{Gal93} for the partial evaluation of
991: logic programs.
992:
993: The computation of a closed set of expressions can be regarded as the
994: construction of a graph containing the program points which are
995: reachable from the initial call. Intuitively, an expression is
996: \emph{closed} whenever its maximal operation-rooted subterms (function
997: calls) are instances of the already partially evaluated terms.
998: Formally, the closedness condition is defined as follows:
999:
1000: \begin{definition}[closedness] \label{closedness}
1001: Let $E$ be a finite set of expressions. We say that an expression
1002: $e$ is closed w.r.t.\ $E$ (or $E$-closed) iff one of the following
1003: conditions hold:
1004: \begin{itemize}
1005: \item $e$ is a variable;
1006: \item $e=c(e_{1},\ldots,e_{n})$ is a constructor call
1007: and $e_{1},\ldots,e_{n}$ are recursively $E$-closed;
1008: \item $e=(f)case\;e'\;of\;\{\ol{p_{m} \to e_{m}}\}$ is a case
1009: expression and $e',e_{1},\ldots,e_{m}$ are recursively $E$-closed;
1010: \item $e$ is operation-rooted, there is an expression $e' \in E$, a
1011: matching substitution $\sigma$ with $e = \sigma(e')$, and, for all
1012: $x \mapsto e'' \in \sigma$, $e''$ is recursively $E$-closed.
1013: \end{itemize}
1014: \end{definition}
1015:
1016: \begin{figure}[t]
1017: \centering
1018: \rule{\linewidth}{.01in}
1019: \begin{minipage}{8cm}
1020: \mbox{}\\
1021: {\bf Input:} a program $\cR$ and a term $t$\\
1022: {\bf Output:} a residual program $\cR'$\\
1023: {\bf Initialization:} $i:= 0;~ E_0 := \{t\}$\\
1024: {\bf Repeat} \mbox{}\\
1025: \mbox{}\hspace{3ex} $E' := \foo{unfold}(E_i,\cR)$;\\
1026: \mbox{}\hspace{3ex} $E_{i+1}:= \foo{abstract}(E_i,E')$;\\
1027: \mbox{}\hspace{3ex} $i := i+1$;\\
1028: {\bf Until} $E_i = E_{i-1}$ (modulo renaming)\\
1029: {\bf Return:} \\
1030: \mbox{}\hspace{3ex} $\cR' := \foo{build\_residual\_program}(E_i,\cR)$\\
1031: \end{minipage}
1032: \rule{\linewidth}{.01in}
1033: \caption{Narrowing-Driven Partial Evaluation Procedure}
1034: \label{pe-alg}
1035: %% \vspace{-2ex}
1036: \end{figure}
1037:
1038: \noindent
1039: The basic partial evaluation procedure is shown in Fig.~\ref{pe-alg}.
1040: Let us explain the operators in this procedure:
1041: \begin{itemize}
1042: \item The operator $\foo{unfold}$ takes a program and a set of
1043: expressions $E_i = \{e_1,\ldots,e_n\}$, computes a \emph{finite} set
1044: of (possibly incomplete) finite derivations $e_j \To^\ast e'_j$, $j
1045: = 1,\ldots,n$, and returns the set of derived expressions $E' =
1046: \{e'_1,\ldots,e'_n\}$. Here, partial computations are performed with
1047: the LNT calculus of Fig.~\ref{standard-lnt} slightly extended to
1048: avoid the backpropagation of bindings: the RLNT (for Residualizing
1049: LNT) calculus of Albert et al.\ \citeyear{AHV03}. The main
1050: difference between the LNT and the RLNT calculi is that the
1051: non-deterministic rule \textsf{guess} of the LNT calculus is
1052: replaced by a deterministic rule that leaves the case structure
1053: untouched and proceeds with the evaluation of the branches.
1054:
1055: \item Function $\foo{abstract}$ is then used to properly add the new
1056: expressions to the current set of (to be) partially evaluated
1057: expressions. For instance, a trivial abstraction operator could be
1058: defined as follows:
1059: \[
1060: \foo{abstract}(E_i,E') = E_i \cup \{ e \in E' \mid \mbox{ there is
1061: no } e'\in E_i \mbox{ such that } e = e' \}
1062: \]
1063: Here, only the new expressions that are not equal (modulo variable
1064: renaming) to some expression in the current set $E_i$ are added.
1065: This abstraction operator, however, does not guarantee the
1066: termination of the process since an infinite number of different
1067: expressions can be derived. In general, a termination test is also
1068: applied, e.g., Alpuente et al.\ \citeyear{AFV98} consider a variant
1069: of the Kruskal tree condition called ``homeomorphic embedding''
1070: \cite{Leu02}: if an expression embeds another expression in the
1071: current set, some form of generalization|usually the \emph{most
1072: specific generalization} operator|is applied and the generalized
1073: term is added to the current set.
1074:
1075: \item The main loop of the algorithm can be seen as a
1076: \emph{pre-processing} stage whose aim is to find a closed set of
1077: expressions. Note that no residual rules are actually constructed
1078: during this phase. Only when a closed set of expressions is
1079: eventually found, residual rules are built as follows:
1080: \[
1081: \foo{build\_residual\_program}(E_i,\cR) = \{ e = e' \mid e \in E_i
1082: \mbox{ and } e \To^\ast e' \mbox{ in } \cR \}
1083: \]
1084: In general, this operator also applies a renaming of expressions and
1085: some post-unfolding transformations which are not relevant for this
1086: work; we refer the interested reader to \cite{AV02}.
1087: \end{itemize}
1088: %
1089: In principle, the NPE scheme has been designed to achieve both
1090: polyvariant and polygenetic specializations. In this work, however, we
1091: are interested in the definition of a less powerful monovariant and
1092: monogenetic scheme. For this purpose, we should impose several
1093: restrictions to the procedure of Fig.~\ref{pe-alg}:
1094: \begin{enumerate}
1095: \item Firstly, the current set $E_i$ should only contain
1096: operation-rooted terms without nested function calls (i.e., of the
1097: form $f(\ol{t_{n}})$, where $f$ is a defined function symbol and
1098: $t_1,\ldots,t_n$ are constructor terms). This is necessary to ensure
1099: that partial evaluation is monogenetic and, thus, we do not produce
1100: residual functions that mix several functions of the original
1101: program.
1102:
1103: \item Secondly, the unfolding operator should perform only a one-step
1104: evaluation of each call rather than a computation of an arbitrary
1105: length. This condition is required to guarantee that no reachable
1106: function is hidden by the unfolding process. For instance, if we
1107: would allow a computation of the form $\pr{f x $\To$ g x $\To$ h
1108: x}$, the unfolding operator would only return $\pr{h x}$, while
1109: $\pr{g x}$ should also be part of the slice.
1110:
1111: \item Finally, the abstraction operator should ensure that the current
1112: set of terms contains at most one term for each function symbol. In
1113: this way, we enforce the monovariant nature of the partial
1114: evaluation process, i.e., that only one residual definition is
1115: produced (at most) for each original function.
1116: \end{enumerate}
1117: %
1118: Unfortunately, such a monovariant/monogenetic partial evaluator would
1119: propagate information poorly. In order to overcome this drawback, in
1120: the next section we introduce a carefully designed operational
1121: mechanism which avoids the loss of information (i.e., program
1122: dependences) as much as possible.
1123:
1124: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1125: \section{Computing Program Dependences} \label{depen}
1126:
1127: In this section, we introduce the kernel of a monovariant and
1128: monogenetic partial evaluator that can be used to compute program
1129: dependences. In principle, such a partial evaluator could proceed as
1130: follows:
1131: \begin{itemize}
1132: \item terms containing nested function symbols are \emph{flattened};
1133: \item terms in the current set of (to be) partially evaluated terms
1134: which are rooted by the same function symbol are generalized with
1135: some appropriate generalization operator (e.g., the \emph{most
1136: specific generalization} operator).
1137: \end{itemize}
1138: However, flattening terms with nested function symbols would imply a
1139: serious loss of precision. For instance, a term of the form ``\pr{fst
1140: (lenmax xs)}'' would be replaced by the terms ``\pr{fst y}'' and
1141: ``\pr{lenmax xs}'', where \pr{y} is a fresh variable, thus missing the
1142: fact that \pr{fst} is called with the result of ``\pr{lenmax xs}''.
1143:
1144: In order to avoid this loss of precision, we drop the first
1145: restriction above, i.e., we consider arbitrary operation-rooted terms
1146: during partial evaluation. However, we should still ensure that only a
1147: one-step of unfolding is applied to each term in order to guarantee
1148: that no reachable function is hidden by the unfolding process. In our
1149: flat language, function calls are evaluated \emph{lazily}: a term
1150: containing nested function calls is evaluated by first unfolding the
1151: outermost function; inner function calls are only evaluated \emph{on
1152: demand}, i.e., when they appear as the argument of some case
1153: expression.
1154: %
1155: For instance, ``\pr{fst (lenmax xs)}'' is unfolded to
1156: \[
1157: \pr{fcase (lenmax xs) of $\{$ (a,b) $\to$ a $\}$}
1158: \]
1159: Then, the evaluation of function ``\pr{fst}'' cannot continue until
1160: the inner call to ``\pr{lenmax}'' is reduced to a value.
1161: Unfortunately, this interleaved evaluation is problematic in our
1162: context since it would give rise to a polygenetic partial evaluation
1163: (i.e., a residual function comprising the evaluation of both \pr{fst}
1164: and \pr{lenmax}) . In contrast, we should perform a \emph{complete
1165: one-step unfolding} of each function call separately, i.e., a
1166: function unfolding followed by the reduction of all the case
1167: structures in the unfolded expression.
1168:
1169: For this purpose, we extend the partial evaluation mechanism in order
1170: to work on \emph{states} rather than on expressions.
1171:
1172: \begin{definition}[state]
1173: A state is a pair of the form $\tuple{e,S}$, where $e$ is an
1174: expression (to be evaluated) and $S$ is a \emph{stack} (a list)
1175: which represents the current ``evaluation
1176: context''.\footnote{Similar operational semantics with a stack can
1177: be found in \cite{AHHOV05,Ses97}.} The empty stack is denoted by
1178: $\nil$.
1179: \end{definition}
1180: %
1181: For example, the previous expression ``\pr{fst (lenmax xs)}'' could
1182: now be flattened as follows (see Example~\ref{ex-flat}): $\tt
1183: \tuple{\pr{lenmax xs},~[(\pr{fst x},x)]}$, which means that
1184: $\pr{lenmax xs}$ is ready to perform a complete one-step unfolding;
1185: when this evaluation is performed, the initial term can be
1186: reconstructed thanks to the information in the stack, $\tt (\pr{fst
1187: x},x)$, which means that the initial term has the form $\pr{fst x}$,
1188: where \pr{x} is the result of evaluating the first component of the
1189: state (i.e., the result of evaluating \pr{lenmax xs}). Thanks to the
1190: use of states, we do not miss the fact that \pr{fst} is called with
1191: the result of ``\pr{lenmax xs}''.
1192:
1193: Figure~\ref{smallstep} shows an extended operational semantics which
1194: is appropriate to deal with states. Let us briefly explain the rules
1195: of this operational semantics.
1196:
1197: Rules {\sf select} and {\sf guess} proceed in a similar way as their
1198: counterpart in the standard semantics of Fig.~\ref{standard-lnt}.
1199:
1200: Rule {\sf flatten} is used to avoid the unfolding of those
1201: (operation-rooted) terms whose unfolding would demand the evaluation
1202: of some inner call. This is necessary to ensure that partial
1203: evaluation is monogenetic. In this case, we delay the function
1204: unfolding and continue with the evaluation of the demanded inner call.
1205: Auxiliary function \emph{flat} is used to flatten these states. Here,
1206: we use subscripts in the arrows to indicate the application of some
1207: concrete rule(s). Function \emph{flat} proceeds as follows:
1208: \begin{itemize}
1209: \item[] When the expression in the input state can be reduced by using
1210: rules {\sf select} and {\sf guess} to a case expression with a
1211: function call in the argument position (which is thus
1212: \emph{demanded}), function \emph{flat} returns a new state whose
1213: first component is the demanded call, $g(\ol{t'_{m}})$, and whose
1214: stack is augmented by adding a new pair
1215: $(f(\ol{t_{n}})[g(\ol{t'_{m}})/x], x)$. Here,
1216: $f(\ol{t_{n}})[g(\ol{t'_{m}})/x]$ denotes the term obtained from
1217: $f(\ol{t_{n}})$ by replacing the selected occurrence of the inner
1218: call, $g(\ol{t'_{m}})$, with a fresh variable $x$. This pair
1219: contains all the necessary information to reconstruct the original
1220: expression once the inner call is evaluated to a value (in rule {\sf
1221: replace}).
1222: \end{itemize}
1223: %
1224: \begin{example} \label{ex-flat}
1225: Consider again the program of Example~\ref{lenapp}. In order to
1226: flatten the following expression: $\tt \tuple{\pr{fst (lenmax
1227: xs)},~\pr{[]}}$, we proceed as follows. First, we perform a
1228: function unfolding so that we get:
1229: \[
1230: \tt \tuple{\pr{fcase (lenmax xs) of } \{ \pr{(a,b)} \to \pr{a} \},~ \nil}
1231: \]
1232: Now, we try to evaluate this state by means of rules \textsf{select}
1233: and \textsf{guess}. Since no reduction is possible and the case
1234: structure has a function call in the argument position, function
1235: $\foo{flat}$ returns the state
1236: \[
1237: \tt \tuple{\pr{lenmax xs},~[(\pr{fst x},\pr{x})]}
1238: \]
1239: where \pr{x} is a fresh variable. Observe that this state cannot be
1240: further flattened since a function unfolding returns the state
1241: \[
1242: \tt \tuple{(\pr{len xs},~\top), ~\nil }
1243: \]
1244: which cannot be reduced by rules \textsf{select} and \textsf{guess}
1245: and which contains no function call in the argument position of a
1246: case expression. Therefore, in this case, function $\foo{flat}$
1247: returns $\bot$ and no step with rule \textsf{flatten} can be done.
1248: \end{example}
1249: %
1250: Rule {\sf fun} performs a simple function unfolding when rule {\sf
1251: flatten} does not apply, i.e., when function \emph{flat} returns
1252: $\bot$.
1253:
1254: Finally, rule {\sf replace} allows us to retake the evaluation of some
1255: delayed function call once the demanded inner call is reduced to a
1256: value.
1257:
1258: \begin{figure}[t]
1259: \rule{\linewidth}{.01in}
1260: \[
1261: \mbox{}\hspace{-5ex}\begin{array}{l@{~~~~~}lr@{~~~\To~~~}lr}
1262: \mbox{\sf (select)} & \l\: \foo{(f)case}\;c(\ol{t_n})\;of\;
1263: \{\ol{p_{k} \to e_{k}}\}, & S\:\r & \l\:\rho(e_i), & S\:\r \\[.5ex]
1264: & \multicolumn{4}{l}{\mbox{if } p_i = c(\ol{x_n}),\;c\in\cC, \mbox{ and }
1265: \rho = \{\ol{x_n \mapsto t_n}\} } \\[1ex]
1266: \mbox{\sf (guess)} & \l\: \foo{(f)case}\;x\;of\;\{\ol{p_{k} \to e_{k}}\},
1267: & S\:\r & \l\:\rho(e_i), & S\:\r \\[.5ex]
1268: & \multicolumn{4}{l}{\mbox{if }
1269: \rho = \{x \mapsto p_{i}\} \mbox{ and } i \in\{1,\ldots,k\}} \\[1ex]
1270: \mbox{\sf (flatten)} & \l\: f(\ol{t_{n}}), & S\:\r &
1271: \l\: g(\ol{t'_{m}}), & S^{f}\:\r \\[.5ex]
1272: & \multicolumn{4}{l}{\mbox{if } \foo{flat}(f(\ol{t_{n}}),S)=
1273: \tuple{g(\ol{t'_{m}}),S^{f}}} \\[1ex]
1274: \mbox{\sf (fun)} & \l\:f(\ol{t_{n}}), & S\:\r & \l\:\rho(e), & S\:\r \\[.5ex]
1275: & \multicolumn{4}{l}{\mbox{if } \foo{flat}(f(\ol{t_{n}}),S)=\bot,\:
1276: f(\ol{x_{n}}) = e \in \cR,\: \mbox{ and }
1277: \rho=\{\ol{x_{n} \to t_{n}}\} } \\[1ex]
1278: \mbox{\sf (replace)} & \l\: v, & (f(\ol{t_{n}}),x):S\:\r
1279: & \l\:\rho(f(\ol{t_{n}})), & S\:\r \\[.5ex]
1280: & \multicolumn{4}{l}{\mbox{if } v \mbox{ is a value and }
1281: \rho=\{x \mapsto v\}} %\\[1ex]
1282: \end{array}
1283: \]
1284: \[
1285: \mbox{}\hspace{-5ex}\begin{array}{lll}
1286: \mbox{\sf where}\;\;\foo{flat}(\tuple{f(\ol{t_{n}}),S}) & \;=\; &
1287: \mbox{\sf if } \tuple{\rho(e),\nil} \:\Longrightarrow^\ast_{\sf select/guess}\:
1288: \tuple{\foo{(f)case}\;g(\ol{t'_{m}})\;of\;\{\;\ldots\;\},\nil} \\
1289: & & \mbox{}\hspace{3em}\mbox{\sf then }\;
1290: \tuple{g(\ol{t'_{m}}),(f(\ol{t_{n}})[g(\ol{t'_{m}})/x],
1291: x):S}\\
1292: & & \mbox{}\hspace{3em}\mbox{\sf else }\;\: \bot \\
1293: & & \mbox{\sf with } f(\ol{x_{n}}) = e \in \cR, \;\mbox{\sf and } \rho = \{\ol{x_{n} \to t_{n}}\}
1294: \end{array}
1295: \]
1296: \rule{\linewidth}{.01in}
1297: \caption{Extended Operational Semantics}
1298: \label{smallstep}
1299: \end{figure}
1300:
1301: The extended operational semantics behaves almost identically to the
1302: standard semantics of Fig.~\ref{standard-lnt}. There are, though, the
1303: following main differences:
1304: \begin{itemize}
1305: \item Now, the one-step relation $\To$ is not labeled with the
1306: computed bindings since we are not interested in computing answers
1307: but only in obtaining the functions which are reachable from the
1308: initial call.
1309:
1310: \item In the standard semantics, rigid case expressions with a free
1311: variable in the argument position \emph{suspend}. In our case, rule
1312: {\sf guess} proceeds with their evaluation as if they were flexible.
1313: This is motivated by the fact that we may have \emph{incomplete}
1314: information; hence, in order to be on the safe side|and do not miss
1315: any reachable function|we should explore all the alternatives of
1316: rigid case expressions.
1317:
1318: \item The order of evaluation is slightly changed. In our extended
1319: semantics, we delay those function unfoldings which cannot be
1320: followed by the reduction of all the case expressions in the
1321: corresponding right-hand side.
1322: \end{itemize}
1323: %
1324: In spite of these differences, both calculi trivially produce the same
1325: results for input expressions involving no suspension. Roughly
1326: speaking, the extended semantics is in between the standard
1327: operational semantics and its residualizing version used to perform
1328: partial computations in the NPE framework \cite{AHV03}.
1329:
1330: \begin{example} \label{ex-comps}
1331: Consider again the program of Example~\ref{lenapp}. Given the
1332: initial term $\pr{fst (lenmax xs)}$, we have (among others) the
1333: following (incomplete) computation with the standard semantics of
1334: Fig.~\ref{standard-lnt}:
1335: \[ \small
1336: \begin{array}{llll}
1337: \pr{fst (lenmax xs)}
1338: & \tt \To_{id} & \pr{fcase (lenmax xs) of } \{ \pr{(a,b)} \to \pr{a} \} & \mbox{(\textsf{fun})}\\
1339: & \tt \To_{id} & \pr{fcase (len xs, max xs) of } \{ \pr{(a,b)} \to \pr{a} \} & \mbox{(\textsf{fun})}\\
1340: & \tt \To_{id} & \pr{len xs} & \mbox{(\textsf{select})}
1341: \end{array}
1342: \]
1343: On the other hand, the extended operational semantics of
1344: Fig.~\ref{smallstep} performs the following equivalent derivation:
1345: \[ \small \hspace{-8ex}
1346: \begin{array}{llll}
1347: \tuple{\pr{fst (lenmax xs)},~\nil}
1348: & \tt \To & \tuple{\pr{lenmax xs},~[(\pr{fst x},\pr{x})]} & \mbox{(\textsf{flatten})}\\
1349: & \tt \To & \tuple{\pr{(len xs, max xs)},~[(\pr{fst x},\pr{x})]} & \mbox{(\textsf{fun})}\\
1350: & \tt \To & \tuple{\pr{fst (len xs, max xs)},~\nil} & \mbox{(\textsf{replace})}\\
1351: & \tt \To & \tuple{\pr{fcase (len xs, max xs) of } \{ \pr{(a,b)} \to \pr{a} \},~\nil} & \mbox{(\textsf{fun})}\\
1352: & \tt \To & \tuple{\pr{len xs},~\nil} & \mbox{(\textsf{select})}\\
1353: \end{array}
1354: \]
1355: \end{example}
1356: %
1357: The relevance of the extended semantics stems from the fact that
1358: computations can now be split into a number of consecutive sequences
1359: of steps of the form:\\[2ex]
1360: $ \mbox{}\hspace{2ex}\Longrightarrow_{\sf flatten}^\ast \underbrace{
1361: \Longrightarrow_{\sf fun} \Longrightarrow^\ast_{\sf select/guess}
1362: }_{seq\_1} \Longrightarrow^\ast_{\sf replace} \Longrightarrow_{\sf
1363: flatten}^\ast \underbrace{ \Longrightarrow_{\sf fun}
1364: \Longrightarrow^\ast_{\sf select/guess} }_{seq\_2}
1365: \Longrightarrow^\ast_{\sf replace} \ldots
1366: $\\[2ex]
1367: where each subsequence, \emph{seq\_i}, represents a complete one-step
1368: unfolding of some function call. From these sequences, a
1369: monogenetic/monovariant partial evaluation scheme can easily be
1370: defined and, thus, the algorithm for computing dependences in our
1371: program slicing technique.
1372:
1373: The algorithm of Fig.~\ref{pe-alg} is now slightly modified in order
1374: to work with states. The new algorithm (depicted in
1375: Fig.~\ref{pe-alg2}) does not compute a residual program but only the
1376: set of states which are reachable from the initial call. In other
1377: words, it returns the counterpart of the final set of \emph{closed}
1378: terms computed by the algorithm of Fig.~\ref{pe-alg}. The new
1379: algorithm starts by flattening the initial term in order to ensure
1380: that a complete one-step unfolding can be performed. We now tackle
1381: the definition of appropriate unfolding and abstraction operators.
1382: First, the \emph{one-step} unfolding operator is defined as follows:
1383:
1384: \begin{figure}[t]
1385: \centering
1386: \rule{\linewidth}{.01in}
1387: \begin{minipage}{11cm}
1388: \mbox{}\\
1389: {\bf Input:} a program $\cR$ and an operation-rooted term $t$\\
1390: {\bf Output:} a set of states $\cS$ \\
1391: {\bf Initialization:} $i:= 0;~ \cS_0 := \{\tuple{t',S}\}$,
1392: where $\tuple{t,\nil} \Longrightarrow^\ast_{\sf flatten} \tuple{t',S}
1393: \not\Longrightarrow_{\sf flatten}$\\
1394: {\bf Repeat} \mbox{}\\
1395: \mbox{}\hspace{3ex} $\cS' := \foo{unfold}(\cS_i,\cR)$;\\
1396: \mbox{}\hspace{3ex} $\cS_{i+1}:= \foo{abstract}(\cS_i,\cS')$;\\
1397: \mbox{}\hspace{3ex} $i := i+1$;\\
1398: {\bf Until} $\cS_i = \cS_{i-1}$ (modulo renaming)\\
1399: {\bf Return:}
1400: ~$\cS := \cS_{i}$\\[-1ex]
1401: \end{minipage}
1402: \rule{\linewidth}{.01in}
1403: \caption{Computation of Reachable Program Points}
1404: \label{pe-alg2}
1405: \vspace{-2ex}
1406: \end{figure}
1407:
1408: \begin{definition}[unfold]
1409: Let $\cS$ be a set of states. The unfolding operator
1410: $\foo{unfold}$ is defined by
1411: \[
1412: \begin{array}{l}
1413: \foo{unfold}(\cS) = {\displaystyle \bigcup_{s \in \cS}} \;\foo{unf}(s)
1414: \end{array}
1415: \]
1416: where\\[1ex]
1417: $ \mbox{}\hspace{2ex} \foo{unf}(\tuple{t,S}) = \{ \tuple{t',S} \mid
1418: \tuple{t,S} \Longrightarrow_{\sf fun}
1419: \tuple{t'',S}\Longrightarrow^\ast_{\sf select/guess} \tuple{t',S}
1420: \not\Longrightarrow_{\sf select/guess} \}
1421: $
1422: \end{definition}
1423: %
1424: This unfolding operator always performs a complete one-step unfolding
1425: of each input expression. The associated stack $S$ remains unchanged
1426: since only rules {\sf flatten} and {\sf replace} can modify the
1427: current stack. Function $\foo{unf}$ returns a \emph{set} of derived
1428: states because of the non-determinism of the underlying operational
1429: semantics.
1430:
1431: \begin{example}
1432: Consider again the program of Example~\ref{lenapp}. We illustrate
1433: function $\foo{unf}$ by means of some simple examples:
1434: \[
1435: \foo{unf}(\tuple{\pr{lenmax xs},~[(\pr{fst x},\pr{x})]}) =
1436: \tuple{\pr{(len xs, max xs)},~[(\pr{fst x},\pr{x})]}
1437: \]
1438: \[
1439: \foo{unf}(\tuple{\pr{fst (len xs, max xs)},~\nil}) = \tuple{\pr{len
1440: xs},~\nil}
1441: \]
1442: according to the partial computation in Example~\ref{ex-comps}.
1443: \end{example}
1444: %
1445: Before defining our abstraction operator, we need the following
1446: auxiliary notion:
1447:
1448: \begin{definition}[flattened state]
1449: Let $s$ be a state returned by the operator $\foo{unfold}$ with
1450: $s \Longrightarrow^\ast_{\sf replace/flatten} s'
1451: \not\Longrightarrow$. Then $s'$ is called a flattened state.
1452: \end{definition}
1453: %
1454: Flattened states have a particular form, as stated by the following
1455: result:
1456:
1457: \begin{lemma} \label{flattened-states}
1458: Let $s$ be a flattened state. Then $s$ has the form
1459: $\tuple{v,\nil}$, where $v$ is a value, or $\tuple{f(\ol{t_{n}}),S}$,
1460: where $f(\ol{t_{n}})$ is an operation-rooted term.
1461: \end{lemma}
1462: %
1463: In order to add new states to the current set of states, we introduce
1464: the following abstraction operator:
1465:
1466: \begin{definition}[abstract]
1467: Let $\cS$ and $\cS' = \{s_{1},\ldots,s_{n}\}$ be sets of states. Our
1468: abstraction operator proceeds as follows:
1469: $
1470: \foo{abstract}(\cS,\cS') = %\{s_{1},\ldots,s_{n}\}) =
1471: \foo{abs}(\foo{abs}(\ldots \foo{abs}(\cS,s'_{1})\ldots,
1472: s'_{n-1}),s'_{n})
1473: $,
1474: where:
1475: \[
1476: s_{i} \Longrightarrow^\ast_{\sf replace/flatten} s'_{i}
1477: \not\Longrightarrow_{\sf replace/flatten}
1478: ~~\mbox{(for all $i = 1,\ldots,n$) }
1479: \]
1480: \end{definition}
1481: %
1482: Basically, function $\foo{abstract}$ starts by flattening the input
1483: states by applying (zero or one step of) rule {\sf replace}, followed
1484: by (zero or more steps of) rule {\sf flatten}.
1485:
1486: \begin{definition}[abs]
1487: Function $\foo{abs}$ is defined inductively on the structure of
1488: flattened states (according to Lemma~\ref{flattened-states}):
1489: \begin{description}
1490: \item[$\foo{abs}(\cS,\tuple{x,\nil}) = \cS$] \mbox{}\\[-2ex]
1491:
1492: \item[$\foo{abs}(\cS,\tuple{c(\ol{t_{n}}),\nil}) =
1493: \foo{abstract}(\cS,\cS')$]
1494: \mbox{}\\
1495: {\sf if $\ol{t'_{m}}$ are the maximal operation-rooted subterms of
1496: $c(\ol{t_{n}})$ and $\cS' = \{ \ol{\tuple{t'_{m},\nil}}\}$ }\\[-2ex]
1497:
1498: \item[$\foo{abs}(\cS,\tuple{f(\ol{t_{n}}),S}) = $]
1499: \mbox{}\\
1500: $\left\{
1501: \begin{array}{l@{~~~~}l}
1502: \cS \cup \{\tuple{f(\ol{t_{n}}),S}\} & \mbox{\sf if there is no state
1503: $\tuple{f(\ol{t'_{n}}),S'}$ in $\cS$ } \\
1504: \cS & \mbox{\sf else if $\tuple{f(\ol{t_{n}}),S}$ is $\cS$-closed } \\
1505: \foo{abstract}(\cS^\ast,\cS'') & \mbox{\sf otherwise, where
1506: $\tuple{f(\ol{t'_{n}}),S'} \in \cS$,} \\
1507: & \mbox{\sf $\foo{msg}(\tuple{f(\ol{t'_{n}}),S'},
1508: \tuple{f(\ol{t_{n}}),S}) = (\tuple{f(\ol{t''_{n}}),S'},\cS'')$, } \\
1509: & \mbox{\sf and
1510: $\cS^\ast = (\cS \:\backslash\: \{ \tuple{f(\ol{t'_{n}}),S'}\}) \cup
1511: \{\tuple{f(\ol{t''_{n}}),S'}\}$ }
1512: \end{array}
1513: \right.
1514: $
1515: \end{description}
1516: \end{definition}
1517: %
1518: Informally speaking, function $\foo{abs}$ determines the corresponding
1519: action depending on the first component of the new state. If it is a
1520: variable, we discard the state. If it is constructor-rooted, we try
1521: to (recursively) add the maximal operation-rooted subterms. If it is
1522: a function call, then we have three possibilities:
1523: \begin{itemize}
1524: \item If there is no call to the same function in the current set, the
1525: new state is added to the current set of states.
1526:
1527: \item If there is a call to the same function in the current set, but
1528: the new call is \emph{closed} w.r.t.\ this set, it is discarded.
1529:
1530: \item Otherwise, we generalize the new state and the existing state
1531: with the same outermost function|which is trivially unique by
1532: definition of $\foo{abstract}$|and, then, we try to (recursively)
1533: add the states computed by function $\foo{msg}$.
1534: \end{itemize}
1535: %
1536: The notion of closedness is easily extended from expressions to
1537: states: a state $\tuple{t,S}$ is \emph{closed} w.r.t.\ a set of states
1538: $\cS$ iff $S[t]$ is $T$-closed (according to Def.~\ref{closedness}),
1539: with $T = \{ S'[t'] \mid \tuple{t',S'} \in \cS \}$. Here, $S[t]$
1540: denotes the term represented by $\tuple{t,S}$, i.e., inner calls are
1541: moved back to their positions in the outer calls of the stack. For
1542: instance, given the state
1543: \[
1544: \tuple{t,S} = \tt \tuple{y, [(len\;x_{2},\; x_{2}),
1545: (fst\;(x_{1},\;snd\;z), \;x_{1})] }
1546: \]
1547: we have $S[t] = \tt fst\;(len\;y,\;snd\;z)$.
1548:
1549: The operator \emph{msg} on states is defined as follows. First, we
1550: recall the standard notion of \emph{msg} on terms: a term $t$ is a
1551: \emph{generalization} of terms $t_{1}$ and $t_{2}$ if both $t_{1}$
1552: and $t_{2}$ are instances of $t$; furthermore, term $t$ is the
1553: \emph{msg} of $t_{1}$ and $t_{2}$ if $t$ is a generalization of
1554: $t_{1}$ and $t_{2}$ and, for any other generalization $t'$ of $t_{1}$
1555: and $t_{2}$, $t$ is an instance of $t'$. Now, the \emph{msg} of two
1556: states is defined by
1557: \[
1558: \foo{msg}(\tuple{t_{1},S_{1}}, \tuple{t_{2},S_{2}})
1559: ~=~(\tuple{t,S_{1}}, \foo{calls}(\sigma_{1}) \cup
1560: \foo{calls}(\sigma_{2}) \cup \foo{calls}(S_{2}))
1561: \]
1562: where $\foo{msg}(t_{1},t_{2}) = t$, and $\sigma_{1}$ and
1563: $\sigma_{2}$ are the matching substitutions, i.e., $\sigma_{1}(t) =
1564: t_{1}$ and $\sigma_{2}(t) = t_{2}$. The auxiliary function
1565: $\foo{calls}$ returns a set of states of the form $\tuple{t,\nil}$
1566: for each maximal operation-rooted term $t$ in (the range of) a
1567: substitution or in a stack.
1568:
1569: \begin{example}
1570: Consider the set of states $\cS = \{ \tuple{\pr{len
1571: xs},\nil},~\tuple{\pr{fst (a,b)},~\nil}\}$. We illustrate
1572: function $\foo(abs)$ by means of some simple examples:
1573: \[
1574: \foo{abs}(\cS,\tuple{\pr{max xs},~\nil}) = \cS \cup \{\tuple{\pr{max
1575: xs},~\nil}\}
1576: \]
1577: since there is no state rooted by function \pr{max} in $\cS$,
1578: \[
1579: \foo{abs}(\cS,\tuple{\pr{len (y:ys)},~\nil}) = \cS
1580: \]
1581: since $\tuple{\pr{len (y:ys)},~\nil}$ is $\cS$-closed (i.e., \pr{len
1582: (y:ys)} is an instance of \pr{len xs}), and
1583: \[
1584: \foo{abs}(\cS,\tuple{\pr{fst z},~\nil}) = \{ \tuple{\pr{len
1585: xs},\nil},~\tuple{\pr{fst w},~\nil}\}
1586: \]
1587: since there is a state $\tuple{\pr{fst (a,b)},\nil}$ rooted by
1588: function \pr{fst}, the state $\tuple{\pr{fst z},~\nil}$ is not
1589: $\cS$-closed (since \pr{fst z} is not an instance of \pr{fst (a,b)},
1590: the most specific generalization of the states $\tuple{\pr{fst
1591: (a,b)}}$ and $\tuple{\pr{fst z},~\nil}$ returns $\tuple{\pr{fst
1592: w},~\nil}$, and
1593: \[
1594: \foo{abs}(\{ \tuple{\pr{len xs},\nil}\}, \tuple{\pr{fst w},~\nil}) =
1595: \{ \tuple{\pr{len xs},\nil},~ \tuple{\pr{fst w},~\nil}\}
1596: \]
1597: since there is no state in $\{ \tuple{\pr{len xs},\nil}\}$ rooted by
1598: function \pr{fst}.
1599: \end{example}
1600: %
1601: Our operator $\foo{abstract}$ can be seen as an instance of the
1602: parametric abstraction operator introduced by Alpuente et al.\
1603: \citeyear{AFV98} particularized to consider states (rather than terms)
1604: and monovariant partial evaluation (thus, only one operation-rooted
1605: term is allowed for each defined function symbol). Our abstraction
1606: operator is safe in the following sense:
1607:
1608: \begin{lemma} \label{safe-abstract}
1609: Let $\cS$ be a set of flattened states and $\cS'$ a set of unfolded
1610: states (as returned by $\foo{unfold}$). Then the states in $\cS \cup
1611: \cS'$ are closed w.r.t.\ $\foo{abstract}(\cS,\cS')$.
1612: \end{lemma}
1613: %
1614: This lemma is a crucial result to ensure the correctness of our
1615: approach. In fact, it will allow us to prove that the generated
1616: program is a correct slice according to Definition~\ref{slice-def}.
1617:
1618: \begin{example} \label{lenapp2}
1619: Consider again the program of Example~\ref{lenapp}. Given the
1620: slicing criterion ``\pr{main Len xs}'', the initial set of states is
1621: $\tt \cS_{0} = \{\tuple{\pr{main Len xs},\nil} \} $. Now, we show
1622: the sequence of iterations performed by the algorithm of
1623: Fig.~\ref{pe-alg2}:
1624: \[
1625: \begin{array}{l}
1626: \cS'_0 = \{ \tuple{\pr{fst (lenmax xs)},\nil} \} \\
1627: \cS_1 = \cS_0 \cup \{ \tuple{\pr{lenmax xs},\;[(\pr{fst x},\pr{x})]} \} \\
1628:
1629: \cS'_1 = \cS'_0 \cup \{ \tuple{(\pr{len xs},\pr{max xs}), \;[(\pr{fst x},\pr{x})] } \} \\
1630: \cS_2 = \cS_1 \cup \{ \tuple{\pr{fst (len xs, max xs)},\nil} \} \\
1631: \cS'_2 = \cS'_1 \cup \{ \tuple{\pr{len xs},\nil} \} \\
1632: \cS_3 = \cS_2 \cup \{ \tuple{\pr{len xs},\nil} \} \\
1633: \cS'_3 = \cS'_2 \cup \{ \tuple{\pr{Zero},\nil},\;\tuple{\pr{Succ (len xs)},\nil} \} \\
1634: \cS_4 = \cS_3
1635: \end{array}
1636: \]
1637: where $\cS'_{i} = \foo{unfold}(\cS_{i},\cR)$ and $\cS_{i+1} =
1638: \foo{abstract}(\cS_{i},\cS'_{i})$, for $i = 0,\ldots,3$.
1639: Therefore, the algorithm returns the following set of states:
1640: \[
1641: \begin{array}{lll}
1642: \cS = \{ & \tuple{\pr{main Len xs},\nil},\;
1643: \tuple{\pr{lenmax xs},\;[(\pr{fst x},\pr{x})]}, \\
1644: & \tuple{\pr{fst (len xs, max xs)},\nil},\;
1645: \tuple{\pr{len xs},\nil} & \}
1646: \end{array}
1647: \]
1648: \end{example}
1649: %
1650: The total correctness of the algorithm in Fig.~\ref{pe-alg2} is stated
1651: in the following theorem:
1652:
1653: \begin{theorem} \label{termination}
1654: Given a flat program $\cR$ and an initial term $t$, the algorithm in
1655: Fig.~\ref{pe-alg2} terminates computing a set of states $\cS$ such
1656: that $\tuple{t,\nil}$ is $\cS$-closed.
1657: \end{theorem}
1658:
1659:
1660: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1661: \section{Extraction of the Slice} \label{extract}
1662:
1663: In this section, we introduce the final step of our slicing process,
1664: i.e., the extraction of the program slice. Let us recall that it must
1665: be a \emph{fragment} of the original program|thus no instantiation of
1666: variables is allowed|and produce the same outputs for the slicing
1667: criterion as the original program. Here, we follow the
1668: \emph{simplified} form for program slices, i.e., case branches of the
1669: form $p \to \top$ are deleted, and function definitions of the form
1670: $f(\ol{x_n}) = \top$ do not appear in the slice.
1671:
1672: First, we need the following auxiliary function that returns the terms
1673: which are relevant in order to extract a program slice from the set of
1674: states computed by the algorithm of Fig.~\ref{pe-alg2}:
1675:
1676: \begin{definition}[residual calls]
1677: Let $\cS$ be a set of states returned by the algorithm of
1678: Fig.~\ref{pe-alg2} and let
1679: $
1680: T_{\cS} = \{ t \mid \tuple{t,S} \in \cS \}
1681: $.
1682: Then, the set of residual calls of $\cS$ is defined as follows:
1683: \[
1684: \mbox{}\hspace{-3ex}\foo{residual\_calls}(\cS) = T_{\cS} \cup \{ t' \mid
1685: \tuple{t,S} \in \cS,~t' \in \foo{calls}(S),~\mbox{\sf and $t'$ is
1686: not $T_{\cS}$-closed} \}
1687: \]
1688: \end{definition}
1689: %
1690: Observe that, in the above definition, $\foo{residual\_calls}$ should
1691: also return the function calls in the computed stacks when they are
1692: not closed w.r.t.\ the set of first components of the states in $\cS$.
1693: This is mandatory in order to ensure a full equivalence w.r.t.\ the
1694: standard semantics.
1695: %
1696: Program slices can now be built as follows:
1697:
1698: \begin{definition}[construction of program slices] \label{cons-slice}
1699: Let $\cS$ be a set of states returned by the algorithm of
1700: Fig.~\ref{pe-alg2}. Then, a program slice is obtained from
1701: $
1702: \foo{build\_slice}(\foo{residual\_calls}(\cS))
1703: $,
1704: where function $\foo{build\_slice}$ is defined as follows:
1705: \[
1706: \begin{array}{lll}
1707: \foo{build\_slice}(\{\:\}) & = & \{\:\} \\
1708: \foo{build\_slice}(\{f(\ol{t_{n}})\} \cup T') & = &
1709: \{f(\ol{x_{n}}) = e'\} \cup \foo{build\_slice}(T') \\
1710: & & \mbox{\sf where } f(\ol{x_{n}}) = e \in \cR,\; \rho=\{\ol{x_{n} \mapsto t_{n}}\},\\
1711: & & \mbox{\sf and }
1712: \sql e\sqr \rho \longrightarrow^\ast e' \not\longrightarrow
1713: \end{array}
1714: \]
1715: \end{definition}
1716: %
1717: The new calculus which is used to construct the rules of the slice is
1718: depicted in Fig.~\ref{simplify-rules}. First, note that the symbols
1719: ``$\sql$'' and ``$\sqr$'' in an expression like $\sql e \sqr \rho$ are
1720: purely syntactical, i.e., they are only used to mark subexpressions
1721: where the inference rules may be applied. The substitution $\rho$ is
1722: used to store the bindings for the program variables. Let us briefly
1723: explain the rules of the new calculus.
1724:
1725: Rule {\sf var} simply returns a variable unchanged. Rule {\sf cons}
1726: applies to constructor-rooted terms; it leaves the outermost
1727: constructor symbol and (recursively) inspects the arguments.
1728:
1729: Rules {\sf select} and {\sf guess} proceed similarly to their
1730: counterpart in Fig.~\ref{smallstep} but leave the case structure
1731: untouched; the substitution $\rho$ is used to check the current value
1732: of the case argument. We only deal with \emph{variable} case
1733: arguments since the considered expression is the right-hand side of
1734: some program rule (cf.\ Fig.~\ref{flat}). Note that rule {\sf guess}
1735: is now deterministic (and, thus, the entire calculus).
1736:
1737: Finally, rules {\sf fun} and {\sf remove} are used to reduce function
1738: calls: when there is some term in $\foo{residual\_calls}(\cS)$ with
1739: the same outermost function symbol,
1740: we proceed as in rule {\sf cons}; otherwise, we return $\top$ (which
1741: means that the evaluation of this function call is not needed).
1742:
1743: \begin{figure}[t]
1744: \begin{center}
1745: $
1746: \begin{array}{l@{~~~}l@{~\longrightarrow~}l}
1747: \mbox{Rule} & \Control & \Control \\\hline\\[-2ex]
1748: \mbox{\sf var} & \sql x \sqr \rho & x \;\\
1749: \mbox{\sf cons} & \sql c(\ol{t_{n}}) \sqr \rho
1750: & c(\sql t_{1} \sqr \rho, \ldots, \sql t_{n} \sqr \rho) \;\\
1751: \mbox{\sf select} & \sql (f)case\;x\;of\;\{\ol{p_{k} \to e_{k}}\} \sqr
1752: \rho & (f)case\;x\;of\;\{p_{i} \to \sql e_{i} \sqr \rho' \} \;\\
1753: \mbox{\sf guess} & \sql (f)case\;x\;of\;\{\ol{p_{k} \to e_{k}}\} \sqr
1754: \rho & (f)case\;x\;of\;\{\ol{p_{k} \to \sql e_{k} \sqr \rho_k }\} \;\\
1755: \mbox{\sf fun} & \sql f(\ol{t_{n}}) \sqr \rho
1756: & f(\sql t_{1} \sqr \rho,\ldots,\sql t_{n} \sqr \rho) \;\\
1757: \mbox{\sf remove} & \sql f(\ol{t_{n}}) \sqr \rho
1758: & \top \;\\\hline
1759: \end{array}$
1760:
1761: $\begin{array}{@{}l@{~}ll}
1762: \\[-2ex]
1763: \mbox{where in} &\mbox{{\sf select}: }& \rho(x) = c(\ol{t_{n}}),\;
1764: p_i = c(\ol{x_n}), \; \rho' = \{\ol{x_n \mapsto t_n}\} \circ \rho,
1765: \mbox{ and }
1766: i\in\{1,\ldots,k\} \\
1767: &\mbox{{\sf guess}: }& \rho(x) \in \cX,\; \rho_i = \{x \mapsto p_i\}\circ\rho, \mbox{ and }
1768: i \in \{1,\ldots,k\} \\
1769: &\mbox{{\sf fun}: }& \mbox{there is some term in $\foo{residual\_calls}(\cS)$ rooted by $f$}\\
1770: %% \rho(f(\ol{t_{n}}))
1771: %%\mbox{ is closed w.r.t.\ $\foo{residual\_calls}(\cS)$} \\
1772: &\mbox{{\sf remove}: }& \mbox{otherwise}
1773: %%\rho(f(\ol{t_{n}}))
1774: %%\mbox{ is not closed w.r.t.\ $\foo{residual\_calls}(\cS)$}
1775: \end{array}
1776: $
1777: \end{center}
1778: \vspace{-2ex}
1779: \caption{Simplified Unfolding Rules}
1780: \label{simplify-rules}
1781: \vspace{-2ex}
1782: \end{figure}
1783:
1784:
1785: \begin{example} \label{lenapp3}
1786: Consider the set of states computed in Example~\ref{lenapp2}. From
1787: this set, function \emph{residual\_calls} returns the set of terms:
1788: \[
1789: \{ \pr{main Len xs},\; \pr{lenmax xs},\; \pr{fst (len xs, max xs)},\;\pr{len xs} \}
1790: \]
1791: Now, we construct a residual rule for each term of the set. For
1792: instance, for the term ``\pr{main Len xs}'', the associated residual
1793: rule is:
1794: \[
1795: \pr{main op xs} \;=\; \pr{fcase op of } \{ \pr{Len} \to \pr{fst (lenmax xs)} \}
1796: \]
1797: since the following derivation can be performed (with $\rho = \{
1798: \pr{op} \mapsto \pr{Len} \}$):\\[2ex]
1799: $
1800: \begin{array}{l}
1801: \sql \pr{fcase op of } \{ \pr{ Len} \to \pr{fst (lenmax xs)};
1802: \pr{ Max} \to \pr{snd (lenmax xs)} \;\} \sqr \rho\\
1803: \hspace{10ex}\longrightarrow_{\mathsf{select}}
1804: \hspace{1ex}\pr{fcase op of } \{ \pr{ Len} \to \sql \pr{fst (lenmax xs)}\sqr \rho \;\} \\
1805: \hspace{10ex}\longrightarrow_{\mathsf{fun}}
1806: \hspace{3ex}\pr{fcase op of } \{ \pr{ Len} \to \pr{fst } (\sql \pr{lenmax xs} \sqr \rho) \;\} \\
1807: \hspace{10ex}\longrightarrow_{\mathsf{fun}}
1808: \hspace{3ex}\pr{fcase op of } \{ \pr{ Len} \to \pr{fst } (\pr{lenmax } \sql \pr{xs} \sqr \rho) \;\} \\
1809: \hspace{10ex}\longrightarrow_{\mathsf{var}}
1810: \hspace{3ex}\pr{fcase op of } \{ \pr{ Len} \to \pr{fst (lenmax xs)} \;\} \\
1811: \end{array}
1812: $\\[2ex]
1813: By constructing a residual rule associated to each of the remaining
1814: terms, the computed slice coincides with the (simplified version of
1815: the) program slice which is shown in Example~\ref{lenapp}.
1816: \end{example}
1817: %
1818: Now, we show that the result of Definition~\ref{cons-slice} is a
1819: program slice of the original program according to
1820: Definition~\ref{prog-abs}.
1821:
1822: \begin{theorem} \label{abs-th}
1823: Let $\cR$ be a flat program and $t$ a term. Let $\cS$ be a set of
1824: states computed by the algorithm of Fig.~\ref{pe-alg2} from $\cR$
1825: and $t$. Then, $\cR' =
1826: \foo{build\_slice}(\foo{residual\_calls}(\cS))$ is a program slice of
1827: $\cR$, i.e., $\cR' \succeq \cR$.
1828: \end{theorem}
1829: %
1830: Finally, the correctness of the computed slices (according to
1831: Def.~\ref{slice-def}) is inherited by the correctness of the
1832: underlying partial evaluation process.
1833:
1834: \begin{theorem} \label{final}
1835: Let $\cR$ be a flat program and $t$ a term. Let $\cS$ be a set of
1836: states computed by the algorithm of Fig.~\ref{pe-alg2} from $\cR$
1837: and $t$. If computations for $t$ in $\cR$ do not suspend, then $t$
1838: computes the same values and answers in $\cR$ and in
1839: $\foo{build\_slice}(\foo{residual\_calls}(\cS))$.
1840: \end{theorem}
1841:
1842:
1843: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1844: \section{Implementation}
1845: \label{exp}
1846:
1847: \begin{table}
1848: \caption{Partial evaluator vs program slicer --- code structure} \label{pe-slicer}
1849: \begin{minipage}{\textwidth}
1850: \begin{tabular}{lrrrrrrr} \hline\hline
1851: & & \texttt{main} & \texttt{global} & \texttt{local} & \texttt{post}
1852: & \texttt{util} & \textbf{Total} \\\hline
1853: Partial evaluator & \emph{(lines)} & 306 & 403 & 888 & 433 & 316 & \textbf{2346} \\
1854: & \emph{(functions)} & 22 & 43 & 83 & 44 & 38 & \textbf{230} \\[2ex]
1855: Program slicer & \emph{(lines)} & 232 & 486 & 249 & 195 & 419 & \textbf{1581} \\
1856: & \emph{(functions)} & 20 & 50 & 29 & 26 & 55 & \textbf{180} \\ \hline\hline
1857: \end{tabular}
1858: \end{minipage}
1859: \end{table}
1860:
1861: In order to check the practicality of the ideas presented so far, a
1862: prototype implementation of the program slicer for Curry programs has
1863: been developed in Curry itself. The resulting tool covers not only the
1864: flat programs of Sect.~\ref{sec-foundations} but also source Curry
1865: programs (which are automatically translated to the flat syntax).
1866: Moreover, it also accepts higher-order functions, overlapping
1867: left-hand sides, several predefined (built-in) functions, etc. The
1868: implemented tool is publicly available from {\tt
1869: http://www.dsic.upv.es/users/elp/german/slicing/}.
1870:
1871: It is worthwhile to note that the development of the program slicer
1872: required a small implementation effort since it was developed by
1873: extending an existing partial evaluator for Curry programs
1874: \cite{AHV02}. Table~\ref{pe-slicer} shows the structure of both the
1875: partial evaluator and the program slicer, including the lines of code
1876: and the number of functions for each basic component:
1877: \begin{description}
1878: \item[\texttt{main:}] basic definitions and data type declarations,
1879: reading of source program, writing of transformed program, etc;
1880:
1881: \item[\texttt{global:}] global control, including termination tests and
1882: generalization operations;
1883:
1884: \item[\texttt{local:}] local control, i.e., a non-standard
1885: meta-interpreter;
1886:
1887: \item[\texttt{post:}] post-processing transformation, i.e., renaming
1888: and post-unfolding compression in the partial evaluator and
1889: extraction of the slice in the program slicer;
1890:
1891: \item[\texttt{util:}] general utilities and pretty printing.
1892: \end{description}
1893: %
1894: Basically, components \texttt{main}, \texttt{local}, and \texttt{util}
1895: were almost straightforwardly adapted from the partial evaluator to
1896: the program slicer. For instance, component \texttt{local} of the
1897: program slicer|which corresponds to the semantics shown in
1898: Fig.~\ref{smallstep}|is a simplified version of the same component in
1899: the partial evaluator, since only a one-step unfolding is required
1900: here. More significant changes were made in component \texttt{global}.
1901: In contrast to the partial evaluator, the program slicer introduces
1902: the use of \emph{states} and, thus, it required the implementation of
1903: rules \textsf{replace} and \textsf{flatten}, as well as the associated
1904: abstraction operator. Finally, component \texttt{post} of the partial
1905: evaluator was entirely replaced, since the program slicer does not
1906: perform neither renaming nor post-unfolding compression but should
1907: only extract the residual rules according to the calculus of
1908: Fig.~\ref{simplify-rules}.
1909:
1910: Our slicing tool is able to compute the slice of Example~\ref{lenapp},
1911: thus it is strictly more powerful than naive approaches based on
1912: graphs of functional dependences. In general, forward slicing has been
1913: proved particularly useful in the areas of program understanding, dead
1914: code removal, and code reuse. Now, we illustrate the application of
1915: the program slicer with some selected examples.
1916: %
1917: First, we consider the program of Example~\ref{lenapp} (in Curry
1918: syntax):
1919: %
1920: \startprog
1921: main Len xs = fst (lenmax xs)
1922: main Max xs = snd (lenmax xs)\\[-1ex]
1923:
1924: lenmax xs = (len xs, max xs)\\[-1ex]
1925:
1926: len [] = Z
1927: len (x:xs) = Succ (len xs)\\[-1ex]
1928:
1929: max [x] = x
1930: max (x:y:ys) = if (x $\sleq$ y) then max (y:ys)
1931: else max (x:ys)
1932:
1933: Z $\sleq$ m = True
1934: (Succ n) $\sleq$ Z = False
1935: (Succ n) $\sleq$ (Succ m) = n $\sleq$ m\\[-1ex]
1936:
1937: fst (a,b) = a
1938: snd (a,b) = b
1939: \stopprog
1940: %
1941: Given the slicing criterion ``\pr{main Len xs}'', our tool returns the
1942: following slice:
1943: %
1944: \startprog
1945: main Len xs = fst (lenmax xs)\\[-1ex]
1946:
1947: lenmax xs = (len xs, $\top$)\\[-1ex]
1948:
1949: len [] = Z
1950: len (x:xs) = Succ (len xs)\\[-1ex]
1951:
1952: fst (a,b) = a
1953: \stopprog
1954: %
1955: Here, the second rule of function \pr{main} as well as the definitions
1956: of functions \pr{max}, \pr{$\sleq$}, and \pr{snd} have been sliced
1957: away, since they are not needed when the first parameter of \pr{main}
1958: is the constant \pr{Len}. Note that the removal of \emph{case
1959: branches} in the flat language is now viewed in Curry as the removal
1960: of \emph{rules} in a function definition, e.g.,
1961: %
1962: \startprog
1963: main op xs = fcase op of $\{$ Len $\to$ fst (lenmax xs);
1964: Max $\to$ $\top$ $\}$
1965: \stopprog
1966: %
1967: is simply written as follows:
1968: %
1969: \startprog
1970: main Len xs = fst (lenmax xs)
1971: \stopprog
1972: %
1973: Let us now consider a similar situation but in a higher-order context:
1974: %
1975: \startprog
1976: trans p xs = map (f p) xs\\[-1ex]
1977:
1978: map f [] = []
1979: map f (x:xs) = f x : map f xs\\[-1ex]
1980:
1981: f A = inc
1982: f B = dec
1983: f C = square
1984: ...\\[-1ex]
1985:
1986: inc x = Succ x
1987: dec (Succ x) = x
1988: square x = x * x
1989: ...
1990: \stopprog
1991: %
1992: Function \pr{trans} applies a parametric function, \pr{f}, to all the
1993: elements of a given list. Now, the computed slice w.r.t.\ the slicing
1994: criterion ``$\tt trans\;A\;xs$'' is as follows:
1995: %
1996: \startprog
1997: trans p xs = map (f p) xs\\[-1ex]
1998:
1999: map f [] = []
2000: map f (x:xs) = f x : map f xs\\[-1ex]
2001:
2002: f A = inc\\[-1ex]
2003:
2004: inc x = Succ x
2005: \stopprog
2006: %
2007: Again, all functions but \pr{inc} and the first rule for \pr{f} have
2008: been deleted, which shows that our approach works well in the presence
2009: of higher-order functions.
2010: Finally, let us show an example which illustrates the removal of dead
2011: code due to lazy evaluation. Consider the following program:
2012: %
2013: \startprog
2014: lenInc n xs = len (incL n xs)\\[-1ex]
2015:
2016: len [] = Z
2017: len (x:xs) = Succ (len xs)\\[-1ex]
2018:
2019: incL n [] = []
2020: incL n (x:xs) = inc n : incL n xs\\[-1ex]
2021:
2022: inc x = Succ x
2023: \stopprog
2024: %
2025: Here, function \pr{lenInc} takes a number and a list, and returns the
2026: length of the list which results from adding the given number to each
2027: element of the original list. Clearly, in a lazy context, function
2028: \pr{inc} will never be executed. Therefore, the computed slice w.r.t.\
2029: ``$\tt lenInc\;n\;xs$'' (i.e., no input data is known) is as follows:
2030: %
2031: \startprog
2032: lenInc n xs = len (incL n xs)\\[-1ex]
2033:
2034: len [] = Z
2035: len (x:xs) = Succ (len xs)\\[-1ex]
2036:
2037: incL n [] = []
2038: incL n (x:xs) = $\top$ : incL n xs\\[-1ex]
2039: \stopprog
2040: %
2041: The occurrence of $\top$ in the definition of \pr{incL} shows that the
2042: values of the elements in the list are not needed to compute the
2043: length of the given list.
2044:
2045: \begin{table}
2046: \caption{Partial evaluator vs program slicer --- selected benchmarks} \label{times}
2047: \begin{minipage}{\textwidth} \footnotesize
2048: \begin{tabular}{lrrrrrrrr} \hline\hline
2049: & \multicolumn{1}{r}{\textsf{PE}} & \multicolumn{1}{r}{\textsf{Slicing}}
2050: & \multicolumn{3}{c}{\textsf{Runtime}} & \multicolumn{3}{c}{\textsf{Size}} \\ \cline{4-6} \cline{7-9}
2051: & \multicolumn{1}{r}{\textsf{time}}
2052: & \multicolumn{1}{r}{\textsf{time}}
2053: & \textsf{Orig} & \textsf{Spec} & \textsf{Sliced} & \textsf{Orig}
2054: & \textsf{Spec} & \textsf{Sliced} \\
2055: \textsf{Benchmark} & \textsf{ms} & \textsf{ms} & \textsf{ms} & \textsf{\%}
2056: & \textsf{\%} & \textsf{bytes} & \textsf{\%} & \textsf{\%} \\ \hline
2057: \texttt{ackermann} & 20490 & 1370 & 1330 & 98.50\% & 99.25\% & 2039 & 228.3\% & 49.93\% \\
2058: \texttt{allones} & 5090 & 1990 & 1140 & 111.40\% & 100.88\% & 3502 & 165.25\% & 63.42\% \\
2059: \texttt{fibonacci} & 150 & 270 & 380 & 81.58\% & 102.63\% & 2438 & 64.93 & 50.82\% \\
2060: \texttt{filtermap} & 280 & 450 & 1460 & 84.93\% & 100.00\% & 2147 & 28.50\% & 69.26\% \\
2061: \texttt{fliptree} & 2800 & 1230 & 1430 & 92.31\% & 93.71\% & 2619 & 202.33\% & 52.20\% \\
2062: \texttt{foldr.map} & 80 & 320 & 630 & 60.32\% & 100.00\% & 1784 & 21.41\% & 64.63\% \\
2063: \texttt{foldr.sq} & 70 & 310 & 670 & 65.67\% & 101.49\% & 1763 & 21.10\% & 64.61\% \\
2064: \texttt{foldr.sum} & 6730 & 1400 & 1570 & 80.25\% & 98.09\% & 4678 & 35.85\% & 13.92\% \\
2065: \texttt{funinter} & 504930 & 2220 & --- & --- & --- & 5288 & 657.19\% & 61.86\% \\
2066: \texttt{gauss} & 11680 & 950 & 700 & 82.86\% & 98.57\% & 2115 & 61.56\% & 42.36\% \\
2067: \texttt{iterate} & 1950 & 750 & 890 & 25.84\% & 103.37\% & 1968 & 117.99\% & 69.61\% \\
2068: \texttt{kmpAAB} & 710 & 990 & 380 & 31.58\% & 105.26\% & 3348 & 42.29\% & 75.30\% \\
2069: \texttt{kmpAAAAAAB} & 9870 & 3250 & 790 & 35.44\% & 100.00\% & 3968 & 104.86\% & 69.78\% \\
2070: \texttt{power} & 12710 & 890 & 620 & 95.16\% & 103.23\% & 2830 & 203.29\% & 46.93\% \\
2071: \texttt{quicksort}& 450 & 670 & 260 & 165.38\% & 103.85\% & 2711 & 84.06\% & 81.48\% \\
2072: \texttt{reverse}& 4590 & 970 & 680 & 98.53\% & 101.47\% & 1873 & 251.09\% & 53.87\% \\
2073: \hline
2074: \textbf{Average} & \textbf{36411} & \textbf{1127}
2075: & \textbf{862} & \hspace{-2ex}\textbf{80.65\%} & \hspace{-2ex}\textbf{100.79\%}
2076: & \textbf{2817} & \hspace{-2ex}\textbf{143.13\%} & \hspace{-2ex}\textbf{58.12\%} \\
2077: \hline\hline
2078: \end{tabular}
2079: \end{minipage}
2080: \vspace{-2ex}
2081: \end{table}
2082:
2083: Let us mention that, in contrast to the original partial evaluator,
2084: the implemented program slicer can deal with larger programs
2085: efficiently. This is mainly due to the monovariant/monogenetic nature
2086: of the underlying partial evaluator, which simplifies the computation
2087: of a closed set of terms. Table~\ref{times} shows a summary of the
2088: experiments conducted on an extensive set of benchmarks. We used the
2089: Curry$\to$Prolog compiler of PAKCS 1.6.0 \cite{PAKCS00} running on a
2090: 2.4 GHz Linux-PC (Intel Pentium IV with 512 KB cache). Runtime input
2091: goals were chosen to give a reasonably long overall time. Code size
2092: was obtained by measuring the intermediate FlatCurry files (suffix
2093: \texttt{.fcy}) generated by PAKCS. The considered benchmarks are
2094: available from {\tt http://www.dsic.upv.es/users/elp/german/slicing/}.
2095:
2096: The results in Table~\ref{times} show that the program slicer is in
2097: almost all cases much faster than the partial evaluation tool. As
2098: expected, the runtime of the sliced programs do not significantly
2099: differ from the runtimes of the original ones, since only some program
2100: rules (or expressions) have been deleted; this shows that little
2101: overhead has to be paid for adding extra functions to a program.
2102: Anyway, the main purpose of slicing is not speedup, but reducing code
2103: size. In this case, slicing has managed an overall code size
2104: reduction of 57.60\% whereas the partial evaluator has increased the
2105: code size by 162.26\%. Indeed, the slicing never increases the code
2106: size, while the partial evaluator has increased the code size by
2107: 657.18\% in the worst case. On the other hand, there are cases where
2108: specialization achieves much smaller code size than slicing, e.g., for
2109: \texttt{filtermap} where the specializer has managed to transform the
2110: composition of several higher-order functions into a single
2111: first-order function.
2112:
2113:
2114: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2115: \section{Related Work}
2116: \label{related}
2117:
2118: Although program slicing was originally introduced in the imperative
2119: programming setting, it has been applied to almost all programming
2120: paradigms, e.g., object-oriented programs \cite{TCFR96,LH96,Ste98},
2121: logic programs \cite{SD96,ZCU01}, functional programs
2122: \cite{Bis97,FT98}, or algebraic specifications \cite{WA98}. Although
2123: we are not aware of any previous work addressing forward slicing of
2124: multi-paradigm functional logic programs, in the following we review
2125: the closest approaches to our work.
2126:
2127: Within imperative programming, the closest approach is that of Blazy
2128: and Facon \citeyear{BF98}, who use partial evaluation for program
2129: understanding in Fortran. Since they do not want to change the
2130: original structure of the code, no unfolding is performed (similarly
2131: to our one-step unfoldings). Also, they neither introduce new
2132: variables nor rename the existing ones. In this work, we have followed
2133: a very similar approach in order to define a forward slicing algorithm
2134: for functional logic programs. In both approaches, a simplified
2135: partial evaluator that does not change the structure of the original
2136: program has been introduced.
2137:
2138: Within the logic programming paradigm, Gyim\'othy and Paakki
2139: \citeyear{GP95} introduce the first approach to slicing. They define a
2140: specific slicing algorithm which computes a slice of the proof tree in
2141: order to reduce the number of questions asked by an algorithmic
2142: debugger \cite{Sha83}. The slice is computed from a static dependency
2143: graph containing only oriented data dependencies. In contrast to our
2144: work, their algorithm cannot be not used to compute \emph{executable}
2145: programs. Schoening and Ducass\'e \citeyear{SD96} define the first
2146: (backward) slicing algorithm for Prolog programs which produce
2147: executable slices. They introduce an abstraction relation in order to
2148: formalize the notion of program slice. Our notion of slice in
2149: Section~\ref{pe} is somehow inspired by this work. Leuschel and
2150: S{\o}rensen \citeyear{LS96} introduce the concept of \emph{correct
2151: erasure} in order to detect and remove redundant arguments from
2152: logic programs. They present a constructive algorithm for computing
2153: correct erasures which can be used to perform a simple form of
2154: slicing. Actually, Leuschel and Vidal \citeyear{LV05} have very
2155: recently introduced a new approach to forward slicing of logic
2156: programs which is based on a combination of the ideas presented in
2157: this work and the redundant argument filtering of Leuschel and
2158: S{\o}rensen \citeyear{LS96}.
2159:
2160: As for functional programs, Field and Tip \citeyear{FT98} present a
2161: very detailed study of the concept of slicing associated with
2162: left-linear term rewriting systems (a notion of ``program'' very close
2163: to the one considered in our work). Their definition of slice is also
2164: based on a notion of \emph{neededness} but, in contrast to our work,
2165: they consider {backward} slicing (and compute slices that are not
2166: executable on the standard interpreter). Another closely related
2167: approach has been introduced by Reps and Turnidge \citeyear{RT96}.
2168: They define a {backward} slicing technique for functional programs
2169: which can be used to perform a sort of program specialization that
2170: cannot be achieved by standard partial evaluation. Their work can be
2171: seen as complementary to ours, since we are interested in the use of
2172: partial evaluation to perform program slicing. On the other hand,
2173: Hallgren \citeyear{Hal03} reports some experiments with a Haskell
2174: slicer. It is mainly based on the construction of a graph of
2175: functional dependences and, thus, it is less powerful than our partial
2176: evaluation-based slicer.
2177:
2178: Very recently, Ochoa et al.\ \citeyear{OSV04} have introduced a novel
2179: approach to \emph{dynamic} backward slicing of functional logic
2180: programs which is based on an extension of the tracing technique of
2181: Bra{\ss}el et al.\ \citeyear{BHHV04}. In particular, their approach
2182: relies on constructing a \emph{redex trail} of a given computation in
2183: order to compute all program dependences. Basically, a redex trail is
2184: a directed graph which records copies of all values and redexes of a
2185: computation, with a backward link from each reduct to the parent redex
2186: that created it. Then, a backward slice can easily be obtained by
2187: mapping the relevant nodes of the redex trail to concrete locations of
2188: the source program. This approach has also been applied to Haskell
2189: programs by Chitil \citeyear{Chi04}. These approaches are not based on
2190: partial evaluation but on well-known techniques for debugging
2191: functional programs. Therefore, the implementation of a
2192: \emph{dynamic} slicer is relatively easy if one already has a debugger
2193: based on redex trails. However, they are not useful in order to
2194: develop a \emph{static} slicing tool. In contrast, our approach can be
2195: used to perform both static and (forward) dynamic slicing.
2196:
2197:
2198:
2199: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2200: \section{Conclusions and Future Work}
2201: \label{sec-concl}
2202:
2203: This work introduced the first approach to forward slicing of
2204: multi-paradigm (functional logic) programs. Although some extensions
2205: were needed, our developments basically rely on adapting and extending
2206: an online partial evaluation scheme for such programs. Thus, the
2207: implementation of an associated slicing tool was easily achieved by
2208: extending an existing partial evaluation tool. Moreover, our approach
2209: helps to clarify the relation between program slicing and partial
2210: evaluation in a functional logic context. The application of our
2211: developments to (first-order) lazy functional programs would be
2212: straightforward, since the considered language is a conservative
2213: extension of a pure lazy functional language and the (online) partial
2214: evaluation techniques are similar, e.g., positive supercompilation
2215: \cite{SGJ93}. On the other hand, similar ideas have already been
2216: applied to define a forward slicing technique for logic programs
2217: \cite{LV05}.
2218:
2219: An interesting topic for future work is the extension of our approach
2220: to perform \emph{backward} slicing. Here, the computed slice should
2221: contain those program statements which are needed to compute some
2222: selected \emph{fragment} of the output. While forward slicing is
2223: useful for program understanding, reuse, maintenance, etc., backward
2224: slicing can be applied to, e.g., program debugging, specialization and
2225: merging.
2226:
2227:
2228: \subsection*{Acknowledgements}
2229:
2230: We gratefully acknowledge the anonymous referees as well as the
2231: participants of LOPSTR 2002 for many useful comments and suggestions.
2232: We also thank Michael Leuschel for his helpful remarks concerning the
2233: relation between partial deduction and slicing in the context of logic
2234: programming.
2235:
2236:
2237: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2238: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2239:
2240: %\bibliography{biblio}
2241:
2242: \begin{thebibliography}{}
2243:
2244: \bibitem[\protect\citeauthoryear{Albert, Hanus, Huch, Olvier, and Vidal}{Albert
2245: et~al\mbox{.}}{2005}]{AHHOV05}
2246: {\sc Albert, E.}, {\sc Hanus, M.}, {\sc Huch, F.}, {\sc Olvier, J.}, {\sc and}
2247: {\sc Vidal, G.} 2005.
2248: \newblock {Operational Semantics for Declarative Multi-Paradigm Languages}.
2249: \newblock {\em Journal of Symbolic Computation\/}~{\em 40,\/}~1, 795--829.
2250:
2251: \bibitem[\protect\citeauthoryear{Albert, Hanus, and Vidal}{Albert
2252: et~al\mbox{.}}{2002}]{AHV02}
2253: {\sc Albert, E.}, {\sc Hanus, M.}, {\sc and} {\sc Vidal, G.} 2002.
2254: \newblock A {P}ractical {P}artial {E}valuation {S}cheme for {M}ulti-{P}aradigm
2255: {D}eclarative {L}anguages.
2256: \newblock {\em Journal of Functional and Logic Programming\/}~{\em 2002,\/}~1.
2257:
2258: \bibitem[\protect\citeauthoryear{Albert, Hanus, and Vidal}{Albert
2259: et~al\mbox{.}}{2003}]{AHV03}
2260: {\sc Albert, E.}, {\sc Hanus, M.}, {\sc and} {\sc Vidal, G.} 2003.
2261: \newblock A {R}esidualizing {S}emantics for the {P}artial {E}valuation of
2262: {F}unctional {L}ogic {P}rograms.
2263: \newblock {\em Information Processing Letters\/}~{\em 85,\/}~1, 19--25.
2264:
2265: \bibitem[\protect\citeauthoryear{Albert and Vidal}{Albert and
2266: Vidal}{2002}]{AV02}
2267: {\sc Albert, E.} {\sc and} {\sc Vidal, G.} 2002.
2268: \newblock The {N}arrowing-{D}riven {A}pproach to {F}unctional {L}ogic {P}rogram
2269: {S}pecialization.
2270: \newblock {\em New Generation Computing\/}~{\em 20,\/}~1, 3--26.
2271:
2272: \bibitem[\protect\citeauthoryear{Alpuente, Falaschi, and Vidal}{Alpuente
2273: et~al\mbox{.}}{1998}]{AFV98}
2274: {\sc Alpuente, M.}, {\sc Falaschi, M.}, {\sc and} {\sc Vidal, G.} 1998.
2275: \newblock {P}artial {E}valuation of {F}unctional {L}ogic {P}rograms.
2276: \newblock {\em ACM TOPLAS\/}~{\em 20,\/}~4, 768--844.
2277:
2278: \bibitem[\protect\citeauthoryear{Antoy}{Antoy}{1992}]{Ant92}
2279: {\sc Antoy, S.} 1992.
2280: \newblock Definitional trees.
2281: \newblock In {\em Proc. of the 3rd Int'l Conference on Algebraic and Logic
2282: Programming (ALP'92)}. Springer LNCS 632, 143--157.
2283:
2284: \bibitem[\protect\citeauthoryear{Antoy, Echahed, and Hanus}{Antoy
2285: et~al\mbox{.}}{2000}]{AEH00}
2286: {\sc Antoy, S.}, {\sc Echahed, R.}, {\sc and} {\sc Hanus, M.} 2000.
2287: \newblock A {N}eeded {N}arrowing {S}trategy.
2288: \newblock {\em Journal of the {ACM}\/}~{\em 47,\/}~4, 776--822.
2289:
2290: \bibitem[\protect\citeauthoryear{Baader and Nipkow}{Baader and
2291: Nipkow}{1998}]{BN98}
2292: {\sc Baader, F.} {\sc and} {\sc Nipkow, T.} 1998.
2293: \newblock {\em Term Rewriting and All That}.
2294: \newblock Cambridge University Press.
2295:
2296: \bibitem[\protect\citeauthoryear{Biswas}{Biswas}{1997}]{Bis97}
2297: {\sc Biswas, S.} 1997.
2298: \newblock {Dynamic Slicing in Higher-Order Programming Languages}.
2299: \newblock Ph.D. thesis, University of Pennsylvania.
2300:
2301: \bibitem[\protect\citeauthoryear{Blazy and Facon}{Blazy and Facon}{1998}]{BF98}
2302: {\sc Blazy, S.} {\sc and} {\sc Facon, P.} 1998.
2303: \newblock {Partial Evaluation for Program Comprehension}.
2304: \newblock {\em ACM Computing Surveys\/}~{\em 30,\/}~3es.
2305:
2306: \bibitem[\protect\citeauthoryear{Brassel, Hanus, Huch, and Vidal}{Brassel
2307: et~al\mbox{.}}{2004}]{BHHV04}
2308: {\sc Brassel, B.}, {\sc Hanus, M.}, {\sc Huch, F.}, {\sc and} {\sc Vidal, G.}
2309: 2004.
2310: \newblock {A Semantics for Tracing Declarative Multi-Paradigm Programs}.
2311: \newblock In {\em Proc.\ of the 6th ACM SIGPLAN Conference on Principles and
2312: Practice of Declarative Programming (PPDP'04)}. ACM Press, 179--190.
2313:
2314: \bibitem[\protect\citeauthoryear{Chitil}{Chitil}{2004}]{Chi04}
2315: {\sc Chitil, O.} 2004.
2316: \newblock {Source-Based Trace Exploration}.
2317: \newblock In {\em In Draft Proc.\ of the 16th Int'l Workshop on Implementation
2318: of Functional Languages (IFL 2004)}. Technical Report 0408, University of
2319: Kiel, 239--244.
2320:
2321: \bibitem[\protect\citeauthoryear{Ferrante, Ottenstein, and Warren}{Ferrante
2322: et~al\mbox{.}}{1987}]{FOW87}
2323: {\sc Ferrante, J.}, {\sc Ottenstein, K.}, {\sc and} {\sc Warren, J.} 1987.
2324: \newblock The {P}rogram {D}ependence {G}raph and {I}ts {U}se in {O}ptimization.
2325: \newblock {\em ACM Transactions on Programming Languages and Systems\/}~{\em
2326: 9,\/}~3, 319--349.
2327:
2328: \bibitem[\protect\citeauthoryear{Field and Tip}{Field and Tip}{1998}]{FT98}
2329: {\sc Field, J.} {\sc and} {\sc Tip, F.} 1998.
2330: \newblock {Dynamic Dependence in Term Rewriting Systems and its Application to
2331: Program Slicing}.
2332: \newblock {\em Information and Software Technology\/}~{\em 40,\/}~11-12,
2333: 609--634.
2334:
2335: \bibitem[\protect\citeauthoryear{Gallagher}{Gallagher}{1993}]{Gal93}
2336: {\sc Gallagher, J.} 1993.
2337: \newblock Tutorial on {S}pecialisation of {L}ogic {P}rograms.
2338: \newblock In {\em Proc.\ of the ACM Symp.\ on Partial Evaluation and
2339: Seman\-tics-Based Program Manipulation (PEPM'93)}. ACM, New York, 88--98.
2340:
2341: \bibitem[\protect\citeauthoryear{Giovannetti, Levi, Moiso, and
2342: Palamidessi}{Giovannetti et~al\mbox{.}}{1991}]{GLMP91}
2343: {\sc Giovannetti, E.}, {\sc Levi, G.}, {\sc Moiso, C.}, {\sc and} {\sc
2344: Palamidessi, C.} 1991.
2345: \newblock Kernel {L}eaf: {A} {Logic} plus {F}unctional {L}anguage.
2346: \newblock {\em Journal of Computer and System Sciences\/}~{\em 42}, 363--377.
2347:
2348: \bibitem[\protect\citeauthoryear{Gl{\"u}ck and S{\o}rensen}{Gl{\"u}ck and
2349: S{\o}rensen}{1996}]{GS96}
2350: {\sc Gl{\"u}ck, R.} {\sc and} {\sc S{\o}rensen, M.} 1996.
2351: \newblock A {R}oadmap to {M}etacomputation by {S}upercompilation.
2352: \newblock In {\em Partial Evaluation, Int'l Seminar, Dagstuhl Castle, Germany},
2353: {O.~Danvy}, {R.~Gl{\"u}ck}, {and} {P.~Thiemann}, Eds. Springer LNCS 1110,
2354: 137--160.
2355:
2356: \bibitem[\protect\citeauthoryear{Gyim\'othy and Paakki}{Gyim\'othy and
2357: Paakki}{1995}]{GP95}
2358: {\sc Gyim\'othy, T.} {\sc and} {\sc Paakki, J.} 1995.
2359: \newblock {Static Slicing of Logic Programs}.
2360: \newblock In {\em Proc.\ of the 2nd Int'l Workshop on Automated and Algorithmic
2361: Debugging (AADEBUG'95)}. IRISA-CNRS, 87--103.
2362:
2363: \bibitem[\protect\citeauthoryear{Hallgren}{Hallgren}{2003}]{Hal03}
2364: {\sc Hallgren, T.} 2003.
2365: \newblock {Haskell Tools from the Programatica Project}.
2366: \newblock In {\em Proc.\ of the 2003 {ACM} {SIGPLAN} Haskell Workshop}. ACM
2367: Press, 103--106.
2368:
2369: \bibitem[\protect\citeauthoryear{Hanus}{Hanus}{1994}]{Han94JLP}
2370: {\sc Hanus, M.} 1994.
2371: \newblock The {I}ntegration of {F}unctions into {L}ogic {P}rogramming: {F}rom
2372: {T}heory to {P}ractice.
2373: \newblock {\em Journal of Logic Programming\/}~{\em 19\&20}, 583--628.
2374:
2375: \bibitem[\protect\citeauthoryear{Hanus}{Hanus}{1997}]{Han97b}
2376: {\sc Hanus, M.} 1997.
2377: \newblock A {U}nified {C}omputation {M}odel for {F}unctional and {L}ogic
2378: {P}rogramming.
2379: \newblock In {\em Proc.\ of ACM Symp.\ on Principles of Programming Languages
2380: (POPL'97)}. ACM, New York, 80--93.
2381:
2382: \bibitem[\protect\citeauthoryear{Hanus}{Hanus}{2003}]{CurryTR}
2383: {\sc Hanus, M.} 2003.
2384: \newblock Curry: {A}n {I}ntegrated {F}unctional {L}ogic {L}anguage.
2385: \newblock Available at: \\ \verb+http://www.informatik.uni-kiel.de/~mh/curry/+.
2386:
2387: \bibitem[\protect\citeauthoryear{Hanus, Antoy, Engelke, H\"{o}ppner, Koj,
2388: {\protect Niederau}, Sadre, and Steiner}{Hanus et~al\mbox{.}}{2004}]{PAKCS00}
2389: {\sc Hanus, M.}, {\sc Antoy, S.}, {\sc Engelke, M.}, {\sc H\"{o}ppner, K.},
2390: {\sc Koj, J.}, {\sc {\protect Niederau}, P.}, {\sc Sadre, R.}, {\sc and} {\sc
2391: Steiner, F.} 2004.
2392: \newblock {PAKCS} 1.6.0: The {P}ortland {A}achen {K}iel {C}urry {S}ystem {U}ser
2393: {M}anual.
2394: \newblock Tech. rep., University of Kiel, Germany.
2395:
2396: \bibitem[\protect\citeauthoryear{Hanus and Prehofer}{Hanus and
2397: Prehofer}{1999}]{HP99}
2398: {\sc Hanus, M.} {\sc and} {\sc Prehofer, C.} 1999.
2399: \newblock Higher-{O}rder {N}arrowing with {D}efinitional {T}rees.
2400: \newblock {\em Journal of Functional Programming\/}~{\em 9,\/}~1, 33--75.
2401:
2402: \bibitem[\protect\citeauthoryear{Harman and Danicic}{Harman and
2403: Danicic}{1997}]{HD97}
2404: {\sc Harman, M.} {\sc and} {\sc Danicic, S.} 1997.
2405: \newblock {Amorphous Program Slicing}.
2406: \newblock In {\em Proc.\ of the 5th Int'l Workshop on Program Comprehension}.
2407: IEEE Computer Society Press.
2408:
2409: \bibitem[\protect\citeauthoryear{Harman, Danicic, and Sivagurunathan}{Harman
2410: et~al\mbox{.}}{1995}]{HDS95}
2411: {\sc Harman, M.}, {\sc Danicic, S.}, {\sc and} {\sc Sivagurunathan, Y.} 1995.
2412: \newblock {Program Comprehension Assisted by Slicing and Transformation}.
2413: \newblock In {\em Proc.\ of the 1st UK Program Comprehension Workshop}.
2414:
2415: \bibitem[\protect\citeauthoryear{Harman and Hierons}{Harman and
2416: Hierons}{2001}]{HH01}
2417: {\sc Harman, M.} {\sc and} {\sc Hierons, R.} 2001.
2418: \newblock {An Overview of Program Slicing}.
2419: \newblock {\em Software Focus\/}~{\em 2,\/}~3, 85--92.
2420:
2421: \bibitem[\protect\citeauthoryear{Hortal\'a-Gonz\'alez and
2422: Ull\'an}{Hortal\'a-Gonz\'alez and Ull\'an}{2001}]{HU01}
2423: {\sc Hortal\'a-Gonz\'alez, T.} {\sc and} {\sc Ull\'an, E.} 2001.
2424: \newblock An {A}bstract {M}achine {B}ased {S}ystem for a {L}azy {N}arrowing
2425: {C}alculus.
2426: \newblock In {\em Proc.\ of the 5th Int'l Symp.\ on Functional and Logic
2427: Programming (FLOPS 2001)}. Springer LNCS 2024, 216--232.
2428:
2429: \bibitem[\protect\citeauthoryear{Huet and L{\'e}vy}{Huet and
2430: L{\'e}vy}{1992}]{HL92}
2431: {\sc Huet, G.} {\sc and} {\sc L{\'e}vy, J.} 1992.
2432: \newblock Computations in orthogonal rewriting systems, {Part I + II}.
2433: \newblock In {\em Computational Logic -- Essays in Honor of Alan Robinson},
2434: {J.~Lassez} {and} {G.~Plotkin}, Eds. 395--443.
2435:
2436: \bibitem[\protect\citeauthoryear{Jones, Gomard, and Sestoft}{Jones
2437: et~al\mbox{.}}{1993}]{JGS93}
2438: {\sc Jones, N.}, {\sc Gomard, C.}, {\sc and} {\sc Sestoft, P.} 1993.
2439: \newblock {\em Partial {E}valuation and {A}utomatic {P}rogram {G}eneration}.
2440: \newblock Prentice-Hall, Englewood Cliffs, NJ.
2441:
2442: \bibitem[\protect\citeauthoryear{Klop}{Klop}{1992}]{Klo91}
2443: {\sc Klop, J.} 1992.
2444: \newblock Term {R}ewriting {S}ystems.
2445: \newblock In {\em Handbook of Logic in Computer Science}, {S.~Abramsky},
2446: {D.~Gabbay}, {and} {T.~Maibaum}, Eds. Vol.~I. Oxford University Press,
2447: 1--112.
2448:
2449: \bibitem[\protect\citeauthoryear{Kuck, Kuhn, Padua, Leasure, and Wolfe}{Kuck
2450: et~al\mbox{.}}{1981}]{KKPLW81}
2451: {\sc Kuck, D.}, {\sc Kuhn, R.}, {\sc Padua, D.}, {\sc Leasure, B.}, {\sc and}
2452: {\sc Wolfe, M.} 1981.
2453: \newblock Dependence {G}raphs and {C}ompiler {O}ptimization.
2454: \newblock In {\em Proc.\ of the 8th Symp.\ on the Principles of Programming
2455: Languages (POPL'81), SIGPLAN Notices}. 207--218.
2456:
2457: \bibitem[\protect\citeauthoryear{Larsen and Harrold}{Larsen and
2458: Harrold}{1996}]{LH96}
2459: {\sc Larsen, L.} {\sc and} {\sc Harrold, M.~J.} 1996.
2460: \newblock Slicing object-oriented software.
2461: \newblock In {\em Proc.\ of the 18th Int'l Conf.\ on Software engineering
2462: (ICSE'96)}. IEEE Computer Society, 495--505.
2463:
2464: \bibitem[\protect\citeauthoryear{Leuschel}{Leuschel}{2002}]{Leu02}
2465: {\sc Leuschel, M.} 2002.
2466: \newblock {Homeomorphic Embedding for Online Termination of Symbolic Methods}.
2467: \newblock In {\em The Essence of Computation, Complexity, Analysis,
2468: Transformation. Essays Dedicated to Neil D. Jones}. Springer LNCS 2566,
2469: 379--403.
2470:
2471: \bibitem[\protect\citeauthoryear{Leuschel and S{\o}rensen}{Leuschel and
2472: S{\o}rensen}{1996}]{LS96}
2473: {\sc Leuschel, M.} {\sc and} {\sc S{\o}rensen, M.} 1996.
2474: \newblock Redundant {A}rgument {F}iltering of {L}ogic {P}rograms.
2475: \newblock In {\em Proc.\ of the Int'l Workshop on Logic-Based Program Synthesis
2476: and Transformation (LOPSTR'96)}. Springer LNCS 1207, 83--103.
2477:
2478: \bibitem[\protect\citeauthoryear{Leuschel and Vidal}{Leuschel and
2479: Vidal}{2005}]{LV05}
2480: {\sc Leuschel, M.} {\sc and} {\sc Vidal, G.} 2005.
2481: \newblock {Forward Slicing by Conjunctive Partial Deduction and Argument
2482: Filtering}.
2483: \newblock In {\em Proc. of the European Symposium on Programming (ESOP 2005)}.
2484: Springer LNCS 3444, 61--76.
2485:
2486: \bibitem[\protect\citeauthoryear{Lloyd}{Lloyd}{1994}]{Llo94}
2487: {\sc Lloyd, J.} 1994.
2488: \newblock Combining {F}unctional and {L}ogic {P}rogramming {L}anguages.
2489: \newblock In {\em Proc. of the International Logic Programming Symposium}.
2490: 43--57.
2491:
2492: \bibitem[\protect\citeauthoryear{Loogen, L{\'o}pez{-F}raguas, and
2493: Rodr{\'{\i}}guez{-A}rtalejo}{Loogen et~al\mbox{.}}{1993}]{LLR93}
2494: {\sc Loogen, R.}, {\sc L{\'o}pez{-F}raguas, F.}, {\sc and} {\sc
2495: Rodr{\'{\i}}guez{-A}rtalejo, M.} 1993.
2496: \newblock A {D}emand {D}riven {C}omputation {S}trategy for {L}azy {N}arrowing.
2497: \newblock In {\em Proc.\ of PLILP'93}. Springer LNCS 714, 184--200.
2498:
2499: \bibitem[\protect\citeauthoryear{L\'opez-Fraguas and
2500: S\'anchez-Hern\'andez}{L\'opez-Fraguas and
2501: S\'anchez-Hern\'andez}{1999}]{LS99}
2502: {\sc L\'opez-Fraguas, F.} {\sc and} {\sc S\'anchez-Hern\'andez, J.} 1999.
2503: \newblock {TOY}: {A} {M}ultiparadigm {D}eclarative {S}ystem.
2504: \newblock In {\em Proc.\ of RTA'99}. Springer LNCS 1631, 244--247.
2505:
2506: \bibitem[\protect\citeauthoryear{Moreno{-N}avarro and
2507: Rodr{\'{\i}}guez{-A}rtalejo}{Moreno{-N}avarro and
2508: Rodr{\'{\i}}guez{-A}rtalejo}{1992}]{MR92}
2509: {\sc Moreno{-N}avarro, J.} {\sc and} {\sc Rodr{\'{\i}}guez{-A}rtalejo, M.}
2510: 1992.
2511: \newblock Logic {P}rogramming with {Functions} and {P}redicates: The language
2512: {B}abel.
2513: \newblock {\em Journal of Logic Programming\/}~{\em 12,\/}~3, 191--224.
2514:
2515: \bibitem[\protect\citeauthoryear{Ochoa, Silva, and Vidal}{Ochoa
2516: et~al\mbox{.}}{2004}]{OSV04}
2517: {\sc Ochoa, C.}, {\sc Silva, J.}, {\sc and} {\sc Vidal, G.} 2004.
2518: \newblock {Dynamic Slicing Based on Redex Trails}.
2519: \newblock In {\em Proc.\ of the ACM SIGPLAN 2004 Symposium on Partial
2520: Evaluation and Program Manipulation (PEPM'04)}. ACM Press, 123--134.
2521:
2522: \bibitem[\protect\citeauthoryear{Reps and Turnidge}{Reps and
2523: Turnidge}{1996}]{RT96}
2524: {\sc Reps, T.} {\sc and} {\sc Turnidge, T.} 1996.
2525: \newblock Program {S}pecialization via {P}rogram {S}licing.
2526: \newblock In {\em Partial Evaluation. Dagstuhl Castle, Germany, February 1996},
2527: {O.~Danvy}, {R.~Gl{\"u}ck}, {and} {P.~Thiemann}, Eds. Springer LNCS 1110,
2528: 409--429.
2529:
2530: \bibitem[\protect\citeauthoryear{Schoenig and Ducasse}{Schoenig and
2531: Ducasse}{1996}]{SD96}
2532: {\sc Schoenig, S.} {\sc and} {\sc Ducasse, M.} 1996.
2533: \newblock A {B}ackward {S}licing {A}lgorithm for {P}rolog.
2534: \newblock In {\em Proc.\ of the Int'l Static Analysis Symposium (SAS'96)}.
2535: Springer LNCS 1145, 317--331.
2536:
2537: \bibitem[\protect\citeauthoryear{Sestoft}{Sestoft}{1997}]{Ses97}
2538: {\sc Sestoft, P.} 1997.
2539: \newblock Deriving a {L}azy {A}bstract {M}achine.
2540: \newblock {\em Journal of Functional Programming\/}~{\em 7,\/}~3, 231--264.
2541:
2542: \bibitem[\protect\citeauthoryear{Shapiro}{Shapiro}{1983}]{Sha83}
2543: {\sc Shapiro, E.} 1983.
2544: \newblock {\em {Algorithmic Program Debugging}}.
2545: \newblock MIT Press, Cambridge, MA.
2546:
2547: \bibitem[\protect\citeauthoryear{S{\o}rensen, Gl{\"u}ck, and Jones}{S{\o}rensen
2548: et~al\mbox{.}}{1996}]{SGJ93}
2549: {\sc S{\o}rensen, M.}, {\sc Gl{\"u}ck, R.}, {\sc and} {\sc Jones, N.} 1996.
2550: \newblock A {P}ositive {S}upercompiler.
2551: \newblock {\em Journal of Functional Programming\/}~{\em 6,\/}~6, 811--838.
2552:
2553: \bibitem[\protect\citeauthoryear{Steindl}{Steindl}{1998}]{Ste98}
2554: {\sc Steindl, C.} 1998.
2555: \newblock {Intermodular Slicing of Object-oriented Programs}.
2556: \newblock In {\em Proc.\ of the 7th Int'l Conf.\ on Compiler Construction
2557: (CC'98)}. Springer LNCS 1383, 264--279.
2558:
2559: \bibitem[\protect\citeauthoryear{Terese}{Terese}{2003}]{Ter03}
2560: {\sc Terese}. 2003.
2561: \newblock {\em Term Rewriting Systems}.
2562: \newblock Cambridge University Press.
2563:
2564: \bibitem[\protect\citeauthoryear{Tip}{Tip}{1995}]{Tip95}
2565: {\sc Tip, F.} 1995.
2566: \newblock A {S}urvey of {P}rogram {S}licing {T}echniques.
2567: \newblock {\em Journal of Programming Languages\/}~{\em 3}, 121--189.
2568:
2569: \bibitem[\protect\citeauthoryear{Tip, Choi, Field, and Ramalingam}{Tip
2570: et~al\mbox{.}}{1996}]{TCFR96}
2571: {\sc Tip, F.}, {\sc Choi, J.-D.}, {\sc Field, J.}, {\sc and} {\sc Ramalingam,
2572: G.} 1996.
2573: \newblock {Slicing class hierarchies in C++}.
2574: \newblock {\em SIGPLAN Notices\/}~{\em 31,\/}~10, 179--197.
2575:
2576: \bibitem[\protect\citeauthoryear{Turchin}{Turchin}{1986}]{Tur86b}
2577: {\sc Turchin, V.} 1986.
2578: \newblock The {C}oncept of a {S}upercompiler.
2579: \newblock {\em ACM Transactions on Programming Languages and Systems\/}~{\em
2580: 8,\/}~3 (July), 292--325.
2581:
2582: \bibitem[\protect\citeauthoryear{Venkatesh}{Venkatesh}{1991}]{Ven91}
2583: {\sc Venkatesh, G.} 1991.
2584: \newblock {The Semantic Approach to Program Slicing}.
2585: \newblock {\em SIGPLAN Notices\/}~{\em 26,\/}~6, 107--119.
2586: \newblock {\em Proc.\ of the ACM SIGPLAN Conf.\ on Programming Language Design
2587: and Implementation (PLDI'91)}.
2588:
2589: \bibitem[\protect\citeauthoryear{Weiser}{Weiser}{1979}]{Wei79}
2590: {\sc Weiser, M.} 1979.
2591: \newblock Program {S}lices: {F}ormal, {P}sychological, and {P}ractical
2592: {I}nvestigations of an {A}utomatic {P}rogram {A}bstraction {M}ethod.
2593: \newblock Ph.D. thesis, The University of Michigan.
2594:
2595: \bibitem[\protect\citeauthoryear{Weiser}{Weiser}{1984}]{Wei84}
2596: {\sc Weiser, M.} 1984.
2597: \newblock Program {S}licing.
2598: \newblock {\em IEEE Transactions on Software Engineering\/}~{\em 10,\/}~4,
2599: 352--357.
2600:
2601: \bibitem[\protect\citeauthoryear{Woodward and Allen}{Woodward and
2602: Allen}{1998}]{WA98}
2603: {\sc Woodward, M.~R.} {\sc and} {\sc Allen, S.~P.} 1998.
2604: \newblock Slicing algebraic specifications.
2605: \newblock {\em Information and Software Technology\/}~{\em 40,\/}~2, 105--118.
2606:
2607: \bibitem[\protect\citeauthoryear{Zhao, Cheng, and Ushijima}{Zhao
2608: et~al\mbox{.}}{2001}]{ZCU01}
2609: {\sc Zhao, J.}, {\sc Cheng, J.}, {\sc and} {\sc Ushijima, K.} 2001.
2610: \newblock {A Program Dependence Model for Concurrent Logic Programs and Its
2611: Applications}.
2612: \newblock In {\em Proc.\ of IEEE Int'l Conf.\ on Software Maintenance
2613: (ICSM'01)}. IEEE Press, 672--681.
2614:
2615: \end{thebibliography}
2616:
2617:
2618: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2619: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2620:
2621: \newpage
2622: \appendix
2623:
2624: \section{Proofs of technical results} \label{proofs}
2625:
2626:
2627: \mbox{}\\
2628: \textsl{Lemma \ref{flattened-states}}\\
2629: %%\begin{lemma} \label{flattened-states}
2630: Let $s$ be a flattened state. Then $s$ has the form
2631: $\tuple{v,\nil}$, where $v$ is a value, or $\tuple{f(\ol{t_{n}}),S}$,
2632: where $f(\ol{t_{n}})$ is an operation-rooted term.
2633: %%\end{lemma}
2634:
2635: \begin{proof}
2636: We prove the claim by contradiction. Let $s$ be a flattened state of
2637: the form $\tuple{v,S}$ where $v$ is a value and $S$ is not empty.
2638: Then rule {\sf replace} could be applied to $s$, thus contradicting
2639: the hypothesis of the lemma. Thus, $s$ should be of the form
2640: $\tuple{v,\nil}$ or $\tuple{e,S}$, where $e$ is not a value. To show
2641: that $e$ must be an operation-rooted term, it suffices to consider
2642: that rules {\sf replace} and {\sf flatten} do not return case
2643: expressions (only operation-rooted terms) and that the initial state
2644: cannot contain case expressions (since it was returned by the
2645: operator $\foo{unfold}$).
2646: \end{proof}
2647:
2648: \mbox{}\\
2649: \textsl{Lemma \ref{safe-abstract}}\\
2650: %%\begin{lemma} \label{safe-abstract}
2651: Let $\cS$ be a set of flattened states and $\cS'$ a set of unfolded
2652: states (as returned by unfold). Then the
2653: states in $\cS \cup \cS'$ are closed w.r.t.\
2654: $\foo{abstract}(\cS,\cS')$.\\
2655: %%\end{lemma}
2656:
2657: \noindent
2658: In order to prove this lemma, we first need the following preparatory
2659: definitions and results. We use the notation $depth(t)$ to denote the
2660: maximum number of nested symbols in the term $t$. Formally, if $t$ is
2661: a constant or a variable, then $depth(t) = 1$. Otherwise,
2662: $depth(f(\ol{t_{n}})) = 1 + max (\{depth(t_1),\ldots, depth(t_n)\})$.
2663: The following result establishes the transitivity of the closedness
2664: relation on terms.
2665:
2666: \begin{proposition}[Alpuente et al.\ 1998] \label{transi-closs}
2667: If term $t$ is $T_1$-closed, and the terms in $T_1$ are
2668: $T_2$-closed, then $t$ is $T_2$-closed.
2669: \end{proposition}
2670: %
2671: We define the complexity $\cM_{T}$ of a set of terms $T$ as the finite
2672: multiset of natural numbers corresponding to the depth of the
2673: elements of $T$. Formally, $\cM_{T}= \{depth(t)\mid t\in T\}$.
2674: We consider the well-founded total ordering $\mathop{<}_{mul}$ over
2675: multiset complexities by extending the well-founded ordering $<$ on
2676: $\nat$ to the set $M(\nat)$ of finite multisets over $\nat$. The
2677: set $M(\nat)$ is well-founded under the ordering $\mathop{<}_{mul}$
2678: since $\nat$ is well-founded under $<$.
2679: % \cite{DJ90}.
2680: Let $\cM, \cM'$ be multiset complexities, then: $\cM \mathop{<}_{mul}
2681: \cM' \;\Leftrightarrow\; \exists X \subseteq \cM, X' \subseteq \cM'$
2682: such that $\cM = (\cM' - X') \cup X\:$ and $\:\forall n \in X,
2683: \:\:\exists n' \in X'$ such that $n < n'$. This ordering is naturally
2684: extended to sets of states by simply considering the terms represented
2685: by the states in each set.
2686:
2687: Now, we can proceed with proof of Lemma~\ref{safe-abstract}. We follow
2688: the scheme of the proof of Lemma~5.13 in \cite{AFV98} but extend it to
2689: deal with states:
2690:
2691: \begin{proof}
2692: We proceed by structural induction on $\cS \cup \cS'$. Since the base case is
2693: trivial ($\cS$ is always $\cS$-closed), we consider the inductive
2694: case. Let $\cS'' = \{s'_{1},\ldots,s'_{n}\}$, $n>1$, be the set of
2695: states resulting from flattening the states in $\cS'$, i.e.,
2696: $\cS'' = \{ s'_{i} \mid s_{i} \in \cS' \mbox{ and } s_{i}
2697: \Longrightarrow^\ast_{\sf replace/flatten}
2698: % s''_{i}\Longrightarrow^\ast_{\sf flatten}
2699: s'_{i} \not\Longrightarrow_{\sf replace/flatten} \}$. Trivially, we
2700: have that $\cM_{\cS'} = \cM_{\cS''}$ and that $\cS \cup \cS'$ is
2701: closed w.r.t.\ $\cS \cup \cS''$, since the process of flattening does
2702: not change the terms represented by the states. By the definition of
2703: $\foo{abstract}$, we have the following equalities:
2704: \[
2705: \begin{array}{lll}
2706: \foo{abstract}(\cS,\cS') & = & \foo{abstract}(\cS,\cS'') \\
2707: & = & \foo{abs}(\foo{abs}(\ldots \foo{abs}(\cS,s'_{1})\ldots,
2708: s'_{n-1}),s'_{n}) \\
2709: & = & \foo{abs}(\foo{abstract}(\cS,\cS'' \:\backslash \:
2710: \{s'_{n}\}), s'_{n}) \\
2711: & = & \foo{abs}(\cS^\ast,s'_{n})
2712: \end{array}
2713: \]
2714: where $\cS^\ast = \foo{abstract}(\cS,\cS'' \:\backslash \:
2715: \{s'_{n}\})$ and
2716: $s'_{n}$ is an arbitrary state of $\cS''$. By the
2717: inductive hypothesis, we know that $\cS \cup (\cS'' \:\backslash\:
2718: \{s'_{n}\})$ is closed w.r.t.\ $\cS^\ast$. Now, we proceed with the
2719: call $\foo{abs}(\cS^\ast,s'_{n})$. Here, we distinguish the
2720: following cases depending on the structure of $s'_{n}$:
2721: \begin{description}
2722: \item[\sf $s'_{n} = \tuple{x,\nil}$:] Then
2723: $\foo{abs}(\cS^\ast,s'_{n}) = \cS^\ast$ and the claim follows by
2724: Lemma~\ref{transi-closs}.
2725:
2726:
2727: \item[\sf $s'_{n} = \tuple{c(\ol{t_{n}}), \nil}$:] Assume that
2728: $\ol{t'_{m}}$ are the maximal operation-rooted subterms of
2729: $c(\ol{t_{n}})$. Then $\foo{abs}(\cS^\ast,s'_{n}) =
2730: \foo{abstract}(\cS^\ast, \cS^c)$, with $\cS^c = \{
2731: \ol{\tuple{t'_{m},\nil}}\}$. Since $\cM_{\cS^\ast \cup \cS^c}$
2732: $\mathop{<}_{mul} \cM_{\cS^\ast \cup \{s'_{n}\}}$, the proof follows
2733: by Lemma~\ref{transi-closs} and the inductive hypothesis.
2734:
2735: \item[\sf $s'_{n} = \tuple{f(\ol{t_{n}}),S}$:] Then, following the
2736: definition of function $\foo{abs}$, we consider three
2737: possibilities:
2738: \begin{itemize}
2739: \item If there is no state in $\cS^\ast$ whose first component is
2740: rooted by $f$, then $\foo{abs}(\cS^\ast,s'_{n}) = \cS^\ast \cup
2741: \{s'_{n}\}$. Thus, the claim follows by Lemma~\ref{transi-closs}.
2742:
2743: \item If the state is ignored (because it is already closed and it is not
2744: equal to any existing state), then $\foo{abs}(\cS^\ast,s'_{n}) =
2745: \cS^\ast$.
2746: Again, the claim follows trivially by Lemma~\ref{transi-closs}.
2747:
2748: \item Otherwise, there exists some state $\tuple{f(\ol{t'_{n}}),S'}$
2749: and\\[2ex]
2750: $
2751: \mbox{}\hspace{2em}
2752: \foo{abs}(\cS^\ast,s'_{n}) = \foo{abstract}((\cS^\ast \:
2753: \backslash
2754: \:\{\tuple{f(\ol{t'_{n}}),S'}\})\cup\{\tuple{f(\ol{t''_{n}}),S'}\},\cS^f)
2755: $\\[2ex]
2756: where
2757: $\foo{msg}(\tuple{f(\ol{t'_{n}}),S'},\tuple{f(\ol{t_{n}}),S}) =
2758: (\tuple{f(\ol{t''_{n}}),S'},\cS^f)$,
2759: $\cS^f = \foo{calls}(\sigma_{1}) \cup$ \linebreak
2760: $\foo{calls}(\sigma_{2}) \cup \foo{calls}(S)$,
2761: $\foo{msg}(f(\ol{t'_{n}}), f(\ol{t_{n}})) = f(\ol{t''_{n}})$,
2762: $\sigma_{1}(f(\ol{t''_{n}})) = f(\ol{t'_{n}})$, and
2763: $\sigma_{2}(f(\ol{t''_{n}})) = f(\ol{t_{n}})$. Now, by definition of
2764: function \emph{msg}, it is easy to check that $\cS^\ast \cup
2765: \{s'_{n}\}$ is closed w.r.t.\ $(\cS^\ast \: \backslash
2766: \:\{\tuple{f(\ol{t'_{n}}),S'}\})\cup
2767: \{\tuple{f(\ol{t''_{n}}),S'}\}\cup \cS^f$ and that $\cM_{(\cS^\ast \:
2768: \backslash \:\{\tuple{f(\ol{t'_{n}}),S'}\})\cup
2769: \{\tuple{f(\ol{t''_{n}}),S'}\}\cup \cS^f} \mathop{<}_{mul}
2770: \cM_{\cS^\ast \cup \{s'_{n}\}} $. Therefore, the proof follows by
2771: Lemma~\ref{transi-closs} and the inductive hypothesis.
2772: \end{itemize}
2773: \end{description}
2774: \end{proof}
2775:
2776: \mbox{}\\
2777: \textsl{Theorem \ref{termination}}\\
2778: %%\begin{theorem} \label{termination}
2779: Given a flat program $\cR$ and an initial term $t$, the algorithm in
2780: Fig.~\ref{pe-alg2} terminates computing a set of states $\cS$ such
2781: that $\tuple{t,\nil}$ is $\cS$-closed.
2782: %%\end{theorem}
2783:
2784: \begin{proof}
2785: The $\cS$-closedness of $\tuple{t,\nil}$ is a direct consequence of
2786: Lemma~\ref{safe-abstract} and Proposition~\ref{transi-closs}.
2787: Lemma~\ref{safe-abstract} ensures that the arguments of the operator
2788: $\foo{abstract}$ are always closed w.r.t.\ the new set of states,
2789: while Proposition~\ref{transi-closs} guarantees that the closedness
2790: of the initial state is correctly propagated through the whole
2791: process.
2792:
2793: The termination of the algorithm can be derived from the following
2794: facts:
2795: \begin{enumerate}
2796: \item Each iteration of the algorithm is finite. The finiteness of the
2797: application of the unfolding operator is obvious (since only one
2798: function unfolding is allowed). The termination of one application
2799: of operator $\foo{abstract}$ can easily be proved by following
2800: the scheme of the proof of Lemma~\ref{safe-abstract}: the
2801: computation terminates since each recursive call to
2802: $\foo{abstract}$ uses a set of states which is strictly lesser
2803: than the previous call (w.r.t.\ $\mathop{<}_{mul}$).
2804:
2805: \item The termination of the whole iterative process is a
2806: consequence of the following facts:
2807: \begin{itemize}
2808: \item The number of states in the current set $\cS_{i}$ cannot be
2809: greater than the number of different functions in the original
2810: program, since the abstraction operator ensures that there is only
2811: one state for each function symbol of the program. Thus, it cannot
2812: grow infinitely.
2813:
2814: \item The number of states in the set $\cS_{i+1}$ is always equal to
2815: or greater than the number of states in the set $\cS_{i}$. This
2816: property is immediate, since we only remove states in the last case
2817: of the definition of $\foo{abstract}$ and, there, we replace one
2818: state by a new (generalized) state.
2819:
2820: \item Finally, each time one state is replaced by a new one, the new
2821: state is equal to or smaller than the previous state (according to
2822: the ordering based on the depth of the terms). If the new state has
2823: the same depth than the old one, then the process would terminate,
2824: since they would be equal (modulo renaming). If it is strictly
2825: smaller, then it will eventually reach an state whose first
2826: component is of the form $f(\ol{x_{n}})$ and, hence, it cannot be
2827: generalized again.
2828: \end{itemize}
2829: \end{enumerate}
2830: \end{proof}
2831:
2832: \mbox{}\\
2833: \textsl{Theorem \ref{abs-th}}\\
2834: %%\begin{theorem} \label{abs-th}
2835: Let $\cR$ be a flat program and $t$ a term. Let $\cS$ be a set of
2836: states computed by the algorithm of Fig.~\ref{pe-alg2} from $\cR$
2837: and $t$. Then, $\cR' =
2838: \foo{build\_slice}(\foo{residual\_calls}(\cS))$ is a program slice of
2839: $\cR$, i.e., $\cR' \succeq \cR$.
2840: %%\end{theorem}
2841:
2842: \begin{proof}
2843: This result is an easy consequence of Def.~\ref{cons-slice} and the
2844: calculus in Fig.~\ref{simplify-rules}:
2845: \begin{itemize}
2846: \item If there is a rule $f(\ol{x_n}) = e \in \cR$ and there is no
2847: term $f(\ol{t_n}) \in \foo{residual\_calls}(\cS)$, then $\cR'$
2848: does not contain a definition for $f$, i.e., $f(\ol{x_n}) = \top
2849: \in \cR'$ and, trivially, $\top \succeq e$.
2850:
2851: \item Otherwise, $f(\ol{x_n}) = e \in \cR$ and $f(\ol{x_n}) = e' \in
2852: \cR'$ with $\sql e\sqr \rho \longrightarrow^\ast e'
2853: \not\longrightarrow$ and $\rho=\{\ol{x_{n} \mapsto t_{n}}\}$.
2854: Now, we prove that $e' \succeq e$ by induction on the length $l$
2855: of the derivation $\sql e\sqr \rho \longrightarrow^\ast e'$:
2856: \begin{description}
2857: \item[\sf Base case ($l = 1$).] In this case, we only have the
2858: following possibilities:
2859: \begin{itemize}
2860: \item $e$ is a variable; thus, $e' = e$ and the claim follows
2861: trivially.
2862: \item $e=c()$ is a constructor constant; then, $e' = e$ and the
2863: claim follows.
2864: \item $e = g(\ol{t'_m})$ is operation-rooted and there is no
2865: term in $\foo{residual\_calls}(\cS)$ rooted by $g$. Then, $e'
2866: = \top$ and $e' \succeq e$.
2867: \end{itemize}
2868: \item[\sf Induction case ($l > 1$).] Here, we distinguish the
2869: following cases:
2870: \begin{itemize}
2871: \item $e = c(t'_1,\ldots,t'_m)$ with $c \in \cC$ and $m>0$.
2872: Then, $e' = c(\sql t'_1\sqr\rho,\ldots,\sql t'_m\sqr\rho)$ and
2873: the claim follows by induction.
2874:
2875: \item $e = \foo{(f)case}\;x\;\foo{of}\;\{p_1\to e_1; \ldots;p_k
2876: \to e_k\}$ with $\rho(x) = c(\ol{t'_{m}})$ and $p_i =
2877: c(\ol{y_m})$. Then, $e' = \foo{(f)case}\;x\;\foo{of}\;\{p_1\to
2878: \top; \ldots;p_i \to \sql e_i\sqr \rho';\ldots;p_k \to \top\}$
2879: with $\rho' = \{\ol{y_m \mapsto t'_m}\} \circ \rho$. By the
2880: inductive hypothesis, we have $\sql e_i\sqr \rho' \succeq e_i$
2881: and, thus, $e' \succeq e$.
2882:
2883: \item $e = \foo{(f)case}\;x\;\foo{of}\;\{p_1\to e_1; \ldots;p_k
2884: \to e_k\}$ with $\rho(x) \in \cX$. Then, $e' =
2885: \foo{(f)case}\;x\;\foo{of}\;\{p_1\to \sql e_1 \sqr \rho_1;
2886: \ldots;p_k \to \sql e_k \sqr \rho_k\}$, with $\rho_i = \{x
2887: \mapsto p_i\}\circ\rho$, $i \in \{1,\ldots,k\}$. By the
2888: inductive hypothesis, we have $\sql e_i \sqr \rho_i \succeq
2889: e_i$ for all $i = 1,\ldots,k$. Therefore, $e' \succeq e$.
2890:
2891: \item $e = g(t'_1,\ldots,t'_m)$ with $g \in \cF$. Then, either
2892: $e' = g(\sql t'_1\sqr\rho,\ldots,\sql t'_m\sqr\rho)$ and the
2893: claim follows by induction, or there is no term in
2894: $\foo{residual\_calls}(\cS)$ rooted by $g$ and $e' = \top
2895: \succeq e$.
2896: \end{itemize}
2897: \end{description}
2898: \end{itemize}
2899: \end{proof}
2900: %
2901:
2902: \mbox{}\\
2903: \textsl{Theorem \ref{final}}\\
2904: %%\begin{theorem} \label{final}
2905: Let $\cR$ be a flat program and $t$ a term. Let $\cS$ be a set of
2906: states computed by the algorithm of Fig.~\ref{pe-alg2} from $\cR$
2907: and $t$. If computations for $t$ in $\cR$ do not suspend, then $t$
2908: computes the same values and answers in $\cR$ and in
2909: $\foo{build\_slice}(\foo{residual\_calls}(\cS))$.
2910: %%\end{theorem}
2911:
2912: \begin{proof}
2913: We present an sketch of the proof; the complete formalization is not
2914: difficult but would require the introduction of many notions and
2915: results from the original narrowing-driven specialization framework.
2916: %
2917: Basically, the proof proceeds in a stepwise manner as follows:
2918: \begin{itemize}
2919: \item First, we consider the construction of a specialized program
2920: from the states in $\cS$ following the standard approach to
2921: narrowing-driven partial evaluation. Formally, we construct a
2922: residual program $\cR'$ by producing a residual rule of the form
2923: \[
2924: \foo{ren}(S[t]) = \foo{ren}(S[t'])
2925: \]
2926: for each term in $\{ S[t] \mid \tuple{t,S} \in \cS\}$, where
2927: $\tuple{t,S} \Longrightarrow_{\sf fun} \tuple{t'',S}
2928: \Longrightarrow^\ast_{\sf select/guess} \tuple{t',S}
2929: \not\Longrightarrow_{\sf select/guess}$. Function $\foo{ren}$ is
2930: applied to rename expressions so that the resulting residual program
2931: fulfills the syntax of flat programs (in spite of the form of
2932: $S[t]$). Basically, $\foo{ren}(S[t])$ returns a term
2933: $f(\ol{x_{n}})$ where $f$ is a fresh function symbol and
2934: $\ol{x_{n}}$ are the different variables of $S[t]$. By the
2935: correctness of narrowing-driven partial evaluation (since $t$ is
2936: $\cS$-closed by Theorem~\ref{termination}), we know that all the
2937: computations for $\tuple{t,\nil}$ in the original program can also
2938: be done for $\tuple{\foo{ren}(t),\nil}$ in the residual program
2939: constructed so far.
2940:
2941: \item Then we consider a new program $\cR''$ which is obtained from
2942: $\cR'$ as follows: each rule in $\cR'$ of the form $\foo{ren}(S[t])
2943: = \foo{ren}(S[t'])$ is replaced by a new rule $\foo{ren}(t) =
2944: \foo{ren}(t')$. This replacement is safe in our context since the
2945: one-step unfolding does not affect to the current stack. A precise
2946: equivalence between the computations in $\cR'$ and $\cR''$ can
2947: easily be established under the extended operational semantics of
2948: Fig.~\ref{smallstep}. Note that renaming is still necessary to
2949: ensure that residual rules fulfill the syntax of Fig.~\ref{flat}.
2950:
2951: \item Now, we define a new program $\cR'''$ which is obtained from
2952: $\cR''$ as follows: each rule $\foo{ren}(t) = \foo{ren}(t')$, with
2953: $t = f(\ol{t_{n}})$, is replaced by a new rule $f(\ol{x_{n}}) = e'$,
2954: where $f(\ol{x_{n}}) = e$ is a rule of the original program $\cR$,
2955: $\ol{x_{n}}$ are fresh variables, $\sql e \sqr \rho
2956: \longrightarrow^\ast e' \not\longrightarrow$, and $\rho =
2957: \{\ol{x_{n} \mapsto t_{n}}\}$. There is no need to apply a renaming
2958: of expressions in this case, since the program so constructed
2959: already fulfills the syntax of Fig.~\ref{flat} (cf.\
2960: Theorem~\ref{abs-th}). Now, each derivation for
2961: $\tuple{\foo{ren}(t),\nil}$ in $\cR''$ can also be done for
2962: $\tuple{t,\nil}$ in $\cR'''$ using the extended operational
2963: semantics of Fig.~\ref{smallstep}. This is justified by the fact
2964: that the only difference between the rules of $\cR''$ and $\cR'''$
2965: is that bindings are applied to program expressions in $\cR''$ while
2966: they are represented implicitly in $\cR'''$ by means of case
2967: expressions in the right-hand sides of the program rules.
2968:
2969: \item Finally, we extend $\cR'''$ by adding a residual rule of the
2970: form $f(\ol{x_{n}}) = e'$ for each call $f(\ol{t_{n}}) \in \{ t'
2971: \mid \tuple{t,S} \in \cS,~t' \in \foo{calls}(S),~\mbox{ and $t'$ is
2972: not $T_{\cS}$-closed} \}$, where $T_{\cS} = \{ t \mid \tuple{t,S}
2973: \in \cS \}$, $f(\ol{x_{n}}) = e$ is a rule of the original program
2974: $\cR$, $\ol{x_{n}}$ are fresh variables, $\sql e \sqr \rho
2975: \longrightarrow^\ast e' \not\longrightarrow$, and $\rho =
2976: \{\ol{x_{n} \mapsto t_{n}}\}$. The extended program coincides with
2977: the result of $\foo{build\_slice}(\foo{residual\_calls}(\cS))$. The
2978: claim follows by checking that each derivation for $\tuple{t,\nil}$
2979: in $\cR'''$ using the extended semantics can also be performed for
2980: $t$ in $\foo{build\_slice}(T)$ using the standard operational
2981: semantics. Intuitively, this equivalence holds because the only
2982: difference---we ignore here the suspension of flexible case
2983: expressions since we only consider computations which do not
2984: suspend---between the standard and the extended operational
2985: semantics is that the unfolding of some outer function call is
2986: (possibly) delayed until a complete one-step evaluation is possible.
2987: Therefore, the same computations can be proved with both calculi,
2988: except when there is some inner call which never reduces to a value
2989: (due to an infinite derivation). However, we ensure the equivalence
2990: even in this case by adding residual rules for the calls in the
2991: stack components which are not $T_{\cS}$-closed, i.e., for those
2992: calls which have some inner call with a non-terminating derivation.
2993: \end{itemize}
2994: \end{proof}
2995:
2996: \end{document}
2997: