Pasé una semana o dos programando un solucionador de lógica simple. Después de haberlo construido, me pregunté si el lenguaje que resuelve es completo o no. Así que codifiqué un pequeño conjunto de ecuaciones que aceptan cualquier expresión válida en el cálculo del combinador SKI, y produzco un conjunto de resultados que contiene la forma normal de esa expresión. Dado que SKI es Turing-complete, lo que demuestra que mi lenguaje puede ejecutar SKI demostraría su integridad Turing.¿Mi programa está completo?
Hay un problema técnico, sin embargo. El solucionador no reduce la expresión en el orden normal. En realidad, lo que hace es probar cada posible orden de reducción. Lo que significa que el conjunto de soluciones suele ser enorme. Si existe una forma normal, estará allí en algún lugar, pero es difícil decir donde.
Esto me lleva a dos preguntas:
es mi lengua Turing completo? ¿O necesito encontrar una mejor prueba?
¿El número de soluciones es una función computable de la entrada?
(Al principio supone que el tamaño del conjunto solución fue exponencial o factorial en el tamaño de la entrada. Pero en una inspección más cercana, esto no es cierto. Puede escribir expresiones enormes que ya están en forma normal, y pequeñas expresiones que no terminan. Tengo la sensación de que determinar el tamaño del conjunto de soluciones puede ser equivalente a resolver el problema de detención, pero no estoy del todo seguro ...)
¿Qué sucede si una orden de reducción no finaliza mientras que otra no? ¿Obtienes la terminación? – augustss
Ah, y su implementación de SKI es toda la prueba que necesito para completar. – augustss
@augustss He arreglado cuidadosamente que el código intente la reducción normal de la orden _primero_. Entonces, si existe una forma normal, estará en una posición finita en el conjunto de soluciones. Sin embargo, si existe una orden de reducción no terminadora, se garantiza que el soler la encontrará y producirá un conjunto de soluciones infinitas.¿Está produciendo un conjunto infinito que contiene la respuesta correcta _en alguna parte_ suficiente para Turing-completitud? Quiero decir, simplemente enumerar todas las posibles expresiones de SKI haría eso ... – MathematicalOrchid