InitRech 2015/2016, sujet 16 : Différence entre versions
(→Main Contribution) |
(→Main Contribution) |
||
| Ligne 23 : | Ligne 23 : | ||
The main contribution of this project is the use of comparisons between two systems of affine recurrence equations to decide if two programs are equals. It is a real innovation in the domain of algorithm recognition. <br/> | The main contribution of this project is the use of comparisons between two systems of affine recurrence equations to decide if two programs are equals. It is a real innovation in the domain of algorithm recognition. <br/> | ||
Moreover, authors explain that in certain cases equivalence can not be demonstrated and they explain that a semi-decision procedure can be implemented. To do that, they use a semi-algorithm, wich is based on the use of computation of transitives closures of affine relations.<br/> | Moreover, authors explain that in certain cases equivalence can not be demonstrated and they explain that a semi-decision procedure can be implemented. To do that, they use a semi-algorithm, wich is based on the use of computation of transitives closures of affine relations.<br/> | ||
| − | + | To conclude this part, the presentation of the prototype and his limits show also that the work is not over and researchers explain some future research ways. | |
= Application = | = Application = | ||
Version du 13 juin 2016 à 18:01
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.
The end of the article suggest that a prototype of the tool is available and work efficiently. The principal problem is the fact that is cannot use semantical information on 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
This article has the objective to implement a way to to recognize algorithms. More precisely, it proposes means to determine if two algorithms are equivalent or not.
The main contribution of this project is the use of comparisons between two systems of affine recurrence equations to decide if two programs are equals. It is a real innovation in the domain of algorithm recognition.
Moreover, authors explain that in certain cases equivalence can not be demonstrated and they explain that a semi-decision procedure can be implemented. To do that, they use a semi-algorithm, wich is based on the use of computation of transitives closures of affine relations.
To conclude this part, the presentation of the prototype and his limits show also that the work is not over and researchers explain some future research ways.
Application
Algotrith recognition is very important in computer science. For the developper to know what he is doing, for the user to determine if the program will do what he wants...
We can imagine several applications of the tool developped by the authors : it could be possible to integrate the tool in compilators in order to minimize errors, gain precision ...
In fact, when you develop a program, it is interesting to know if you have done an error but it is also important to know why you have done it. And with algorithm recognition, we can know what we are realy doing. In fact if you want to develop a specific mathematic function and the tool does not analyse it, you can conlude that what you have done is certainly wrong.
Of course, it is also interesting when many programmers are working on the same project. Sometimes, it is complicated to understand what our colleagues have developed. And thanks to algorithm recognition it is easier to understand what they have realy wanted to do.
We can also imagine applications for beginners in computer science : with this tool, they could see whether they are doing well or not by compare with concrete and functional programs.
