We introduce a formal meta-language for probabilistic programming, capable of
expressing both programs and the type systems in which they are embedded. We
are motivated here by the desire to allow an AGI to learn not only relevant
knowledge (programs/proofs), but also appropriate ways of reasoning
(logics/type systems). We draw on the frameworks of cubical type theory and
dependent typed metagraphs to formalize our approach. In doing so, we show that
specific constructions within the meta-language can be related via bisimulation
(implying path equivalence) to the type systems they correspond. This allows
our approach to provide a convenient means of deriving synthetic denotational
semantics for various type systems. Particularly, we derive bisimulations for
pure type systems (PTS), and probabilistic dependent type systems (PDTS). We
discuss further the relationship of PTS to non-well-founded set theory, and
demonstrate the feasibility of our approach with an implementation of a
bisimulation proof in a Guarded Cubical Type Theory type checker.

我们引入了一个正式的元语言来进行概率编程，旨在让 AGI 不仅学习相关知识（程序 / 证明），而且学习适当的推理方式（逻辑 / 类型系统）。我们利用立方型类型理论和依赖类型元图的框架来形式化我们的方法。通过这样做，我们展示了元语言中的特定构造可以通过双模拟（意味着路径等效）与它们相应的类型系统相关联，从而为各种类型系统推导出综合指称语义。特别是，我们推导出了纯类型系统（PTS）和概率依赖类型系统（PDTS）的双模拟。我们进一步讨论了 PTS 与非良基础集合论的关系，并在立方保护类型理论类型检查器中实现了双模拟证明的可行性.

一种元概率编程语言，用于概率和非良基础类型系统的双模拟

A meta-probabilistic-programming language for bisimulation of probabilistic and non-well-founded type systems

We give an adequate denotational semantics for languages with recursive
higher-order types, continuous probability distributions, and soft constraints.
These are expressive languages for building Bayesian models of the kinds used
in computational statistics and machine learning. Among them are untyped
languages, similar to Church and WebPPL, because our semantics allows recursive
mixed-variance datatypes. Our semantics justifies important program
equivalences including commutativity.
Our new semantic model is based on `quasi-Borel predomains'. These are a
mixture of chain-complete partial orders (cpos) and quasi-Borel spaces.
Quasi-Borel spaces are a recent model of probability theory that focuses on
sets of admissible random elements. Probability is traditionally treated in cpo
models using probabilistic powerdomains, but these are not known to be
commutative on any class of cpos with higher order functions. By contrast,
quasi-Borel predomains do support both a commutative probabilistic powerdomain
and higher-order functions. As we show, quasi-Borel predomains form both a
model of Fiore's axiomatic domain theory and a model of Kock's synthetic
measure theory.

本文为具有递归高阶类型、连续概率分布和软约束的语言提供了充分的指称语义，以建立计算统计和机器学习中使用的贝叶斯模型，其中包括类似于 Church 和 WebPPL 的无类型语言，因为我们的语义允许递归混合方差数据类型，并建立在 “拟 - 波雷尔代数” 之上，这些代数是链完整部分序列 (cpos) 和拟 - 波雷尔空间的混合。

统计概率编程的领域理论

A Domain Theory for Statistical Probabilistic Programming

In this paper we provide an alternative semantics for Equilibrium Logic and
its monotonic basis, the logic of Here-and-There (also known as G\"odel's G3
logic) that relies on the idea of "denotation" of a formula, that is, a
function that collects the set of models of that formula. Using the
three-valued logic G3 as a starting point and an ordering relation (for which
equilibrium/stable models are minimal elements) we provide several elementary
operations for sets of interpretations. By analysing structural properties of
the denotation of formulas, we show some expressiveness results for G3 such as,
for instance, that conjunction is not expressible in terms of the other
connectives. Moreover, the denotational semantics allows us to capture the set
of equilibrium models of a formula with a simple and compact set expression. We
also use this semantics to provide several formal definitions for entailment
relations that are usual in the literature, and further introduce a new one
called "strong entailment". We say that $\alpha$ strongly entails $\beta$ when
the equilibrium models of $\alpha \wedge \gamma$ are also equilibrium models of
$\beta \wedge \gamma$ for any context $\gamma$. We also provide a
characterisation of strong entailment in terms of the denotational semantics,
and give an example of a sufficient condition that can be applied in some
cases.

该论文提供了 Equilibrium Logic 和它的基础 Here-and-There Logic 的另一种语义学方法，并利用公式的 denotation 函数分析了 G3 的结构特性，展示了它的表现力和强蕴含量的定义，提出了一种简单的 compact set expression 来捕捉公式的 Equilibrium 模型集合。