La correspondance de modèle d'ordre élevé est un problème indécidable. Cela signifie qu’il n’existe aucun algorithme qui, étant donné une équation a => b
, où a
et b
sont des termes ouverts sur le calcul lambda simplement typé, trouve une substitution S
telle que aS => bS
, où =>
signifie «a la même forme normale de Bn». Pourtant, les humains peuvent résoudre ce problème efficacement. Par exemple, étant donné le problème suivant:
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))))))
Tout être humain ayant une connaissance suffisante du calcul lambda pourra remarquer F
la fonction "double" des numéros d'église, avec la solution
F = (λ a b c . (a b (a b c)))
Ma question est la suivante: si ce problème est indécidable, comment l’être humain peut-il le résoudre rapidement et sans effort?
computability
MaiaVictor
la source
la source
Réponses:
Les humains peuvent résoudre efficacement certains cas de ce problème, mais il n’ya aucune raison de croire qu’ils peuvent résoudre tous les cas de manière efficace. Montrer une instance qu'un humain peut résoudre efficacement ne signifie pas que l'homme peut résoudre toutes les instances efficacement.
Indécidable signifie "aucun algorithme ne peut résoudre toutes les instances et se termine toujours". Il pourrait toujours exister un algorithme capable de résoudre certains cas , même pour un problème indécidable.
Donc, il n'y a pas de contradiction.
la source
F = (λ a b c . (a b (a b c)))
et arrêtez-vous". C'est un algorithme informatique qui résout le problème dans certains cas (en particulier, dans exactement un cas). Oui, ça va. Poser une nouvelle question comme celle-là semble être la bonne chose à faire. Comme d'habitude, dites-nous quelles recherches vous avez effectuées dans la question (vous devez en faire avant de demander).Comme l’a noté l’un des commentaires, il faut savoir qu’il existe de très bons algorithmes permettant de résoudre en pratique la correspondance de modèle d’ordre élevé (comme le révélera une recherche rapide sur Google ).
Je n'en connais aucun qui résolve ce problème particulier, mais ce problème de «doublage» semble plus proche du domaine de la synthèse de programme . Je pense qu’il existe des systèmes de synthèse de programmes capables de résoudre ce type de problème.
Il est facile de créer des exemples qui étouffent ce système, et il semble que les humains sont particulièrement doués pour ce type de problèmes. Créer des algorithmes plus proches de l'homme dans sa capacité à résoudre ce type de problèmes relève de la démonstration automatique de théorèmes et de l'intelligence artificielle (pour les tentatives les plus ambitieuses / irréalistes).
la source
Les humains essaient toujours de résoudre le problème avec leurs propres connaissances. Ils ont donc développé un algorithme pour résoudre le problème avec quelques exemples de problèmes. Alors, un humain a développé un algorithme, mais rien ne dit que cet algorithme puisse résoudre tous les problèmes. Donc, aucun algorithme ne peut résoudre tous les problèmes, mais il y a toujours un problème qui peut être résolu par un humain même s'il n'existe pas d'algorithme parfait pour cela. Nous pouvons dire que nous savons comment résoudre un problème mais nous n'avons pas d'algorithme. .
la source