% rtsemantics.tex

% Author: Olaf Chitil
% Created: 30.6.2000
% Last Update: 
  
\documentclass[12pt]{article}

\usepackage{pst-node}
\usepackage[a4paper]{geometry}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{alltt}
\usepackage{url}
\usepackage[thmmarks]{ntheorem}

%------------------------------------------------------------------------------
% Einstellungen f"ur die floats (bewegliche Objekte) auf einer Seite
\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{\troot}[2]
{\rput(#1,#2){\rnode{root}{\psframebox{\strut{}Root}}}}
\newcommand{\touter}[5]
{\rput(#1,#2){\rnode{#3}{\psframebox{\strut{}#5}}}\ncline{->}{#3}{#4}}
\newcommand{\tinner}[2]
{\rnode{bbbb}{\psframebox{\strut{}#2}}\ncline{->}{bbbb}{#1}}
\newcommand{\sub}[1]
{\rnode{bbbb}{$\bullet$}\ncline[linestyle=dotted]{->}{bbbb}{#1}}
\newcommand{\result}[3]
{\rput(#1,#2){\rnode{bbbb}{$\bullet$}}\ncline{->}{bbbb}{#3}}




% Mathematical symbols:
% set of natural numbers
\newcommand{\nat}{I\!\!N}

\newcommand{\rulename}[1]{\textsc{#1}}

% syntax of the core language
\newcommand{\caseL}{\texttt{case}}
\newcommand{\letL}{\texttt{let}}
\newcommand{\caseOf}[3]{\mbox{\tt{case }} #1 \mbox{\tt{ of }} \{#2\}#3}
\newcommand{\letIn}[3]{\mbox{\tt{let }} \{#1\}#2 \mbox{\tt{ in }} #3}
\newcommand{\app}[2]{#1\,#2}
\newcommand{\ifthenelse}[3]{\mbox{\tt{if }} #1 \mbox{\tt{ then }} #2 \mbox{\tt{ else }} #3}
\newcommand{\True}{\texttt{True}}
\newcommand{\False}{\texttt{False}}
\newcommand{\trust}{\texttt{trust}}
\newcommand{\suspect}{\texttt{suspect}}

\newcommand{\trustedRed}{\operatorname{trustedRed}}
\newcommand{\markHidden}{\operatorname{markHidden}}
\newcommand{\dom}{\operatorname{dom}}
\newcommand{\hole}{[\cdot]}
\newcommand{\contexte}{\mathbb{E}}

\newcommand{\reduce}[2]{#1\,\rs\,#2}
\newcommand{\eval}[2]{#1\,\rs^*\,#2}
\newcommand{\graph}[2]{#1:#2}
\newcommand{\ggraph}[2]{#1\,:\,#2}

\newcommand{\valueAt}[3]{#1\succ_{#2} #3}
\newcommand{\reduceAt}[3]{#1\,\rs_{#2}\,#3}
\newcommand{\reduceAtA}[4]{#1\,\rs_{#2}^{#3}\,#4}
\newcommand{\mismatch}[3]{#1 \bowtie^{#2} #3}
\newcommand{\patCon}[1]{\mathbb{C}_{#1}}

\newenvironment{mlines}{\begin{array}{@{}l@{}}}{\end{array}}

\newenvironment{seqproofl}%
{\begin{quote}\begin{math}\begin{array}{c@{\,\,}l}}{\end{array}\end{math}\end{quote}}%
\newcommand{\seqnext}[1]{\\[-1.2ex]#1&\\[-1.2ex]}
\newcommand{\seqtext}[2]{\\[0.7ex]#1&\quad\text{\{#2\}}\\[0.7ex]}
\newcommand{\seqtextl}[2]{\\[0.7ex]#1&\quad\left\{\text{\begin{lines}#2\end{lines}}\right\}\\[2ex]}



\newcommand{\RA}{\mathop{\raisebox{0pt}[3pt][-2pt]{$\rightarrow$}}\limits}
\newcommand{\LRA}{\mathop{\raisebox{0pt}[3pt][-2pt]{$\longrightarrow$}}\limits}
\newcommand{\LA}{\mathop{\raisebox{0pt}[3pt][-2pt]{$\leftarrow$}}\limits}
\newcommand{\LLA}{\mathop{\raisebox{0pt}[3pt][-2pt]{$\longleftarrow$}}\limits}

\newcommand{\rs}{\mathop{\raisebox{0pt}[3pt][-2pt]{$\Rightarrow$}}\limits}


% Settings for the theorem package:
\theoremnumbering{arabic}
\theoremstyle{plain}
\theoremsymbol{\ensuremath{_\Box}}
\theorembodyfont{\itshape}
\theoremheaderfont{\normalfont\bfseries}
\theoremseparator{}
\newtheorem{theorem}{Theorem}[section]
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}

\theorembodyfont{\upshape}
\newtheorem{example}[theorem]{Example}
\newtheorem{remark}[theorem]{Remark}
\newtheorem{definition}[theorem]{Definition}

\theoremstyle{nonumberplain}
\theoremheaderfont{\scshape}
\theorembodyfont{\normalfont}
\theoremsymbol{\ensuremath{_\blacksquare}}
\newtheorem{proof}{Proof}
\qedsymbol{\ensuremath{_\blacksquare}}


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

\title{ART Memo 7 (Version 2)\\A Semantics for Redex Trails} 
\author{Olaf Chitil}
\date{\today}

\maketitle

\begin{abstract}
We define a small step operational semantics for a core of Haskell.
We extend this semantics to additionally create redex trails.
This small and direct semantics of redex trails shall improve our understanding of them and shall help to modify or extend them in a useful way.
\end{abstract}

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

\section{Introduction}

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

\subsection{Redex Trails}

A redex trail is a directed graph. Every node is labelled with an expression which 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
expression, if it created that expression.  An expression 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 expression is the graph consisting of its parent and the
parents of its subexpressions and recursively the redex trails of
these parents.  Although the
sequence of parents can be seen as the main redex trail of an
expression, 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 a node expression 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 any arrow. Note that a redex is a proper subexpression
of a node expression only if this redex was never evaluated. Hence it
cannot be the target of an arrow.

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

\subsection{Definition of Redex Trails}

The current definition of redex trails in 
\cite{sparudruncimanplilp97,sparudruncimanifl97} is insufficient.
Redex trails are introduced informally only at the hand of a few examples.
The only formal definition of redex traces is given through 
the transformation that enables the creation of the trace. However, this definition is inadequate. The fact that the description of the transformation is incomplete and contains errors is only a minor problem.

To obtain the redex trail of a program, the program has to be transformed as described and then be executed to create the trail. This has the following disadvantages:

\begin{itemize}
\item 
It is not easy to determine the redex trail of even a simple program by hand. 
\item 
The second stage of obtaining a redex trail is based on the semantics of the \emph{transformed} program. This is rather confusing, because 
the purpose of a redex tail is to give an abstract view of the computation of the \emph{original} program. 
\item 
Although it is the purpose of a redex tail to give an abstract view of a computation, a description of the computation of a program is not part of the definition. It remains unclear which assumptions about the operational semantics are made, both in that a redex trace shall be an abstraction of a computation and that the execution of the transformed program shall yield the desired redex trail.
\end{itemize}

So the transformation defines a redex trail only in a very indirect manner, as depicted here:

$$\text{computation} \LLA^{semantics} \text{program 1} \LRA^{transformation} \text{program 2} \LRA^{result~semantics} \text{redex trail}$$

We conclude that the transformation is a good definition of an implementation of redex trails but not a good definition of redex trails themselves.

Hence we give a direct definition of redex trails here.
Because a redex trail shall give an abstract view of a computation, we start with a high-level semantics of a functional language and then extend it to describe redex trails beside the normal semantics. This semantics will not have the disadvantage listed before and we can furthermore use it for the following purposes:

\begin{itemize}
\item
Inconsistencies between the two definitions of redex trails will improve our understanding of them.
The final consistency of the two definitions of redex trails will give us confidence that we have defined what we had in mind.

\item 
To prove the correctness of the transformation that implements redex trails.

\item
To extend redex trails systematically to language constructs for which they are not yet (properly) defined, for example list comprehensions and IO.

\item
In \cite {sparudruncimanifl97} it is claimed that the redex trail of a program 
is complete, that ``every reduction occurring in the computation can be observed in the trail''. It would be nice to prove this property.
\end{itemize}


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

\subsection{The Importance of Sharing}

The notions of reduction and reducible expression (redex) are certainly operational. Hence we have to start with an operational semantics although a redex trail does not fully describe a full computation.

A simple term-based call-by-name reduction semantics unfortunately does not suffice, even if we ignore that the redex trail shall desribe the sharing of subexpressions correctly. The redex trail shall also hold all subexpressions in most evaluated form.
The following example demonstrates this:

\begin{align*}
(\lambda b.\, b~\&\&~b)~(\text{True}~\&\&~\text{False})
\end{align*}

Call-by-name reduction:

\begin{seqproofl}
& (\lambda b.\,b~\&\&~b)~(\text{True}~\&\&~\text{False})
\seqnext{\Rightarrow}
& (\text{True}~\&\&~\text{False})~\&\&~(\text{True}~\&\&~\text{False})
\seqnext{\Rightarrow}
& \text{False}~\&\&~(\text{True}~\&\&~\text{False})
\seqnext{\Rightarrow}
& \text{False}
\end{seqproofl}

The redex trail:

\begin{trace}{14}{4}
\troot{1}{3}
\touter{6}{1}{and2}{root}{True~\&\&~False}
\touter{5}{3}{app}{root}{$(\lambda b.\,b~\&\&~b)~\tinner{and2}{\text{False}}$}
\touter{10}{3}{and}{app}{$\tinner{and2}{\text{False}}~\&\&~\tinner{and2}{\text{False}}$}
\touter{13}{3}{false}{and}{False}
\end{trace}

The above representation of the redex trail does not show that the three occurrences of False which have the same parent are actuall the same shared expression. Nonetheless the call-by-name reduction and this representation of the redex trail differ in an essential point: In the redex trail both arguments of \&\& in the parent of the result are False, whereas in the call-by-name reduction the second argument of \&\& is left unevaluated. So the fact that an expression is shared becomes important for the redex trail when it is \emph{updated}.

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

\section{A High-Level Operational Call-by-Need Semantics}

We do not want to tie ourselves to a specific abstract machine.
Hence Launchbury's natural semantics for call-by-need \cite{Launchbury93a} is the obvious choice for an operational semantics.
However, for our goal of defining redex trails many modifications are necessary.

A natural semantics only describes computations of expressions that have a value, that is, a weak head normal form. However, we are also interested in obtaining a redex trail for expressions that have value $\bot$, that is, whose computation leads to an error, a black hole, or an infinite computation that has to be interrupted. To be able to obtain a computation in this case we use a
small step variant of Launchbury's semantics (cf. \cite{WanPey99}).
To avoid confusion we postpone a detailed discussion of the similarities and differences between our semantics and variants of Launchbury's semantics to Section~\ref{Launchbury}.

In our first definition of the semantics we still restrict ourselves to a small language. We discuss further language constructs in subsequent sections.
Especially we forget about IO for the moment. In our semantics an expression just evaluates to a value.
The syntax is defined in Figure~\ref{syntax}. We give a semantics to an expression by defining to which value it evaluates. 


\begin{figure*}[htb]
\strut\hrulefill\strut
\begin{displaymath}
\begin{array}{rrrll}
\text{variable} & x,y,z \\
\\
\text{graph node (pointer)} & p,q,r \\
\\
\text{expression} & M,N & := 
& x & \text{variable}\\
&& \mid & p & \text{node}\\
&& \mid & \lambda x .\,M & \text{abstraction}\\
&& \mid & \app{M}{N} & \text{application}\\
\\
\text{value} & V & := & \lambda x.\,M & \text{abstraction}\\
\\
\text{simple evaluation context} & \contexte & := & \app{\hole}{p} & \text{application context}
\end{array}
\end{displaymath}
\caption{Syntax}\label{syntax}
\begin{gather*}
\cfrac
{\valueAt{\Gamma}{p}{\app{(\lambda x.\,N)}{q}}}
{\reduceAt{\Gamma}{p}{\Gamma[p \mapsto N[q/x]]}}
~\rulename{application reduction}
\\[3ex]
\cfrac
{\Gamma(p) = \app{M}{N} \quad \text{$N$ not a node} \quad q \notin \dom(\Gamma)}
{\reduceAt{\Gamma}{p}{\Gamma[p \mapsto \app{M}{q}]+\{q \mapsto N\}}}
~\rulename{ensure argument sharing}
\\[3ex]
\cfrac
{\Gamma(p)= \contexte[M] \quad \text{$M$ not a node} \quad \text{there is no redex $N$ with $\valueAt{\Gamma}{p}{N}$} \quad q \notin \dom(\Gamma)}
{\reduceAt{\Gamma}{p}{\Gamma[p \mapsto \contexte[q]] + \{q \mapsto M\}}}
~\rulename{new node for every redex}
\\[3ex]
\cfrac
{\Gamma(p) = \contexte[q] \quad \text{(there is no redex $N$ with $\valueAt{\Gamma}{p}{N}$)} \quad \reduceAt{\Gamma}{q}{\Delta}}
{\reduceAt{\Gamma}{p}{\Delta}}
~\rulename{follow need / enter context}
\\[3ex]
\cfrac
{\Gamma(p) = q \quad \reduceAt{\Gamma}{q}{\Delta}}
{\reduceAt{\Gamma}{p}{\Delta}}
~\rulename{follow variable}
\end{gather*}
\caption{Small step reduction rules}\label{semantics}
\begin{gather*}
\cfrac{}{\valueAt{\Gamma}{p}{\Gamma(p)}}
\quad\quad\quad
\cfrac
{\Gamma(p) = \contexte[q] \quad \valueAt{\Gamma}{q}{V}}
{\valueAt{\Gamma}{p}{\contexte[V]}}
\quad\quad\quad
\cfrac
{\Gamma(p) = q \quad \valueAt{\Gamma}{q}{V}}
{\valueAt{\Gamma}{p}{V}}
\end{gather*}
\caption{Value lookup}\label{lookup}
\strut\hrulefill\strut
\end{figure*}


To express sharing the semantics operates on rooted graphs instead
of expressions. 
An expression is respresented by a rooted graph, that is, a graph plus a graph node or pointer which indicates the top of the expression.
A graph, denoted by $\Gamma$ or $\Delta$, is a partial mapping from
nodes to expressions.
We write it as a set of tuples $p \mapsto M$.
The nodes of the graph are its domain, that is, the domain of the mapping.
The operator $+$ combines two graphs under the assumption that their domains are disjunct.
Computation is performed only on closed graphs, that is, graphs where the nodes of all terms in the graph are a subset of the domain of the graph.
So a closed graph represents a closed term with shared subterms.


In Figure~\ref{semantics} we define a reduction relation on rooted graphs, where $\reduce{\graph{\Gamma}{p}}{\graph{\Delta}{p}}$ or simply
$\reduceAt{\Gamma}{p}{\Delta}$ means that the graph
$\graph{\Gamma}{p}$ reduces to the graph $\graph{\Delta}{p}$.
A computation is a finite or infinite sequence of rooted graphs $G_1,G_2,\ldots$ with $\reduce{G_i}{G_{i+1}}$ for all rooted graphs in the sequence. Note that the reduction relation is actually a function, that is, the second graph is determined by the first. The computation of an expression $M$ is the computation beginning with the graph $\graph{\{p \mapsto M\}}{p}$. $M$ evaluates to a value, if its computation is finite with the last graph $\graph{\Delta}{p}$ having the property $\valueAt{\Delta}{p}{V}$. We write
$\eval{\graph{\{p \mapsto M\}}{p}}{\graph{\Delta}{p}}$.

Note that a redex is of the form $\contexte[V]$.

The \rulename{new node} rule assures that a redex will never be a proper subexpression of a node expression, but that every redex will be a node expression.
On the one hand this simplifies the \rulename{application reduction} rule; it does not require an evaluation context.
However, most importantly we will need this property later when we extend the semantics for redex trails.

Note that there is no reduction inside a variable binding expression.
Hence we also never break up a variable binding expression into several nodes. So we can instantiate a bound variable by standard substitution.


\begin{lemma}[Reduction is deterministic]
For a graph $\Gamma$ and $p \in \dom(\Gamma)$ there exists at most one graph $\Delta$ with $\reduceAt{\Gamma}{p}{\Delta}$. 
\end{lemma}

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

\section{Extension for Redex Trails}

\begin{figure*}[hbt]
\strut\hrulefill\strut
\begin{gather*}
\cfrac
{\valueAt{\Gamma}{p}{\app{(\lambda x.\,N)}{q}} \quad t \notin \dom(\Gamma)}
{\reduceAt{\Gamma}{p}{\Gamma[p \mapsto t \cdot N[q/x]] + \{t \mapsto \Gamma(p)\}}}
~\rulename{application reduction}
\\[3ex]
\cfrac
{\Gamma(p) = t \cdot \app{M}{N} \quad \text{$N$ not a node} \quad q \notin \dom(\Gamma)}
{\reduceAt{\Gamma}{p}{\Gamma[p \mapsto t \cdot \app{M}{q}]+\{q \mapsto t \cdot N\}}}
~\rulename{ensure argument sharing}
\\[3ex]
\cfrac
{\Gamma(p)= t \cdot \contexte[M] \quad \text{$M$ not a node} \quad \text{there is no redex $N$ with $\valueAt{\Gamma}{p}{N}$} \quad q \notin \dom(\Gamma)}
{\reduceAt{\Gamma}{p}{\Gamma[p \mapsto t \cdot \contexte[q]] + \{q \mapsto t \cdot M\}}}
~\rulename{new node for every redex}
\\[3ex]
\cfrac
{\Gamma(p) = t \cdot \contexte[q] \quad \text{(there is no redex $N$ with $\valueAt{\Gamma}{p}{N}$)} \quad \reduceAt{\Gamma}{q}{\Delta}}
{\reduceAt{\Gamma}{p}{\Delta}}
~\rulename{follow need / enter context}
\\[3ex]
\cfrac
{\Gamma(p) = t \cdot q \quad \reduceAt{\Gamma}{q}{\Delta}}
{\reduceAt{\Gamma}{p}{\Delta}}
~\rulename{follow variable}
\\[3ex]
\\[3ex]
\cfrac{\Gamma(x) = t \cdot M}
{\valueAt{\Gamma}{p}{M}}
\quad\quad\quad
\cfrac
{\Gamma(p) = t \cdot \contexte[q] \quad \valueAt{\Gamma}{q}{V}}
{\valueAt{\Gamma}{p}{\contexte[V]}}
\quad\quad\quad
\cfrac
{\Gamma(p) = t \cdot q \quad \valueAt{\Gamma}{q}{V}}
{\valueAt{\Gamma}{p}{V}}
\end{gather*}
\caption{Small step reduction rules for redex trails}\label{trailSemantics}
\strut\hrulefill\strut
\end{figure*}

We allocate the redexes which form the redex trails in the graph as well. It is not possible to completely separate redex trails from the expression that is under evaluation anyway, because the argument of a redex may be evaluated later and the redex trail shall hold the most evaluated form.
So the redex trail has to refer to unevaluated subexpressions of the evaluated expression.

To every heap cell we add a node which points to the redex that created this heap cell. We also add such a node to the top level expression.
Figure~\ref{trailSemantics} shows the extended semantics. To increase readability we use $s$ and $t$ for these special nodes.

Every redex reduces to an expression with its own history.
Hence every redex needs its own heap cell and we introduced the \rulename{new node} rule to reach this goal.
An alternative would be to add trail variables to subexpressions. This would, however, also require a modification of syntax and make expressions far less readable.

So for a (possible incomplete) computation $\eval{\graph{\emptyset}{\text{Root} \cdot M}}{\graph{\Delta}{t \cdot N}}$ the result is $\graph{\Delta}{N}$ and the redex trail is $\graph{\Delta}{t}$????????????? Thus the last top level redex would be the starting point.



Note that the definition of contexts $\contexte$ has no influence on how redex trails are constructed. It should be possible to make even clearer, that evaluation order has no influence on the redex trail structure, only on how far arguments in redexes are evaluated. Maybe I should define a non-deterministic semantics that may evaluate more than necessary (covering both call-by-value and call-by-need)?




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

\section{Data Structures}

Introduction of algebraic data types and the corresponding \texttt{case} construct is straightforward. The \texttt{case} construct gives a second kind of redex. Figure~\ref{data} shows all the necessary extensions.

\begin{figure*}[htb]
\strut\hrulefill\strut
\begin{displaymath}
\begin{array}{rrrllll}
\text{expression} & M,N & := & \ldots \\
&& \mid & C & \text{data constructor} \\
&& \mid & \caseOf{M}{\app{C_i}{\overline{x}_i} \mapsto N_i}{_{i=1}^k} & \text{data destruction} \\
\\
\text{value} & V & := & \ldots \mid  \app{C}{p_1\ldots p_n} \text{ with } n \geq 0 & \text{(partially) applied constructor}
\\
\text{context} & \contexte & := & \ldots \mid  \caseOf{\hole}{\app{C_i}{\overline{x}_i} \mapsto N_i}{_{i=1}^k} \\
\end{array}
\end{displaymath}
\begin{gather*}
\cfrac
{\valueAt{\Gamma}{p}{\caseOf{\app{C_j}{\overline{q}}}{\app{C_i}{\overline{x}_i} \mapsto N_i}{_{i=1}^k}} \quad t \notin \dom(\Gamma)}
{\reduceAt{\Gamma}{p}{\Gamma[p \mapsto t \cdot N_j[\overline{q}/\overline{x}_j]] + \{t \mapsto \Gamma(p)\}}}
\end{gather*}
\caption{Extension of syntax and semantics for data structures}\label{data}
\strut\hrulefill\strut
\end{figure*}

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

\section{Functions with Arity}


Until now a redex is an application of a $\lambda$-abstraction to one argument. This leads to a large number of redexes and reductions. We want a function value to have an arity. Only the application of a function value of arity $n$ to $n$ arguments is a redex. Figure~\ref{arity} shows that syntax and semantics can easily be modified to cater for functions with arity. 

Note that for a one-argument function the semantics remains unchanged.

Note that it is no longer possible to statically determine the subexpressions of an expression that will become redexes. This is because the arity of function component of an application is not known statically. Consider for example the application $\app{\app{p}{q}}{r}$. It may be a single redex, the application of a binary function to two arguments. Or it may consist of two redexes, $\app{p}{q}$, which evaluates to a unary function applied to $r$. Or it may be a value, because the function $p$ requires at least three arguments. Further possibilities exist.
For this reason the syntax still has only binary application. Thus the reduction rule is simple and every redex is an application, not just part of an $n$-ary application.


\begin{figure*}[hbt]
\strut\hrulefill\strut
\begin{displaymath}
\begin{array}{rrrll}
\text{expression} & M,N & := & \ldots \\
&& \mid & \lambda x_1 \ldots x_n .\,M \text{~with~} n \geq 1 & \text{abstraction of arity $n$}\\
\\
\text{value} & V & := & \app{(\lambda x_1 \ldots x_n .\,M)}{p_1\ldots p_m} \text{~with~} 0 \leq m < n & \text{partial application}\\
\end{array}
\end{displaymath}
\begin{gather*}
\cfrac
{\valueAt{\Gamma}{p}{\app{(\lambda x_1\ldots x_n.\,N)}{q_1\ldots q_n}} \quad t \notin \dom(\Gamma)}
{\reduceAt{\Gamma}{p}{\Gamma[p \mapsto t \cdot N[\overline{q}/\overline{x}]] + \{t \mapsto \Gamma(p)\}}}
~\rulename{application reduction}
\end{gather*}
\caption{Changes in syntax and semantics for redex trails for functions with arity}\label{arity}
\strut\hrulefill\strut
\end{figure*}


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

\section{Complete Redex Trails of Interrupted Computations}

For a complete, successful computation the result graph (reachable parts) is the redex trail. However, for computations that were interrupted oder aborted with \texttt{error} (should be a special syntactic symbol) the redex trail is the last graph of the computation with the node that is currently under evaluation (the innermost in a sequence of evaluation contexts) as root node. Unfortunately not all parts of the redex trail that have been created are reachable from this root node. Also all nodes in the sequence of evaluation contexts, the nodes that are currently under evaluation, have not yet even been entered into the redex trail although they may be the source of the error.

Registering redexes when expressions are entered (i.e. evaluation starts).

When an expression is entered it is already itself added as parent to the redex trail. The entered expression is marked with a $\hat{~}$ over the parent node.

$\graph{\Gamma}{p}$ is only a value if $\Gamma(p)$ is not marked as entered.

The fact that with $n$-ary functions function application redexes cannot be statically determined makes it impossible to add them correctly to the redex trail at the time when they are entered.
When an $n$-ary application is entered, it is added as its own parent.
(if the computation is interrupted, then the function component will have value $\bot$, which is assumed to have just the arity of any application in which it is used, returning $\bot$). However, when the function component is evaluted, then redexes may be removed or new ones added to reflect the true redexes.

Note that in the application reduction rules the application may actually consist of several applications. The syntax of application was especially chosen to make the nesting of applications invisible. However, in all other cases an application is a single $n$-ary application. (Not nice, but making it explicit would be really cumbersome.)

For the $n$-ary application we need a new \rulename{ensure argument sharing} rule.

\begin{figure*}[hbt]
\strut\hrulefill\strut
\begin{gather*}
\cfrac
{\Gamma(p) = t \cdot \contexte[q] \quad s \notin \dom(\Gamma)}
{\reduceAt{\Gamma}{p}{\Gamma[p \mapsto \hat{s} \cdot \contexte[q]] + \{s \mapsto \Gamma(p)\}}}
~\rulename{redex to trail}
\\[3ex]
\cfrac
{\valueAt{\Gamma}{p}{\hat{t} \cdot \app{(\lambda x.\,N)}{q}}}
{\reduceAt{\Gamma}{p}{\Gamma[p \mapsto t \cdot N[q/x]]}}
~\rulename{application reduction}
\\[3ex]
\cfrac
{\Gamma(p) = t \cdot \app{M}{N} \quad \text{$N$ not a node} \quad q \notin \dom(\Gamma)}
{\reduceAt{\Gamma}{p}{\Gamma[p \mapsto t \cdot \app{M}{q}]+\{q \mapsto t \cdot N\}}}
~\rulename{ensure argument sharing}
\\[3ex]
\cfrac
{\Gamma(p)= t \cdot \contexte[M] \quad \text{$M$ not a node} \quad q \notin \dom(\Gamma)}
{\reduceAt{\Gamma}{p}{\Gamma[p \mapsto t \cdot \contexte[q]] + \{q \mapsto t \cdot M\}}}
~\rulename{new node for every redex}
\\[3ex]
\cfrac
{\Gamma(p) = \hat{t} \cdot \contexte[q] \quad \reduceAt{\Gamma}{q}{\Delta}}
{\reduceAt{\Gamma}{p}{\Delta}}
~\rulename{follow need / enter context}
\\[3ex]
\cfrac
{\Gamma(p) = t \cdot q \quad \reduceAt{\Gamma}{q}{\Delta}}
{\reduceAt{\Gamma}{p}{\Delta}}
~\rulename{follow variable}
\\[3ex]
\\[3ex]
\cfrac{}
{\valueAt{\Gamma}{p}{\Gamma(p)}}
\quad\quad\quad
\cfrac
{\Gamma(p) = \hat{t} \cdot \contexte[q] \quad \valueAt{\Gamma}{q}{s \cdot V}}
{\valueAt{\Gamma}{p}{\hat{t} \cdot \contexte[V]}}
\quad\quad\quad
\cfrac
{\Gamma(p) = \hat{t} \cdot q \quad \valueAt{\Gamma}{q}{s \cdot V}}
{\valueAt{\Gamma}{p}{\hat{t} \cdot \contexte[V]}}
\end{gather*}
\caption{Small step reduction rules for redex trails}\label{trailSemantics2}
\strut\hrulefill\strut
\end{figure*}


\begin{figure*}[hbt]
\strut\hrulefill\strut
\begin{gather*}
\cfrac
{\valueAt{\Gamma}{p}{\hat{t} \cdot \caseOf{\app{C_j}{\overline{q}}}{\app{C_i}{\overline{x}_i} \mapsto N_i}{_{i=1}^k}}}
{\reduceAt{\Gamma}{p}{\Gamma[p \mapsto t \cdot N_j[\overline{q}/\overline{x}]]}}
\end{gather*}
\caption{Extension of syntax and semantics for data structures}\label{data2}
\strut\hrulefill\strut
\end{figure*}


\begin{figure*}[hbt]
\strut\hrulefill\strut
\begin{displaymath}
\begin{array}{rrrll}
\text{expression} & M,N & := & \ldots \\
&& \mid & \lambda x_1 \ldots x_n .\,M \text{~with~} n \geq 1 & \text{abstraction of arity $n$}\\
&& \mid & N\,M_1\,\ldots\,M_n \text{~with~} n \geq 1 & \text{application of arity $n$}\\
\\
\text{value} & V & := & \ldots \mid \app{(\lambda x_1 \ldots x_n .\,M)}{y_1\ldots y_m} \text{~with~} 0 \leq m < n & \text{partial application}\\
\\
\text{simple evaluation context} & \contexte & := & \ldots \mid \app{\hole}{p_1\ldots p_n} \text{~with~} n \geq 1 & \text{application context}
\end{array}
\end{displaymath}
\begin{gather*}
\cfrac
{\valueAt{\Gamma}{p}{\hat{t} \cdot \app{(\lambda x_1\ldots x_n.\,N)}{q_1\ldots q_n}}}
{\reduceAt{\Gamma}{p}{\Gamma[p \mapsto t \cdot N[\overline{q}/\overline{x}]]}}
~\rulename{application reduction}
\\[3ex]
\cfrac
{\valueAt{\Gamma}{p}{\hat{t} \cdot \app{(\lambda x_1\ldots x_n.\,N)}{q_1\ldots q_m}} \quad m < n \quad \Gamma(t) = s \cdot M }
{\reduceAt{\Gamma}{p}{\Gamma[p \mapsto s \cdot M]}}
~\rulename{partial application}
\\[3ex]
\cfrac
{\Gamma(p) = \hat{t} \cdot M\,q_i\,\ldots\,q_m \quad
\valueAt{\Gamma}{p}{\hat{t} \cdot \app{(\lambda x_1\ldots x_n.\,N)}{q_1\ldots q_m}} \quad i \leq n < m \quad \Gamma(t) = s \cdot M\,q_i\,\ldots\,q_m}
{\reduceAt{\Gamma}{p}{\Gamma[p \mapsto \hat{t} \cdot \app{r}{q_{n+1}\ldots q_m}] [t \mapsto s \cdot \app{r}{q_{n+1}\ldots q_m}] + \{r \mapsto t \cdot \app{M}{q_i\,\ldots\,q_n}\}}}
~\rulename{oversaturated application}
\\[3ex]
\cfrac
{\Gamma(p) = t \cdot \app{N}{M_1\ldots M_n} \quad \text{$M_j$ not a node} \quad q \notin \dom(\Gamma)}
{\reduceAt{\Gamma}{p}{\Gamma[p \mapsto t \cdot \app{N}{M_1\ldots M_{j-1}\,q\,M{j+1}\ldots M_n}]+\{q \mapsto t \cdot M_j\}}}
~\rulename{ensure argument sharing}
\end{gather*}
\caption{Changes in syntax and semantics for redex trails for functions with arity}\label{arity2}
\strut\hrulefill\strut
\end{figure*}

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

\section{What is a Parent? The \texttt{if-then-else} Problem}

The \texttt{if-then-else} construct has a special syntax and hence require special reduction rules. 
\begin{displaymath}
\begin{array}{rrrll}
\text{expression} & M,N & := & \ldots \\
&& \mid & \ifthenelse{N}{M_1}{M_2}\\
\end{array}
\end{displaymath}
Unfortunately there are two different natural choices which give different redex trails.

The first version (which Hat currently implements) describes $\ifthenelse{N}{M_1}{M_2}$ similar to $\caseOf{N}{\True \mapsto M_1, \False \mapsto M_2}{}$: 

\begin{figure*}[hbt]
\strut\hrulefill\strut
\begin{gather*}
 \contexte  :=  \ldots \mid \ifthenelse{\hole}{M_1}{M_2}
\\[3ex]
\cfrac
{\valueAt{\Gamma}{p}{\ifthenelse{\True}{M_1}{M_2}}}
{\reduceAt{\Gamma}{p}{\Gamma[p \mapsto M_1]}}
\quad\quad\quad\quad
\cfrac
{\valueAt{\Gamma}{p}{\ifthenelse{\False}{M_1}{M_2}}}
{\reduceAt{\Gamma}{p}{\Gamma[p \mapsto M_2]}}
\end{gather*}
\strut\hrulefill\strut
\end{figure*}

For the expression $\ifthenelse{\True}{\app{(\lambda x.\,x)}{\False}}{\False}$ the redex trail augmented version of the rules gives us

\begin{trace}{16}{4}
\troot{1}{3}
\touter{6}{3}{if}{root}{$\ifthenelse{\True}{\app{(\lambda x.\,x)}{\False}}{\False}$}
\touter{14}{1}{ifalse}{if}{\False}
\touter{12}{3}{app}{if}{$\app{(\lambda x.\,x)}{\mbox{\sub{ifalse}}}$}
\touter{14}{3}{false}{app}{\sub{ifalse}}
\result{15}{3}{false}
\end{trace}

The expression $\caseOf{\True}{\True \mapsto \app{(\lambda x.\,x)}{\False}, \False \mapsto \False}$ gives the same redex trail (except for one node expression of course).

The second version describes $\ifthenelse{N}{M_1}{M_2}$ similar to 
$f~N~M_1~M_2$ where $f$ is defined as
\begin{align*}
f~\True~M_1~M_2 & = M_1 \\
f~\False~M_1~M_2 & = M_2 
\end{align*}
(the semantics of such definitions has not yet been described).


\begin{figure*}[hbt]
\strut\hrulefill\strut
\begin{gather*}
 \contexte  :=  \ldots \mid \ifthenelse{\hole}{p_1}{p_2}
\\[3ex]
\cfrac
{\valueAt{\Gamma}{p}{\ifthenelse{\True}{p_1}{p_2}}}
{\reduceAt{\Gamma}{p}{\Gamma[p \mapsto p_1]}}
\quad\quad\quad\quad
\cfrac
{\valueAt{\Gamma}{p}{\ifthenelse{\False}{p_1}{p_2}}}
{\reduceAt{\Gamma}{p}{\Gamma[p \mapsto p_2]}}
\\[3ex]
\cfrac
{\valueAt{\Gamma}{p}{\ifthenelse{\True}{M_1}{p_2}} \quad \text{$M_1$ not a node} \quad q \notin \Gamma}
{\reduceAt{\Gamma}{p}{\Gamma[p \mapsto \ifthenelse{\True}{q}{p_2}] + \{q \mapsto M_1\}}}
\\[3ex]
\cfrac
{\valueAt{\Gamma}{p}{\ifthenelse{\False}{M_1}{M_2}} \quad \text{$M_2$ not a node} \quad q \notin \Gamma}
{\reduceAt{\Gamma}{p}{\Gamma[p \mapsto \ifthenelse{\False}{M_1}{q}] + \{q \mapsto M_2\}}}
\end{gather*}
\strut\hrulefill\strut
\end{figure*}

For the expression $\ifthenelse{\True}{\app{(\lambda x.\,x)}{\False}}{\False}$ the redex trail augmented version of the rules gives us

\begin{trace}{12}{6}
\troot{1}{5}
\touter{7}{1}{iifalse}{root}{\False}
\touter{6}{3}{app}{root}{$\app{(\lambda x.\,x)}{\mbox{\sub{iifalse}}}$}
\touter{11}{3}{ifalse}{app}{\sub{iifalse}}
\touter{6}{5}{if}{root}{$\ifthenelse{\True}{\mbox{\sub{ifalse}}}{\False}$}
\touter{11}{5}{false}{if}{\sub{ifalse}}
\result{12}{5}{false}
\end{trace}

Note that the parent of the $\app{(\lambda x.\,x)}{\False}$ node is Root, not the \texttt{if-then-else}.
The expression $f~\True~(\app{(\lambda x.\,x)}{\False})~\False$ gives the same redex trail (except for one node expression of course).

So the central question is: who are the parents of the second and third argument of \texttt{if-then-else}?
The parent of the alternatives of a \texttt{case} construct has to be the \texttt{case} construct itself, because in general the alternatives may bind variables. In contrast, the two arguments of \texttt{if-then-else} are normal expressions, they do not bind variables.

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

\section{Local Definitions, the \texttt{let} construct}

Figure~\ref{let} defines the reduction of \texttt{let}.
The reduction rule is straightforward. 
However, it is unclear what the redex trail producing rule should look like:
should a \texttt{let} redex be ignored, should it be registered in the trail like other redexes (rather large), should only the defined subexpressions have a special trail which mainly declares to which defined variables they belong?


\begin{figure*}[htb]
\strut\hrulefill\strut
\begin{gather*}
\cfrac
{\Gamma(p) = \letIn{x_i = M_i}{_{i=1}^k}{N}
\quad q_i \notin \dom(\Gamma)}
{\reduceAt{\Gamma}{p}{\Gamma[p \mapsto N[\overline{q}/\overline{x}]]] + \{q_i \mapsto M_i[\overline{q}/\overline{x}]\}}}
~\rulename{\texttt{let} reduction}
\end{gather*}
\begin{gather*}
\cfrac
{\Gamma(p) = t \cdot \letIn{x_i = M_i}{_{i=1}^k}{N}
\quad q_i \notin \dom(\Gamma)}
{\reduceAt{\Gamma}{p}{\Gamma[p \mapsto t \cdot N[\overline{q}/\overline{x}]] + \{q_i \mapsto t \cdot M_i[\overline{q}/\overline{x}]\}}}
~\rulename{1. redex \texttt{let} reduction}
\end{gather*}
\begin{gather*}
\cfrac
{\Gamma(p) = t \cdot \letIn{x_i = M_i}{_{i=1}^k}{N}
\quad q_i \notin \dom(\Gamma) \quad s \notin \dom(\Gamma)}
{\reduceAt{\Gamma}{p}{\Gamma[p \mapsto s \cdot N[\overline{q}/\overline{x}]] + \{q_i \mapsto s \cdot M_i[\overline{q}/\overline{x}]\} 
+ \{s \mapsto t \cdot \letIn{x_i = q_i}{_{i=1}^k}{p}\}}}
~\rulename{2. redex \texttt{let} reduction}
\end{gather*}
\begin{gather*}
\cfrac
{\Gamma(p) = t \cdot \letIn{x_i = M_i}{_{i=1}^k}{N}
\quad q_i \notin \dom(\Gamma) \quad s_i \notin \dom(\Gamma)}
{\reduceAt{\Gamma}{p}{\Gamma[p \mapsto t \cdot N[\overline{q}/\overline{x}]] + \{q_i \mapsto s_i \cdot M_i[\overline{q}/\overline{x}]\} 
+ \{s_i \mapsto t \cdot x_i \}}}
~\rulename{3. redex \texttt{let} reduction}
\end{gather*}
\caption{\texttt{let}}\label{let}
\strut\hrulefill\strut
\end{figure*}


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

\section{Comparison with other Semantics}\label{Launchbury}

To achieve sharing easily, Launchbury requires that arguments of functions (and later also data constructors) are variables. So a preliminary transformation is needed that introduces \texttt{let} constructs to remove non-variable arguments.
For our purposes this transformation is undesirable. A redex trail shall describe the computation of the original, non-transformed program. Especially \texttt{let} redexes that were only introduced by the transformation should not be registered in the redex trail.

In Launchbury's semantics a graph is a tuple of a heap and a term, the latter of which represents the top of the term and has variables pointing into the heap. This top term component is used to give values upwards. So in the small step version of Launchbury's semantics given in \cite{WanPey99}, there is a rule like
\begin{gather*}
\cfrac{}
{\reduce{\graph{\Gamma+\{x \mapsto V\}}{x}}{\graph{\Gamma + \{x \mapsto V\}}{V}}}
\end{gather*}
We cannot simply give values upwards in this way, because this would conflict with the construction of redex trails. The copied values would loose their parents.
Instead of giving values upwards we use the value lookup relation which we introduced especially for this purpose..

The additional trail variables are reminiscence of the cost centers in \cite{Sansom:1997:FBP}. 

The major difference with respect to the graph reduction semantics of 
\cite {bakruntgros00} is, that the latter explicitly models the stack whereas in the semantics given here every reduction step has to completely restart searching for the next redex. For our purposes the stack is not needed and would unnecessarily complicate the semantics.

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

\section{Pattern Matching}

This section has not been updated.

Launchbury only gives the semantics for a core language. The idea is that standard functional language can be translated into this core language, for example by transforming pattern matching into nested case constructs. For our purposes such a preliminary translation is undesirable, because the close link to the original program would be lost. Although we will obviously not give a semantics for full Haskell, we at least outline how it could be done without requiring a translation into the core language.

Patterns can be arbitrarily nested, but we demand that they are linear, that is, a variable occurs at most once in a pattern.
\begin{displaymath}
\begin{array}{rrrll}
\text{pattern} & p & := & x & \text{variable}\\
&& \mid & \app{C}{p_1 \ldots p_n}\quad\text{$n$ is arity of $C$} & \text{full constructor application} 
\end{array}
\end{displaymath}

The simple $\lambda$-abstraction is replaced by an abstraction with pattern matching:
\begin{displaymath}
\lambda p_1.N_1;\ldots;p_n.N_n
\end{displaymath}
For simplicity we only consider single argument functions here.

A pattern $p'$ \emph{matches} a pattern $p$ if there is a variable substitution $\sigma$ such that $p\sigma = p'$.

We define the relation that a pattern does not match a graph $\Gamma$ at a variable $x$ as follows:

\begin{gather*}
\cfrac
{\valueAt{\Gamma}{x}{\app{D}{p_1'\ldots p_m'}}}
{\mismatch{\Gamma}{x}{\app{C}{p_1\ldots p_n}}}
\quad\quad\quad\quad
\cfrac
{\valueAt{\Gamma}{x}{\app{C}{x_1\ldots x_n}}\quad
\valueAt{\Gamma}{x_1}{p_1\sigma}~\ldots~\valueAt{\Gamma}{x_{i-1}}{p_{i-1}\sigma}
\quad \mismatch{\Gamma}{x_i}{p_i}}
{\mismatch{\Gamma}{x}{\app{C}{p_1\ldots p_n}}}
\end{gather*}

Note that we require that everything to the left of the mismatching constructor does match, because matching is performed from left to right. 

For the process of evaluating an argument to test if it matches a pattern $p$ we define a pattern contexts $\patCon{p}$:
\begin{displaymath}
\begin{array}{rrrll}
 & \patCon{x} & := & \hole \\
& \patCon{\app{C}{p_1 \ldots p_n}} & := & \hole \mid \app{C}{\patCon{p_1}x_2\ldots x_n} \mid \app{C}{p_1\patCon{p_2}x_3\ldots x_n} \mid \ldots \mid
\app{C}{p_1\ldots p_{n-1}\patCon{p_n}}
\end{array}
\end{displaymath}

The final step: the reduction rules for an abstraction with patterns:

\begin{gather*}
\cfrac
{\valueAt{\Gamma}{z}{\app{(\lambda p_1.N_1;\ldots;p_n.N_n)}{y}} \quad
\mismatch{\Gamma}{y}{p_1}~\ldots~\mismatch{\Gamma}{y}{p_{i-1}} \quad
\valueAt{\Gamma}{y}{\patCon{p_i}[x]} \quad
\reduceAt{\Gamma}{x}{\Delta}}
{\reduceAt{\Gamma}{z}{\Delta}}
\\[3ex]
\cfrac
{\valueAt{\Gamma}{z}{\app{(\lambda p_1.N_1;\ldots;p_n.N_n)}{y}} \quad
\mismatch{\Gamma}{y}{p_1}~\ldots~\mismatch{\Gamma}{y}{p_{i-1}} \quad
\valueAt{\Gamma}{y}{p_i\sigma}}
{\reduceAt{\Gamma}{z}{\Gamma[z \mapsto t \cdot N_i\sigma] + \{t \mapsto \Gamma(z)\}}}
\end{gather*}

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

\section{Projections}

In the transformation that implements redex trails functions that are projections have to be handled specially, otherwise the reduction of the projection would not be registered in the redex trail of the result \cite{sparudruncimanifl97}. The source of the probem might be that in the transformation system only values carry redex trails, not expressions that are under evaluation.

In our operational semantics we do not have to handle projections in any special way to make redex trail construction work correctly as the following little example demostrates:

\begin{seqproofl}
& \{ 1 \mapsto \text{Root}\cdot\letIn{head = \lambda xs.\,\caseOf{xs}{y:ys \mapsto y}{}}{}{\app{head}{(\text{True}:\text{[]})}}\}
\seqnext{\rs_1}
& \{ 1 \mapsto \text{Root}\cdot \app{2}{(\text{True}:\text{[]})}, 
2 \mapsto \text{Root}\cdot \lambda xs.\,\caseOf{xs}{y:ys \mapsto y}{}\}
\seqnext{\rs_1}
& \{ 1 \mapsto \text{Root}\cdot \app{2}{3}, 
2 \mapsto \text{Root}\cdot \lambda xs.\,\caseOf{xs}{y:ys \mapsto y}{},
3 \mapsto \text{Root}\cdot \text{True}:\text{[]}\}
\seqnext{\rs_1}
& \{ 1 \mapsto 4 \cdot \caseOf{3}{y:ys \mapsto y}{} , 
2 \mapsto \text{Root}\cdot \ldots,
3 \mapsto \text{Root}\cdot \text{True}:\text{[]} \\ &,
4 \mapsto \text{Root}\cdot \app{2}{3}\}
\seqnext{\rs_1}
& \{ 1 \mapsto 4 \cdot \caseOf{3}{y:ys \mapsto y}{} , 
2 \mapsto \text{Root}\cdot \ldots,
3 \mapsto \text{Root}\cdot 6:5 \\ &,
4 \mapsto \text{Root}\cdot \app{2}{3},
5 \mapsto \text{Root}\cdot \text{[]},
6 \mapsto \text{Root}\cdot \app{(:)}{\text{True}} \}
\seqnext{\rs_1}
& \{ 1 \mapsto 4 \cdot \caseOf{3}{y:ys \mapsto y}{} , 
2 \mapsto \text{Root}\cdot \ldots,
3 \mapsto \text{Root}\cdot 6:5 \\ &,
4 \mapsto \text{Root}\cdot \app{2}{3},
5 \mapsto \text{Root}\cdot \text{[]},
6 \mapsto \text{Root}\cdot \app{(:)}{7},
7 \mapsto \text{Root}\cdot \text{True} \}
\seqnext{\rs_1}
& \{ 1 \mapsto 8 \cdot 7 , 
2 \mapsto \text{Root}\cdot \ldots,
3 \mapsto \text{Root}\cdot 6:5 \\ &,
4 \mapsto \text{Root}\cdot \app{2}{3},
5 \mapsto \text{Root}\cdot \text{[]},
6 \mapsto \text{Root}\cdot \app{(:)}{7},
7 \mapsto \text{Root}\cdot \text{True} \\ &,
8 \mapsto 4 \cdot \caseOf{3}{y:ys \mapsto y}{} \}
\end{seqproofl}


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

\section{IO}

For a program that performs IO the value to which it evaluates is irrelevant (it may not even terminate) but its semantics is determined by the sequence of actions it performs. We consider two actions, \texttt{put C} can be interpreted as writing a nullary constructor \texttt{C} and \texttt{get C} can be interpreted as reading a nullary constructor \texttt{C}. A program does not determine a single action sequence. If a sequence has a \texttt{get C} action, then there exists for every nullary constructor $C$ a sequence which is identical up to this action, followed by a \texttt{get $C$}.

We extend the language by two functions \texttt{put} and \texttt{get} that create the actions, a function \texttt{>>=} to sequence actions and a special function \texttt{return}. The latter is handled like a data constructor except that it cannot be destructed by a \texttt{case} construct. Only \texttt{>>=} can destruct this special value and thus we ensure that actions are sequenced correctly and referential transparency is preserved. So we do not have a static type system but we dynamically check that actions are sequenced correctly.

Our reduction relation may now carry an additional action (a missing action could also be viewed as an non-observable action $\tau$). Note that we use \texttt{>>=} infix. For simplicity the \texttt{put $C$} action returns the constructor $C$.
Figure~\ref{IO} shows the extension of our semantics to IO.

\begin{figure*}[htb]
\strut\hrulefill\strut
\begin{displaymath}
\begin{array}{rrrll}
\text{expression} & M,N & := & \ldots \mid \texttt{put} \mid \texttt{get} \mid \texttt{>>=} \mid \texttt{return} 
\\
\text{value} & V & := & \ldots \mid \app{\texttt{return}}{x_1 \ldots x_n} \text{ with } n \geq 0
\\
\text{simple evaluation context} & \contexte & := & \ldots \mid \texttt{put $\hole$} \mid \texttt{$\hole$ >>= p}
\end{array}
\end{displaymath}
\begin{gather*}
\cfrac
{\valueAt{\Gamma}{p}{\texttt{put}~C} \quad \Gamma(p) = \texttt{put}~q}
{\reduceAtA{\Gamma}{p}{\app{\texttt{put}}{C}}{\Gamma[p \mapsto \texttt{return $q$}]}}
\quad\quad\quad\quad
\cfrac
{\Gamma(p) = \texttt{get} \quad q \notin \dom(\Gamma)}
{\reduceAtA{\Gamma}{p}{\app{\texttt{get}}{C}}{\Gamma[p \mapsto \texttt{return $q$}] + \{q \mapsto C\}}}
\\[3ex]
\cfrac
{\valueAt{\Gamma}{p}{\texttt{$(\texttt{return $q$})$ >>= $r$}}}
{\reduceAt{\Gamma}{p}{\Gamma[p \mapsto \app{r}{q}]}}
\end{gather*}
\caption{Extension of syntax and semantics for IO}\label{IO}
\strut\hrulefill\strut
\end{figure*}

Next we have to extend our IO semantics for redex trails. We do this in a way that resembles the current implementation. Thus it highlights the shortcomings of the current implementation. Figure~\ref{traceIO} shows the extension.

\begin{figure*}[htb]
\strut\hrulefill\strut
\begin{gather*}
\cfrac
{\valueAt{\Gamma}{p}{\texttt{put}~C} \quad \Gamma(p) = s \cdot \texttt{put $q$} \quad t \notin \dom(\Gamma)}
{\reduceAtA{\Gamma}{p}{t \cdot \app{\texttt{put}}{C}}{\Gamma[p \mapsto \text{IO} \cdot \texttt{return $q$}] + \{t \mapsto \Gamma(p)\}}}
\\[3ex]
\cfrac
{\Gamma(p) = s \cdot \texttt{get} \quad q \notin \dom(\Gamma)}
{\reduceAtA{\Gamma}{p}{\app{\texttt{get}}{C}}{\Gamma[p \mapsto \text{IO} \cdot \texttt{return $q$}] + \{q \mapsto t \cdot C\}} + \{t \mapsto \Gamma(p)\}}
\\[3ex]
\cfrac
{\valueAt{\Gamma}{p}{\texttt{$(\texttt{return $q$})$ >>= $r$}}}
{\reduceAt{\Gamma}{p}{\Gamma[p \mapsto \text{IO} \cdot \app{r}{q}]}}
\end{gather*}
\caption{Extension of IO semantics for redex trails}\label{traceIO}
\strut\hrulefill\strut
\end{figure*}

So every \texttt{put} action has a parent. Conversely every constructor that was read by a \texttt{get} action has the \texttt{get} redex as parent.
IO is just a dummy trace variable. We note that the newly allocated \texttt{return} heap cells do not have parents. Furthermore, the reduction of the sequencing function \texttt{>>=} is not registered in any trail. Thus computations that construct actions are not registered at all in the trail.

It is not quite clear how the Haskell function \texttt{getContents} should be modelled in our framework.  It actually leads to an interleaving of independent action sequences. However, the assumption is that the environment provides \texttt{getContents} with characters independent of the interleaving sequence. This gives ideas for interesting further research. It should be possible to model \texttt{unsafePerformIO} in this way and state precisely which proof obligations or assumptions the programmer has to make to ensure referential transparency.

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

\section{Named Functions}

$\lambda$-abstractions are very difficult to read. Usually functions have names and we prefer to show these names. Although we do not support%
\footnote{It simplifies the semantics that a $\lambda$-abstraction is just an expression. For example, we can thus easily store it in the heap.} 
the syntax $f x_1 \ldots x_n = M$ we can name a function nonetheless by binding a $\lambda$-abstraction to a variable in a \texttt{let} construct: $\letIn{f = \lambda x_1 \ldots x_n.M}{}{\ldots}$. When we show a redex trail we would like to be able to show this variable instead of the $\lambda$-abstraction. We achieve this by adding yet another variable to every heap cell. Note that this variable only serves as a name and may not be in the domain of the heap. 

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

\section{Trusting}

This section is rather incomplete, because it is unclear how trusting should work. The current implementation leads to trails in which some untrusted redexes are unreachable.

We introduce two new syntactic forms trust and suspect to mark an expression as being trusted or suspected. In practise these syntactic forms may be combined either with local definitions ($\letIn{x = \app{\trust}{M}}{}{N}$) or with $\lambda$-abstractions ($\app{\trust}{\lambda x.\,M}$).

A well-formed condition should hold: A trusted expression should only contain trusted functions. This is natural and avoids some anomalies.

To every heap cell we add the boolean information if it is trusted ($\True$) or not.

Note that we modify the rules for the complete redex trail for interrupted computations.

The idea is that an application redex is trusted (and hence not recorded in the trail), if the application and the function are trusted. Here already the problem arises, if we should consider the trustedness of the possibly unevaluated function or the $\lambda$-abstraction, just before reduction. The trustedness of the result is definitely the trustedness of the $\lambda$-abstraction.

The handling of an application redex suggests that a \texttt{case} or \texttt{if} redex should be handled similarly: both the boolean argument and the \texttt{case} respectively \texttt{if} should be trusted.
(An experimental change of PreludeDebug lead to always visible \texttt{case} and \texttt{if} redexes and some traces were not well defined (segementation fault))

A dropped trusted redex is marked by a special hidden redex in the trail. The point is that a whole sequence of trusted redexes is replaced by a single hidden redex.

Here we do not consider functions with arity. What happens if part of an $n$-ary application is trusted and part is suspected will lead to new problems.

\begin{figure*}[hbt]
\strut\hrulefill\strut
\begin{gather*}
\cfrac
{\Gamma(p) = t \stackrel{\tau}{\cdot} \app{\trust}{M}}
{\reduceAt{\Gamma}{p}{\Gamma[p \mapsto t \stackrel{\True}{\cdot} M]}}
\quad\quad\quad
\cfrac
{\Gamma(p) = t \stackrel{\tau}{\cdot} \app{\suspect}{M}}
{\reduceAt{\Gamma}{p}{\Gamma[p \mapsto t \stackrel{\False}{\cdot} M]}}
\\[3ex]
\cfrac
{\trustedRed(\Gamma,p)}
{\reduceAt{\Gamma}{p}{\markHidden(\Gamma,p)}}
~\rulename{trusted redex not to trail}
\\[3ex]
\cfrac
{\neg\trustedRed(\Gamma,p) \quad \Gamma(p) = t \stackrel{\tau}{\cdot} \contexte[q] \quad s \notin \dom(\Gamma)}
{\reduceAt{\Gamma}{p}{\Gamma[p \mapsto \hat{s} \stackrel{\tau}{\cdot} \contexte[q]] + \{s \mapsto \Gamma(p)\}}}
~\rulename{suspected redex to trail}
\\[3ex]
\cfrac
{\Gamma(p) = t \stackrel{\True}{\cdot} \app{M}{q} \quad \text{$M$ not a pointer}}
{\trustedRed(\Gamma,p)}
\quad\quad\quad
\cfrac
{\Gamma(p) = t \stackrel{\True}{\cdot} \app{r}{q} \quad \Gamma(r) = s \stackrel{\True}{\cdot} M}
{\trustedRed(\Gamma,p)}
\\[3ex]
\cfrac
{\valueAt{\Gamma}{p}{\hat{t} \cdot \app{(\lambda x.\,N)}{q}}}
{\reduceAt{\Gamma}{p}{\Gamma[p \mapsto t \cdot N[q/x]]}}
~\rulename{application reduction}
\end{gather*}
\caption{Small step reduction rules for redex trails with trusting}\label{trailSemantics3}
\strut\hrulefill\strut
\end{figure*}

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

\section{Extraction of Redex Trail}

Intermediate expressions and final values of a computation are mixed with redex trails in the heap. For a given graph we would like to extract the redex trail. A normal garbage collector with the final value or redex as root does just that. We could modify the garbage collector to replace $\lambda$-abstractions by their names as far as possible and remove the $\lambda$-abstractions.

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

\section{CAFs}

The names of CAFs are not registered in the redex trail. The parent of an instance right hand side of a CAF is the next enclosing $\lambda$-abstraction. Should we introduce nullary $\lambda$-abstractions for CAFs or handle the \texttt{let} construct differently?

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

\section{Are Small Steps Small Enough?}

We chose a small step semantics to handle infinite and interrupted computations. However, in our semantics a single step is still complex and its derivation usually requires numerous uses of the \rulename{follow variable} rule. This rule basically searches for the current redex and does so for each step anew.
Sestoft's Mark 1 machine \cite{JFP::Sestoft1997} has a stack that keeps track of redex positions. Every step is just an instance of a rule, it does not require an arbitrarily large derivation. Hence it may be more suitable, especially because it allows more fine grained interruption of a computation.

When a computation is stopped before reaching a value, the question arises which redex or value is the one that determines the redex trail of the computation.
we distinguish several cases:

\begin{itemize}
\item 
blackhole: the source of the redex trail should be the variable that depends on itself. The redex trail should include this self-dependence. However, a variable is neither a redex nor a value. Example: \texttt{let x = x in x}.
\item
error: the source should be the \texttt{error} redex itself.
\item
interruption:
next redex to evaluate.
\item
insufficient space (heap,stack):
redex whose reduction caused space problem.
\end{itemize}

In the last two cases the redex might actually be a \texttt{let} expression. Should the last ``real'' redex be chosen in that case?

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

\bibliographystyle{alpha}
\bibliography{functional,semantics,biblio}
 
%------------------------------------------------------------------------------
 
\end{document}