Dopasowywanie wzorca wysokiego rzędu jest nierozstrzygalnym problemem. Oznacza to, że nie ma algorytmu, który, biorąc pod uwagę równanie a => b, gdzie ai bsą otwartymi terminami na prostym typie rachunku lambda, znalazłby podstawienie Stakie, że aS => bSgdzie =>skrót oznacza „ma tę samą postać normalną Bn”. Jednak ludzie mogą skutecznie rozwiązać ten problem. Na przykład biorąc pod uwagę następujący 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))))))
Każdy człowiek z wystarczającą wiedzą na temat rachunku lambda będzie w stanie zauważyć, Fże funkcja „podwójna” dla liczb kościelnych szybko pojawia się wraz z rozwiązaniem, które
F = (λ a b c . (a b (a b c)))
Moje pytanie brzmi: jeśli ten problem jest nierozstrzygalny, jak ludzie mogą go szybko i bez wysiłku rozwiązać?