2012-06-04 13 views
12

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 ...)

+1

¿Qué sucede si una orden de reducción no finaliza mientras que otra no? ¿Obtienes la terminación? – augustss

+2

Ah, y su implementación de SKI es toda la prueba que necesito para completar. – augustss

+0

@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

Respuesta

5

A) Como dice augustss, su sistema está claramente completo.

B) Tiene razón en que determinar el tamaño de la solución es el mismo que el problema de detención. Si una secuencia no termina, entonces obtienes una solución infinita. Entonces, para determinar si el conjunto es infinito, debe determinar si una secuencia de reducción termina. Pero eso es precisamente el problema de detención!

C) Como recuerdo, un sistema que, dado un conjunto de instrucciones a una máquina de turing, simplemente dice cuántos pasos dan para terminar (que es, supongo, la cardinalidad de su conjunto de soluciones) o falla en terminar si las instrucciones en sí no pueden terminar es en sí mismo turing completo. Entonces eso debería ayudar con la intuición aquí.

+1

Una respuesta agradable, pero una cosa todavía me preocupa: es posible que una expresión posea una forma normal, y aún existe una orden de reducción que no termina. En este caso, el conjunto de solución sigue siendo infinito, aunque la reducción de orden normal finaliza. Por lo tanto, la cardinalidad del conjunto de soluciones no es exactamente lo mismo que si la reducción termina o no ... No estoy seguro de si esto invalida su argumento. – MathematicalOrchid

2

En respuesta a mi propia pregunta ... Encontré que al ajustar el código fuente, puedo hacerlo de modo que si la expresión de entrada SKI tiene una forma normal, esa forma normal siempre será la solución n. ° 1. Entonces, si simplemente ignoras cualquier otra solución, el programa reduce cualquier expresión de SKI a su forma normal.

Creo que esto constituye una "mejor prueba". ;-)

Cuestiones relacionadas