La coincidencia de patrones de alto orden es un problema indecidible. Eso significa que no existe un algoritmo que, dada una ecuación a => b
, donde a
y b
son términos abiertos en el cálculo lambda simplemente tipeado, encuentre una sustitución S
tal que aS => bS
, donde =>
significa "tiene la misma forma normal de Bn". Sin embargo, los humanos pueden resolver ese problema de manera eficiente. Por ejemplo, dado el siguiente problema:
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))))))
Cualquier humano con suficiente conocimiento sobre el cálculo lambda podrá notar que F
es la función "doble" para los números de la iglesia, que viene rápidamente con la solución que
F = (λ a b c . (a b (a b c)))
Mi pregunta es: si ese problema es indecidible, ¿cómo pueden los humanos resolverlo rápida y fácilmente?
computability
MaiaVictor
fuente
fuente
Respuestas:
Los humanos pueden resolver algunos casos de ese problema de manera eficiente, pero no hay razón para creer que los humanos puedan resolver todos los casos de manera eficiente. Mostrar una instancia que un humano puede resolver de manera eficiente no implica que los humanos puedan resolver todas las instancias de manera eficiente.
Indecidible significa "no existe un algoritmo que pueda resolver todas las instancias y que siempre termine". Todavía podría haber un algoritmo que pueda resolver algunas instancias , incluso para un problema indecidible.
Entonces no hay contradicción.
fuente
F = (λ a b c . (a b (a b c)))
y pare". Ese es un algoritmo informático que resuelve el problema para algunos casos (en particular, para exactamente 1 caso). Sí, está bien, hacer una nueva pregunta como esa parece ser lo correcto. Como de costumbre, díganos qué investigación ha hecho en la pregunta (debe hacer un poco antes de preguntar).Como señala uno de los comentarios, uno debe tener en cuenta que hay algunos algoritmos bastante buenos para resolver la coincidencia de patrones de orden superior en la práctica (como revelará una búsqueda rápida en Google ).
No conozco ninguno que resuelva este problema en particular, pero este problema de "duplicación" se siente más cercano al campo de la síntesis de programas . Creo que existen sistemas de síntesis de programas que pueden abordar este tipo de problema.
Sin embargo, es fácil crear ejemplos que hagan que esos sistemas se ahoguen, y parece que los humanos son particularmente buenos en este tipo de problemas. Crear algoritmos que estén más cerca de los humanos en su capacidad para resolver este tipo de problemas es el ámbito de la prueba automática de teoremas y la inteligencia artificial (para los intentos más ambiciosos / poco realistas).
fuente
Los humanos siempre intentan resolver el problema con su propio conocimiento, por lo que los humanos desarrollan algún algoritmo para resolver el problema con algunas instancias de problema. Por lo tanto, los humanos desarrollan un algoritmo, pero no hay certeza de que el algoritmo particular pueda resolver cada problema. Por lo tanto, ningún algoritmo puede resolver todos los problemas, pero todavía hay algún problema que puede resolver el ser humano a pesar de que no hay un algoritmo perfecto para eso, como podemos decir que sabemos cómo resolver un problema pero no tenemos un algoritmo .
fuente