% Author: Olaf Chitil
% Created: 8.11.2001
% Last Update: 
  
\documentclass[12pt]{article}
\usepackage[a4paper]{geometry}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{alltt}
\usepackage{url}

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

\begin{document}
\thispagestyle{empty}

\title{ART Memo 27 (Version 1)\\Pragmatics of an Augmented Redex Trail} 
\author{Olaf Chitil}
\date{\today}
\maketitle

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

\section{Introduction}

Discussion of the meaning of a trace, an Augmented Redex Trail, in practise.
Design options brought to light.

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

\section{Functions and Applications with Arity}

\subsection{Functions with Arity}

In pure $\lambda$-calculus any application of a $\lambda$-abstraction is a redex. In contrast, in Haskell a function definition usually has several arguments and it would be rather unnatural to model Haskell functions as taking one argument at a time. Hence every Haskell function (a defined variable or a $\lambda$-abstraction) has an arity. An application of a function of arity $n$ to $m$ expressions is a value iff $n > m$.

\subsection{Applications with Arity}

The presence of n-ary functions does not force the presence of $n$-ary applications. In fact, given a language with n-ary functions, it is usually easier to formulate an operational semantics with binary applications than with n-ary applications. A semantics for the latter requires the distinction between three cases when considering an $m$-ary application of an $n$-ary function:
\begin{enumerate}
\item $n > m$: the application is undersaturated; the application is a partial application, it is a value.
\item $n = m$: the application is saturated, it is a redex.
\item $n < m$: the application is oversaturated; \emph{part} of the application is a redex.
\end{enumerate}
The semantics of an oversaturated application is the most complex of the three and just that case does not exist if all applications are binary.

Saturatedness of an application is only defined for an application whose function subexpression is a value (only functional \emph{values} have an arity). Hence in a higher-order language it is not possible to classify applications in the \emph{program} as undersaturated, saturated or oversaturated. Only when an application in a computation is evaluated its functional part is evaluated and then the saturatedness is known. 

However, the trace language ART has n-ary applications, because it would be rather expensive in time and space to build every n-ary application from binary applications. So an n-ary application in the program will give rise to n-ary applications in the trace. 

\subsection{Representation in the Trace}

An application node is created in the trace at the moment when a redex is reduced and its rhs has to be created in the trace. At that point the saturatedness of the applications is in general still undetermined.

Different sorts of applications are represented as follows in the trace. During computation and hence trace creation the sort of an application can still change. I hope this is correct. The square brackets refer to the planned new trace design.

\begin{description}
\item[Unevaluated] Saturatedness has not been determined.

A SatA pointing to the application node just in front of it.
[An application node with result root.]

\item[Entered but not evaluated] Saturatedness may have been determined.

A SatB pointing to the application node just in front of it.
[An application node with result pointing to rhs as in following cases?]

\item[Evaluated, undersaturated]
A SatC pointing to the application node just in front of it.
[An application node with result pointing to itself.]

\item[Evaluated, saturated]
A SatC with the application node (redex) just in front, but it points to the rhs.
[An application node with result pointing to the rhs.]

\item[Evaluated, oversaturated]
A SatC. The application node is just in front. The SatC points to another Sat(A/B/C) with an application node in front. This second application can again be of any of the sorts described here. Both application nodes have the same parent (this marks oversaturatedness). The second application node applies the result of the redex of the first application to the superfluous arguments of the first application.
[The result pointer takes the role of the Sat and it points to the second application, not just its result pointer.]

Example:
\begin{alltt}
g z = z
f x y = g
main = f 3 2 1
\end{alltt}
$$\texttt{main} \to \texttt{f 3 2 1} \to \texttt{g 1} \to \texttt{1}$$

Both \texttt{f 3 2 1} and \texttt{g 1} have \texttt{main} as parent.
\texttt{g} has \texttt{f 3 2 1} as parent.

So an application node in the trace is either a redex or a value, except if it is an oversaturated application. It is the task of the viewing tools to recognise oversaturated applications and to rearrange that part of the trace to show it correctly (currently not done).

Here \texttt{f 3 2 1} and \texttt{g 1} have to be replaced by an application of the reduction $\texttt{f 3 2} \to \texttt{g}$ to the single argument \texttt{1}.
\end{description}

It seems impossible to create the trace for oversaturated applications correctly. At the latest when an application needs to be evaluated, it must be recorded in the trace. However, only when the function part is evaluated the saturatedness of the application is known. If the computation is aborted between these two events, this must be visible in the trace. Then the result of the reduction is $\bot$ and the aborted computation is reachable in the trace though the function part.


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

\section{Granularity of Tracing}

Tracing shows a computation at a certain level of detail.
The granularity of the (shown) trace may be coarser or finer.
On the one hand fine granularity may yield unnecessary, distracting details, on the other hand only fine granularity may expose the desired information.
Hence switching between different levels of granularity may be desirable.
It is important for a level of granularity to be natural and to have a simple definition.

For example, currently hat-detect and hat-observe only show redexes of top-level functions, whereas hat-trail shows redexes of all functions. In the future there may be two levels of granularity for all tools: show redexes of either top-level functions only or of all functions.

Both the problem of the meaning of \texttt{\_} and untraced computation yield several different answers with different granularity.

There is a tradeoff not only between level of detail and cost, but also between accuracy and cost.

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

\section{Superfluous Detail --- The Meaning of \texttt{\_}}

By default both hat-detect and hat-observe represent some subexpressions by the symbol \texttt{\_}. The idea is that knowledge about these subexpressions is not needed for the purpose of the tools (certainly not needed to answer the questions of hat-detect) and avoiding superfluous details improves the usability of a viewer. Unfortunately hat-trail is not able to show unevaluated applications as \texttt{\_}, so that speculations that this might improve the usability of hat-trail could not be verified.

Currently those expressions are represented by \texttt{\_}, that are not literals or static saturated constructor applications and that were not needed by the whole computation. This definition of \texttt{\_} is rather complex and nonintuitive.
For example, for the program
\begin{alltt}
main = print (const 42 3, const ((+) 1) 3) 
\end{alltt}
hat-detect and hat-trail will show redexes \texttt{const 42 3} and \texttt{const \_ 3}. Both \texttt{42} and \texttt{(+) 1} are values and both are not needed by the computation.

\subsection{Values}

An expression is a value iff it is irreducible. An oversaturated application is not a value, because to reduce its redex part the whole application has to be replaced by a new application.

To understand the observed actions of a computation, those subexpressions of redexes and results that are not values are not needed. A non-value subexpression was definitely not needed by the computation. Hence all non-value subexpressions could be shown as \texttt{\_}.

Currently it is impossible to determine which expression in the trace is a value, because this decision cannot be made for applications of function values. It could be determined if such an application is a value, if the arity of the function was known. The current trace does not contain the arity.

\subsection{Needed Expressions / Values}

Freja shows subexpressions of redexes and results only if they are needed by the full computation. Hood even only shows values which are needed by the context of its observation.
So to understand the observed actions of a computation, only those subexpressions of redexes and results are needed which are needed by the computation.

A needed subexpression that is not a value indicates that the computation was aborted when the subexpression was evaluated. Such a subexpression is represented as $\bot$.

An ART contains and the Hat tools show values which are never needed by the computation. Consider for example:
\begin{alltt}
f x = [x,x,x]
main = print (null (f 42))
\end{alltt}
The trace contains the expression \texttt{[42,42,42]} and the tools show this expression for example as argument of \texttt{null}, although in the whole computation only the outermost cons constructor of the list is ever needed.

Admittedly, showing only the needed value \texttt{\_:\_} might be irritating to the user, because according to the program and its na\"ive semantics, the whole list has clearly been constructed.

An ART contains unneeded values, because every time a redex is reduced the whole rhs is created in the trace. The tools show such unneeded values, because currently it is impossible to determine from the trace if a value was needed or not; at least for literals and saturated constructor applications, for partial applications neededness can be determined.

Marking needed values is straightforward but will increase trace size and tracing time slightly (values could have Sat's or result pointers like applications or a special bit could be used).


\subsection{Superfluous Subexpressions in Trace}

Above we suggested that only those subexpressions of redexes and results which are values or even only needed values should be shown. We discussed which information would need to be added to traces to classify subexpressions.
Assuming that we are not interested in finer granularity, it would be even better not to store any subexpressions that are not shown in the trace. The trace would be smaller. However, it is unclear if creating it would be easier. Current experience with implementing untraced code suggests that it could even be more complicated and time consuming.


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

\section{Untraced Computations}

Part of a program can be designated as untraced to first of all avoid unnecessary detail in the trace. A good first intuition is to view untraced functions as internal primitives; for untraced functions only inputs and outputs are visible. However, the fact that traced or untraced functions can be part of inputs or outputs makes a definition of untracedness hard.

\subsection{Properties of the Trace of Untraced Computation}

A few desirable properties:
\begin{itemize}
\item the application of an untraced function called from traced code is in the trace, including (needed) arguments
\item the (needed) value of the redex is in the trace
\item there is no distinction in input and output between first-order and higher-order values (partial applications); all are in the trace
\item if evaluation of the untraced function causes evaluation of a traced function, the whole computation of this traced function, from application to final value, are in the trace
\item the parent of all traces of untraced code is the hidden original application of the untraced function (currently the top of the rhs of the original application has the original application as parent, unhidden)
\item the trace of a non-needed untraced expression is the hidden original application of the untraced function (except possibly for literals and saturated constructor applications).
\item all hidden expressions must be non-needed expressions, because in hat-detect hidden expressions will be shown as \texttt{\_}
\item intermediate untraced computation may not need SatB's; important are only SatB's in the result to represent $\bot$
\item untraced code that does not appear in any redex or result mentioned above does not yield any trace
\item I/O actions should always be registered in the trace, even if performed by untraced code
\end{itemize}

An application belongs into the trace if the application or the function value are traced (and it is needed?). The program statically determines the tracedness of an application, but the tracedness of the function part is only known after it has been evaluated.

\subsection{Visibility of Identifiers}

It seems natural to demand that when an abstract data type is designated as untraced, the trace should only show those identifiers of the abstract data type which are in the public interface. The internal representation of abstract data and probably also partial applications of internal functions should not be visible. 

Instead of seeing the name of the internal function and the supplied arguments, it might be desirable to see the mapping a la Hood of such the partial application.
Similarly, instead of seeing an abstract value, it might be desirable to see all uses of the value in the computation.

To implement such kind of tracing, the visibility frontier needs to be \emph{defined}. There exist several interfaces between traced and untraced code, because entities of a single untraced module may be imported from several traced modules via different routes with different visibility. Second, the visibility of every identifier must be accessible at program transformation or at tracing time.

%------------------------------------------------------------------------------
\end{document}
