Halting problem proof’s leak (en construcción)

 Advertencia:

Tratándose de un resultado clásico, la irresolubilidad del Halting Problem se considera un tema cer

rado. Al oponer objeciones a la demostración canónica, no pretendo haber logrado la refutación de la misma; sólo espero que se vea que hay ambigüedades que deberían ser aclaradas para precisar los alcances del resultado, y especialmente, las asunciones tácitas que provienen del documento original de Turing, donde él mismo reconoce ciertas lagunas que no quiere tratar por el momento.

Punto de fuga en la demostración 

del Halting Problem

Tomaré como referencia la siguiente demostración de la irresolubilidad del Halting Problem, en la versión de Martin Davis, Ron Sigal y Elaine J. Weyuker (“Computability, Complexity and Languages”, 2nd. Edition, 1994), aceptando que refleja fielmente la demostración original de Alan M. Turing de 1936, y las múltiples versiones de la misma que ha habido desde entonces:

Nótese que HALT(x, y) no está explícitamente definida si se le pasa el código G de una fórmula abierta. Y no se trata de decir que la función argumento es indefinida, pues no se trata de indefinición del valor de la función (variable dependiente) sino del valor del argumento (variable independiente). Y eso es exactamente lo que sucede cuando se usa y0   como argumento.
Debe tenerse en cuenta que y0 es el código de P(x), pero P(y0) ya no tiene código y0.

Así, la demostración se obtiene a costa de suponer que, si no se define el valor de la variable libre, la función intérprete puede igualmente tomar un valor como si la función interna estuviera indefinida para un argumento determinado. En tren de aceptar ambigüedades, esto es como suponer que la función interna no está definida para ningún valor de su argumento, lo que sesga totalmente la demostración, porque una función que no está definida para ningún valor no existe.
Eso se podría solucionar con la función sub( x, #x, #’x’ ).
En este punto cabría preguntarse si sub() termina. Porque si no lo hace, el argumento queda tan indeterminado como si la variable no hubiera sido reemplazada por la función. En efecto, sub() termina, pero la interpretación que debe hacer la función anfitrión no, porque el resultado es una función compuesta con una función que tiene una variable libre. Y recomienza el problema.
Pero aún así, se puede hacer escapar de la refutación a HALT() si se la define de este modo:

HALT(X,Y){
    IF ( X = Y )
        IF ( CANT_LLAMADAS_HALT(Y) ES PAR )
            RETURN TRUE;
        ELSE
            RETURN FALSE;
    ELSE
        RETURN OLD_VERSION_HALT (X, Y);
}

Es fácil ver que si una función debe determinar si otras paran o no con determinado input, puede también determinar si hay en ellas llamados a ella misma, y cuántas veces cuando están anidadas.




El funcionamiento es el siguiente. El programa contradictor de Turing sigue cumpliendo su cometido, es decir, para cuando ~HALT(y0, y0), y no para cuando HALT(y0, y0); pero la instancia de HALT() que envuelve al contradictor es la que se comporta diferente. No lo hace como las instancias internas, ya que tiene en cuenta si los argumentos son iguales, y el número de veces que ha sido invocada. Así, cuando es invocada sin argumentos definidos en la instancia más interna, decide que la falta de definición equivale a PARAR. En la instancia posterior, teniendo en cuenta que ya habrá un contradictor en medio, decidirá que éste (el contradictor) NO PARA. 


Por supuesto, para esta definición de HALT() no se cumple la contradicción que señala Davis.

  [tex] x^3 [/tex]