42
$\begingroup$

High-order pattern matching is an undecidable problem. That means there is no algorithm that, given an equation a => b, where a and b are open terms on the simply typed lambda calculus, finds a substitution S such that aS => bS, where => stands for "has the same Bn normal form". Yet, humans can solve that problem efficiently. For example, given the following problem:

a = (λt . t 
    (F (λ f x . (f (f (f x))))) 
    (F (λ f x . (f (f x)))))
b = (λ t . t
    (λ f x . (f (f (f (f (f (f x)))))))
    (λ f x . (f (f (f (f x))))))

Any human with sufficient knowledge on the lambda calculus will be able to notice F is the "double" function for church numbers, quickly coming with the solution that

 F = (λ a b c . (a b (a b c)))

My question is: if that problem is undecidable, how can humans quickly and effortlessly solve it?

$\endgroup$
  • 23
    $\begingroup$ "humans can solve that problem efficiently" - citation needed. What's your evidence for that? Showing one example where you can solve it efficiently does not mean you can solve it efficiently for all instances of the problem. You can't prove "X is true, for all X" by showing one example of X where X is true. $\endgroup$ – D.W. Sep 29 '15 at 23:25
  • 32
    $\begingroup$ A problem is undecidable means that there is no algorithm that correctly answers "yes" or "no" for every instance of the problem. It doesn't imply that one can find an algorithm that solves some (or many) instances of the problem. [Heh. As DW answered while I was composing this remark.] $\endgroup$ – Rick Decker Sep 29 '15 at 23:29
  • 22
    $\begingroup$ Solve this problem? I don't even understand this problem. $\endgroup$ – MikeTheLiar Sep 30 '15 at 14:24
  • 2
    $\begingroup$ The way I understood it is this: That solution is an ad hoc one. Each instance of the problem has one -- in most cases not as easily motivated as in your example, but you can always say 'if you get instance X, output Y' since an algorithm can be judged only on the basis of correctness -- but hard-coding all such solutions in this way does not produce a finite procedure (which is the only reasonable kind and thus what is usually meant). Alternatively stated, in order for a problem to be decidable you're not allowed to see which instance is given before choosing the algorithm's strategy. $\endgroup$ – Vandermonde Oct 1 '15 at 2:11
  • $\begingroup$ Also, this is why only problems with an infinite number of instances are generally considered or called such, since you could otherwise just enumerate all the solutions as above. $\endgroup$ – Vandermonde Oct 1 '15 at 2:39
77
$\begingroup$

Humans can solve some instances of that problem efficiently, but there is no reason to believe that humans can solve all instances efficiently. Showing one instance that a human can solve efficiently does not imply that humans can solve all instances efficiently.

Undecidable means "there is no algorithm that can solve all instances and that always terminates". There could still be an algorithm that can solve some instances, even for an undecidable problem.

So there is no contradiction.

$\endgroup$
  • 22
    $\begingroup$ @srvm, yup, it does mean that. For instance, here is a stupid example of a computer algorithm: "if the input is exactly the example given in your question, then output F = (λ a b c . (a b (a b c))) and halt". That's a computer algorithm that solves the problem for some cases (in particular, for exactly 1 case). Yes, that is OK -- asking a new question like that seems like the right thing to do. As usual, please do tell us what research you've done in the question (you should do some before asking). $\endgroup$ – D.W. Sep 29 '15 at 23:33
  • 9
    $\begingroup$ Where the Really Hard Problems Are claims that even in NP complete problems most instances can be solved easily. This matches my experience. Usually there are features of the problem that make (at least part of) the solution obvious. The hard ones are carefully balanced between success and failure, but there are not many of those. $\endgroup$ – Ross Millikan Sep 30 '15 at 4:47
  • 3
    $\begingroup$ @srvm if you think about it, solving difficult problems like these in special cases is exactly what an optimizer has to do. $\endgroup$ – Cort Ammon Oct 1 '15 at 5:15
  • 2
    $\begingroup$ @srvm: An excellent example of an undecidable problem that we make computers solve almost every day is the halting problem. We know that the halting problem is undecidable yet we still persist in writing linters, static analyzers and compilers that tries to detect unwanted infinite loops. How we do it is by "rule-of-thumb". That is, we know from human experience (not algorithm) that certain kinds of code enters infinite loop. So we ask the computer to look for the cases we know. We know that such programs will never catch all bugs. But it's better than nothing. $\endgroup$ – slebetman Oct 1 '15 at 8:10
  • 2
    $\begingroup$ for posterity, a new link to: Where The Really Hard Problems Are $\endgroup$ – Alex Moore-Niemi Sep 12 '16 at 2:55
3
$\begingroup$

As one of the comments notes, one should be aware that there are some pretty good algorithms for solving Higher Order Pattern Matching in practice (as a quick google search will reveal).

I don't know of any that solve this particular problem, but this "doubling" problem feels closer to the field of program synthesis. I do believe that there are program synthesis systems which can tackle this kind of problem.

It's easy to create examples which make those system choke though, and it does seem that humans are particularly good at these kinds of problems. Creating algorithms which are closer to humans in their ability to solve these kinds of problems is the purview of automatic theorem proving and artificial intelligence (for the more ambitious/unrealistic attempts).

$\endgroup$
1
$\begingroup$

Humans always try to solve the problem with their own knowledge , so humans develop some algorithm to solve the problem with some instances of problem .So human develop an algorithm, but there is no surety that the particular algorithm can solve every single problem . So no algorithm can solve every problem , but there is still some problem that can be solve by human even though there is not a perfect algorithm for that like we can say that we know how to solve a problem but we don't have an algorithm.

$\endgroup$
  • 8
    $\begingroup$ Isn't this just a paraphrase of the existing answer? I know I've criticized most of your answers so the following might sound insincere, but it's not. It really is great that you want to contribute to the site. It would be really great if you could help us to answer some of our 2500 unanswered questions, rather than questions where we already have an answer that says everything you want to say. Thanks! $\endgroup$ – David Richerby Feb 3 '17 at 9:18

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.