Recientemente, Dana Scott propuso el cálculo lambda estocástico, un intento de introducir elementos probabilísticos en el cálculo lambda (sin tipo) basado en una semántica llamada modelo gráfico. Puede encontrar sus diapositivas en línea, por ejemplo, aquí y su artículo en Journal of Applied Logic , vol. 12 (2014).
Sin embargo, mediante una búsqueda rápida en la Web, encontré una investigación previa similar, por ejemplo, para el sistema de tipo Hindley-Milner . La forma en que introducen la semántica probabilística es similar a la de Scott (en el primero, usan mónadas, mientras que en el último Scott usa el estilo de paso continuo).
¿De qué manera el trabajo de Scott es diferente del trabajo anterior disponible, en términos de las teorías mismas o sus posibles aplicaciones?
Respuestas:
Una fortaleza aparente de su enfoque es que permite que las funciones de orden superior (es decir, los términos lambda) sean resultados observables, lo que generalmente hace que la teoría de la medición sea bastante complicada. (El problema básico es que los espacios de funciones medibles generalmente no tienen Borel álgebra para la cual la función de aplicación, a veces llamada "eval" - es medible; vea la introducción a las estructuras de Borel en papel para espacios de funciones ). Scott lo hace usando una codificación de Gödel desde términos lambda a números naturales, y trabajando directamente con los términos codificados. Una debilidad de este enfoque puede ser que la codificación podría ser difícil de extender con números reales como valores de programa. (Editar: Esto no es una debilidad; vea el comentario de Andrej a continuación).σ
El uso de CPS parece ser principalmente para imponer un orden total en los cálculos, para imponer un orden total en el acceso a la fuente aleatoria. La mónada estatal debería funcionar igual de bien.
Las "variables aleatorias" de Scott parecen ser las mismas que las "funciones de muestreo" de Park en su semántica operativa . La técnica de transformar valores uniformes estándar en valores con cualquier distribución se conoce más ampliamente como muestreo de transformación inversa .
Creo que solo hay una diferencia fundamental entre la semántica de Ramsey y Scott. Ramsey's interpreta los programas como cálculos que construyen una medida sobre los resultados del programa. Scott asume una medida uniforme existente en las entradas e interpreta los programas como transformaciones de esas entradas. (La medida de salida se puede calcular en principio usando preimágenes ). Scott es análogo al uso de la mónada aleatoria en Haskell.
En su enfoque general, la semántica de Scott parece más similar a la segunda mitad de mi disertación sobre lenguajes probabilísticos , excepto que me quedé con valores de primer orden en lugar de usar una codificación inteligente, usé infinitos árboles de números aleatorios en lugar de secuencias, e interpreté programas como cálculos de flecha. (Una de las flechas calcula la transformación del espacio de probabilidad fijo a las salidas del programa; las otras calculan imágenes previas y aproximadas). El capítulo 7 de mi disertación explica por qué creo que interpretar los programas como transformaciones de un espacio de probabilidad fijo es mejor que interpretarlos como cálculos. que construyen una medida Básicamente se reduce a "los puntos de fijación de las medidas son muy complicados, pero entendemos bastante bien los puntos de fijación de los programas".
fuente