% Here follows the style file for the compilation of the RTA96 referee reports.
% Please save this file as ``RTA96.sty''.
% The actual referee reports are appended below.

----------------------------------- cut ---------------------------------------
 % Document Type: LaTeX
 % Harald Ganzinger, who borrowed from Jieh Hsiang,
 %                   who borrowed from : [Claude Kirchner: Dec 10 92]
 % macros for the
 % RTA96
 % referee report form


 %%%% The page size
\setlength{\oddsidemargin}{-6mm}
\setlength{\textwidth}{169mm}
\setlength{\textheight}{235mm}
\setlength{\topmargin}{-3mm}
\setlength{\headsep}{-2mm}
\pagestyle{empty}
\thispagestyle{empty}
\sloppy



\newcommand{\refbox}[1]{ {
                \setlength{\unitlength}{1ex}\begin{picture}(4,3)(0,0)
                \put(0,0){\framebox(4.2,3.2){#1}}
                \end{picture}
                       }
                     }
\makeatletter
\newcommand{\PaperNumber}[1]{\def\@PaperNumber{#1}}
\newcommand{\Title}[1]{\def\@Title{#1}}
\newcommand{\Authors}[1]{\def\@Authors{#1}}
\newcommand{\Accuracy}[1]{\def\@Accuracy{#1}}
\newcommand{\Significance}[1]{\def\@Significance{#1}}
\newcommand{\Originality}[1]{\def\@Originality{#1}}
\newcommand{\Presentation}[1]{\def\@Presentation{#1}}
\newcommand{\Appropriateness}[1]{\def\@Appropriateness{#1}}
\newcommand{\Overall}[1]{\def\@Overall{#1}}
\newcommand{\Confidence}[1]{\def\@Confidence{#1}}
\newcommand{\OverallPC}[1]{\def\@OverallPC{#1}}


\def\makeform{%
%%
%%  dates
%%
\begin{tabular}{@{}lp{13cm}@{}}
{\bf Paper Number:} & \@PaperNumber \\[1ex]
{\bf Title:}        & \@Title       \\[1ex]
{\bf Author(s):}    & \@Authors
\end{tabular}\\[1ex]
\noindent\rule{\textwidth}{.01in}
%%
%%   ratings
%%
\begin{tabular*}{\textwidth}{@{}c@{\extracolsep{\fill}}c@{}}
~\\
\multicolumn{2}{c}{Rating of the following qualities from
                   0 to 10, with 10 being the best.}\\[2ex]
\begin{tabular}{@{}p{6.2cm}l@{}}
{\bf Technical accuracy:}       & \refbox{\@Accuracy}\\
{\bf Significance:}             & \refbox{\@Significance}\\
{\bf Originality:}              & \refbox{\@Originality}\\
{\bf Quality of presentation:}  & \refbox{\@Presentation} \\
{\bf Appropriateness:}          & \refbox{\@Appropriateness}
\end{tabular}
&
\begin{tabular}{@{}r@{--}l@{~:~~}ll@{}}
\multicolumn{3}{@{}p{6.3cm}@{}}{{\bf Overall evaluation of the
paper:}}&\refbox{\bf\@Overall}\\[2ex]
10 &  8 & strong accept \\
7  &  6 & weak accept   \\
5  &  4 & weak reject   \\
3  &  1 & strong reject \\
\multicolumn{2}{r@{~:~~}}{0} & outside the scope of RTA
\end{tabular}
\end{tabular*}
                \rule{\textwidth}{.01in}
\begin{tabular*}{\textwidth}{@{}c@{\extracolsep{\fill}}c@{}}
\parbox[b]{7.5cm}{
\parbox[b]{6cm}{{\bf Referee's confidence in the evaluation:}}
\hfill
\parbox[b]{1cm}{\raggedleft\refbox{\@Confidence}}
}
&
\parbox[b]{7.5cm}{
\parbox[b]{6cm}{{\bf Overall evaluation of the paper by the
PC member
(if different from reviewer):}}
\hfill
\parbox[b]{1cm}{\raggedleft\refbox{\@OverallPC}}%
}
\end{tabular*}
                \rule{\textwidth}{.01in}
%% end makeform
}

\makeatother


\newenvironment{Justification}{\makeform\newline\noindent{\bf Justification}
                        (why is the paper rated as above):
                        \newline}{~\newline}
\newenvironment{Recommendation}{\noindent{\bf Recommendation to the author(s)
                        for possible improvements:}
                        \newline}{~\newline}

\newenvironment{ToProgramCommittee}{\newline\noindent{\bf Confidential
                        comments to the PC:\\[1ex]}}{}

\newcommand{\CommitteeMember}[1]{\noindent\rule{\textwidth}{.01in}\\
                        {\bf Here starts the confidential
                        part of the report which is NOT
                        forwarded to the authors.}
                        \rule{\textwidth}{.01in}\\
                        \noindent{\bf Name of committee member: }{#1}
                        \vspace{1ex}\newline}
\newcommand{\Reviewer}[1]{\noindent{\bf Name of reviewer (if different):}
                        {#1} \vspace{1ex}}

\newenvironment{RefReport}{
        \newpage
        \font\tencmssdc=cmssdc10 scaled \magstep4
        \newfam\cmssdcfam
        \textfont\cmssdcfam=\tencmssdc
        \def\cmssdc{\fam\cmssdcfam\tencmssdc}
        {\noindent
        \LARGE{\sf Referee Report Form}}
        \hfill
        \begin{minipage}{45mm}
        \begin{center}
        {\cmssdc RTA--96}\\
        {\bf July 27--30\\
        Rutgers University\\
        {\sc New Jersey}}
        \end{center}
        \end{minipage}\\[5mm]
        }{}

% End of RTA96.sty
---------------------------------- cut ---------------------------------------




% Begin of LaTeX Referee Reports:







\documentstyle[11pt,RTA96]{article}
%-----------------------------------------------------------------------%
%                        Report form for RTA96                          %
%-----------------------------------------------------------------------%
\begin{document}
\begin{RefReport} % -----------------------------------------------------
\PaperNumber{60}
\Title{Discrete Normalization and Standardization in Deterministic
Residual Structures}
\Authors{Z. Khasidashvili and J. Glauert}
%-----------------------------------------------------------------------%
% Common part for authors and the PC.                                   %
% Replace the question marks below by ratings from 0 to 10,             %
% with 10 being the best.                                               %
%-----------------------------------------------------------------------%
\Accuracy{7}            % technical accuracy                            %
\Significance{6}        % significance of the work                      %
\Originality{7}         % originality of the work                       %
\Presentation{5}        % quality of presentation                       %
\Appropriateness{8}     % appropriateness for RTA                       %
\Overall{6}             % overall evaluation of the paper by the referee%
                        %   10 - 8  : strong accept                     %
                        %    7 - 6  : weak accept                       %
                        %    5 - 4  : weak reject                       %
                        %    3 - 1  : strong reject                     %
                        %        0  : outside the scope of RTA          %
\Confidence{7}          % referee's confidence in the paper's subject   %
\OverallPC{ }           % overall evaluation of the paper               %
                        % by the PC Member, if different; leave empty   %
                        % otherwise                                     %
%-----------------------------------------------------------------------%
\begin{Justification}   % Why do you rate the paper as above?           %
                        % An explanation is mandatory.                  %
                        %-----------------------------------------------%

In previous work the authors presented the
theory of Huet and L\'evy on needed reductions in the
abstract setting of {\em deterministic residual structures\/}
(DRSs), which covers many different kinds of rewrite systems.
In the present paper they pursue two different extensions:
\begin{itemize}
\item
The authors develop a neededness theory for permutation equivalent
rewrite sequences between two (arbitrary) terms $s$ and $t$.
Although this clearly generalizes their previous work in [GlKh96],
it seems to me that the most interesting cases ($t$ is a normal form,
$t$ is a weak head-normal form, etc.) were already obtained in [GlKh96].
Also the proofs appear to be quite similar to those in [GlKh96].
\item
The authors consider infinite rewrite sequences and show that the
standardization theorem doesn't hold in the infinitary setting.
This is interesting, surely, but I somehow have the impression
that this is more due to their definition of standard
reductions---Definition~4.3: standard $=$ self-essential---than to
an inherent problem in the theory of infinitary rewriting. More
precisely, I don't believe that essential redexes are more fundamental
than needed redexes when it comes to infinitary normalization. Consider
e.g.\ the TRS $\{ f(x) \to g(f(x)), a \to a \}$ and the term
$f(a)$. Because the TRS is non-erasing both redexes are essential,
but repeated contraction of the $a$ doesn't result in the
infinite normal form $g^\omega$.
\end{itemize}

\end{Justification}
%-----------------------------------------------------------------------%
\begin{Recommendation}  % Recommendation to the author(s) for           %
                        % possible improvements                         %
                        %-----------------------------------------------%


\begin{itemize}
\item
Illustrate the many technical definitions by means of
concrete (TRS) examples.
\item
(p.4)
What does the notation $t \to \hspace{-8pt} \to$ mean?
\item
(p.6)
The first occurrence of the rewrite rule $f(x) \to x$ has to be
$f(x) \to h(x,x)$.
\item
What's the difference between Definitions~3.1 and~4.5?
\item
Concerning the last paragraph in Section~6, isn't it about
time to combine all your results on DRSs into a journal
submission?
\item
There are quite a number of careless mistakes in the
references. Reference [KKSV93] is ambiguous.
There is no ``graph'' in the title of the second one.
Moreover it appeared last year in Information and Computation
{\bf 119}(1), pp.\ 18--38, 1995.
Add page numbers to [AEH94], [HuL\'e91], and
(the first) [KKSV93].
The first editor in [OR94] is called Nerode.
[SeRa90] appeared in LICS-90, not LICS-95! Its journal version is:
R.C.~Sekar and I.V.~Ramakrishnan, {\sl Programming in Equational
Logic: Beyond Strong Sequentiality},
Information and Computation {\bf 104}(1), pp.\ 78--109, 1993.
\end{itemize}
\end{Recommendation}
%-----------------------------------------------------------------------%
\end{RefReport} %--------------------------------------------------------

\end{document}


\documentstyle[11pt,RTA96]{article}
%-----------------------------------------------------------------------%
%                        Report form for RTA96                          %
%-----------------------------------------------------------------------%
\begin{document}
\begin{RefReport} % -----------------------------------------------------
\PaperNumber{60}
\Title{ Discrete Normalization and Standardization in
                        Deterministic Residual Structures}
\Authors{Z. Khasidashvili and J. Glauert         }
%-----------------------------------------------------------------------%
% Common part for authors and the PC.                                   %
% Replace the question marks below by ratings from 0 to 10,             %
% with 10 being the best.                                               %
%-----------------------------------------------------------------------%
\Accuracy{8}            % technical accuracy                            %
\Significance{8}        % significance of the work                      %
\Originality{7}         % originality of the work                       %
\Presentation{7}        % quality of presentation                       %
\Appropriateness{7}     % appropriateness for RTA                       %
\Overall{7}             % overall evaluation of the paper by the referee%
                        %   10 - 8  : strong accept                     %
                        %    7 - 6  : weak accept                       %
                        %    5 - 4  : weak reject                       %
                        %    3 - 1  : strong reject                     %
                        %        0  : outside the scope of RTA          %
\Confidence{?}          % referee's confidence in the paper's subject   %
\OverallPC{ }           % overall evaluation of the paper               %
                        % by the PC Member, if different; leave empty   %
                        % otherwise                                     %
%-----------------------------------------------------------------------%
\begin{Justification}   % Why do you rate the paper as above?           %
                        % An explanation is mandatory.                  %
                        %-----------------------------------------------%
The essence this paper is hard to capture, since it is based on a
stack or earlier papers (see the number of references in bot the
introduction and the text). The paper seems correct scientifically, but
it is hard to figure out the importance of the result.

Perhaps a paper better suited for a journal than for a conference.
\end{Justification}
%-----------------------------------------------------------------------%
\begin{Recommendation}  % Recommendation to the author(s) for           %
                        % possible improvements                         %
                        %-----------------------------------------------%
Page 2, {\it regular\/} is over-used specifically in TRS, choose
an other word.
\end{Recommendation}
%-----------------------------------------------------------------------%
\end{RefReport} %--------------------------------------------------------

\end{document}


\documentstyle[11pt,RTA96]{article}
%-----------------------------------------------------------------------%
%                        Report form for RTA96                          %
%-----------------------------------------------------------------------%
\begin{document}
\begin{RefReport} % -----------------------------------------------------
\PaperNumber{60}
\Title{ Discrete Normalization and Standardization in
                        Deterministic Residual Structures}
\Authors{Z. Khasidashvili and J. Glauert         }
%-----------------------------------------------------------------------%
% Common part for authors and the PC.                                   %
% Replace the question marks below by ratings from 0 to 10,             %
% with 10 being the best.                                               %
%-----------------------------------------------------------------------%
\Accuracy{?}            % technical accuracy                            %
\Significance{6}        % significance of the work                      %
\Originality{7}         % originality of the work                       %
\Presentation{6}        % quality of presentation                       %
\Appropriateness{6}     % appropriateness for RTA                       %
\Overall{6}             % overall evaluation of the paper by the referee%
                        %   10 - 8  : strong accept                     %
                        %    7 - 6  : weak accept                       %
                        %    5 - 4  : weak reject                       %
                        %    3 - 1  : strong reject                     %
                        %        0  : outside the scope of RTA          %
\Confidence{5}          % referee's confidence in the paper's subject   %
\OverallPC{ }           % overall evaluation of the paper               %
                        % by the PC Member, if different; leave empty   %
                        % otherwise                                     %
%-----------------------------------------------------------------------%
\begin{Justification}   % Why do you rate the paper as above?           %
                        % An explanation is mandatory.                  %
                        %-----------------------------------------------%
Deterministic residual structures (DRS) are abstract reduction systems
equipped with a residual relation. These structures are useful to study
the notion of rewriting in a very abstract setting. Here a version of
the standardization theorem and of the discrete normalization theorem
are proved for DRS that are stable and semi-linear.
\vspace{0.2cm}

On the one hand, due to the many forms of `reduction systems' known
in the literature it is very useful to study properties of rewriting
in an abstract setting. On the other hand, the definitions and results
are so very technical that I found it impossible to really follow all
the given arguments within a reasonable amount of time.

\end{Justification}
%-----------------------------------------------------------------------%
\begin{Recommendation}  % Recommendation to the author(s) for           %
                        % possible improvements                         %
                        %-----------------------------------------------%
{\bf Some detailed remarks:}
\vspace{+0.2cm}

\noindent
{\bf p.3, line 27:} ... $u\in t$ denotes that $u$ is a ...
\vspace{+0.1cm}

\noindent
{\bf p.6, line -13:} Shouldn't the first rule of $R$ be
$f(x)\rightarrow h(x,x)$?

\end{Recommendation}
%-----------------------------------------------------------------------%
\end{RefReport} %--------------------------------------------------------

\end{document}


\documentstyle[11pt,RTA96]{article}
%-----------------------------------------------------------------------%
%                        Report form for RTA96                          %
%-----------------------------------------------------------------------%
\begin{document}
\begin{RefReport} % -----------------------------------------------------
\PaperNumber{60}
\Title{ Discrete Normalization and Standardization in
                        Deterministic Residual Structures}
\Authors{Z. Khasidashvili and J. Glauert         }
%-----------------------------------------------------------------------%
% Common part for authors and the PC.                                   %
% Replace the question marks below by ratings from 0 to 10,             %
% with 10 being the best.                                               %
%-----------------------------------------------------------------------%
\Accuracy{10}           %                                               %
\Significance{5}        % significance of the work                      %
\Originality{5}         % originality of the work                       %
\Presentation{2}        % quality of presentation                       %
\Appropriateness{10}    % appropriateness for RTA                       %
\Overall{5}             % overall evaluation of the paper by the referee%
                        %   10 - 8  : strong accept                     %
                        %    7 - 6  : weak accept                       %
                        %    5 - 4  : weak reject                       %
                        %    3 - 1  : strong reject                     %
                        %        0  : outside the scope of RTA          %
\Confidence{5}          % referee's confidence in the paper's subject   %
\OverallPC{ }           % overall evaluation of the paper               %
                        % by the PC Member, if different; leave empty   %
                        % otherwise                                     %
%-----------------------------------------------------------------------%
\begin{Justification}

Deterministic residual structures were introduced by the authors in a
previous paper, and provide an abstract account of rewriting, along
similar lines to the Abstract Reduction Systems of Gonthier et al,
with in addition an axiomatised account  of residuals. Under mild
conditions, this paper develops a theory of neededness for these
reduction systems relative to a particular reduction $P: t
\rightarrow s$. They prove two main results:
\begin{enumerate}

\item a standardisation theorem for finite reductions---they also show
that this result does not extend to infinitary reductions;

\item a so-called discrete normalisation theorem.
\end{enumerate}

This paper is unfortunately extremely difficult to read; even the
introduction is not easy to decipher. The results are probably worth
publishing at some point, although it is difficult to assess the
statement of the discrete normalisation theorem without considerable
effort to understand the technical definitions. I recommend that the
paper is rejected at this stage.

\end{Justification}
%-----------------------------------------------------------------------%
\begin{Recommendation}

An abstract account of reduction systems and residuals seems to be a
good idea, although I would have liked to have seen some examples to
motivate this level of abstraction and to illustate the differences
with other definitions of reduction systems.  It is not at all obvious
that the technical details need to be quite so complicated. Much more
intuition is required: for example, I'm sure that the introduction can
be written with much less notation.  Also, the paper should be
self-contained: in particular, more details regarding residuals should
be given.

Paul Mellies of Edinburgh University has some results in his thesis
which may relate to this work.

\end{Recommendation}
%-----------------------------------------------------------------------%
\end{RefReport} %--------------------------------------------------------

\end{document}