So this sounds like this might lead to an undecidable theory but I thought I would give it a try and ask about it after I found nothing on the subject. I am somewhat interested in finding functions which are counter examples to predicates (or solutions to the inverse rather). I would like to restrict the functions to some small class however (possibly even smaller than primitive recursive) so I think there is hope of this working if I restrict them enough.

Has any work been done in this area? Have any tools been written for such things?

  • $\begingroup$ What kind of predicates? For some kinds what you propose is trivial, for many others it's undecidable. $\endgroup$ – Raphael Dec 8 '14 at 20:00
  • $\begingroup$ The Keyword you are looking for is Higher-Order Unification. See also here. $\endgroup$ – cody Dec 8 '14 at 20:34
  • $\begingroup$ Perhaps I just don't see the trivial way to use Higher-Order Unification as a means to find solutions to this. For instance $len (xs ++ ys) = (len xs) + (len ys)$. This is clearly easy to find a counter example to (constant 1 function) but I don't see how higher order unification helps me with that. $\endgroup$ – Jake Dec 9 '14 at 0:19
  • $\begingroup$ $\newcommand\doubleplus{+\kern-1.3ex+\kern0.8ex}$ looks like the latex came out really bad this looks better: $len(xs \doubleplus ys) = len\,\,xs + len\,\,ys$ $\endgroup$ – Jake Dec 9 '14 at 2:21

SMT solvers do support uninterpreted-functions as part of many logics. If there's a counter-example, then they will also print a "counter-example" function, which will be the predicate you're looking for. If you have a concrete example, we can surely see if one can be coded up using Z3.

| cite | improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.