Mostrando la función =? es imposible

Question

Aquí hay un laboratorio de un curso de informática de primer año, que se enseña en el esquema: https://www.student.cs.uwaterloo.ca/~cs135/assns/a07/a07.pdf

Al final del laboratorio, básicamente presenta el problema de detención y muestra que es imposible resolver introduciendo la función diagonal, que se define como:

(define (diagonal x)
  (cond
     [(halting? x x) (eternity 1)]
     [else true]))

Dónde eternity es un programa no terminado definido como (define (eternity x) (eternity x)). Que pasa cuando te alimentas diagonal su propia definición como entrada ...?

Todo esto es algo bastante estándar. Entonces, el laboratorio dice:

Para un desafío real, responda definitivamente la pregunta planteada al final del ejercicio 20.1.3 del texto, con la interpretación de esa función =? consume dos listas que representan el código para las dos funciones. Esta es la situación que la iglesia consideró en su prueba.

Entonces la esencia de esto es que function=? toma dos entradas. Cada uno es una lista, que representa la definición de una función, es decir, es una lista del formulario (define (id args ...) body ...). Podemos suponer que ambas funciones son sintácticamente válidas y terminarán para todas las entradas (sin errores de tiempo de ejecución). function=? Devuelve verdadero si y solo si las dos funciones siempre devolverán el mismo resultado cuando se les dan las mismas entradas. Por ejemplo,

(function=? '(define (foo x) (* 2 x)) 
            '(define (bar x) (+ x x))) ; should return #t

(function=? '(define (foo x) (+ x 1)) 
            '(define (bar x) (+ x 2))) ; should return #f

Ahora, function=? obviamente es imposible de escribir: el desafío es demostrar Es imposible. Pensé en esto por un tiempo, y la mejor solución que podría encontrar es la siguiente:

(define (disprove-function=? x)
  ((lambda (snip)
     (let ((self (list 'define '(disprove-function=? x)
                       (list snip (list 'quote snip)))))
       (if (function=? self '(define (id x) x))
           (list x)
           x)))
   '(lambda (snip) 
      (let ((self (list 'define '(disprove-function=? x)
                        (list snip (list 'quote snip)))))
        (if (function=? self '(define (id x) x))
            (list x)
            x)))))

Básicamente, disprove-function=? utiliza técnicas de quining estándar para generar su propio código fuente (la variable self), y luego pregunta function=? Si es equivalente a la función de identidad. Si function=? dice #f, entonces disprove-function=? siempre se comportará como la función de identidad. ¡Contradicción! Si function=? dice #t, entonces disprove-function=? siempre se comportará de manera diferente a la identidad; En particular, se comportará como el list función. ¡Contradicción! De este modo, function=? no puedo existir. Qed.

Mi pregunta es: ¿hay una forma más elegante de abordar este problema? Mi solución parece ... larga y fea. No tan agradable como el diagonal Función para demostrar que el problema de detención es insoluble.

NB: ¡Por favor, dame respuestas y no pistas! Aunque esta es una pregunta de tarea, no es mi Pregunta de tarea: ¡No voy a esta universidad! Además, como puede ver en el laboratorio, esta pregunta está bajo el Enhancements Categoría y no vale la pena, así que incluso si no me crees, todavía no hay problema para darme una respuesta. Finalmente ya tener Una solución, que estoy bastante seguro es correcta; Me preguntaba si había un mejor solución.

Answer 1

Usar el problema de detención parece la buena solución. Supongamos que tienes una función red que toma el código de una función (o λ a término) (o una función sin tipo), reduce un paso (o β-redex) en él y devuelve el código de la función resultante. Supongamos también que tienes una función normal Eso dice si el término está en forma normal.

En lenguaje de turing máquinas, red sería el cálculo de un paso y normal volvería verdadero cuando estamos en un estado final.

Simulemos el cálculo de $ n $ pasos, devolviendo $ 43 $ en lugar de $ 1 $ si alcanzamos el final del cálculo:

(define (run t n)
  (if (= n 0) 1
    (if (normal t) 43
      (run (red t) (n-1)))))

Entonces podemos decidir si la ejecución de un término terminará o no:

(define (one x) 1)
(define (terminate t) (not (function=? (run t) one)))

De eso podemos usar el argumento diagonal habitual:

(define (loop x) (loop x))
(define (f x) (if (terminate (code-of-application x (quote x))) (loop 0) 1)
(f code-of-f)

Si f terminar en code-of-f después (terminate (code-of-application code-of-f (quote code-of-f)) Volverá true y entonces f encenderá code-of-f. Entonces debería bucle. Después (terminate ...) debería regresar false y f terminará en code-of-f, contradicción.

Tecnicidades: uno necesita definir un lenguaje base que sea lo suficientemente expresivo como para poder escribir todo está escrito anteriormente. Entonces necesitas red y normal Lo cual puede ser más difícil de lo que uno puede imaginar. También necesita las técnicas estándar de Quine: quote que, dado el código de un término, devuelve un término que representa el código del término, code-of-application a b es fácil y por sí mismo, y, por supuesto, debe escribir todo lo anterior internamente para escribir code-of-f.

El Lambda-Calculus es sorprendentemente simple y expresivo para escribir todo esto y demostrar su corrección, por lo que Church lo usó para resolver El décimo problema de Hilbert, pero uno puede hacerlo en muchos idiomas, posiblemente de una manera más simple, utilizando trucos de quine específicos del lenguaje.