Y a-t-il un CCC connu fermé dans le cadre d'une opération de domaine de puissance probabiliste?

De manière équivalente, existe-t-il une sémantique dénotationnelle connue pour les langages de programmation fonctionnels d'ordre supérieur probabilistes? Plus précisément, existe-t-il un modèle de domaine de -calculus pur non typé étendu par une opération de choix binaire aléatoire symétrique.$\lambda$

Motivation

Les catégories fermées cartésiennes fournissent une sémantique aux -calculi d' ordre supérieur. Les domaines de puissance probabilistes fournissent une sémantique aux programmes stochastiques. Un CCC fermé sous une opération de domaine de puissance probabiliste fournirait une sémantique à un langage de programmation fonctionnel d'ordre supérieur stochastique.$\lambda$

Travaux connexes

Tix, Keimel et Plotkin (2004) [1] donnent des constructions modernes des opérations du domaine de puissance inférieur, supérieur et convexe, mais remarquent que

Reste à savoir s'il existe une catégorie fermée cartésienne de domaines continus qui est fermée par la construction de domaines de pouvoir probabilistes.

Mislove (2013) [2,3] donne la sémantique des variables aléatoires continues dans un langage de premier ordre, mais remarque que

Même si le domaine de puissance probabiliste laisse le CCC des posets complets dirigés (dcpos, pour faire court) et des cartes Scott-continues invariantes, il n'y a pas de catégorie fermée cartésienne de domaines - dcpos qui satisfont à l'hypothèse d'approximation habituelle - qui est connue pour être invariante sous cette construction. Le mieux connu est que la catégorie des domaines cohérents est invariante sous la monade de choix probabiliste [4], mais cette catégorie n'est pas fermée cartésienne.

Références

1. Regina Tix, Klaus Keimel et Gordon Plotkin (2004) "Domaines sémantiques pour combiner probabilité et non-déterminisme" .
2. Michael Mislove (2013) "Anatomie d'un domaine de variables aléatoires continues I"
3. Michael Mislove (2013) "Anatomie d'un domaine de variables aléatoires continues II"
4. Jung, A. et R. Tix (1998) "Le domaine de pouvoir probabiliste gênant"

Ce qui suit est un commentaire étendu, il ne répond pas à votre question dans les termes que vous lui avez posés mais donne une sémantique pour les calculs probabilistes d'ordre supérieur que vous pouvez trouver intéressants.

Au cours des dernières années, il y a eu une ligne de recherche très active autour de la soi-disant sémantique dénotationnelle quantitative de la logique linéaire, basée sur l'idée (originellement due à Girard [1]) que les programmes d'ordre supérieur peuvent être modélisés par des séries de puissance. Dans le cas probabiliste, cela prend la forme d' espaces dits de cohérence probabilistes (PCS), également introduits par Girard [2] et étudiés en profondeur par Danos et Ehrhard [3]. Les PCS produisent des modèles de calculs probabilistes typés et non typés qui sont de nature très différente des domaines de puissance et d'autres modèles liés à la monade. En particulier, PCS donne ce qui est jusqu'à présent le seul modèle entièrement abstrait connu de PCF probabiliste [4], qui est notoirement difficile et apparemment impossible à réaliser avec des domaines de puissance (cf. les travaux deJean Goubault-Larrecq ).

Outre Ehrhard, la sémantique quantitative est maintenant activement développée par Michele Pagani et ses coauteurs, je vous suggère de consulter sa page Web pour des références supplémentaires.

[1] Jean-Yves Girard, foncteurs normaux, séries de puissance et -calculus. Annals of Pure and Applied Logic 37 (2): 129-177, 1988.$\lambda$

[2] Jean-Yves Girard, Entre logique et quantique: un tract . Dans Logique linéaire en informatique , CUP, 2004.

[3] Vincent Danos et Thomas Ehrhard, Les espaces de cohérence probabilistes comme modèle de calcul probabiliste d'ordre supérieur . Information et calcul 209 (6): 966-991, 2011.

[4] Thomas Ehrhard, Michele Pagani et Christine Tasson, Les espaces de cohérence probabilistes sont entièrement abstraits pour le PCF probabiliste . Dans Actes de POPL , pp.309-320 , 2014.

Le commentaire ci-dessous est correct, mais il est important de comprendre la signification des éléments "finis" ou "compacts" d'un domaine. Ce sont les dénotations d'objets calculables en temps fini, donc leur apparition dans un modèle sémantique n'est pas pour la commodité de la preuve - elles représentent la forte connexion entre le modèle et le calcul réel.

Eh bien, la citation de Mislove contient déjà une réponse positive: la catégorie des dcpos est fermée par carteisan et également fermée sous le domaine de pouvoir probabiliste. Il peut en effet être utilisé pour donner une sémantique dénotationnelle au calcul probabiliste d'ordre supérieur. Cependant, les dcpos ne satisfont pas aux "hypothèses d'approximation habituelles" selon lesquelles chaque élément peut être approximé par des éléments "finis" dans un certain sens, comme c'est le cas pour les cpos algébriques et continus. Ces hypothèses aident à certains arguments de dénotation mais ne sont pas nécessaires pour donner une sémantique en soi.