As a consequence, the semantics of DC and differ in the absence of continuous random variables, while is a strict generalization of (<ref>).

An early attempt of equipping a probabilistic logic programming language with continuous random variables can be found in [Islam et al., 2012], which was dubbed .
Similar to , 's semantics are based again on [Sato, 1995]'s distribution semantics.
However, assumes, just like , pairwise mutually exclusive proofs (we refer again to Appendix <ref> for details on this).
On the expressivity side, only supports linear equalities – in contrast to , where also inequalities are included in the semantics of the language (<ref>).
An advantage of restricting possible constraints to equalities is the possibility of performing exact symbolic inference. In this regard, , together with its symbolic inference algorithm, can be viewed as a logic programming language that has access to a computer algebra system. Swapping out the approximate Sampo-inspired inference algorithm in by an exact inference algorithm using symbolic expression manipulations would result in an inference approach closely related to that of . One possibility would be to use the Symbo algorithm presented in [Zuidberg Dos Martires et al., 2019], which uses the PSI-language [Gehr et al., 2016] as its (probabilistic)  computer algebra system.

§.§ Probabilistic Constraint Logic Programming

Impressive work on extending probabilistic logic programs with continuous random variables was presented by Michels et al., 2015 with the introduction of Probabilistic Constraint Logic Programming (PCLP). The semantics of PCLP are again based on [Sato, 1995]'s distribution semantics and the authors also presented an approximate inference algorithm for hybrid probabilistic logic programs.
Interestingly, the algorithm presented in [Michels et al., 2015] to perform (conditional) probabilistic inference extends weighted model counting to continuous random variables using imprecise probabilities, and more specifically credal sets.

A shortcoming of PCLP's semantics is the lack of direct support for generative definitions of random variables, , random variables can only be interpreted within constraints, but not within distributions of other random variables as is possible in (<ref>).
Azzolini et al., 2021 define a non-credal version of this semantics using a product measure over a space that explicitly separates discrete and continuous random variables, assuming that a measure over the latter is given as part of the input without further discussion of how this part of the measure is specified in a program. Furthermore, they do not define any inference tasks (<ref>), computing conditional probabilities (Section <ref>), nor
do they provide an inference algorithm (<ref>).

A later proposal for the syntax of such programs [Azzolini and Riguzzi, 2021] combines two classes of terms (logical and continuous ones) with typed predicates and functors, and defines mixture variables as well as arithmetic expressions over random variables through logical clauses. In other words, user-defined predicates define families of random variables through the use of typed arguments of the predicate identifying a specific random variable, arguments providing parameters for the distribution, and one argument representing the random variable itself.
In contrast, the syntax of clearly identifies all  random variables through explicit terms introduced through distributional facts or distributional clauses, explicitly exposes the probabilistic dependency structure by using random variable terms inside distribution terms, and avoids typing through argument positions.
Moreover, takes a uniform view on all random variables in terms of semantics, thereby avoiding treating discrete and continuous random variables separately (<ref>).

Notable in the domain of probabilistic logic programming is also the BLOG language [Milch et al., 2005, Wu et al., 2018]. Contrary to the aforementioned probabilistic logic programming languages, BLOG's semantics are not specified using [Sato, 1995]'s distribution semantics but via so-called measure-theoretic Bayesian networks (MTBN), which were introduced in [Wu et al., 2018]. MTBNs can be regarded as the assembly language for BLOG: every BLOG program is translated or compiled to an MTBN.
With we follow a similar pattern: every program with syntactic sugar (annotated disjunctions)  is transformed into program. The semantics are defined on the bare-bones program. Note that the assembly language for () is Turing complete. This is not the case for MTBNs (<ref>).

§.§ Non-logical Probabilistic Programming

As first pointed out by Russell, 2015 and later on elaborated upon by Kimmig and De Raedt, 2017, probabilistic programs fall either into the possible worlds semantics category or the probabilistic execution traces semantics category. The former is usually found in logic based languages, while the latter is the prevailing view in imperative and functional probabilistic languages.

While, the probabilistic programming languages discussed so far follow the possible worlds paradigm,
many languages follow the execution traces paradigm, either as a probabilistic functional language [Goodman et al., 2008, Wood et al., 2014] or as a imperative probabilistic language [Gehr et al., 2016, Salvatier et al., 2016, Carpenter et al., 2017, Bingham et al., 2019, Ge et al., 2018]. Generally speaking, functional and imperative probabilistic programming languages target first and foremost continuous random variables, and discrete random variables are only added as an afterthought. A notable exception is the functional probabilistic programming language Dice [Holtzen et al., 2020], which targets discrete random variables exclusively.

Concerning inference in probabilistic programming, we can observe general trends in logical and non-logical probabilistic languages. While the latter are interested in adapting and speeding up approximate inference algorithms, such as Markov chain Monte Carlo sampling schemes or variational inference, the former type of languages are more invested in exploiting independences in the probabilistic programs, mainly by means of knowledge compilation. Clearly, these trends are not strict. For instance, Obermeyer et al., 2019 proposed so-called funsors to express and exploit independences in  [Bingham et al., 2019], an imperative probabilistic programming language, and Gehr et al., 2016 developed a computer algebra system to perform exact symbolic probabilistic inference.

§.§ Representation of Probabilistic Programs at Inference Time

Lastly, we would like to point out a key feature of the IALW inference algorithm that sets it apart from any other inference scheme for probabilistic programming in the hybrid domain. But first, let us briefly talk about computing probabilities in probabilistic programming. Roughly speaking, probabilities are computed summing and multiplying weights. These can for example be represented as floating point numbers or symbolic expressions. The collection of all operations that were performed to obtain the probability of a query to a program is called the computation graph. Now, the big difference between IALW and other inference algorithms lies in the structure of the computation graph. IALW represents the computation graph as a directed acyclic graph (DAG), while all other languages, except some purely discrete languages [Fierens et al., 2015, Holtzen et al., 2020], use a tree representation. IALW is the first inference algorithm in the discrete-continuous domain that uses DAGs (<ref>)! In cases where the computation graph can be represented as a DAG the size of the representation might be exponentially smaller compared to tree representations, which leads to faster inference times.

Note that Gutmann et al., 2010 and more recently Saad et al., 2021 presented implementations of hybrid languages where the inference algorithm leverages directed acyclic graphs, as well. However, the constraints that may be imposed on random variables are limited to univariate equalities and inequalities. In the weighted model integration literature it was shown that such probability computations can be mapped to probability computations of discrete random variables only [Zeng and Van den Broeck, 2020].

§ CONCLUSIONS

We introduced , a hybrid PLP language for the discrete-continuous domain and its accompanying hybrid distribution semantics.
strictly extends the discrete language [De Raedt et al., 2007, Fierens et al., 2015] and the negation-free  [Gutmann et al., 2011] language.
In designing the language and its semantics we adapted  Poole, 2010's design principle of percolating probabilistic logic programs into two separate layers: the random variables and the logic program.

Boolean comparison atoms then form the  link between the two layers.
It is this clear separation between the random variables and the logic program that has allowed us to use simpler language constructs and to write programs using a  more concise and intuitive syntax than alternative hybrid PLP approaches [Gutmann et al., 2010, Nitti et al., 2016, Speichert and Belle, 2019, Azzolini et al., 2021].

Separating random variables from the logic program also allowed us to develop the IALW algorithm to perform inference in the hybrid domain.
IALW is the first algorithm based on knowledge compilation and algebraic model counting for hybrid probabilistic programming languages
and as such it generalizes the standard knowledge compilation based approach for PLP.
It is noteworthy that IALW correctly computes conditional probabilities in the discrete-continuous domain using the newly introduced infinitesimal numbers semiring.

Interesting future research directions include adapting ideas from functional probabilistic programming (the other declarative programming style besides logic programming) in the context of probabilistic logic programming. For instance, extending with a type system [Schrijvers et al., 2008] or investigating more recent advances, such as quasi-Borel spaces [Heunen et al., 2017] in the context of the distribution semantics.

§ ACKNOWLEDGEMENT

This research received funding from the Wallenberg AI, Autonomous Systems and Software Program (WASP) of the Knut and Alice Wallenberg Foundation, the Flemish Government (AI Research Program),
the KU Leuven Research Fund, the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No [694980] SYNTH: Synthesising Inductive Data Models), and
the Research Foundation - Flanders.

[Azzolini and Riguzzi, 2021]
Damiano Azzolini and Fabrizio Riguzzi.
Syntactic requirements for well-defined hybrid probabilistic logic
In Technical communications of ICLP 2021, 2021.

[Azzolini et al., 2021]
Damiano Azzolini, Fabrizio Riguzzi, and Evelina Lamma.
A semantics for hybrid probabilistic logic programs with function
Artificial Intelligence, 294, 2021.

[Bellman, 1957]
Richard Bellman.
Dynamic Programming.
Princeton University Press, 1957.

[Bingham et al., 2019]
Eli Bingham, Jonathan P. Chen, Martin Jankowiak, Fritz Obermeyer, Neeraj
Pradhan, Theofanis Karaletsos, Rohit Singh, Paul A. Szerlip, Paul Horsfall,
and Noah D. Goodman.
Pyro: Deep universal probabilistic programming.
J. Mach. Learn. Res., 20:0 28:1–28:6, 2019.
URL <http://jmlr.org/papers/v20/18-403.html>.

[Carpenter et al., 2017]
Bob Carpenter, Andrew Gelman, Matthew D Hoffman, Daniel Lee, Ben Goodrich,
Michael Betancourt, Marcus Brubaker, Jiqiang Guo, Peter Li, and Allen
Stan: A probabilistic programming language.
Journal of statistical software, 760 (1), 2017.

[Casella and Robert, 1998]
George Casella and Christian P Robert.
Post-processing accept-reject samples: recycling and rescaling.
Journal of Computational and Graphical Statistics, 70
(2):0 139–157, 1998.

[Cherchago et al., 2007]
Natalia Cherchago, Pascal Hitzler, and Steffen Hölldobler.
Decidability under the well-founded semantics.
In International Conference on Web Reasoning and Rule Systems,
pages 269–278. Springer, 2007.

[Darwiche, 2001]
Adnan Darwiche.
On the tractable counting of theory models application to truth
maintenance and belief revision.
Journal of Applied Non-Classical Logics, 2001.

[Darwiche and Marquis, 2002]
Adnan Darwiche and Pierre Marquis.
A knowledge compilation map.
Journal of Artificial Intelligence Research, 17:0
229–264, 2002.

[De Raedt and Kimmig, 2015]
Luc De Raedt and Angelika Kimmig.
Probabilistic (logic) programming concepts.
Machine Learning, 1000 (1):0 5–47, 2015.

[De Raedt et al., 2007]
Luc De Raedt, Angelika Kimmig, and Hannu Toivonen.
Problog: A probabilistic prolog and its application in link
In IJCAI, volume 7, pages 2462–2467. Hyderabad, 2007.

[De Raedt et al., 2016]
Luc De Raedt, Kristian Kersting, Sriraam Natarajan, and David Poole.
Statistical Relational Artificial Intelligence: Logic,
Probability, and Computation.
Synthesis Lectures on Artificial Intelligence and Machine Learning.
Morgan & Claypool Publishers, 2016.

[Fierens et al., 2015]
Daan Fierens, Guy Van den Broeck, Joris Renkens, Dimitar Shterionov, Bernd
Gutmann, Ingo Thon, Gerda Janssens, and Luc De Raedt.
Inference and learning in probabilistic logic programs using weighted
boolean formulas.
Theory and Practice of Logic Programming, 150
(3):0 358–401, 2015.

[Fung and Chang, 1990]
Robert Fung and Kuo-Chu Chang.
Weighing and integrating evidence for stochastic simulation in
bayesian networks.
Machine Intelligence and Pattern Recognition, 10:0
209–219, 1990.

[Ge et al., 2018]
Hong Ge, Kai Xu, and Zoubin Ghahramani.
Turing: A language for flexible probabilistic inference.
In International Conference on Artificial Intelligence and
Statistics, pages 1682–1690, 2018.

[Gehr et al., 2016]
Timon Gehr, Sasa Misailovic, and Martin Vechev.
PSI: Exact symbolic inference for probabilistic programs.
In International Conference on Computer Aided Verification.
Springer, 2016.

[Goodman et al., 2008]
Noah D Goodman, Vikash K Mansinghka, Daniel Roy, Keith Bonawitz, and Joshua B
Church: a language for generative models.
In Proceedings of the Twenty-Fourth Conference on Uncertainty
in Artificial Intelligence, pages 220–229, 2008.

[Gutmann et al., 2010]
Bernd Gutmann, Manfred Jaeger, and Luc De Raedt.
Extending problog with continuous distributions.
In International Conference on Inductive Logic Programming.
Springer, 2010.

[Gutmann et al., 2011]
Bernd Gutmann, Ingo Thon, Angelika Kimmig, Maurice Bruynooghe, and Luc
De Raedt.
The magic of logical inference in probabilistic programming.
Theory and Practice of Logic Programming, 110
(4-5):0 663–680, 2011.

[Heunen et al., 2017]
Chris Heunen, Ohad Kammar, Sam Staton, and Hongseok Yang.
A convenient category for higher-order probability theory.
In 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer
Science (LICS), pages 1–12. IEEE, 2017.

[Holtzen et al., 2020]
Steven Holtzen, Guy Van den Broeck, and Todd Millstein.
Dice: Compiling discrete probabilistic programs for scalable
arXiv preprint arXiv:2005.09089, 2020.

[Islam et al., 2012]
Muhammad Asiful Islam, CR Ramakrishnan, and IV Ramakrishnan.
Inference in probabilistic logic programs with continuous random
Theory and Practice of Logic Programming, 120
(4-5):0 505–523, 2012.

[Iverson, 1962]
Kenneth E Iverson.
A programming language.
In Proceedings of the May 1-3, 1962, spring joint computer
conference, 1962.

[Jacobs, 2021]
Jules Jacobs.
Paradoxes of probabilistic programming: And how to condition on
events of measure zero with infinitesimal probabilities.
Proceedings of the ACM on Programming Languages, 50
(POPL):0 1–26, 2021.

[Janhunen, 2004]
Tomi Janhunen.
Representing normal programs with clauses.
In Proceedings of the 16th European Conference on Artificial
Intelligence, pages 358–362, 2004.

[Jaynes, 2003]
Edwin T Jaynes.
Probability theory: The logic of science.
Cambridge university press, 2003.

[Kadane, 2011]
Joseph B Kadane.
Principles of uncertainty.
CRC Press, 2011.

[Kahn, 1950]
Herman Kahn.
Random sampling (monte carlo) techniques in neutron attenuation
problems. i.
Nucleonics (US) Ceased publication, 60 (See also NSA
3-990), 1950.

[Kersting and De Raedt, 2000]
Kristian Kersting and Luc De Raedt.
Bayesian logic programs.
In Proceedings of the 10th International Conference on
Inductive Logic Programming, Work-in-progress reports, pages 1–18, 2000.

[Kimmig and De Raedt, 2017]
Angelika Kimmig and Luc De Raedt.
Probabilistic logic programs: Unifying program trace and possible
world semantics.
In Workshop on probabilistic programming semantics, 2017.

[Kimmig et al., 2017]
Angelika Kimmig, Guy Van den Broeck, and Luc De Raedt.
Algebraic model counting.
Journal of Applied Logic, 2017.

[Kloek and Van Dijk, 1978]
Tuen Kloek and Herman K Van Dijk.
Bayesian estimates of equation system parameters: an application of
integration by monte carlo.
Econometrica: Journal of the Econometric Society, pages 1–19,

[Kolb et al., 2019]
Samuel Kolb, Pedro Zuidberg Dos Martires, and Luc De Raedt.
How to exploit structure while solving weighted model integration
In Uncertainty in Artificial Intelligence, pages 744–754.
PMLR, 2019.

[Lloyd, 2012]
John W Lloyd.
Foundations of logic programming.
Springer Science & Business Media, 2012.

[Mansinghka et al., 2014]
Vikash Mansinghka, Daniel Selsam, and Yura Perov.
Venture: a higher-order probabilistic programming platform with
programmable inference.
arXiv preprint arXiv:1404.0099, 2014.

[Mantadelis and Janssens, 2010]
Theofrastos Mantadelis and Gerda Janssens.
Dedicated tabling for a probabilistic setting.
In Technical Communications of the 26th International
Conference on Logic Programming, 2010.

[Michels et al., 2015]
Steffen Michels, Arjen Hommersom, Peter JF Lucas, and Marina Velikova.
A new probabilistic constraint logic programming language based on a
generalised distribution semantics.
Artificial Intelligence, 228:0 1–44, 2015.

[Milch et al., 2005]
Brian Milch, Bhaskara Marthi, Stuart Russell, David Sontag, Daniel L Ong, and
Andrey Kolobov.
Blog: Probabilistic models with unknown objects.
In 19th International Joint Conference on Artificial
Intelligence, IJCAI 2005, pages 1352–1359, 2005a.

[Milch et al., 2005]
Brian Milch, Bhaskara Marthi, David Sontag, Stuart Russell, Daniel L Ong, and
Andrey Kolobov.
Approximate inference for infinite contingent bayesian networks.
In International Workshop on Artificial Intelligence and
Statistics, pages 238–245. PMLR, 2005b.

[Milch, 2006]
Brian Christopher Milch.
Probabilistic Models with Unknown Objects.
PhD thesis, University of California, Berkeley, 2006.

[Nitti et al., 2016]
Davide Nitti, Tinne De Laet, and Luc De Raedt.
Probabilistic logic programming for hybrid relational domains.
Machine Learning, 1030 (3):0 407–449, 2016.

[Obermeyer et al., 2019]
Fritz Obermeyer, Eli Bingham, Martin Jankowiak, Du Phan, and Jonathan Chen.
Functional tensors for probabilistic programming.
arXiv:1910.10775, 2019.

[Poole, 1993]
David Poole.
Probabilistic horn abduction and bayesian networks.
Artificial intelligence, 640 (1):0 81–129,

[Poole, 2010]
David Poole.
Probabilistic programming languages: Independent choices and
deterministic systems.
Heuristics, probability and causality: A tribute to Judea
Pearl, pages 253–269, 2010.

[Riguzzi, 2018]
Fabrizio Riguzzi.
Foundations of Probabilistic Logic Programming.
River Publishers, 2018.

[Riguzzi and Swift, 2011]
Fabrizio Riguzzi and Terrance Swift.
The pita system: Tabling and answer subsumption for reasoning under
Theory and Practice of Logic Programming, 110
(4-5):0 433–449, 2011.

[Russell, 2015]
Stuart Russell.
Unifying logic and probability.
Communications of the ACM, 580 (7):0 88–97,

[Saad et al., 2021]
Feras A Saad, Martin C Rinard, and Vikash K Mansinghka.
Sppl: Probabilistic programming with fast exact symbolic inference.
In Conference on Programming Language Design and
Implementation, 2021.

[Salvatier et al., 2016]
John Salvatier, Thomas V Wiecki, and Christopher Fonnesbeck.
Probabilistic programming in python using pymc3.
PeerJ Computer Science, 2:0 e55, 2016.

[Sato, 1995]
Taisuke Sato.
A statistical learning method for logic programs with distribution
In In Proceedings of the 12th International Conference On Logic
Programming (ICLP’95. Citeseer, 1995.

[Sato and Kameya, 1997]
Taisuke Sato and Yoshitaka Kameya.
Prism: a language for symbolic-statistical modeling.
In IJCAI, volume 97, pages 1330–1339, 1997.

[Schrijvers et al., 2008]
Tom Schrijvers, Vítor Santos Costa, Jan Wielemaker, and Bart Demoen.
Towards typed prolog.
In ICLP, 2008.

[Shan and Ramsey, 2017]
Chung-chieh Shan and Norman Ramsey.
Exact Bayesian inference by symbolic disintegration.
In ACM SIGPLAN Notices, volume 52, pages 130–144. ACM, 2017.

[Speichert and Belle, 2019]
Stefanie Speichert and Vaishak Belle.
Learning probabilistic logic programs over continuous data.
In International Conference on Inductive Logic Programming,

[Staton et al., 2016]
Sam Staton, Frank Wood, Hongseok Yang, Chris Heunen, and Ohad Kammar.
Semantics for probabilistic programming: higher-order functions,
continuous distributions, and soft constraints.
In 2016 31st Annual ACM/IEEE Symposium on Logic in Computer
Science (LICS), pages 1–10. IEEE, 2016.

[Valiant, 1979]
Leslie G Valiant.
The complexity of computing the permanent.
Theoretical Computer Science, 1979.

[Van Gelder et al., 1991]
Allen Van Gelder, Kenneth A Ross, and John S Schlipf.
The well-founded semantics for general logic programs.
Journal of the ACM (JACM), 380 (3):0 619–649,

[Vennekens et al., 2004]
Joost Vennekens, Sofie Verbaeten, and Maurice Bruynooghe.
Logic programs with annotated disjunctions.
In International Conference on Logic Programming, pages
431–445. Springer, 2004.

[Vlasselaer et al., 2014]
Jonas Vlasselaer, Joris Renkens, Guy Van den Broeck, and Luc De Raedt.
Compiling probabilistic logic programs into sentential decision
In Proceedings Workshop on Probabilistic Logic Programming
(PLP), pages 1–10, 2014.

[Wood et al., 2014]
Frank Wood, Jan Willem van de Meent, and Vikash Mansinghka.
A new approach to probabilistic programming inference.
In Proceedings of the 17th International conference on
Artificial Intelligence and Statistics, pages 1024–1032, 2014.

[Wu et al., 2018]
Yi Wu, Siddharth Srivastava, Nicholas Hay, Simon Du, and Stuart Russell.
Discrete-continuous mixtures in probabilistic programming:
Generalized semantics and inference algorithms.
In International Conference on Machine Learning, pages
5339–5348, 2018.

[Zeng and Van den Broeck, 2020]
Zhe Zeng and Guy Van den Broeck.
Efficient search-based weighted model integration.
In Uncertainty in Artificial Intelligence, pages 175–185.
PMLR, 2020.

[Zuidberg Dos Martires, 2020]
Pedro Zuidberg Dos Martires.
From Atoms to Possible Worlds: Probabilistic Inference in the
Discrete-Continuous Domain.
KU Leuven, 2020.

[Zuidberg Dos Martires et al., 2019]
Pedro Zuidberg Dos Martires, Vincent Derkinderen, Robin Manhaeve, Wannes Meert,
Angelika Kimmig, and Luc De Raedt.
Transforming probabilistic programs into algebraic circuits for
inference and learning.
In Transformations for Machine Learning Workshop,

[Zuidberg Dos Martires et al., 2019]
Pedro Zuidberg Dos Martires, Anton Dries, and Luc De Raedt.
Exact and approximate weighted model integration with probability
density functions using knowledge compilation.
In Proceedings of the AAAI Conference on Artificial
Intelligence, volume 33, pages 7825–7833, 2019b.

§ LOGIC PROGRAMMING

We briefly summarize key concepts of the syntax and semantics of logic programming; for a full introduction, we refer to [Lloyd, 2012].

§.§ Building Blocks

The basic building blocks of logic programs are variables (denoted by strings starting with upper case letters), constants, functors and
predicates (all denoted by strings starting with lower case letters).  A term is a variable, a constant, or a functor
$f$ of arity $n$ followed by $n$ terms $t_i$, ,
An atom is a predicate $p$ of arity $n$ followed by $n$ terms $t_i$, ,
$p(t_1,\dots,t_n)$. A predicate $p$ of arity $n$ is also written as pn. A literal is an
atom or a negated atom $ not(p(t_1,\dots,t_n))$.

§.§ Logic Programs

A definite clause is a universally quantified expression of the form $h
\lpif b_1, \dots, b_n$ where $h$ and the $b_i$ are atoms.
$h$ is called the head of the clause, and $b_1, \dots, b_n$ its
body. Informally, the meaning of such a clause is that if all
the $b_i$ are true, $h$ has to be true as well.
A normal clause  is a universally quantified expression of the form $h
\lpif l_1, \dots, l_n$ where $h$ is an atom and the $l_i$ are
If $n=0$, a clause is called fact and simply written
as $h$.
A definite clause program or logic program for
short is a finite set of definite clauses. A normal logic
program is a finite set of normal clauses.

§.§ Substitutions

A substitution $\theta$ is an expression of the form
$\{V_1/t_1,\dots,V_m/t_m\}$ where the $V_i$ are different variables and
the $t_i$ are terms. Applying a substitution $\theta$ to an expression
$e$ (term or clause) yields the instantiated expression $e\theta$
where all variables $V_i$ in $e$ have been simultaneously replaced by
their corresponding terms $t_i$ in $\theta$. If an expression does not
contain variables it is ground. Two expressions $e_1$ and $e_2$ can be unified if and only if there are substitutions $\theta_1$ and $\theta_2$ such that $e_1\theta_1 = e_2\theta_2$.

§.§ Herbrand Universe

The Herbrand universe of a logic program is the set of ground terms that can be constructed using the functors and constants occurring in the program.

The Herbrand base of a logic program is the set of ground atoms that can be constructed from the predicates in the program and the terms in its Herbrand universe.
A truth value assignment to all atoms in the
Herbrand base is called Herbrand interpretation, and is also represented as the set of atoms that are true according to the assignment.
A Herbrand interpretation is a model of a clause $h \lpif b_1,\ldots ,b_n\ldotp$ if for every substitution $\theta$ such that all $b_i\theta$ are in the interpretation, $h\theta$ is in the interpretation as well. It is a model of a logic program if it is a model of all clauses in the program. The model-theoretic semantics of a definite clause program is given by its smallest Herbrand model with respect to set inclusion, the so-called least Herbrand model (which is unique). We say that a logic program $\dcpprogram$ entails an atom $a$, denoted $\dcpprogram\models a$, if and only if $a$ is true in the least Herbrand model of $\dcpprogram$.

§ TABLE OF NOTATIONS

symbol     meaning     for details, see
$\distributionfunctors$      set of distribution functors      Definition <ref>

$\arithmeticfunctors$        set of arithmetic functors     Definition <ref>

$\comparisonpredicates$        set of comparison  predicates     Definition <ref>

$\samplespace_\nu$     sample space of random variable $\nu$     Definition <ref>

$\samplefunction(\cdot)$     value assignment function     Definition <ref>

$\distdb$     distributional database     Definition <ref>

$\randomvariableset$     set of random variables     Definition <ref>

$\measurerandomvariableset$     probability measure over $\randomvariableset$ defined by $\distdb$     Proposition <ref>

$\comparisonfacts$     set of Boolean comparison atoms     Definition <ref>

$\measurecomparisonfacts$     probability measure over interpretations of $\comparisonfacts$ induced by $\measurerandomvariableset$     Proposition <ref>

$\dfprogram=\distdb  \cup \logicprogram$     program     Definition <ref>

$\comparisonfacts_{\samplefunction(\randomvariableset)}$     consistent comparison database induced by $\samplefunction$ on the random variables in $\randomvariableset$     Definition <ref>

$\probabilitymeasure_\dfprogram$     probability measure over Herbrand interpretations defined by $\dfprogram$     Proposition <ref>

$\program$      program     Definition <ref>

AD-free program     Definition <ref>

$\headsdc_\adfreeprogram$     set of heads of distributional clauses in     Definition <ref>

$\randomtermset_\adfreeprogram$     random terms in $\headsdc _\adfreeprogram$     Definition <ref>

$\dclauses_{\adfreeprogram}$     set of distributional clauses in $\adfreeprogram$     Definition <ref>

$\contextfunc(\cdot)$      contextualization function     Definition <ref>

$\dfadfreeprogram$      program providing the semantics of $\adfreeprogram$     Definition <ref>

$MOD(\dcpprogram)$     models of a program $\dcpprogram$     Theorem <ref>

$ENUM(\phi)$     models of a propositional formula $\phi$     Theorem <ref>

$\alpha(\cdot)$     labeling function of a propositional literal     Definition <ref>

$\ive{\cdot}$     Iverson bracket denoting an indicator function     Definition <ref>

$\E[\cdot]$     expected value     Theorem <ref>

$\mathbb{I}$     set of infinitesimal numbers     Equation <ref>

$\mathcal{S}$     set of ancestral samples     Equation <ref>

§ PROOFS OF PROPOSITIONS IN SECTION <REF>

§.§ Proof of Proposition <ref>

The proof is analogous to that for the semantics of well-defined Bayesian Logic Programs (BLPs) <cit.>. They show that such a probability measure exists over a non-empty set of random variables if the ancestor structure of the random variables is acyclic and every random variable has a finite set of ancestors, which are exactly  conditions W2 and W1 in Definition <ref>. The key idea is that under these conditions,
for each finite subset of random variables closed under the ancestor relation, the joint distribution on that set has the form of a Bayesian network, and factorizes into the product of the individual variables' distributions.
This family of distributions forms the basis of the unique measure over the potentially infinite set $\randomvariableset$. We refer to <cit.> for  technical details.

Note that while BLPs also use LP syntax to define the random variables and structure of a Bayesian network, the way they use that syntax is fundamentally different from ours.

§.§ Proof of Proposition <ref>

To show existence of the  measure $\measurecomparisonfacts$ (i.e. the basic distribution),
we fix an arbitrary enumeration  $\mu_1$, $\mu_2$, …, of the atoms in $\comparisonfacts$.
Each $\mu_i$ depends on a finite set $\randomvariableset_i\subseteq \randomvariableset$ of random variables, namely  those mentioned in $\mu_i$, as well as their ancestor sets. We write $\randomvariableset_{\leq n}=\bigcup_{1\leq j\leq n} \randomvariableset_j $ for the union of random variables that the first $n$ atoms in the enumeration depend on. By $\probabilitymeasure_{\randomvariableset_{\leq n}}$ we denote the measure restricted to this set.

By definition, all queries $\mu_i\in \comparisonfacts$ are  Lebesgue-measurable, and we thus get a family of distributions

\begin{align}
\measurecomparisonfacts^{(n)}(\mu_1=\boolval_1,\ldots,\mu_n=\boolval_n) = \int_{\samplespace(\randomvariableset_{\leq n})} \mathbf{1}_{[\mu_1=\boolval_1\wedge\ldots\wedge \mu_n=\boolval_n]}(\samplefunction(\randomvariableset_{\leq n})) \differential{\probabilitymeasure_{\randomvariableset_{\leq n}}}
\end{align}

where the $\boolval_i$ belong to the set  $\{ \bot, \top\}$, $\probabilitymeasure_{\randomvariableset_{\leq n}}$ factorizes over the random variables in $\randomvariableset_{\leq n}$, $\samplespace(\randomvariableset_{\leq n})$ denotes the space of possible assignments for variables in $\randomvariableset_{\leq n}$, and $\mathbf{1}_{[\varphi]}$ is the indicator function, , equals $1$ if $\varphi$ is true and $0$ otherwise. The definition in terms of an indicator function and the measurability of the underlying Boolean queries ensures that this family of distributions is of the form required for the distribution semantics, they are well-defined probability distributions satisfying the compatibility condition: $\measurecomparisonfacts^{(n)}$ can be obtained from $\measurecomparisonfacts^{(n+1)}$ by summing out $\mu_{n+1}$. There thus exists a completely additive probability measure $\measurecomparisonfacts$ over the space of truth value assignments to $\comparisonfacts$ such that for any $n$, we have

\begin{align}
\measurecomparisonfacts(\mu_1=\boolval_1,\ldots,\mu_n=\boolval_n) =\measurecomparisonfacts^{(n)}(\mu_1=\boolval_1,\ldots,\mu_n=\boolval_n)
\end{align}

§.§ Proof of Proposition <ref>

To show this, we consider two cases.
If $\distdb$ is empty, does not define any random variables,  the semantics of is the well-founded model of $\logicprogram$. Thus, normal logic programs (with total well-founded models) are a special case of .

If $\distdb$ is not empty, we follow Sato's construction to obtain the probability measure $\probabilitymeasure_\dfprogram$ over Herbrand interpretations from $\measurecomparisonfacts$. To do so, we fix an enumeration $\mu_1,\mu_2,\ldots$ of all atoms in the Herbrand base, which includes those in $\comparisonfacts$.
As is valid, for every consistent comparison database $\comparisonfacts_{\samplefunction(\randomvariableset)}$ (Definition <ref>), the logic program
$\comparisonfacts_{\samplefunction(\randomvariableset)}\cup \logicprogram$
has a total well-founded model $M_{\samplefunction(\randomvariableset)}$, and we can thus define

\begin{align}
\probabilitymeasure_\dfprogram^{(n)}(\mu_1=\boolval_1,\ldots,\mu_n=\boolval_n) := \measurecomparisonfacts(\{\comparisonfacts_{\samplefunction}~|~ M_{\samplefunction(\randomvariableset)}\models \mu_1^{\boolval_1}\wedge\ldots\wedge \mu_n^{\boolval_n}\})
\end{align}

where, $b_i\in \{\bot,\top \}$, $\mu_i^1=\mu_i$, and $\mu_i^0=\neg \mu_i$. It follows again that there is a completely additive probability measure $\probabilitymeasure_\dfprogram$ over Herbrand interpretations.

§ BEYOND MIXTURES

By definition, we impose on distributional clauses mutual exclusivity of their bodies when they share a random term (Definition <ref>). That is, if we have a set of distributional clauses: $\{ \tau \sim \delta_i\lpif \beta_1 \dots, \tau \sim \delta_n\lpif \beta_n  \}$ we impose that the conjunction of two distinct bodies $\beta_i$ and $\beta_j$ ($i \neq j$) is false.

A further condition that we might impose, which is, however, not necessary to define a valid distributional clause, is exhaustiveness. Let us consider again the set of distributional clauses  $\{ \tau \sim \delta_i\lpif \beta_1 \dots, \tau \sim \delta_n\lpif \beta_n  \}$. We call this set exhaustive if the disjunction of all the $\beta_i$'s is equivalent to true.

A set of exhaustive distributional clauses can be interpreted as a mixture models as they assign a unique distribution to the random term in any possible context. When, the bodies of such distributional clauses are not exhaustive, however, they may
interact with the logic program in rather subtle ways, especially if negation is involved. We demonstrate this in the examples below.

Consider the  following program fragments

q :- not (x=:=1).

aux :- x=:=1.
q :- not aux.

and now assume x follows a mixture distribution, ,

x flip(0.5) :- b.
x flip(0.9) :- not b.

With such a mixture model, as in the case of a distributional fact, "x has an associated distribution" is always true, and both fragments agree on the truth value of q.

In general, however, only the first of these two conditions is necessary, and it is thus possible to  associate a distribution with a random term in some contexts only.

Consider again the two program fragments above with the following non-exhaustive definition of x:

x flip(0.5) :- b.

With this definition, "x has an associated distribution" is true if and only if b is true, and the two fragments therefore no longer agree on the truth values of q, as we more easily see after eliminating the distributional clause. We omit the transformation of the probabilistic fact for brevity. The fragment defining x transforms to

v1 flip(0.5).
rv(x,v1) :- b.

The first program fragment maps to

q :- rv(x,v1), not (v1=:=1).

and the second one to

aux :- rv(x,v1), v1=:=1.
q :- not aux.

which clearly exposes the difference in how the negation is interpreted.

As this example illustrates, if random variables are defined through non-exhaustive sets of DCs, we can no longer refactor the logic program independently of the definition of the random variables in general, as it interacts with the context structure. The reason is that 's declarative semantics builds upon the principle that the distributional database is declared independently of the logic program, and can thus be combined modularly and declaratively with any logic program over its comparison atoms. This is no longer the case with such arbitrary sets of DCs, which intertwine the definition of the two parts of a program. We note that this differs from the procedural view on the existence of random variables taken in the language [Nitti et al., 2016], as we
discuss in more detail in Appendix <ref>.

§ RELATION TO THE DC LANGUAGE

Distributional clauses were first introduced in the language of the same name  by [Gutmann et al., 2011], which at that point did not support negation. For negation-free programs, our interpretation of distributional clauses exactly corresponds to theirs, and thus generalizes both ProbLog (with negation) and the original (definite) distributional clause language.

In the following, we first discuss how the semantics of differs from [Nitti et al., 2016]'s procedural view on negated comparison atoms, and then how 's acyclicity conditions imposed on valid programs differ from those of [Gutmann et al., 2011].

§.§ Non-exhaustive sets of DCs

[Nitti et al., 2016]  have extended the procedural view of the stochastic $T_P$ operator to locally stratified programs with negation under the perfect models semantics.[Local stratification is a necessary condition for perfect models semantics, and a sufficient one for well-founded semantics. On this class of programs, both semantics agree [Van Gelder et al., 1991]] In their view, a distributional clause x d :- body is informally interpreted  as "if body is true, define a random variable x with distribution d". They then use the principle that "any comparison involving a non-defined variable will fail; therefore, its negation will succeed", , they apply negation as failure to comparison atoms.
In contrast, as already illustrated in Section <ref>, we take a purely declarative view here, where all random variables are defined up front, independently of logical reasoning, and distributional clauses serve as syntactic sugar to compactly talk about a group of random variables. Then, truth values of comparison atoms are fully determined by their external interpretation, and do not involve reasoning about whether a random variable is defined or not. That is, we apply classical negation to comparison atoms, and restrict negation as failure to atoms defined by the logic program itself.

The following example adapted from [Nitti et al., 2016] illustrates the difference.

Consider the following program about the color of certain objects, where the number of objects is given by the random variable n:

n   uniform([1,2,3]).
color(1)   uniform([red,green,blue]) :- 1=<n .
color(2)   uniform([red,green,blue]) :- 2=<n .
color(3)   uniform([red,green,blue]) :- 3=<n .
not_red :- not color(2)=:=red .
not_red_either :- color(2)=r̄ed.

The semantics is given by the transformed program:

v0   uniform([1,2,3]).
v1   uniform([red,green,blue]).
v2   uniform([red,green,blue]).
v3   uniform([red,green,blue]).

rv(color(1),v1) :- rv(n,v0), 1=<v0.
rv(color(2),v2) :- rv(n,v0), 2=<v0.
rv(color(3),v3) :- rv(n,v0), 3=<v0.

not_red :- rv(color(2),v2), not v2=:=red.
not_red_either :- rv(color(2),v2), v2=r̄ed.

If $\mathprobloginline{n}=1$ (i.e., $\mathprobloginline{v0}=1$), neither color(2) nor color(3) are associated with a distribution.  Thus, rv(color(2),v2) fails, and both not_red and not_red_either therefore fail as well, independently of the values of the comparison literals.
In contrast, under
the procedural semantics of [Nitti et al., 2016], color(2)=:=red fails in this case, and not_red thus succeeds. Similarly, color(2)=r̄ed fails, and  not_red_either thus fails.
Both views agree for $n>1$.

This example again illustrates that DC-ProbLog's semantics clearly follows the spirit of the distribution   semantics of defining a distribution over interpretations of basic facts (comparison atoms in this case) independently of the logic program rules.

We note that the expressive power of logic programs allows the programmer to explicitly model the procedural view of "failure through undefined variable" in the program if desired, as illustrated in the following example.

The following DC-ProbLog program is equivalent to the procedural interpretation of the program in  Example <ref>:
n   uniform([1,2,3]).
color(1)   uniform([red,green,blue]) :- 1=<n .
color(2)   uniform([red,green,blue]) :- 2=<n .
color(3)   uniform([red,green,blue]) :- 3=<n .
not_red :- not color(2)=:=red.
not_red :- not 2=<n.
not_red_either :- 2=<n, color(2)=r̄ed.

We explicitly model that not_red is true if either color(2) can be interpreted and color(2)=:=red is false (line 5, which is how interprets the first clause), or color(2) cannot be interpreted (line 6, negating the body of the DC in line 3). Similarly, not_red_either is true if and only if color(2) can be resolved and color(2)=r̄ed is true (line 7, repeating the body of the DC in line 3).

§.§ Program validity

To define valid programs, Gutmann et al., 2011 impose acyclicity criteria based on the structure of the clauses in the program, whereas we use the ancestor relation between random variables in . This means that accepts certain cycles in the logic program structure that are rejected by , as illustrated in the following example.

We model a scenario where a property of a node in a network is either initiated locally with probability $0.1$, or propagated from a neighboring node that has the property with probability $0.3$. We consider a two node network with directed edges from each of the nodes to the other one, and directly ground the program for this situation.

local(n1)   flip(0.1).
local(n2)   flip(0.1).
transmit(n1,n2)   flip(0.3) :- active(n1).
transmit(n2,n1)   flip(0.3) :- active(n2).
active(n1) :- local(n1)=:=1.
active(n2) :- local(n2)=:=1.
active(n1) :- transmit(n2,n1)=:=1.
active(n2) :- transmit(n1,n2)=:=1.

This program is not distribution-stratified based on [Gutmann et al., 2011], where in order to avoid cyclic probabilistic dependencies 1) DC heads have to be of strictly higher rank than any of their body atoms, 2) heads of regular clauses have to have at least the same rank as each body atom, and 3) atoms involving random terms have to have at least the same rank as the head of the DC introducing the random term. This is impossible with our program due to the cyclic dependency between active-atoms and transmit-random terms. The semantics, in contrast,  is clearly specified through the mapping:

x1   flip(0.1).
x2   flip(0.1).
x3   flip(0.3).
x4   flip(0.3).
rv(transmit(n1,n2),x3) :- active(n1).
rv(transmit(n2,n1),x4) :- active(n2).
active(n1) :- rv(local(n1),x1), x1=:=1.
active(n2) :- rv(local(n2),x2), x2=:=1.
active(n1) :- rv(transmit(n2,n1),x4), x4=:=1.
active(n2) :- rv(transmit(n1,n2),x3), x3=:=1.

We have four independent random variables, and a definite clause program whose meaning is well-defined despite of the cyclic dependencies between derived atoms. We can equivalently rewrite the logic program part to avoid deterministic auxiliaries:

x1   flip(0.1).
x2   flip(0.1).
x3   flip(0.3).
x4   flip(0.3).
active(n1) :- x1=:=1.
active(n2) :- x2=:=1.
active(n1) :- active(n2), x4=:=1.
active(n2) :- active(n1), x3=:=1.

Furthermore, agrees with the ProbLog formulation of the original program, ,

0.3::transmit_cause(n1,n2) :- active(n1).
0.3::transmit_cause(n2,n1) :- active(n2).
active(n1) :- local_cause(n1).
active(n2) :- local_cause(n2).
active(n1) :- transmit_cause(n2,n1).
active(n2) :- transmit_cause(n1,n2).

The AD-free program is

v1   flip(0.1).
local_cause(n1) :- v1=:=1.
v2   flip(0.1).
local_cause(n2) :- v2=:=1.
v3   flip(0.3).
transmit_cause(n1,n2) :- v3=:=1, active(n1).
v4   finite(0.3).
transmit_cause(n2,n1) :- v4=:=1, active(n2).
active(n1) :- local_cause(n1).
active(n2) :- local_cause(n2).
active(n1) :- transmit_cause(n2,n1).
active(n2) :- transmit_cause(n1,n2).

As this already is a program, we can skip the further rewrites. While the definite clauses are factored differently compared to the earlier variants, their meaning is the same.

§ PROOFS OF THEOREMS AND PROPOSITIONS IN SECTION <REF> AND SECTION <REF>

§.§ Proof of Theorem <ref>

The semantics of $\dcpprogram$ is given by the ground program that is obtained by first grounding $\dcpprogram$ with respect to its Herbrand base and reducing it to a program as specified in Section <ref>. The resulting program consists of distributional facts and ground normal clauses only, and includes clauses defining rv-atoms as well as calls to those atoms in clause bodies. However, as the definitions of these atoms are acyclic, and each ground instance is defined by a single rule (with the body of the DC that introduced the new random variable), we can eliminate all references to such atoms by recursively applying the well-known unfolding transformation, which replaces atoms in clause bodies by their definition. The result is an equivalent ground program using only predicates from , but where rule bodies have been expanded with the contexts of the random variables they interpret. We know from Theorem 1 in [Fierens et al., 2015] that for given query and evidence, it is sufficient to use the part of this logic program that is encountered during backward chaining from those atoms. We note that in our case, this also includes the distributional facts providing the distributions for relevant random variables, , random variables in relevant comparison atoms as well as their ancestors.

§.§ Proof of Theorem <ref>

The probability of a model $\varphi$ of the relevant ground program $\dcpprogram_g$ is, according to the distribution semantics (cf. Appendix <ref>), given by:

\begin{align}
P_{\dcpprogram_g}(\varphi) = \int \mathbf{1}_{[\mu_1=\boolval_1\wedge\ldots\wedge \mu_n=\boolval_n]}(\samplefunction(\randomvariableset)) \differential{\probabilitymeasure_{\randomvariableset}}
\end{align}

where the $\mu_i$ are the comparison atoms that appear (positively or negatively) in $\dcpprogram_g$ and the $b_i$ the truth values these atoms take in $\varphi$.
We can manipulate the probability into:

\begin{align}
\int \left( \prod_{i =1}^n \mathbf{1}_{[\mu_i=b_i]}(\samplefunction(\randomvariableset)) \right) \differential{\probabilitymeasure_{\randomvariableset}} \\
\int \left( \prod_{i: b_i=\bot} \mathbf{1}_{[\mu_i=b_i]}(\samplefunction(\randomvariableset)) \right)  \left( \prod_{i: b_i=\top} \mathbf{1}_{[\mu_i=b_i]}(\samplefunction(\randomvariableset)) \right)  \differential{\probabilitymeasure_{\randomvariableset}} \\
\int \left( \prod_{i: b_i=\bot} \ive{\neg c_i(vars(\mu_i))} \right)  \left( \prod_{i: b_i=\top}  \ive{ c_i(vars(\mu_i))}  \right)  \differential{\probabilitymeasure_{\randomvariableset}}
\label{eq:program_prob_label_equi}
\end{align}

Turning our attention now to the expected value of $\alpha(\varphi)$ we have:

\begin{align}
\E_{\randomvariableset \sim  \dcpprogram_g} [\alpha( \varphi )]
\int \alpha \left( \bigwedge_{\ell_i \in \varphi} \ell_i \right) \differential{P_\randomvariableset}
\int  \left( \prod_{\ell_i \in \varphi} \alpha \left(  \ell_i \right) \right)  \differential{P_\randomvariableset}
\end{align}

The literals $\ell_i \in \varphi$ fall into four groups: atoms whose predicate is a comparison and that are true in $\varphi$ (denoted by $CA^+(\varphi)$), non-comparison atoms that are true in $\varphi$ (denoted $NA^+(\varphi)$), and similarly the atoms that are false in $\varphi$ (denoted by $CA^-(\varphi)$ and $NA^-(\varphi)$). This yields:

\begin{align}
&\E_{\randomvariableset \sim  \dcpprogram_g} [\alpha( \varphi )]  \\
\int
\left( \prod_{\ell_i \in CA^+(\varphi)} \alpha (  \ell_i ) \right)
\left( \prod_{\ell_i \in CA^-(\varphi)} \alpha (  \neg \ell_i ) \right)
\left( \prod_{\ell_i \in NA^+(\varphi)} \alpha (  \ell_i ) \right)
\left( \prod_{\ell_i \in NA^-(\varphi)} \alpha (  \neg \ell_i ) \right)
\nonumber
\differential{P_\randomvariableset}
\end{align}

Plugging in the definition of the labeling function the last two products reduce to $1$ and we obtain for the remaining expression:

\begin{align}
\E_{\randomvariableset \sim  \dcpprogram_g} [\alpha( \varphi )]
\int
\left( \prod_{i: \ell_i \in CA^+(\varphi)} \ive{  c_i(vars(\ell_i)) } \right)
\left( \prod_{i: \ell_i \in CA^-(\varphi)} \ive{  \neg c_i(vars(\ell_i)) } \right)
\differential{P_\randomvariableset}
\label{eq:formula_prob_lable_equi}
\end{align}

Identifying now the set $\{ i: \ell_i \in CA^+(\varphi) \}$ with the set $\{i : \mu_i=\top   \} $ and the set  $\{ i: \ell_i \in CA^-(\varphi) \}$ with the set $\{i : \mu_i=\bot   \} $ proves the theorem, as this equates Equation <ref> and Equation <ref>

§.§ Proof of Proposition <ref>

First we write the conditional probability as a ratio of expected values invoking Theorem <ref>, on which we then use Defintion <ref>:

\begin{align}
P_\dcpprogram(\mu=q\mid\evidenceset = e)
&= \frac{\E_{\randomvariableset \sim  \dcpprogram_g} [\alpha( \phi \wedge \phi_q)] }{\E_{\randomvariableset \sim  \dcpprogram_g} [\alpha( \phi )] }
\\
\frac{
\E_{\randomvariableset \sim  \dcpprogram_g} \left[ \sum_{\varphi\in ENUM(\phi \land \phi_{q}) } \prod_{\ell \in \varphi} \alpha(\ell) \right]
\E_{\randomvariableset \sim  \dcpprogram_g} \left[ \sum_{\varphi\in ENUM(\phi) } \prod_{\ell \in \varphi} \alpha(\ell)  \right]
\\
\frac{
\E_{\randomvariableset \sim  \dcpprogram_g} \left[ \sum_{\varphi\in ENUM(\phi \land \phi_{q}) } \alpha(\varphi) \right]
\E_{\randomvariableset \sim  \dcpprogram_g} \left[ \sum_{\varphi\in ENUM(\phi) } \alpha(\varphi)  \right]
\end{align}

We can now express the conditional probability in terms of the sampled values $\mathcal{S}$:

\begin{align}
\frac{
\lim_{ \rightarrow \infty} \nicefrac{1}{\lvert \mathcal{S} \rvert} \sum_{i=1}^{\lvert \mathcal{S} \rvert}  \sum_{\varphi\in ENUM(\phi \land \phi{q}) } \alpha^{(i)}(\varphi)
\lim_{N\rightarrow \infty} \nicefrac{1}{\lvert \mathcal{S} \rvert} \sum_{i=1}^{\lvert \mathcal{S} \rvert} \sum_{\varphi\in ENUM(\phi) } \alpha^{(i)}(\varphi)
} \\
\frac{
\sum_{i=1}^{\lvert \mathcal{S} \rvert}  \sum_{\varphi\in ENUM(\phi \land \phi_{q}) } \alpha^{(i)}(\varphi)
\sum_{i=1}^{\lvert \mathcal{S} \rvert} \sum_{\varphi\in ENUM(\phi) } \alpha^{(i)}(\varphi)
}, & \quad \lvert \mathcal{S} \rvert<\infty \label{eq:mc_prob_cond}
\end{align}

§.§ Proof of Proposition <ref>

First we manipulate the expected value on the left hand side of Equation <ref>:

\begin{align}
&\E \left[ \sum_{\varphi \in ENUM(\phi)} \prod_{\ell \in \varphi}  \alpha \left(\ell \right) \bigg| \mathcal{S} \right]\\
\lim_{ \lvert \mathcal{S} \rvert\rightarrow\infty} \sum_{i=1}^{ \lvert \mathcal{S} \rvert}  \sum_{\varphi \in ENUM(\phi)} \prod_{\ell \in \varphi}  \alpha^{(i)} \left(\ell \right) \\
\lim_{ \lvert \mathcal{S} \rvert \rightarrow\infty} \sum_{i=1}^{ \lvert \mathcal{S} \rvert}  \sum_{\varphi \in ENUM(\phi)}
\left(\prod_{\ell \in \varphi \setminus DI(\varphi)}  \alpha^{(i)} \left(\ell \right) \prod_{\ell \in DI(\varphi)}  \alpha^{(i)} \left(\ell \right)   \right)
\end{align}

As the samples are ancestral samples, they satisfy by construction the delta invervals appearing in the second product. This means that $\prod_{\ell \in DI(\varphi)}  \alpha^{(i)} \left(\ell \right) =1$ and that we can write the expected value in function of non delta interval atoms only:

\begin{align}
\E \left[ \sum_{\varphi\in ENUM(\phi)} \prod_{\ell \in \varphi}  \alpha \left(\ell \right) \bigg| \mathcal{S} \right]
\E \left[ \underbrace{\sum_{\varphi\in ENUM(\phi)} \prod_{\ell \in \varphi \setminus DI(\varphi)}  \alpha \left(\ell \right)}_{\coloneqq f(\phi)} \bigg| \mathcal{S} \right]  \label{eq:ALW_exp_simplified}
\end{align}

Let us now manipulate the expression in the numerator on the right hand side of Equation <ref>:

\begin{align}
&\bigoplus_{i=1}^{ \lvert \mathcal{S} \rvert}  \bigoplus_{\varphi \in ENUM(\phi)} \bigotimes_{\ell \in \varphi}  \alpha_{IALW}^{(i)} \left(\ell \right)\\
\bigoplus_{i=1}^{ \lvert \mathcal{S} \rvert}  \bigoplus_{\varphi \in ENUM(\phi)}
\underbrace{\left(  \bigotimes_{\ell \in \varphi \setminus DI(\varphi)}  \alpha_{IALW}^{(i)} \left(\ell \right) \right) }_{\left( r_\varphi^{(i)} , 0  \right)}  \otimes
\underbrace{\left( \bigotimes_{\ell \in DI(\varphi)}  \alpha_{IALW}^{(i)} \left(\ell \right) \right) }_{\left( t_\varphi^{(i)} , m_\varphi^{(i)}  \right)} \label{eq:alw_proof_intermediate_1}
\end{align}

The expressions $\left( r_\varphi^{(i)} , 0  \right)$ and $\left( t_\varphi^{(i)} , m_\varphi^{(i)}  \right)$ denote infinitesimal numbers. Note how only the latter of the two picks up a non-zero second part.

From the definition of the addition of two infinitesimal numbers we can see that only those infinitesimal numbers with the smallest integer in the second part survive the addition. This also means that in Equation <ref> only those terms that have the smallest integer in their second part among all terms will contribute. We denote this smallest integer by:

\begin{align}
m^* =  \min_{ \substack{i\in \{ 1, \dots,  \lvert \mathcal{S} \rvert \} \\ \varphi\in ENUM(\phi) }} m^{(i)}_\varphi
\end{align}

We rewrite Equation <ref> in function of $m^*$:

\begin{align}
&\bigoplus_{i=1}^{ \lvert \mathcal{S} \rvert}  \bigoplus_{\varphi \in ENUM(\phi)}
\left(  \ive{m_{\varphi}^{(i)}{=} m^* } , 0  \right) \otimes
\left( r_\varphi^{(i)} , 0  \right) \otimes
\left( t_\varphi^{(i)} , m^*  \right) \\
\bigoplus_{i=1}^{ \lvert \mathcal{S} \rvert}  \bigoplus_{\varphi \in ENUM(\phi)}
\left( \ive{m_{\varphi}^{(i)}{=} m^* } r_\varphi^{(i)}  t_\varphi^{(i)} , 0  \right) \otimes \left( 1, m^* \right) \\
\left( \sum_{i=1}^{ \lvert \mathcal{S} \rvert}  \sum_{\varphi \in ENUM(\phi)}  \ive{m_{\varphi}^{(i)}{=} m^* } r_\varphi^{(i)}  t_\varphi^{(i)} , 0   \right)  \otimes \left( 1, m^* \right) \label{eq:ALW_num_simplified}
\end{align}

Similarly we get for the denominator in Equation <ref>:

\begin{align}
&\bigoplus_{i=1}^{ \lvert \mathcal{S} \rvert}  \bigoplus_{\varphi \in ENUM(\phi)} \bigotimes_{\ell \in  DI(\varphi)}  \alpha_{IALW}^{(i)} \left(\ell \right) \\
\left( \sum_{i=1}^{ \lvert \mathcal{S} \rvert}  \sum_{\varphi\in ENUM(\phi)}  \ive{m_{\varphi}^{(i)}{=} m^* }  t_\varphi^{(i)} , 0   \right)  \otimes \left( 1, m^* \right)  \label{eq:ALW_den_simplified}
\end{align}

We can now plug Equation <ref>, Equation <ref> and Equation <ref> back into Equation <ref> and obtain:

\begin{align}
&\phantom{{}\Leftrightarrow{}}  \left( \E \left[  f(\phi) | \mathcal{S} \right],  0 \right)
\left(
\frac
{ \sum_{i=1}^{ \lvert \mathcal{S} \rvert} \sum_{\varphi \in ENUM(\phi)}  \ive{m_{\varphi}^{(i)}{=} m^* } r_\varphi^{(i)}  t_\varphi^{(i)} }
{ \sum_{i=1}^{ \lvert \mathcal{S} \rvert}  \sum_{\varphi\in ENUM(\phi)}  \ive{m_{\varphi}^{(i)}{=} m^* }  t_\varphi^{(i)}   }
, 0
\right) \quad ( \lvert \mathcal{S} \rvert\rightarrow \infty) \\
&\Leftrightarrow \E \left[  f(\phi) | \mathcal{S} \right]
\frac
{ \sum_{i=1}^{ \lvert \mathcal{S} \rvert}  \sum_{\varphi \in ENUM(\phi)}  \ive{m_{\varphi}^{(i)}{=} m^* } r_\varphi^{(i)}  t_\varphi^{(i)} }
{ \sum_{i=1}^{ \lvert \mathcal{S} \rvert}  \sum_{\varphi\in ENUM(\phi)}  \ive{m_{\varphi}^{(i)}{=} m^* }  t_\varphi^{(i)}   } \label{eq:llw}
\end{align}

We realize that $r_\varphi^{(i)}$ is actually $f(\phi)$ evaluated at the $i$-th sample at the instantiation $\varphi$ and evoke <cit.> to prove Equation <ref>, which also finishes this proof.

§.§ Proof of Proposition <ref>

We start the proof by invoking Theorem <ref>, which expresses the conditional probability as a ratio of expectations. In the numerator and the denominator we then write the label of the propositional logic formulas as the sum of the labels of the respective possible worlds.

\begin{align}
P_\dcpprogram(\mu=q|\evidenceset=e)  \label{eq:cond_amc_1}
&=\frac{\E_{\randomvariableset \sim  \dcpprogram_g} [\alpha( \phi \wedge \phi_q)] }{\E_{\randomvariableset \sim  \dcpprogram_g} [\alpha( \phi )] } \\
\frac
\E_{\randomvariableset \sim  \dcpprogram_g} \left[ \sum_{\varphi\in ENUM(\phi \land \phi_{q e}) } \alpha(\varphi) \right]
\E_{\randomvariableset\sim  \dcpprogram_g} \left[ \sum_{\varphi\in ENUM(\phi) } \alpha(\varphi)  \right]
}  \label{eq:cond_amc_2}
\end{align}

Next, we approximate the expectation using a set of ancestral samples $\mathcal{S}$, followed by pulling out the query from the summation index in the numerator:

\begin{align}
\E_{\randomvariableset \sim  \dcpprogram_g} \left[ \sum_{\varphi\in ENUM(\phi \land \phi_{q}) } \alpha(\varphi) \right]
\E_{\randomvariableset \sim  \dcpprogram_g} \left[ \sum_{\varphi\in ENUM(\phi) } \alpha(\varphi)  \right]
\\
\frac
\E \left[ \sum_{\varphi\in ENUM(\phi \land \phi_{q})   } \alpha(\varphi) |  \mathcal{S}  \right]
\E \left[ \sum_{\varphi\in ENUM(\phi) } \alpha(\varphi) |  \mathcal{S}   \right]
}  \label{eq:cond_amc_approx}
\\
\frac{
\E \left[ \sum_{\varphi\in ENUM(\phi)   } \ive{\varphi \models \phi_q} \alpha(\varphi) |  \mathcal{S}  \right]
\E \left[ \sum_{\varphi\in ENUM(\phi) } \alpha(\varphi) |  \mathcal{S}   \right]
\label{eq:cond_amc_expanded}
\end{align}

We now rewrite the fraction of two real numbers in Equation <ref> as the fraction of two infinitesimal numbers and plug in the definition of the infinitesimal algebraic likelihood weight (cf. Definition <ref>):

\begin{align}
\E \left[ \sum_{\varphi\in ENUM(\phi)   } \ive{\varphi \models \phi_q} \alpha(\varphi) |  \mathcal{S}  \right]
\E \left[ \sum_{\varphi\in ENUM(\phi) } \alpha(\varphi) |  \mathcal{S}   \right]
\\
\frac{
\left(\E \left[ \sum_{\varphi\in ENUM(\phi)   } \ive{\varphi \models \phi_q} \alpha(\varphi) |  \mathcal{S}  \right], 0 \right)
\left( \E \left[ \sum_{\varphi\in ENUM(\phi) } \alpha(\varphi) |  \mathcal{S}   \right],0 \right)
} \\
\frac
\displaystyle \bigoplus_{i=1}^{\lvert \mathcal{S} \rvert}  \bigoplus_{\varphi\in ENUM(\phi)} \ive{\varphi \models \phi_q} \bigotimes_{\ell \in \varphi}   \alpha_{IALW}^{(i)} \left(\ell \right)}
\displaystyle  \cancel{ \bigoplus_{i=1}^{\lvert \mathcal{S} \rvert}  \bigoplus_{\varphi\in ENUM(\phi)} \bigotimes_{\ell \in  DI(\varphi)}  \alpha_{IALW}^{(i)} \left(\ell \right) }}
\otimes
\frac
\displaystyle \cancel{\bigoplus_{i=1}^{\lvert \mathcal{S} \rvert}  \bigoplus_{\varphi\in ENUM(\phi)} \bigotimes_{\ell \in  DI(\varphi)}  \alpha_{IALW}^{(i)} \left(\ell \right) } }
\displaystyle \bigoplus_{i=1}^{\lvert \mathcal{S} \rvert}  \bigoplus_{\varphi\in ENUM(\phi)} \bigotimes_{\ell \in \varphi}  \alpha_{IALW}^{(i)} \left(\ell \right)
} \label{eq:cond_amc_canel}
\end{align}

In the last line the first factor corresponds to the numerator of the previous equation and the second factor corresponds to the reciprocal of the denominator.
Note that the consistency of the infinitesimal algebraic likelihood weight of the numerator (first factor) is guaranteed by defining a new labeling function $\alpha^q(\varphi)\coloneqq \ive{\varphi \models \phi_q} \alpha(\varphi)$ and evoking Proposition <ref> with $\alpha^q$.

Finally, we push the expression $\ive{\varphi \models \phi_q}$ in the numerator back into the index of the summation ($\oplus$), which yields the following expression:

\begin{align}
\frac
{ \bigoplus_{i=1}^{\lvert \mathcal{S} \rvert}  \bigoplus_{\varphi\in ENUM(\phi \land \phi_{q})} \bigotimes_{\ell \in \varphi}  \alpha_{ALWI}^{(i)} \left(\ell \right)}
{ \bigoplus_{i=1}^{\lvert \mathcal{S} \rvert}  \bigoplus_{\varphi\in ENUM(\phi)} \bigotimes_{\ell \in \varphi}  \alpha_{IALW}^{(i)} \left(\ell \right)}
\label{eq:cond_alw_last}
\end{align}

which proves the proposition.

§.§ Proof of Proposition <ref>

Algorithm <ref> first compiles both propositional formulas into equivalent d-DNNF representations, cf. Lines <ref> and <ref>.
In Lines <ref> and <ref> it then computes the (unnormalized) infinitesimal algebraic likelihood weight for both formulas by calling Algorithm <ref>. In other words, we compute the numerator and denominator in Equation <ref>. We observe that Algorithm <ref> evaluates a given d-DNNF formula for each conditioned topological sample using the  function, which evaluates a d-DDNF formula given a labeling function, cf. Algorithm <ref> [Kimmig et al., 2017]. The correctness of Algorithm <ref> now hinges on the correctness of the  function, which was proven by Kimmig et al., 2017 for the evaluation of a d-DNNF formula using a semiring and labeling function pair that adheres to the properties described in Lemmas <ref> to <ref>. Effectively, Algorithm <ref> correctly computes the algebraic model count for each ancestral sample, adds up the results, and returns the unnormalized algebraic model count to Algorithm <ref>. Line <ref> finally return the ratio of the two unnormalized algebraic likelihood weights, which corresponds to the conditional probability $P_\dcpprogram(\mu=q|\evidenceset=e)$, as proven in Equations <ref> to <ref>.

In Section <ref> where we describe the conversions performed by the inference algorithm on a queried program we used labeled propositional formulas as an intermediate representation. This, however, ignored the arithmetic meaning inherent to the comparison predicates. We will now refine this our understanding of labeled propositional logic formulas by making the link with weighted model integration <cit.>.

On the logic formula level we have been treating comparisons, , (temp<25.0), as purely logical, with no inherent meaning. For instance, we never exploited facts like $(\text{\probloginline{temp<25}} \land \text{\probloginline{temp>30}}) \leftrightarrow \bot $. Only through the labeling function (cf. Definition <ref>) have comparisons been assigned an arithmetic meaning. For instance, the labeling function interprets the predicate </2 as an arithmetic comparison and the two arguments (temp, 25.0) as arithmetic expressions.[Note that logic programming languages, such as , often include a non-logical external arithmetics engine. Through such engines logic programming languages are capable of interpreting arithmetic expressions and comparison predicates, 25>5+2 and assign a logical meaning to the comparison <cit.>. In a sense, probabilistic logic programming languages extend logic programming with probabilistic arithmetics engines.]

Interpreting comparisons can also be performed on the formula level, without the use of labeled atoms. Such formulas are called satisfiability modulo theory (SMT) formulas and extend propositional logic with interpreted first-order predicates.

We refer the reader to <cit.> for a formal definition and in-depth treatment of SMT formulas.
Using the so-called refinement operation one can obtain SMT formulas from Boolean formulas.

[Refinement of a Boolean Formula]
Consider the Boolean formula $\support_g $ from Example <ref>, ,:

\begin{align}
%\support_g  \nonumber
&\Big( \phi_{\text{\probloginline{works(1)}}} \leftrightarrow \phi_{\text{\probloginline{cool(1)}}}
\lor \phi_\text{\probloginline{hot}} \land  \phi_\text{\probloginline{temp(hot)<25.0}}
\lor\neg \phi_\text{\probloginline{hot}}  \land \phi_\text{\probloginline{temp(not_hot)<25.0}}   \Big)  \nonumber \\
\land ~~	& \Big(
\phi_{\text{\probloginline{cool(1)}}} \leftrightarrow  \phi_{\text{\probloginline{rv_cool(1)=:=1}}} \Big) \nonumber \\
\land ~~ 	& \Big(
\phi_\text{\probloginline{hot}} \leftrightarrow \phi_{\text{\probloginline{rv_hot}=:=1}} \Big)
\end{align}

Refining the Boolean literals that encode a comparison in yields the following SMT formula $\support_g ^\uparrow$:

\begin{align}
%	\support_g ^\uparrow \nonumber
%	&\leftrightarrow
&\Big( \phi_{\text{\probloginline{works(1)}}} \leftrightarrow \phi_{\text{\probloginline{cool(1)}}}
\lor \phi_\text{\probloginline{hot}} \land  (temp_{hot}{<}25.0)
\lor\neg \phi_\text{\probloginline{hot}}  \land  (temp_{not\_hot}{<}25.0)    \Big) \nonumber \\
\land ~~ 		& \Big(
\phi_{\text{\probloginline{cool(1)}}} \leftrightarrow (rv\_cool_1=1)\Big) \nonumber \\
\land ~~ 	& \Big(
\phi_\text{\probloginline{hot}} \leftrightarrow  (rv\_hot=1)\Big)
\end{align}

Here the $\uparrow$ in $\support_g ^\uparrow$ indicates that the formula is the refinement of $\support_g $. The formula $\support_g ^{\uparrow}$ is now an SMT formula over the propositional variables
$\phi_{\text{\probloginline{works(1)}}}$, $\phi_{\text{\probloginline{cool(1)}}}$  and $\phi_\text{\probloginline{hot}}$, the binary SMT variables $rv\_cool_1$ and $rv\_hot$, and the real-valued SMT variables $temp_{hot}$ and $temp_{not\_hot}$.

[Abstraction of SMT Formula]
The process of going from an SMT formula back to a propositional logic formula is called abstraction and we denote it by $\downarrow$. If we have, for instance, the SMT formula $\phi$ defined as

\begin{align*}
\phi_{\text{\probloginline{cool(1)}}} \lor \phi_\text{\probloginline{hot}} \land  (temp_{hot}{<}25.0)
\end{align*}

we obtain the corresponding propositional formula $\phi^\downarrow$ as:

\begin{align*}
\phi_{\text{\probloginline{cool(1)}}}
\lor \phi_\text{\probloginline{hot}} \land  \phi_\text{\probloginline{temp(hot)<25.0}}
\end{align*}

An obvious query to pose is that of the satisfiability of an SMT formula, to figure out whether there is a satisfying assignment to the variables in an SMT formula ( <cit.>). An equally important query, however, is the weighted counting problem on SMT formulas, which was dubbed weighted model integration <cit.>.

We refer the reader to the survey paper of <cit.> for an overview of the field.

Under the assumption that the values of the variables in an SMT formula are distributed according to a given probability distribution, the weighted model integral of an SMT formula is identical to the expected value of the SMT formula with  respect to the probability distributions of its variables.
This observation gives us the following Lemma <ref>.

Let $\phi$ denote the logic propositional formula derived from a relevant ground program $\dcpprogram_g$ with evidence asserted, and let $\alpha$ be the labeling function as defined in Definition <ref>. Computing the expected value of the label of $\phi$ is a weighted model integration problem.

We start by expressing the expected value of the label of a specific $\omega$ in terms of Iverson brackets (Equation <ref>). We then rewrite the integral by putting the Iverson brackets in the boundary of the integral (Equation <ref>) and slightly rewrite the boundary (Equation <ref>).

\begin{align}
&\E_{vars(\omega) \sim  \dcpprogram_g} [\alpha( \omega )] \nonumber \\
\int
\left( \prod_{i: a_i \in CA^+(\omega)} \ive{  c_i(vars(a_i)) } \right)
\left( \prod_{i: a_i \in CA^-(\omega)} \ive{  \neg c_i(vars(a_i)) } \right)
dP_{vars(\omega)}(\omega) \label{proof:label_wmieq:iverson} \\
&= \int_{\{ a_i^\uparrow: a_i \in CA^+(\omega) \} \cup \{a_i^\uparrow : a_j \in CA^-(\omega)\} }     dP_{vars(\omega)}(\omega)   \label{proof:label_wmieq:boundary1} \\
&= \int_{ \{  a_i^\uparrow : a_i \in ( CA^+(\omega) \cup CA^-(\omega) )   \} } dP_{vars(\omega)}(\omega)  \label{proof:label_wmieq:boundary2}
\end{align}

To get the expected value of the label of $\phi$ we sum over all $\omega \in ENUM(\phi)$ (Equation <ref>). We then rewrite the expected label in terms of the Lebesgue measure $\lambda$ and a counting measure $\xi$ for integer variables (Equation <ref>). We refer to <cit.> for a stringent measure theoretic formulation of weighted model integration. Note how we now explicitly integrate over the function $w_\omega$ representing the probability distributions and which was hidden before in the measure $P_{vars(\omega)}$. Referring again to <cit.>, we equate Equation <ref> with the measure theoretic formulation of weighted model integration (Equation <ref>).

\begin{align}
&\sum_{\omega \in ENUM(\phi) } \int_{ \{  a_i^\uparrow : a_i \in ( CA^+(\omega) \cup CA^-(\omega) )   \} } dP_{vars(\omega)}(\omega) \label{proof:label_wmieq:expected_label_formula}   \\
&= \sum_{\omega \in ENUM(\phi) } \int_{ \{  a_i^\uparrow : a_i \in ( CA^+(\omega) \cup CA^-(\omega) )   \} } \weight_{\omega} d( \lambda \times \xi) \label{proof:label_wmieq:product_measure}\\
&=\int_{\mathcal{M}(\phi^\uparrow)} w d(\lambda\times \xi \times \mu)\\
&= \lwmi(\phi^\uparrow,w) \label{proof:label_wmieq:wmi}
\end{align}

In the second but last line the integration goes over all models of the SMT formula $\phi^\uparrow$ using the product measure $\lambda\times \xi \times \mu$, where $\mu$ is a counting measure for the Boolean variables in $\phi^\uparrow$ (cf. <cit.>). This then corresponds to the definition of the measure theoretic formulation of WMI, denoted in Equation <ref> by $\lwmi$ (the `L' stands for Lebesgue integration).

Lemma <ref> has the delightful property of  allowing us to compute the expected value of the label of a Boolean formula by adopting inference algorithms that have been developed as approaches to weighted model integration <cit.>.