¿Alguien puede señalarme la referencia para la no definibilidad del módulo de continuidad funcional en PCF?
Andrej Bauer ha escrito una muy buena publicación de blog explorando algunos de los problemas con más detalle, pero resumiré solo un poco de su publicación para dar un poco de contexto a esta pregunta. El espacio Baire es el conjunto de secuencias de números naturales, o equivalentemente el conjunto de funciones de naturals a naturals . Para esta pregunta, restringiremos nuestra atención solo a las secuencias que son computables.
Ahora, una función es continua si para cada , el valor de depende solo de un número finito de los elementos de , y es computablemente continuo si realmente podemos calcular un valor superior dependiente de cuántos elementos de se necesitan. En algunos modelos de computación, en realidad es posible escribir un programa que toma una función computable en el espacio de Baire y un elemento del espacio de Baire, y devuelve el límite superior en el número de elementos de la secuencia. x s ∈ B f ( x s ) x s x s m o d u l u s : ( B → b o o l ) → B →
Un truco para implementar esto es utilizar el almacenamiento local para registrar el índice máximo en la secuencia vista:
let modulus f xs =
let r = ref 0 in
let ys = fun i -> (r := max i !r; xs i) in
f ys;
!r
Por supuesto, el ys
argumento ya no es un programa puramente funcional. Mi interés en este programa proviene del hecho de que solo hace uso de la tienda local y, por lo tanto, es puramente extensional . Trabajo (entre otras cosas) en programación imperativa de orden superior, y estoy diseñando teorías de tipos que podrían clasificar esto como una función pura.
También hay ejemplos más prácticos, que incluyen cosas como la memorización y la agrupación de conexiones, pero este es un ejemplo particularmente hermoso.
fuente