User:Realazthat/Projects wishlist/LLVM/Algorithm Synthesis: Difference between revisions

From Rosetta Code
Content added Content deleted
No edit summary
No edit summary
 
(One intermediate revision by the same user not shown)
Line 3: Line 3:
Have an interpreter of language L.
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, and a weight W representing the time taken to execute it.
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:
Create a function, '''F''' in language '''L''' to accomplish a task '''T'''. So '''F''' would be executed as follows:
Line 13: Line 13:
<pre>
<pre>
//G is input from user
//G is input from user
constrain( Interpret(G,T).r == Interpret(F,T).r ) ///the results must always be equal
constrain( Interpret(G,T).R == Interpret(F,T).R ) ///the results must always be equal
assert( !(Interpret(G,T).w < Interpret(F,T)) ) ///w must always be less. We assert that this is false, hoping for a counter example.
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.
</pre>
</pre>


Line 22: Line 22:


Notes:
Notes:
* '''w''' should probably be calculated, or compared asymptotically.
* '''W''' should probably be calculated, and/or compared asymptotically.
⚫
* 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 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.
* 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:
References:
* http://www.eecs.berkeley.edu/Pubs/TechRpts/2010/EECS-2010-15.pdf
* http://www.eecs.berkeley.edu/Pubs/TechRpts/2010/EECS-2010-15.pdf
* http://scholarworks.umass.edu/cgi/viewcontent.cgi?article=1178&context=open_access_dissertations

Latest revision as of 18:13, 7 December 2010

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"