¿Hay algún CCC conocido cerrado bajo una operación probable de dominio de potencia?

De manera equivalente, ¿existe una semántica denotacional conocida para los lenguajes de programación funcional probabilísticos de orden superior? Específicamente, ¿existe un modelo de dominio de cálculo puro sin tipo extendido por una operación de elección binaria aleatoria simétrica.$\lambda$

Motivación

Las categorías cerradas cartesianas proporcionan una semántica a los cálculos orden superior. Los dominios de poder probabilísticos proporcionan semántica a los programas estocásticos. Un CCC cerrado bajo una operación probable de dominio de potencia proporcionaría una semántica a un lenguaje de programación funcional de orden superior estocástico.$\lambda$

Trabajo relacionado

Tix, Keimel y Plotkin (2004) [1] dan construcciones modernas de las operaciones de dominio de potencia inferior, superior y convexa, pero observan que

Todavía es un problema abierto si existe una categoría cerrada cartesiana de dominios continuos que se cierra bajo la construcción de dominios de poder probabilísticos.

Mislove (2013) [2,3] proporciona semántica para variables aleatorias continuas en un lenguaje de primer orden, pero señala que

Aunque el dominio de poder probabilístico deja invariable el CCC de los posets completos dirigidos (dcpos, para abreviar) y los mapas continuos de Scott, no existe una categoría cerrada de dominios cartesianos, dcpos que satisfaga el supuesto de aproximación habitual, que se sabe que es invariante bajo Esta construcción. Lo mejor que se sabe es que la categoría de dominios coherentes es invariable bajo la mónada de elección probabilística [4], pero esta categoría no está cerrada cartesiana.

Referencias

1. Regina Tix, Klaus Keimel y Gordon Plotkin (2004) "Dominios semánticos para combinar probabilidad y no determinismo" .
2. Michael Mislove (2013) "Anatomía de un dominio de variables aleatorias continuas I"
3. Michael Mislove (2013) "Anatomía de un dominio de variables aleatorias continuas II"
4. Jung, A. y R. Tix (1998) "El problemático dominio de poder probabilístico"

El siguiente es un comentario extendido, no responde a su pregunta en los términos que lo planteó, pero proporciona una semántica para cálculos probabilísticos de orden superior que puede encontrar de interés.

En los últimos años ha habido una línea de investigación muy activa en torno a la llamada semántica denotativa cuantitativa de la lógica lineal, basada en la idea (originalmente debido a Girard [1]) de que los programas de orden superior pueden ser modelados por series de potencia. En el caso probabilístico, esto toma la forma de los llamados espacios de coherencia probabilística (PCS), también introducidos por Girard [2] y estudiados en profundidad por Danos y Ehrhard [3]. Los PCS producen modelos de cálculos probabilísticos con y sin tipo que son de una naturaleza muy diferente a los dominios de poder y otros modelos relacionados con la mónada. En particular, PCS da lo que hasta ahora es el único modelo completamente abstracto conocido de PCF probabilístico [4], que es notoriamente difícil y aparentemente imposible de lograr con dominios de poder (cf. el trabajo deJean Goubault-Larrecq ).

Además de Ehrhard, la semántica cuantitativa ahora es desarrollada activamente por Michele Pagani y sus coautores, le sugiero que consulte su página web para obtener referencias adicionales.

$\lambda$

[2] Jean-Yves Girard, Entre lógica y cuántica: un tratado . En lógica lineal en informática , CUP, 2004.

[3] Vincent Danos y Thomas Ehrhard, espacios de coherencia probabilística como modelo de cálculo probabilístico de orden superior . Información y cálculo 209 (6): 966-991, 2011.

[4] Thomas Ehrhard, Michele Pagani y Christine Tasson, Los espacios de coherencia probabilística son completamente abstractos para PCF probabilística . En Proceedings of POPL , pp. 309-320, 2014.

El comentario a continuación es correcto, pero es importante comprender el significado de elementos "finitos" o "compactos" de un dominio. Estas son las denotaciones de objetos computables en tiempo finito, por lo que su aparición en un modelo semántico no es por conveniencia teórica de prueba: representan la fuerte conexión entre el modelo y el cómputo real.

Bueno, la cita de Mislove ya contiene una respuesta positiva: la categoría de dcpos es carteisan cerrada y también cerrada bajo el dominio de poder probabilístico. De hecho, se puede usar para dar una semántica denotacional al cálculo probabilístico de orden superior. Sin embargo, los dcpos no satisfacen los "supuestos de aproximación habituales" de que cada elemento puede ser aproximado por elementos "finitos" en algún sentido, como es el caso de los cpos algebraicos y continuos. Estos supuestos ayudan con ciertos argumentos denotacionales, pero no son necesarios para dar una semántica per se.