InitRech 2015/2016, sujet 16

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 !

Main Contribution

blabla

Application

blabla