% debuggingMethods.tex

% Author: Olaf Chitil
% Created: 8.6.2000
% Last Update: 
  
\documentclass{article}
\usepackage{pst-node}
\usepackage[a4paper]{geometry}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{alltt}
\usepackage{url}
\usepackage{afterpage}



%------------------------------------------------------------------------------

\newcommand{\art}{\paragraph{Redex Trails}}
\newcommand{\freja}{\paragraph{Freja}}
\newcommand{\buddha}{\paragraph{Buddha}}
\newcommand{\edt}{\paragraph{EDT}}
\newcommand{\hood}{\paragraph{HOOD}}
\newcommand{\stories}{\paragraph{Stories}}
\newenvironment{example}{\begin{quote}\begin{alltt}}{\end{alltt}\end{quote}}

\renewcommand{\textfraction}{0}
\renewcommand{\topfraction}{1}
\renewcommand{\bottomfraction}{1}
\renewcommand{\floatpagefraction}{1}

% define commands for typesetting redex trails:
\setlength{\unitlength}{1cm}
\newenvironment{trace}[2]
{\begin{picture}(#1,#2)(0,0)}{\end{picture}}
\newcommand{\oute}[4]
{\rput(#1,#2){\rnode{#3}{\psframebox{\strut\texttt{#4}}}}}
\newcommand{\ine}[2]
{\rnode{#1}{\psframebox{#2}}}
\newcommand{\toParent}[2]{\ncline{->}{#1}{#2}}
\newcommand{\dtoParent}[2]{\ncline[linestyle=dotted]{->}{#1}{#2}}

\newcommand{\fromParent}[2]{\ncline{->}{#1}{#2}}

\newcommand{\evaluation}[5]
{\rput(#1,#2){\rnode{#3}{\psframebox{{\strut\texttt{#5}}}}}\ncline[linestyle=dashed]{->}{#4}{#3}}
\newcommand{\redex}[5]
{\rput(#1,#2){\rnode{#3}{\psframebox{{\strut\texttt{#5}}}}}\ncline[linestyle=dashed]{->}{#3}{#4}}
\newcommand{\redexe}[5]
{\rput(#1,#2){\rnode{#3}{\psframebox{{\strut\texttt{#5}}}}}\ncline{->}{#3}{#4}}
\newcommand{\sub}[1]
{\rnode{bbbb}{$\bullet$}\ncline[linestyle=dotted]{->}{bbbb}{#1}}
\newcommand{\subc}[3]
{\rnode{bbbb}{$\bullet$}\nccurve[angleA=#1,angleB=#2,ncurv=1,linestyle=dotted]{->}{bbbb}{#3}}
\newcommand{\result}[3]
{\rput(#1,#2){\rnode{bbbb}{$\bullet$}}\ncline{->}{bbbb}{#3}}

%------------------------------------------------------------------------------
 
\begin{document}
\thispagestyle{empty}

\title{ART Memo 2 (Version 2)\\Comparison of Dependency-Based Debuggers\\ for Lazy Functional Languages} 
\author{Olaf Chitil}
\date{\today}
\maketitle

%------------------------------------------------------------------------------

\tableofcontents

%------------------------------------------------------------------------------

\section{Methods}
The following methods/systems for debugging lazy functional programs are all based on a trace structure which is not just a sequence of expressions refering to the actual computation steps.

\art \cite{sparudruncimanplilp97}, \cite{sparudruncimanifl97}.
\freja \cite{nilssonphd98}, \cite{nilssonsparud97}.
\buddha \cite{pope98}, \cite{naishbarbour96}. Basically same trace as Freja.
\stories \cite{jonesbooth95},\cite{boothjones97}. Trace similar to Freja.
\hood (\url{http://www.cse.ogi.edu/~andy/hood/}). Doesn't seem to produce a single trace structure. It is a kind of lazy man's \texttt{printf}, that is, the function \texttt{trace} without changing evaluation order.

\medskip\noindent
Possibly interesting, but not discussed here:
\begin{itemize}
\item \cite{AADEBUG::HazanM1993}. Transformed program constructs call path, a kind of strict stack trace.
\end{itemize}

\medskip\noindent
Older work:
\begin{itemize}
\item \cite{hallodonnell85}, \cite{odonnellhall88}. Trace similar to EDT but too much is evaluated.

\item \cite{toynrunciman86}, \cite{Toyn87}. Trace contains last redex for each value.

\item \cite{kamin90}. Trace similar to EDT, but simplified language and implementation.
\end{itemize}

\medskip\noindent
A comparison of various debugging/tracing methods is made in
\begin{itemize}
\item Section 2.2 of \cite{watsonphd96}.
\item Chapter 2 (also 7.5) of \cite{penneyphd99}.
\item Chapter 11 of \cite{nilssonphd98} (shorter).
\end{itemize}

%------------------------------------------------------------------------------

\section{Logical Structure of Trace}

\art 
A redex trail is a directed graph with an application at every node.  An
application is either a redex or a value (constant, constructor
application, partial application).  The redex trail shows the
computation history of an application.  A redex is the parent of an
application, if it created that application.  An application has
exactly one parent (except for root redexes), but every of its
subexpressions also has a parent which may be distinct.  The redex
trail of an application is the graph consisting of its parent and the
parents of its subexpressions and recursively the redex trails of
these parents and the subexpressions of these parents.  Although the
sequence of parents can be seen as the main redex trail of an
application, the whole trail is a complex branching structure.

The trace of a program run is the redex trail of its result. This
trace contains the redex trails of all intermediate values and also of
redexes that were created but have never been evaluated during the
computation.

Because an application consists of values and sometimes redexes, the
graph structure of the trace is complex.  A redex is the source of a
single arrow and the target of (possibly several) arrows.  A value or
a subexpressions of an application is the source of a single arrow but
never the target of an arrow. Note that a redex is a subexpression
of an application only if this redex was never evaluated. Hence it
cannot be the target of an arrow.

\freja
The trace structure is the evaluation dependency tree (EDT).

\buddha
The trace structure is the evaluation dependency tree (EDT).

\edt
An EDT is a tree where a node is a pair of a redex and a value.  It is
the derivation/proof tree for a call-by-value reduction with
miraculous stops where expressions are not needed for the result. The
derivation tree only contains function application, not other context
rules.

\stories 
A story is a tree structure which describes the computational
history of a value. A story is either a value (full normal form) or an
application node with three children: the story of the function, the
story of the argument and the story of the result.

The story of a value is the same value, if this value appears
literally in the program text.  The story of a value is an application
node, if this application was reduced to compute the value.   Let us
define the value of a story to be just the story, if the story is a
value, and the value of the result story, if the story is an
application node.  Then the value of the story of a value is this very
value.

A story has a top-down structure like the EDT, but it differs in that
a story is always attached to a value, not an application node. In
this respect it resembles the redex trail.

\hood
The trace describes data structures created by the program. That is,
the creation of data constructors (and primitive value) is observed.
The trace is a set of observations. An observation states \emph{where} in the
computation term/graph (with respect to an occurrence of an
\texttt{observe} combinator) reduction to \emph{which} data
constructor (or primitive value) took place. 

\medskip\noindent
Figure \ref{traces} shows the various trace structures for an example program.

\begin{figure*}[t]
\strut\hrulefill\strut\\
\begin{minipage}{20em}
\begin{example}
fac 0 = 1
fac n = n * fac (n-1)

main = fac 2
\end{example}
\end{minipage}
\begin{minipage}{30ex}
\begin{trace}{8}{10}
\put(3,2.5){redex trail}
\oute{1}{1}{t2}{2}
\oute{1}{2}{tm2}{\ine{tm21}{2}*\ine{tm22}{1}}
\oute{2}{3}{tm1}{\ine{tm11}{1}*\ine{tm12}{1}}
\oute{6}{4}{tf0}{fac \ine{tf01}{0}}
\oute{6}{5}{ti1}{\ine{ti11}{1}-1}
\oute{4}{5.4}{tf1}{fac \ine{tf11}{1}}
\oute{4}{7}{ti2}{\ine{ti21}{2}-1}
\oute{2}{7.5}{tf2}{fac 2}
\oute{1}{9}{tmain}{main}
\toParent{t2}{tm2}
\toParent{tm2}{tf2}
\toParent{tm21}{tmain}
\toParent{tm22}{tm1}
\toParent{tm1}{tf1}
\toParent{tm11}{ti2}
\toParent{tm12}{tf0}
\toParent{tf0}{tf1}
\toParent{tf01}{ti1}
\toParent{tf1}{tf2}
\toParent{tf11}{ti2}
\toParent{tf2}{tmain}
\toParent{ti1}{tf1}
\toParent{ti11}{ti2}
\toParent{ti2}{tf2}
\toParent{ti21}{tmain}
\end{trace}
\end{minipage}

\begin{minipage}{40ex}
\begin{trace}{8}{5}
\put(0,4){EDT}
\oute{3}{4}{em}{main = 2}
\oute{3}{3}{ef2}{fac 2 = 2}
\oute{1}{2}{ei2}{2 - 1 = 1}
\oute{3}{2}{ef1}{fac 1 = 1}
\oute{5}{2}{em2}{2 * 1 = 2}
\oute{1}{1}{ei1}{1 - 1 = 0}
\oute{3}{1}{ef0}{fac 0 = 0}
\oute{5}{1}{em1}{1 * 1 = 1}
\fromParent{em}{ef2}
\fromParent{ef2}{ei2}
\fromParent{ef2}{ef1}
\fromParent{ef2}{em2}
\fromParent{ef1}{ei1}
\fromParent{ef1}{ef0}
\fromParent{ef1}{em1}
\end{trace}
\end{minipage}
\begin{minipage}{40ex}
\begin{trace}{9}{5}
\oute{1}{4}{sm}{main = \ine{smm}{}}
\oute{3.5}{4}{sf2}{fac 2 = \ine{sf21}{}}
\oute{6}{2}{si2}{2 - 1 = 1}
\oute{6}{3}{sf1}{fac \ine{sf11}{} = \ine{sf12}}
\oute{6}{4}{sm2}{2 * \ine{sm21}{} = 2}
\oute{8.5}{1}{si1}{1 - 1 = 0}
\oute{8.5}{2}{sf0}{fac \ine{sf01}{} = 0}
\oute{8.5}{3}{sm1}{1 * \ine{sm11}{} = 1}
\put(1,3){Story of \texttt{main}}
\put(1,2.5){(arrow is always equality)}
\fromParent{smm}{sf2}
\fromParent{sf21}{sm2}
\fromParent{sm21}{sf1}
\fromParent{sf11}{si2}
\fromParent{sf12}{sm1}
\fromParent{sm11}{sf0}
\fromParent{sf01}{si1}
\end{trace}
\end{minipage}
\caption{Traces for an example program\label{traces}}
\strut\hrulefill\strut\\
\end{figure*}


\begin{figure*}[ht]
\strut\hrulefill\strut\\
\begin{minipage}{20em}
\begin{example}
fac 0 = 1
fac n = n * fac (n-1)

main = fac 2
\end{example}
\end{minipage}
\\
\begin{minipage}{60ex}
\begin{trace}{9}{8}
\oute{4}{7.5}{rfmain}{main}
\redex{2.5}{5}{rf2}{rfmain}{2}
\redexe{4}{5.5}{rff2}{rfmain}{fac \sub{rf2}}
\redex{1}{3}{rfm2}{rff2}{\sub{rf2}{} - 1}
\redexe{2.5}{3}{rfm2v}{rfm2}{1}
\redex{4}{3.5}{rff1}{rff2}{fac \sub{rfm2v}}
\redex{1}{1}{rfm1}{rff1}{\sub{rfm2v}{} - 1}
\redexe{2.5}{1}{rfm1v}{rfm1}{0}
\redex{4}{1.5}{rff0}{rff1}{fac \sub{rfm1v}}
\redexe{5.5}{1.5}{rff0v}{rff0}{1}
\redexe{7}{2}{rfmm1}{rff1}{\sub{rfm2v}{} * \sub{rff0v}}
\redexe{8.5}{2}{rfmm1v}{rfmm1}{1}
\redexe{7}{4}{rfmm2}{rff2}{\sub{rf2}{} * \sub{rfmm1v}}
\redexe{8.5}{4}{rfmm2v}{rfmm2}{2}
\result{9}{4}{rfmm2v}
\end{trace}
\end{minipage}
%
\begin{minipage}{40ex}
\begin{trace}{9}{8}
\oute{2.5}{6.5}{rfmain}{main}
\redex{2.5}{5}{rf2}{rfmain}{2}
\redexe{4}{6.5}{rff2}{rfmain}{fac \sub{rf2}}
\redex{1}{3}{rfm2}{rff2}{\sub{rf2}{} - 1}
\redexe{2.5}{3}{rfm2v}{rfm2}{1}
\redex{4}{4.5}{rff1}{rff2}{fac \sub{rfm2v}}
\redex{1}{1}{rfm1}{rff1}{\sub{rfm2v}{} - 1}
\redexe{2.5}{1}{rfm1v}{rfm1}{0}
\redex{4}{2.5}{rff0}{rff1}{fac \sub{rfm1v}}
\redexe{5.5}{2.5}{rff0v}{rff0}{1}
\redexe{5.5}{4.5}{rfmm1}{rff1}{\sub{rfm2v}{} * \sub{rff0v}}
\redexe{7}{4.5}{rfmm1v}{rfmm1}{1}
\redexe{5.5}{6.5}{rfmm2}{rff2}{\sub{rf2}{} * \sub{rfmm1v}}
\redexe{7}{6.5}{rfmm2v}{rfmm2}{2}
\result{7.5}{6.5}{rfmm2v}
\end{trace}
\end{minipage}
\\
\begin{minipage}{15em}
\begin{alltt}
main = let xs = [4*2, 3+6, 1*3]
         in (head xs, last xs)

head (x:xs) = x

last [x]    = x
last (x:xs) = last xs
\end{alltt}
Data structures,\\
unevaluated redexes and\\
indirections.
\end{minipage}
\begin{minipage}{40ex}
\begin{trace}{11}{8}
\oute{3}{7}{main}{main}
\redex{1}{3}{m42}{main}{4 * 2}
\redexe{2.2}{3}{m42v}{m42}{8}
\redex{5}{3}{p36}{main}{3 + 6}
\redex{7}{3}{m13}{main}{1 * 3}
\redexe{8.2}{3}{m13v}{m13}{3}
\redex{9}{5}{l3}{main}{\sub{m13v}{} : []}
\redex{6}{5}{l2}{main}{\sub{p36}{} : \sub{l3}}
\redex{3}{5}{l1}{main}{\sub{m42v}{} : \sub{l2}}
\redex{2}{1}{head}{main}{head \sub{l1}}
\redexe{3.5}{1}{headv}{head}{\sub{m42v}}
\redex{5}{1}{last1}{main}{last \sub{l1}}
\redexe{7}{1}{last2}{last1}{last \sub{l2}}
\redexe{9}{1}{last3}{last2}{last \sub{l3}}
\redexe{10.5}{1}{last3v}{last3}{\sub{m13v}}
\redexe{5}{7}{tupel}{main}{(\sub{headv},\sub{last3v})}
\result{7}{7}{tupel}
\end{trace}
\end{minipage}
\\
\begin{minipage}{40ex}
\begin{trace}{11}{4}
\oute{5}{4}{main}{main = (8,3)}
\redex{1}{3}{m42}{main}{4 * 2 = 8}
\redex{4}{3}{head}{main}{head [8,?,3] = 8}
\redex{7}{3}{m13}{main}{1 * 3 = 3}
\redex{10}{3}{last1}{main}{last [8,?,3] = 3}
\redex{10}{2}{last2}{last1}{last [?,3] = 3}
\redex{10}{1}{last3}{last2}{last [3] = 3}
\end{trace}
\end{minipage}
\caption{More redex trails, presented differently\label{traces2}}
\strut\hrulefill\strut\\
\end{figure*}

\begin{figure*}[htp]
\strut\hrulefill\strut\\
\begin{center}
\begin{minipage}{17em}
\begin{alltt}
main = let xs = [4*2, 3+6]
         in (head xs, last xs)

head (x:xs) = x

last (x:xs) = last xs
last [x]    = x
\end{alltt}
\end{minipage}
\end{center}
\caption{Example program\label{showExample}}
\begin{center}
\begin{trace}{12}{4.5}
\oute{5}{4}{main}{main $\Rightarrow$ (8,3)}
\evaluation{1}{2.5}{m42}{main}{4 * 2 $\Rightarrow$ 8}
\evaluation{4}{2.5}{head}{main}{head [8,?,3] $\Rightarrow$ 8}
\evaluation{7}{2.5}{m13}{main}{1 * 3 $\Rightarrow$ 3}
\evaluation{10}{2.5}{last1}{main}{last [8,?,3] $\Rightarrow$ 3}
\evaluation{10}{1.25}{last2}{last1}{last [?,3] $\Rightarrow$ 3}
\evaluation{10}{0}{last3}{last2}{last [3] $\Rightarrow$ 3}
\end{trace}
\end{center}
\caption{Evaluation Dependency Tree\label{showEdt}}
\begin{center}
\begin{trace}{13}{6.5}
\oute{5.2}{6}{main}{main}
\redex{0.5}{4}{m42}{main}{4 * 2}
\redexe{1.7}{4}{m42v}{m42}{8}
\redex{6.5}{4}{p36}{main}{3 + 6}
\redex{8}{4}{m13}{main}{1 * 3}
\redexe{9.2}{4}{m13v}{m13}{3}
\redex{6.7}{0.5}{l3}{main}{\sub{m13v}{} : []}
\redex{5.2}{0.5}{l2}{main}{\sub{p36}{} : \sub{l3}}
\redex{3.7}{0.5}{l1}{main}{\sub{m42v}{} : \sub{l2}}
\redex{3}{4}{head}{main}{head \sub{l1}}
\redexe{4.2}{4}{headv}{head}{\subc{270}{270}{m42v}}
\redex{10.5}{4}{last1}{main}{last \sub{l1}}
\redexe{10.5}{2}{last2}{last1}{last \sub{l2}}
\redexe{10.5}{0}{last3}{last2}{last \sub{l3}}
\redexe{11.7}{0}{last3v}{last3}{\subc{150}{270}{m13v}}
\redexe{6.7}{6}{tupel}{main}{(\sub{headv},\subc{20}{70}{last3v})}
\result{8}{6}{tupel}
\end{trace}
\end{center}
\caption{Redex Trail\label{showRT}}
\strut\hrulefill\strut\\
\end{figure*}
\afterpage{\clearpage}


Figure~\ref{traces2} shows redex trails in different ways, which stress the similarity to EDTs and equaltiy relationships. A solid arrow points to a component and both dashed and dotted arrows point to the parent. A dashed arrow is used when equality holds, because the source is not just a subexpression of the instance of the right hand side but is the complete instance of the right hand side.

\subsection{Does Trace Structure Reflect Program Structure?}

\art
Yes. A parent redex is always the left hand side of an instance of a function definition. Its children are parts of the (partially evaluated) right hand side of this instance. At least the outer part (application in case of a redex) of a child occurs textually in the right hand side of the function definition.

\edt
Yes. The same relationship holds for the redex of a parent with
respect to the redexes of its children.

\stories
Yes. Similar to EDT, but whereas the children of an EDT node are
unordered, a story orders them reflecting the subexpression structure
of the right hand side of a definition.

\hood
Not really. Every observation belongs to an occurrence of the
\texttt{observe} combinator, that was inserted in the program.
However, the relationship between the  observations belonging to a
single occurrence is independent of the program structure (they are
related according to the data structure that they form).

\subsection{Does Trace Contain Mostly Values or Arbitrary Expressions?}

\art
A redex contains function names/$\lambda$-expressions, values and
sometimes unevaluated expressions (see below). 

\edt
A redex contains function names/$\lambda$-expressions, values and a
special symbol for unevaluated expressions.

\stories
Only values, that is, the function, argument and result of an
application node are values. In case of non-termination the story may
not be constructed completely.

\hood
The trace contains only (partial) values. 

\subsection{How is an Expression (Argument) Handled That is Never Evaluated?}

\art
It is not evaluated for trace creation. So the termination behaviour does not change.
The expression is shown as unevaluated redex. It may be visually represented by a special symbol. It has a parent like all other expressions of the trace.

\edt
It is not evaluated for trace creation. So the termination behaviour
does not change. In the trace the unevaluated expression is just
represented by a special symbol.

\stories
It is evaluted for trace creation! Creating the story only up to a
given depth prevents non-termination, but not black holes.

\hood
It is not evaluated for trace creation. So the termination behaviour
does not change. Unevaluated expressions correspond to missing
observations in the trace.

\subsection{Does Trace Contain Source Code References?}

\art
Yes. Every expression is linked to the part of a definition body which created it and additionally every function name is linked to its definition.

\freja
Every node is linked to the definition of the function of its redex.

\buddha
Every node contains the definition body of the function of its redex.

\stories
Yes. Every node contains a source code reference (to the part of a
definition body that created it?)

\hood
Observations refer to the name (string) that the user gives as first argument
to the \texttt{observe} combinator.

\subsection{Is Sharing Visible?}

\art
Yes. The trace is shared just as the arguments in the original computation are.
This sharing is made visible to the user through a colour coding (identical, parent, siblings) to indicate which parts of a trace have already been viewed and to locate circular dependencies.

Furthermore, sharing also influences how far arguments are evaluated.

\edt
Sharing is only indirectly visible through how far arguments are evaluated.
The values of free variables of the right hand side of a local
function definition are shown as part of a redex. However, this is not
intended to point out that these values are shared.

\stories
I believe not at all.

\hood
In so far that every evaluation of the \texttt{observe} combinator
leads to a separate set of observations. Hence sharing of this
evaluation pays a role.

\subsection{How is Trace Defined/Explained?}

\art
By example and outline of the transformation that enables the creation of the trace.

\freja
By example, by informal definition, by an extended continuation-based semantics of the language and the description of the implementation.

\buddha
By example, by informal definition and outline of the transformation
that enables the creation of the trace. Rather informally discussed
correctness of the trace with respect to the original program
behaviour.

\stories
By example, by informal explanation and by outline of the
transformation that enables the creation of the trace.

\hood
Structure of trace only outlined in textual description.

%------------------------------------------------------------------------------

\section{Supported Language Features}

\hood
Language features are irrelevant for the trace (except for IO, see
later), because not reductions but data are traced.

\subsection{Free Variables in Local Definitions}

\art
Are handled like other variables. A redex node does not contain the values of its free variables. This lack of information may hinder understanding of the traced computation (Problem that needs attention).

\freja
Every EDT node contains the values of its free variables, so that the node represents an equation whose validity can be judged.

\buddha
Currently uses $\lambda$-lifting to remove local definitions and thus changes program structure. In the future $\lambda$-lifting shall be hidden from the user, so that EDT nodes contain the values of free variables as additional information.

\stories
Not discussed.

\subsection{Partial Applications}

An application of a function to arguments is a redex if the number of arguments is equal to the arity of the function, which is given through its definition.

\art
Redexes are represented correctly in the trace.
 To distinguish non-saturated or over-saturated applications from redexes the implementation uses an impure pointer comparison of trails.

\freja
Redexes are represented correctly in the trace.
To distinguish non-saturated or over-saturated applications from redexes the implementation stores the arity with every function name.

\buddha
If a definition body is a partial application, then $\eta$-expansion of the definition is performed to remove the partial application. So the arity used for redexes in the EDT may be different from the arity of the function definition.

Partial applications that appear as arguments are handled specially so
that they can be shown as argument values. How to do this in general
has not yet been solved.

\stories
A redex is the application of a function to a single argument, that
is, application to several arguments is broken down into several
applications and represented like this in the story.
The value of a partial application is
always shown as a constant \texttt{Partial}.

\subsection{CAFs}

\begin{minipage}{25em}
\begin{example}
ones = 1 : ones

main = print (head ones)
\end{example}
\end{minipage}
\begin{minipage}{30ex}
\begin{trace}{8}{6}
\oute{1}{1}{result}{1}
\oute{1}{2}{print}{print \ine{print1}{1}}
\oute{3}{3}{head}{head \ine{headones}{1:ones}}
\oute{3}{4}{ones}{ones}
\oute{1}{5}{main}{main}
\toParent{result}{print}
\toParent{print1}{head}
\toParent{headones}{ones}
\dtoParent{ones}{main}
\toParent{head}{main}
\toParent{print}{main}
\end{trace}
\end{minipage}

\art
A CAF is a special redex that has no parent, because its value may be
required by several redexes, but it is only evaluated once.

Hence a CAF has an empty redex trail and no link to the source code
position where it is used. In the preceding example \texttt{main} and
\texttt{ones} are CAFs. The indicated parent arrow from \texttt{ones} to
\texttt{main} does \emph{not} exist.

The description of the transformation does not handle CAFs; it should look as follows:

$${\cal F}[\![ f = e ]\!] \Rightarrow f = {\cal E}[\![e ]\!]_{(\texttt{Nm}~\texttt{Root}~{\cal N}[\![f]\!])}$$

Note that pseudo-CAFs, for example of type \texttt{Num n => n}, do not
have redex trails either, although they are usually not shared.

It could be useful for a CAF to have a parent, if evaluation of a CAF
fails. Although the value of the CAF lead to the error, it may be
important to know where the CAF was called, because this evaluation of
the CAF may not have been intended. However, because the error (or in
case of non-termination the redex under evaluation) is the starting
point of the redex trail of the program, the redex that called the CAF
is not part of the redex trail.  The following example demonstrates
the lack of information:

\begin{minipage}{25em}
\begin{example}
caf :: (Int,Int) 
caf = (3 `div` 0, 3 `div` 0)

main = print (snd caf)
\end{example}
\end{minipage}
\begin{minipage}{30ex}
\begin{trace}{5}{4}
\oute{1}{1}{error}{\mbox{\rm division by zero}}
\oute{1}{2}{div}{div 3 0}
\oute{1}{3}{caf}{caf}
\toParent{error}{div}
\toParent{div}{caf}
\end{trace}
\end{minipage}

A more realistic example. The infinite computation is interrupted by
the user:

\begin{minipage}{25em}
\begin{example}
nats :: [Int]
nats = 0 : map (+1) nats

main = print (last nats)
\end{example}
\end{minipage}
\begin{minipage}{30ex}
\begin{trace}{5}{3}
\oute{1}{1}{map}{map ($\backslash$) (0 : (($\backslash$) 0) : $\Box$ : $\Box$)}
\oute{1}{2}{nats}{nats}
\toParent{map}{nats}
\end{trace}
\end{minipage}

The redex trail would be more interesting, if the user had interrupted
the program while a recursive call of \texttt{last nats} was evaluated.

It would be possible for a CAF to have a redex trail. However, this implies loss of sharing of the CAF.

$${\cal F}[\![ f = e ]\!] \Rightarrow f~\texttt{t} = {\cal E}[\![e ]\!]_{(\texttt{Nm}~\texttt{t}~{\cal N}[\![f]\!])}$$

\freja
Every CAF has its own EDT. So a program has a forest of EDTs which are ordered according to dependency (as far as possible).

\buddha
Not described. It seems that no EDT is produced for a CAF and its evaluation history is lost. 

\stories
Not discussed.


\subsection{Guards}

\begin{minipage}{20em}
\begin{example}
f x | x < 0 = -1
f x | x > 0 = 1
f x = 0

main = print (f 0)
\end{example}
\end{minipage}
\begin{minipage}{30ex}
\begin{trace}{7}{8}
\oute{6}{1}{gnull}{0}
\oute{6}{2}{gprint}{print \ine{gprintnull}{0}}
\oute{3}{4}{gf}{|\ine{gf1}{False} $\lhd$ \ine{gfg}{|\ine{gf2}{False} $\lhd$ \ine{gff}{f 0}}}
\oute{1}{6}{gless}{\ine{gless0}{0} < 0}
\oute{3}{6}{ggreater}{\ine{ggreater0}{0} > 0}
\oute{6}{7}{gmain}{main}
\toParent{gnull}{gprint}
\toParent{gprint}{gmain}
\toParent{gprintnull}{gf}
\toParent{gf1}{gless}
\toParent{gf2}{ggreater}
\toParent{gless}{gfg}
\toParent{ggreater}{gff}
\toParent{gless0}{gmain}
\toParent{ggreater0}{gmain}
\toParent{gff}{gmain}
\nccurve[angleA=260,angleB=280]{->}{gf}{gfg}
\nccurve[angleA=260,angleB=280]{->}{gfg}{gff}
\end{trace}
\end{minipage}

\art
A function definition with guards leads to a special, extended
redex. The redex has an additional list of truth values, each with its
own redex trail, for the values of all the guards that were needed to
reduce the redex. See preceeding example. This is not discussed in any paper.

\edt
There is no special node for guards.

\freja
Guards are not discussed. Expect guard derivations as children of the
redex whose definition contains the guards.

\buddha
The EDTs of all guards and redexes that were evaluated to evaluate a
guard are direct children of the redex whose definition contains the
guards. This is only so for a single equation of a function
definition. If all guards fail computation continues with a subsequent
equation, then all EDTs of the guards are lost (probably easier to
implement; hence Buddha forbids overlapping left hand sides).

\stories
Not discussed

\subsection{List Comprehensions}

\art
Not yet dealt with. Shown in terms of the functions that internally implement them.

\freja
A list comprehension is a redex. A simple, intuitive semantics of list comprehensions, which reduces a comprehension to a similar one, is used for the construction of the EDT. Not yet implemented.

\buddha
Not yet dealt with.

\stories
Not part of the language.


\subsection{I/O}

\begin{minipage}{20em}
\begin{example}
putLine "" = return ()
putLine (c:cs) = do
  putChar c
  putLine cs

main = do
  xs <- getLine
  putLine xs
\end{example}
\end{minipage}
\begin{minipage}{30ex}
\begin{trace}{6}{8}
\oute{2}{1}{io1}{o}
\oute{3}{1}{io2}{k}
\oute{2}{2}{iopc}{putChar 'o'}
\oute{2}{3}{iopl}{putLine "ok"}
\oute{2}{4}{iook}{($\backslash$) "ok"}
\oute{2}{5}{ioio1}{\ine{ioin1}{IO $\Box\!\!\!/$} >> \ine{ioin3}{IO ($\backslash$)}}
\oute{2}{6}{ioio2}{\ine{ioin2}{IO $\Box\!\!\!/$} >> ($\backslash$)}
\oute{2}{7}{ioget}{getLine}
\oute{4}{7}{iomain}{main}
\oute{5}{6}{ioexit}{exitWith prim}
\toParent{io1}{iopc}
\toParent{iopc}{iopl}
\toParent{iopl}{iook}
\toParent{iook}{ioio1}
\toParent{ioin1}{ioio2}
\toParent{ioio2}{iomain}
\toParent{ioin2}{ioget}
\toParent{ioin3}{ioexit}
\end{trace}
\end{minipage}


\art
Handles IO for standard input and output. Leads to some weird redexes
as for example \texttt{IO $\Box$ >> IO ($\backslash$)} (see preceding)
partial redex trail). The output is divided into fixed parts. Each part was
created by a single output action and has this action as parent.
It is not possible to select several parts at the same time. Not described in any paper.

\freja
No IO. The function \texttt{main} of type \texttt{String} is reduced and its normal form printed.

\buddha
No IO. Older paper discusses how stream based IO can be handled. It does not suggest to hide any IO details from the user.

\stories
Not part of the language.

\hood
Also values of type IO (actions) can be observed. Only the return
value of an action is shown, not the action itself.

%------------------------------------------------------------------------------

\section{Design of the Implementation}

\subsection{How is Trace Created?}

\art 
A transformer transforms the program into another one which creates a trace besides the original output. The transformation is uniform for expressions of all types. Running the compiled transformed program creates the trace.

\freja
By the object code of the compiled program. The low-level implementation promises better performance.

\buddha
A transformer transforms the program into another one which creates a trace besides the original output. The transformation is not uniform. Only expressions of functional type are transformed, others are left unchanged. Hence type information is required.

\stories A transformer transforms the program into another one which
creates a trace besides the original output. The transformation is
purely syntax-directed.

\hood A programmer annotates his program with the combinator
\texttt{observe}, which is defined in a library that has to be
imported.  When the program is run, the occurrences of the combinator
create the trace by writing to a file as a side-effect. The combinator
\texttt{observe} does not influence the program semantics in any other
way.

\subsection{Parts of Debugger}

\art The system consists of three pieces: a source-to-source program
transformer, which is currently integrated into the nhc compiler, an
extension of the runtime system and a browser.  When the compiled
transformed program stops, the extension of the runtime system takes
over and connects to the separately running browser, transfering trace
information to it.

\freja A new compiler produces code that creates the trace.  A quite
separate navigator/debugger is linked to the object code. When the
program stops its usual task the debugger automatically takes over.

\buddha The system consists of a source-to-source program transformer
and a Haskell library which implements the debugger.  When the program
stops its usual task the debugger automatically takes over.

\stories The system consists of a soure-to-source program transformer
and a browser for walking through a story. Walking through the story
with the browser forces the execution of the respective parts of the
program.  Unclear how debugger and language execution
(Gofer interpreter?) is implemented.

\hood
The system consists of the library with combinators such as
\texttt{observe} and a separate browser that reads the trace file.

\subsection{How is Trace Represented?}

\art
As Haskell data structure with links to C tables for information about
names and source references. All data type definitions of the original
program are transformed. The data structures of the program are
interwoven with links to the trace structure. There are no links from
the trace to data structures of the program. 

\freja
As C data structure with links to the data structures of the original program.
(opposite direction with respect to redex trails!). The normal heap nodes also contain additional information.

\buddha
As Haskell data structure, separate from the data structures of the
original program. However, it is separate only at the end when trace
has been built. At runtime the trace has links to the expressions of
the original program that
are under evaluation.

\stories Seems to be represented by a Gofer data structure. It is
separate from the data structures of the original program.  However,
it is separate only when full trace has been built. At runtime the
trace has links to the expressions of the original program that are
under evaluation.

\hood
As an XML file.

\subsection{How is Printable Form Obtained?}

\art
Some trace nodes contain a string and a source reference. The printable
form of a node is constructed from the strings of several nodes.

\freja
An EDT node contains a string and source references for that purpose.

\buddha
The primitive function \texttt{dirt} transforms any value into printable form.
Partial applications as arguments carry additional information in a
string.

\stories
A value node of a story contains a value which is printable. The
printable form of an application node is constructed from the
printable form of its three stories (value of these stories).

\hood
An observation contains the observed constructor as string?


\subsection{How is Assured That No Additional Evaluation Occurs?}

\art
The C part which connects to the browser can distinguish unevaluated from evaluated heap objects.

\freja
The interface to the debugger permits distinguishing unevaluated from evaluated heap objects.

\buddha
\texttt{dirt} transforms a value into printable form without
evaluating it further.

\stories
Additional evaluation does occur, because only values are printed.

\hood
Evaluation triggers creation of the trace. Expressions that are not
evaluated do not contribute to the trace.

%------------------------------------------------------------------------------

\section{Intended/Possible Use of Trace}

\art
Main application of the trace and only one discussed in papers is locating bugs. Also intended for understanding why/how a correct program works.

\freja
Only debugging is stated as intended use of the system.

\buddha
Only debugging is stated as intended use of the system.

\stories
Only debugging is stated as intended use of the system.

\hood
Only debugging is stated as intended use of the system.

\medskip\noindent
Use of systems for teaching functional programming is not mentioned anywhere.


\subsection{How is Trace Used for Locating Bugs?}

\art
By following redex trails backwards from erroneous values. No general
rule for locating bugs (Memo needed!).

\edt
Either by algorithmic debugging, answering yes/no questions, or by
stepping through the strictified computation like in debugging of
imperative languages.

\stories 
According to the authors by both ``algorithmic debugging and
faulty function investigation''. The examples resemble stepping
through the strictified computation like in debugging of imperative
languages.

\hood 
Trace enables programmer to locate differences between what the
computer has been told to do and what the programmer thinks the
computer should be doing.  No general rule for locating bugs.


\subsection{Possible to Investigate Specific Function Definitions?}

\art
By making uninteresting functions trusted, only redexes for others are shown.
However, its not possible to make functions trusted or untrusted in the browser for focusing. Not possible to find occurrences of specific function within a trace.

\freja
An EDT may be created that starts with the first application of a
specific function, skipping all computation needed to reach this application.
Functions can be made trusted or untrusted in the navigator.

\buddha
No.

\stories
No.

\hood
Not specific function definitions, but data at specific program
locations. Likewise a function can be observed at a given location.

%------------------------------------------------------------------------------

\section{Kinds of Errors for which Debugger is suitable}

\subsection{Termination with Wrong Result}

\art
Yes. Debugging consists of following the trace of a wrong result. 

\freja
Yes. Answer to first question will be ``no''.

\buddha
Yes. Answer to first question will be ``no''.

\stories
Yes. Debugging will follow result of \texttt{main}.

\hood
Yes.


\subsection{Termination with an Error?}

\art
Yes. If an error occurs, then process connects to browser. An error
has value $\bot$. The error is the starting point of the trace.

\freja
Yes. If an error occurs, then debugger takes over. An error has value $\bot$.

\buddha
No. Non-erroneous termination is required.

\stories
No. Non-erroneous termination is required.

\hood
Applicable but not necessarily helpful. The trace does not show where
error occurred. Programmer must observe the right locations.

\subsection{Non-Termination (How Interrupt in Consistent State?)}

\art
Yes. The user can interrupt a non-terminating program. Then the process connects to the browser. The redex which was under evaluation at the time of interruption is the starting point of the trace.

Papers do not discuss how interruption is handled.

\freja
Yes. The user can interrupt a non-terminating program. Then the debugger takes over. The result value of all redexes which were under evaluation at the time of interruption is $\bot$.

Test for interruption every time new heap space is claimed (problem if non-terminating program does not require heap).

\buddha
No. Non-erroneous termination is required.

\stories
Yes. Debugger forces evaluation and creates story only up to given depth.

\hood
Applicable but not necessarily helpful. The trace does not show where
the infinite recursion occurred. Especially difficult if the infinite
recursion does not produce any data. Programmer must observe the right locations.


\subsection{Black Hole}

\art
Yes. Similar to non-termination except that the program stops by itself.

\freja
Yes. Similar to non-termination except that the program stops by itself.

\buddha
No. Non-erroneous termination is required.

\stories
No.

\hood
Same as non-termination.

%------------------------------------------------------------------------------

\section{Performance}

\subsection{How is Space Problem Attacked?}

\art

First, a function can be trusted so that no redex created by its definition body for a trusted function appears in the trace.
Second, all redex trails can be limited to a given maximal size
(either to given depth or to global heap size limit). At garbage collection time all redexes that are longer are pruned.

\freja

First, a function can be trusted so that no EDT node appears for calls to it (for recursive functions the first call appears in the EDT).
Second, the EDT may only be produced up to a given depth. When the cut-off part of the EDT is needed during debugging, then the program is reexecuted to produce another part of the EDT.

\buddha
Mentions trusting of functions and production of upper part of EDT with reexecution. Authors believe that lazy evaluation of EDT will save space.

\stories
Not discussed.

\hood
Only data at programmer selected locations are observed. Because trace
is written in file, the increase in required heap space should be
modest (no measurements).

\subsection{Incremental Archiving Feasible?}

\art
Yes, see Memo 3.

\freja
Very difficult, because EDT grows at so many edges.

\buddha
Not discussed.

\stories.
Not discussed.

\hood
Yes, always done. XML trace file may be compressed by a standard tool.

\subsection{How is Run-Time Problem Attacked?}

\art
Programs run 6-36 times slower (without consideration of garbage collection). 
For improvement key auxiliary functions may be moved into the run-time system.

\freja
Low level implementation was chosen to gain good run-time results.
In the worst case a program ran 17 times slower, including garbage collection time, which by far took the major part.

\buddha
Time is not discussed.

\stories
Time is not discussed.

\hood
Time is not discussed. However, if data at only a few program
locations is observed, then additional cost should be limited.

%------------------------------------------------------------------------------

\section{Practical Side of Debugger}

\subsection{Portability to Different Haskell systems}

\art
Although the transformational approach was chosen to acquire portability, the system is currently not portable. The transformation is performed on the abstract syntax within nhc. The compiler and especially the runtime system have been modified in several parts. The graphical browser is portable, because it is separate and written in Java.

\freja
Not portable, because it would require modification of nearly every phase of a Haskell compiler/system. It is a Haskell system of its own.

\buddha
Buddha really performs a source-to-source transformation. The declarative debugger is a library written in Haskell which is imported by the program that is to be debugged. These parts are perfectly portable. However, the function \texttt{dirt}, which is used by the debugging library, is not portable and may be very difficult to implement for all Haskell compilers, because the required information is not available at runtime. 

\stories
If debugger is implemented as library, then system should be portable.

\hood 
Highly portable (proven in practise), because the library only
requires Haskell 98, except for the special function
\texttt{unsafePerformIO}, which is provided by all Haskell
implementations.  The graphical browser is portable, because it is
separate and written in Java.


\subsection{Which influence have compiler optimisations on trace construction?}

For all methods the semantics of the program is not changed by compiler optimisations.

\art
Optimisations which duplicate or share expressions change the observed sharing properties. The trace reflects the real sharing of the program, not the sharing of a simple semantics of the original program.

\edt
Transformations that change sharing may indirectly show up in how far arguments are evaluated.

\freja
Is a comiler of its own with its own optimisations. Every compiler transformation must be implemented so that a mapping between original program text and final abstract machine code is preserved. 

\stories
Should have no effect.

\hood
Optimisations which duplicate non-value expressions may duplicate occurrences of the \texttt{observe} combinator and thus lead to irritating repeated observations.

\subsection{Availability}

\art
Distributed as part of nhc. Interactive graphical browser. Covers most of Haskell 98.

\freja
Executable for Solaris available. Lacks especially most of class system, \texttt{do}-notation, monadic IO and standard libraries.

\buddha
Does not seems to be available. 
Supports the subset of Haskell that resembles Miranda.

\stories
Does not seems to be available. 
Supports a tiny toy language.

\hood
Available from the haskell.org CVS repository. Covers full Haskell 98
plus extensions.

%------------------------------------------------------------------------------

\section{Specific Advantages and Disadvantages}

\edt
Provides a method for locating bugs (algorithmic debugging). However,
a large number of questions may have to be answered and they may be
difficult to answer because of the size of data structures.

%------------------------------------------------------------------------------

\section{Others}


\buddha
Considers soundness and completeness of a debugging method.

%------------------------------------------------------------------------------

\appendix
\section{Debugging with Freja (hhc) in York}

\begin{enumerate}
\item You have to login on a Solaris 2 machine (tested on doozer)
\item You must have \texttt{/grp/fp/bin/solaris2} in your
\texttt{Path} (good idea anyway)
\item Compile a Freja program with \texttt{hhc -g \emph{name}.fr}
\item Run the resulting program with \texttt{\emph{name} -- -d}
\item Use the command \texttt{help} to obtain a list of debugger commands
\end{enumerate}

Several example programs are in
\texttt{/grp/fp/lib/FrejaDist/Examples}.

\medskip\noindent
Stolen from the readme file:

\medskip\noindent
Please be aware of the following:
\begin{itemize}

\item The Freja compiler does currently not implement Haskell, only
  a Haskell subset. In particular:
\begin{itemize}
  \item No user-defined type classes.
  \item No support for monadic programming (do-notation).
  \item No (monadic) I/O. Only output in the form of a list of characters.
\end{itemize}

\item There are many other bugs and shortcomings. Some bugs to watch out for:
\begin{itemize}
  \item Top-level pattern bindings does not work.
  \item It is not verified that main has type [Char]. If it has some
    other type, the program will crash when executed.
\end{itemize}
\end{itemize}           

The compiler is normally invoked via the compiler driver ifc. ifc expects to
find Freja source code in files with the extension ".fr". Interface files have
the extension ".fi", and Runtime System Dependence files the extension ".rsd".
There are no limitations regarding the number of modules that can be put in a
file. Nor are there any naming conventions regarding what a file containing a
module must be called. Thus the Freja compiler needs to be invoked on all
files which are relevant; i.e., if one module depends on another, either its
source must be present in one of the ".fr" files given on the command line,
or, when doing separate compilation, its interface must be present in one of
the ".fi" files given on the command line.

Example. If the current working directory contains a set of ".fr" files
containing a set of modules making up a program, the following command could
be used to compile it, placing the executable in the file foo:

\begin{verbatim}
    ifc -o foo *.fr
\end{verbatim}

In order to compile for debugging, supply the -g flag:

\begin{verbatim}
    ifc -g -o foo *.fr
\end{verbatim}

In order to invoke the debugger, the binary has to be invoked in debugging
debugging mode:

\begin{verbatim}
    foo -- -d
\end{verbatim}

The debugger has a built-in help facility.

Both ifc and fcomp, the compiler proper, have fairly extensive descriptions
of their command line options. Use the flag -h.
 


%------------------------------------------------------------------------------

\bibliographystyle{alpha}
\bibliography{biblio}
 
%------------------------------------------------------------------------------
 
\end{document}