1: \vspace{-0.3cm}

2: \section{Related Work} \label{rw}

3: \vspace{-0.2cm}

4: 

5: The Mercury programming language~\cite{Somogyi96-Mercury} is associated with a whole range of analysis tools for optimisation purposes. In Mercury also, the programmer has to annotate the program with information about modes, types, success and determinacy. A main difference is that not all logic programs are accepted by Mercury (only limited forms of unification are allowed). There are restrictions on the form of the programs and queries in order to generate more efficient code. Mercury is not based on the Warren's Abstract Machine, but has specialised - more efficient - algorithms, depending on the determinacy information. So our approach is more appealing to programmers who are willing to keep the full power of Prolog. Unlike Mercury, we do not change the usual execution model of Prolog based on the WAM~\cite{AitKaci91-WAM,Warren83-WAM}: our optimiser performs some transformations at the Prolog code level. Actually, our optimiser should be able to generate low-level code. But performing source-to-source transformations is more portable (and easier to explain) than generating specialised WAM's instructions. Most Mercury annotations can be translated into our formal specification language. A current limitation to our language is that, for instance, we cannot express that an input list contains only free distinct variables (this can be expressed in Mercury). On the other hand, more general directionalities can be described in our language. For instance, we can express that some argument is a list possibly non-instantiated and possibly non-linear, and that two terms possibly share a variable (this cannot be expressed in Mercury), like in the following formal specification for {\tt append}:

6: \vspace{-.1cm}

7: \small

8: \begin{verbatim}

9:       append

10:         in(L1:list(any), L2:list(any), L3:any)

11:         out(_, _, list(any))

12:         sol(sol =< 1)

13: \end{verbatim}

14: \normalsize

15: \vspace{-.1cm}

16: 

17: The Ciao preprocessor CiaoPP~\cite{Hermenegildo05-IntegratedProgramDebuggingVerificationOptimization} is a powerful static analyser based on abstract interpretation, which features many analyses similar to ours and other ones. The system can infer and/or check properties like regular types, modes, sharing, non-failure and determinacy, bounds on computational cost, bounds on sizes of terms in the program, and termination. In that system, procedures can be optionally annotated by assertions, which partially corresponds to specifications of our system. The system can perform automatic optimisations such as source-to-source transformation, specialisation, partial evaluation of programs, program parallelisation. Some transformations like cut insertion and semantic denormalisation are not performed in CiaoPP.

18: 

19: The authors of~\cite{Debray90-BanishingCut} consider how most of the common uses of cut can be eliminated from Prolog source programs, by relying on static analysis to generate them at compile time. Static analysis techniques are used to detect situations where to place cuts. In our approach, the insertion of cuts is only one part of the optimisation process: several source-to-source transformations are applied to find the best place where to place the cut (e.g., clause and literal reordering, semantic normalisation, etc.), to remove literals becoming useless due to the execution of cut in previous clauses, and to perform some partial evaluation.

20: