== Question ==

Can we establish a useful theory and collection of design patterns for lightweight checking?


== Summary ==

For many problems it is easier to check if an answer is correct than to compute an answer (e.g. multiplying a set of numbers together is easier than factoring, polynomial evaluation is easier than root finding, validating a proposed satisfying assignment is easier than finding a satisfying assignment).  Such checks can be used to guard the correctness of a computation instead of brute force replicated computation.  While there are numerous, useful examples where this is true, it is not clear when we can find such lightweight checks or how to do so.

== Subquestions ==
   
  * What computational classes are lightweight checkable (i.e., for what class of computations is it provably (asymptotically or a constant-factor) less expensive to check (deterministically or probabilistically) the solution than to compute it? 
         * A good target for the constant-factor benefit might be 10x (i.e., at least one-tenth the cost of computing)
  * Can we enlarge this class by ''extending'' the output of the base computation so its results include a certificate to assist checking? (e.g. Extended GCD).
  *  How do we express checks in computation and optimize their use?

== Relevant Scenarios ==

 * [[Scenarios/S1|Scenario 1]]

== Workshop Materials ==

 * [[attachment:Meetings/First/Program/lightweight.pdf|Workshop 1 Slides]]

== Existing Work ==

 * Extended GCD and some examples of checkability are described in: Manuel Blum and Sampath Kannan. ''[[http://doi.acm.org/10.1145/200836.200880|Designing Programs that Check Their Work]],'' in ''Journal of the ACM,'' volume 42, number 1, pp. 269--291, 1995.

 * ''add additional references here''

== Comments ==

 * ''To comment, please add another bullet to this list.''