49
$\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?

Improve this question
$\endgroup$
5
  • 29
    $\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. ♦
    Commented Sep 29, 2015 at 23:25
  • 39
    $\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
    Commented Sep 29, 2015 at 23:29
  • 27
    $\begingroup$ Solve this problem? I don't even understand this problem. $\endgroup$
    – User1000547
    Commented Sep 30, 2015 at 14:24
  • 3
    $\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
    Commented Oct 1, 2015 at 2:11
  • 1
    $\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
    Commented Oct 1, 2015 at 2:39

4 Answers 4

Reset to default
89
$\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.

Improve this answer
$\endgroup$
10
  • 25
    $\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. ♦
    Commented Sep 29, 2015 at 23:33
  • 12
    $\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
    Commented Sep 30, 2015 at 4:47
  • 4
    $\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
    Commented Oct 1, 2015 at 5:15
  • 4
    $\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
    Commented Oct 1, 2015 at 8:10
  • 3
    $\begingroup$ for posterity, a new link to: Where The Really Hard Problems Are $\endgroup$
    – Alex Moore-Niemi
    Commented Sep 12, 2016 at 2:55
4
$\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).

Improve this answer
$\endgroup$
3
$\begingroup$

Humans can solve some instances of undecidable problems and so can computers. Computers cannot solve all instances of undecidable problems, and not can humans.

Improve this answer
$\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.

Improve this answer
$\endgroup$
1
  • 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
    Commented Feb 3, 2017 at 9:18

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