\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}
