User:Realazthat/Projects wishlist/LLVM/Algorithm Synthesis

From Rosetta Code

Using an SMT solver, do the following:

Have an interpreter of language L.

So, for example, Interpret(X,A) will interpret X, which is of language L, and execute it with input A, and return the result, R, and a weight W representing the time taken to execute it.

Create a function, F in language L to accomplish a task T. So F would be executed as follows: 

Interpret( F, T )

Assert that there is no other function, say G, that is equivalent to F, that will have a lower weight. 

//G is input from user
constrain( Interpret(G,T).R == Interpret(F,T).R ) ///the results must always be equal
assert( !(Interpret(G,T).W < Interpret(F,T)).W ) ///W must always be less. We assert that this is false, hoping for a counter example.

All of this should be converted to SMT, the assertion declared to result true, the formula declared unsatisfiable, and hopefully the assertion proven false with a counter example.

Rinse and repeat, using the resulting G as the next F until unsatisfiable is true (in which case it is the optimal algorithm).

Notes:

  • W should probably be calculated, and/or compared asymptotically.
  • For the weight, one would probably give each instruction a weight, then sum up the weights during execution. Or, use a decidable language, and compute the complexity by counting loops etc. if possible.
  • There should be a memory constraint as well, as a huge constant array with precomputed results will probably yeild the lowest W. The memory should probably be constrained to a constant times the size of the input, again, asymptotically, for a good algorithm.

References:

Retrieved from "https://rosettacode.org/wiki/User:Realazthat/Projects_wishlist/LLVM/Algorithm_Synthesis?oldid=166475"