Version du 4 juin 2016 à 17:09

Article summary

This article is about algorithm recognition. It is show how we can analyse programs with using comparisons between systems of affine recurrence equations.

When we are coding something, we would like that a tool could analyse what we have done and describe it. Many solutions exist already, using regognition of the structure of the code, with specifics grammar and pattern. This article suggest an other way to analyse a program. It is proposed to analyse a program by comparing the source code with library of algorithms. Unfortunately, in the general case, the equivalence between two programs is undecidable. But we will see that find cases for which the equivalence problem is solvable is possible.

The first part of the work is to normalize programs in order to compare them. To do this, we need to have similiar type of data, wich are easily computable. That is why it is decided to normalize programs to a system of affine recurrence equations. Indeed, programs can be automaticaly converted to this type of equations. It can be interesting to notify that a system of recurrence equations is said to be computable if none of its variable instances depends on itself. This is this type of equations wich is used by the Turing Machine to determine if a system is computable or not.

When convertion to recurrence equations is done, we have two systems of equations with their input and output variables
Now, we will see how compare them in order to design an equivalence between these systems if it is possible. Basically, we can say that two systems are equivalent only if the output evaluate to the same values provided that the input variables are equal. Also, we suppose that values belong to the Herbrand universe (or the initial algebra) of the operators occurring in the computation(The Herbrand universe is defined by a vocabulary that is defined solely by the syntactical properties of it).

As we have seen above, the equivalence between two reccurence equations can be undecidable.
That is why we define here a procedure which may prove or disprove the equivalenc e of two systems... or fails !

To design this procedure, a memory state automaton is associated to each pair of equations in such a way that the equivalence of our expressions can be expressed as problems of reachability in the corresponding automatons.
Automatons are constructed on the initial state of the systems and transitions are built according to the fact that a state can be replaced by is successor, provided the firing relation. We do that for the entire equations and finally we can say two systems are equivalent if the equivalent automaton is such that all failures state are unreachable and the reachability relation of each success state is included in the identify relation.

A prototype of the tool is available and work efficiently, the principal problem is the fact that is cannot use semantical informationon the underlying operator. Futur work will be focused on building a library of reference algorightms wich can be compared with programs of users.

Main Contribution

blabla

Application