2
$\begingroup$

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?

Improve this question
$\endgroup$
4
  • $\begingroup$ What kind of predicates? For some kinds what you propose is trivial, for many others it's undecidable. $\endgroup$
    – Raphael
    Commented Dec 8, 2014 at 20:00
  • $\begingroup$ The Keyword you are looking for is Higher-Order Unification. See also here. $\endgroup$
    – cody
    Commented Dec 8, 2014 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
    Commented Dec 9, 2014 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
    Commented Dec 9, 2014 at 2:21

1 Answer 1

Reset to default
1
$\begingroup$

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.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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