\documentstyle[11pt]{article}
\marginparwidth 0pt
\oddsidemargin  0pt
\evensidemargin  0pt
\marginparsep 0pt

\topmargin   0pt

\textwidth   6.5in
\textheight  8.5 in
%\def \dred {\mbox {$\,\ \rightarrow\kern-0.7em\rightarrow\ $}}
\def \doar{\mbox {$\,\ \rightarrow\kern-0.7em\rightarrow\ $}}
%\documentstyle[fullpage,11pt,amssymbols]{article}
%\input{diagrams} % Paul Taylor's Macro Package
\begin{document}
\newtheorem{thm}{Theorem}[section]
\newtheorem{lem}{Lemma}[section]
\newtheorem{cor}{Corollary}[section]
\newtheorem{ex}{Example}[section]
\newtheorem{rem}{Remark}[section]
\newtheorem{prop}{Proposition}[section]
%%%%\newtheorem{proof}{Proof}
%\newenvironment{proof}{{\it Proof:}}{{\it Q.e.d.}}
\newenvironment{akn}{\noindent{\bf Acknowledgments }}{}
\newenvironment{proof}{\noindent{\bf Proof }}{}
\newtheorem{deff}{Definition}[section]
\newcommand{\notation}{{\bf Notation }}
\newcommand{\note}{{\bf Note }}
\newcommand{\newl}{\mbox{ }\\}
\newcommand{\ar}{\rightarrow}
\newcommand{\undl}{\underline}
\newcommand{\impl}{\Rightarrow}
%\newcommand{\doar}{\twoheadrightarrow}
\newcommand{\trar}{\Rightarrow}
\newcommand{\red}[1]{\mbox{$\stackrel{#1}{\ar}$}}
\newenvironment{prsk}{\noindent{\bf Proof sketch }}{}
\newenvironment{altpr}{\noindent{\bf Alternative proof }}{}
\newcommand \inputpic[1] {\begin{center} \input{#1} \end{center}}
\newcommand{\ssq}{\subseteq}
\newcommand{\sset}{\subset}
\hyphenation{meta-var-ia-ble}
\newcommand{\vect}[1]{\mbox{$\overline{#1}$}}
\newcommand{\rpsim}{\mbox{$\stackrel{r}{\psim}$}}
\newcommand{\rpessim}{\mbox{$\stackrel{r}{\pessim}$}}
\newcommand{\ressim}{\mbox{$\stackrel{r}{\essim}$}}
\newcommand{\rsim}{\mbox{$\stackrel{r}{\sim}$}}
\newcommand{\muer}[1]{\mbox{$[{#1}]_{\mu}$}}
\newcommand{\lclas}[1]{\mbox{$[{#1}]_L$}}
\newcommand{\ines}[2]{\mbox{$\overbrace{#1}^{#2}$}}
\newcommand{\unin}[2]{\mbox{$\undl{#1}_{#2}$}}
\newcommand{\dist}[2]{\mbox{$\vert{#1},{#2}\vert$}}
\def\pessim{\prec\!\!\prec}
\def\steq{\approx_{st}}
\def\essim{\approx}
\def\psim{\prec}
\def\orth{\perp}
\def\esorth{\perp_{es}}
\def\subt{\subseteq}
%\def\lleq{\triangleleft}
%\def\lles{\triangleleft}
\def\lleq{\unlhd}
\def\lles{\lhd}
\def\leeqv{\approx_L}
\def\ind{\ddagger}
\def\hole{\circ}
\def\restr{\vert}
\def\exten{\updownarrow}
\def\zig{\simeq}


\begin{titlepage}


\title{Euclidean Reduction Spaces: Independence, Context Sharing, and Modularity}
\author{John Glauert \hspace{2cm} Zurab Khasidashvili \\
University of East Anglia, UK }
\maketitle

\thispagestyle{empty}

\begin{abstract}
We define a {\em residual structure} or a {\em L\'evy-Klop structure} as an abstract reduction system where L\'evy's notion of strong equevalence and the zig-zag family relation is defined based on the notion of residual and elementary diagrams as primitives. We furrher define the notion of {\em independence} of reductions and {\em distance} between reductions in any  L\'evy-Klop structure, which makes the latter a {\em Euclidean reduction space}. We investigate the metric for the  L\'evy-Klop structure of Orthogonal Combinatory Reduction systems (OCRSs), finding how a Euclidean bases at a term $t$ can be constructed so that each reduction starting from $t$ can be decomposed as a least upper bound of subreductions of directions of the bases in the corresponding upper semilattice. This leads to a study of computations of components (i.e., contexts) of a term rather than subterms independently, i.e., in parallel; computatitions of different occurrences of a component whose corresponding subterms are not the same can also be ahared. Since the independent computations are feasible only in OCRSs where restricted kinds of redex-creation is possible, one is forced to consider probabilistic strategies that do independent computations in components with higher digrees of independence. However, an elegant implimentation of terms with shared components is possible using {higher order} invironments.
\end{abstract}

\bigskip

\subsection*{Correspondence Address}

\begin{tabbing}
Dr. Zurab Khasidashvili \\
School of Information Systems \\
University of East Anglia \\
Norwich NR4 7TJ England \\
\\
Email: zurab@sys.uea.ac.uk \\
Tel: +44 603 592607 \\
Fax: +44 603 507720
\end{tabbing} 

\end{titlepage}

\section{Introduction}

We study computation as an abstract reduction process. Our aim is to identify the conditions for independence of reduction sequences, thus identfying the potential for concurrent computation. Further, we aim for a Euclidean measure of distance between reductions, allowing us characterise the amount of independent computation present between components of a computation before interaction is required.

Such a measure is proposed/developed and applied to OCRS ...

Essentiality: enables us to avoid unnecessary work

Optimality: avoids doing the same work twice

Context Sharing: enables us to share even PARTS of similar tasks, doing the common parts only once.

\section{Euclidean Reduction Spaces}

An ARS consists of a set of {\em objects}, often called terms, and {\em labelled transitions} between objects. Each transition is uniquely labelled. The labels form sets of {\em redexes} associated with the source objects of their transitions. A {\em reduction} is a sequence transitions.

Examples of ARS are TRS, TGRS, LC, CRS though several ARS objects may map to the same term in such systems.

A redex captures the computational notion of an atomic task. When one redex is reduced, other tasks may remain. The {\em residual} concept formalises the relationship between redexes under reduction, capturing the idea of the same computation remaining to be done.

If $t\red{u}t'$ there is a partial function from redexes of $t'$ to redexes of $t$. Redexes of $t$ not in the domain of the function are {\em created} by $u$. Redexes of $t$ not in the range of the function are {\em erased} by $u$. $u$ is always erased by $u$. Note that a reduction may produce multiple residuals, or copies, of a redex.

A {\em development} of is a reduction which only reduces residuals of some set of initial redexes. Hence it does not reduce any created redexes.

[We require developments to terminate. Do we need more?]

A {\em L\'evy-Klop Structure} captures the equivalence of reductions which do the same work. {\em L\'evy embedding} formalises the idea of reductions which do all the work of others, and possibly more.

An elementary diagram considers complete developments of pairs of redexes, reducing one redex, then all residuals of the other. For a L\'evy-Klop structure
we require that all developments lead to the same object.

The concept of a {\em family} of redexes captures the idea of all copies of the same work. It is formed by the [reflexive?] symmetric transitive closure of the residual relation. 

[I need convincing that the more complex definition is required]


[If family is essential (has an essential redex) then family completion will do all other members of the family: nf wrt family...]

The concept of a redex being {\em needed} in a reduction
unneeded/inessential: u is inessential in P + u + Q if Q' =L u + Q and Q' does not contract u or any residual of u

Needed: Canonical form of R: [need this?] Same order as R but omits all inessential redexes. "omits all unnecessary work, whose results are discarded later". 

Applications:

Essential Similarity: For each subterm, identifies which parts of the term will influence its "essentiality status". Use for GC and Modules?

HO environments = context rewriting

\end{document}





