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 a
i b
są otwartymi terminami na prostym typie rachunku lambda, znalazłby podstawienie S
takie, że aS => bS
gdzie =>
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ć?