martes, enero 02, 2007

Hasta la vista baby...

Alan Turing hizo grandes aportes a la ciencias de la computación. Pese a ser conocido principalmente por la maquina de Turing, Turing fue de los pioneros en temas como la hipercomputación con su famosa Turing con oráculo, redes neuronales (redes "B-Type") y muchas otras cosas.

Dentro de su trabajo con la maquina de Turing, es famosa su demostración sobre la indecibilidad del problema de la parada, la cual implica la inexistencia de un programa el cual recibiendo como entrada otro programa pueda decir que este termina o se queda en un bucle infinito. Esta demostración (como la mayoría de demostraciones de inexistencia) parte del hecho que el algoritmo existe, pero a partir de la elección de una entrada particular (en este caso el algoritmo mismo) se llega a una paradoja.

Recuerdo que cuando leí por primera vez esto, me preguntaba si seria posible un replanteamiento del algoritmo que en vez de 2 salidas (si, no) pudiese dar como salidas (si, no, tal vez), es decir, dividir las entradas en "definitivamente paran" "no paran" "realmente no se"... En medio de mi ingenuidad creía que la mayoría de los problemas de parada con los que se encontraría un programador serian de la clase "se me olvido incrementar i" (donde i es un entero de 32 bits) y otro tipo de bobadas que se podían hallar simplemente a punta de fuerza bruta.

La pregunta que me intrigaba en ese entonces era; mas que hacer un algoritmo que espere a ver si para otro algoritmo (eso lo puedo hacer yo :P); ver que tan lejos podría llegar un algoritmo en disminuir la cantidad de "tal vez" dentro del espacio de posibles entradas. Tenia hasta la ligera idea (sin absolutamente ningún argumento para creerla) que los "tal vez" podían llevarse a un porcentaje mínimo...

Sin divagar mas, hace poco leí en el "new-scan" de Scientific American sobre un software que precisamente hacia el debug anti "freeze" , el cual lo estan utilizando especificamente para los drivers del Windows Vista. El nombre del programa... Terminator. El programa convierte la representación del código fuente (los loops y esas cosas) y lo convierte a una representación finita, y luego busca una demostración de correctitud (muy a lo Dijkstra).

Este programa no tiene ningún problema con la demostración de Turing, el programa puede resolver el 99.5% de las entradas (como sacaron el 99.5%? ni put@ idea)... ademas hacen la salvedad que en el "pequeño" espacio de entradas solubles, no entran problemas difíciles matemáticos, así que la ideita de hacer un driversito que incluya una version de la conjetura de Goldberg, o algunos problemas de Hilbert y esperar una respuesta del debugger es mas bien ingenua.

Los drivers ademas de lo anteriormente mencionado tienen mas simplificaciones que hacen posible a Terminator. Son relativamente independientes de otras instancias de software (llámense librerías o procesos) son relativamente pequeños y la interacción con usuarios es nula. Estas ventajas para análisis son vistas como retos a enfrentar para los autores de Terminator, y no es del todo absurdo algún día tener un mensaje de error de la forma:


Semantic Error at line 247
...While's condition never breaks

(me late que eso esta en un muy mal ingles)

1 comentario:

Federico dijo...

Esto me recordó el inspector de Javascript integrado de Firefox, que te puede decir "Amigo, parecen haber problemas con el programa JS de este sitio, ¿desea detenerlo?". Valdria la pena revisar las fuentes para saber si estan realmente inspeccionando el codigo de alguna forma o solo revisan una condicion de tiempo (mientras tiempo_pasado < N siga)...