Causal Modeling with Probabilistic Simulation Models?

Abstract

Recent authors have proposed analyzing conditional reasoning through a notion of intervention on a simulation program, and have found a sound and complete axiomatization of the logic of conditionals in this setting. Here we extend this setting to the case of probabilistic simulation models. We give a natural de nition of probability on formulas of the conditional language, allowing for the expression of counterfactuals, and prove foundational results about this de nition. We also nd an axiomatization for reasoning about linear inequalities involving probabilities in this setting. We prove soundness, completeness, and NPcompleteness of the satis ability problem for this logic.

Keywords

• Counterfactuals conditional reasoning probabilistic programs conditional simulation

Introduction

Accounts of subjunctive conditionals based on internal causal models o er an alternative to approaches based on ranking possible worlds by similarity [ 9 ]. One might, e.g., employ structural equation models (SEMs), i.e. systems of equations connecting the values of relevant variables, as the causal model; the semantics of conditionals are then based on a precise notion of intervention on the SEM [ 11 ]. Recently, some authors [ 8, 10, 4, 3, 1 ] have proposed using arbitrary programs, rather than systems of equations, as causal models. This approach emphasizes the procedural nature of many internal causal simulations over the purely declarative SEMs.

It is possible to de ne precisely this idea of programs as causal models and to generalize the idea of intervention from SEMs to programs [ 8 ]. It is also possible to give a sound and complete logic of conditionals in this setting [ 6 ]. However, these preliminary results have not fully explored the very important case|from, e.g., the Bayesian Logic modeling language [ 10 ] and implicit in the use of probabilistic programs as cognitive models [ 3 ]|of conditionals in a probabilistic setting, via using stochastic programs as the underlying causal model. In the present contribution we will establish foundational de nitions and logical results for this setting, thus extending the causal simulation framework to probabilistic simulation programs. Probabilities over a causal modeling language are de ned and results showing that they may actually be interpreted as probabilities are given. The probabilities are used to give the semantics of a language for probabilistic reasoning, for which an axiomatization is given. The language and axiomatization are extensions of an analogous probabilistic language considered for the purely propositional case by [ 2 ]. Soundness and completeness of the axiom system is proven, and the satis ability problem is found to be NP-complete. 2

Probabilistic Simulation Models and the Logical Language 2.1

Simulation Models

We work toward the de nition of a language L for expressing probabilities involving probabilistic simulation models. Probabilistic simulation models extend the non-probabilistic1 causal simulation models of [ 8, 6 ]. Formally, a non-probabilistic simulation model is a Turing machine2, and a probabilistic simulation model is a probabilistic Turing machine, i.e., a deterministic Turing machine (that of course still has a read-write memory tape) given read access to a random bit tape whose squares represent the results of independent fair coin ips. The use of Turing machines is meant to allow for complete generality and encompasses, e.g., both logic programming and imperative programming. We sometimes use intuitive pseudocode in describing simulation models; such pseudocode is readily convertible to Turing machine code.

We suppose that simulation models are run initially from an empty tape.3 As a simulation model runs, it reads and writes the values of binary variables on its tape squares. Eventually, the model either halts with some resultant tape, or does not halt, depending on the results of the coin ips the model performs in the course of its simulation. Every probabilistic simulation model thus induces a distribution on these possible outcomes. We are interested not only in these outcomes, but also in the dynamics and counterfactual information embodied in the model. That is, we are interested in what would happen were we to hold the 1 The use of \non-probabilistic" rather than \deterministic" is intended to prevent confusion of the probabilistic/non-probabilistic distinction with the deterministic Turing machine/non-deterministic Turing machine distinction. The former distinction is about the presence of a source of randomness while the latter is about the number of possible halting executions. 2 [ 6 ] does not require these machines to be deterministic, and isolates an additional logical principle that is valid when the machines are deterministic. However here we will suppose \non-probabilistic simulation model" always refers to one whose Turing machine is deterministic. This de nition is more useful for comparison with the probabilistic case, in which all underlying machines are deterministic. 3 [ 6 ] also includes an initial input tape in the de nition of the model. This di erence is inconsequential. values of the tape square variables xed in a particular way that counterfactually di ers from the actual values the squares take on|in the distribution over outcomes that results under a particular intervention: De nition 1 (Intervention [ 8 ]). Let S be a speci cation of binary values for a nite number of tape squares: S = fxigi2I for a nite index set I N. Then the intervention IS is a computable function from Turing machines to Turing machines speci ed in the following way. Given a machine T, the intervened machine IS (T) does the same thing as T but holds the variables in S to their xed values speci ed by S throughout the run. That is, IS (T) rst writes xi to square i for all i 2 I, then runs T while ignoring any writes to any of the squares whose indices are in I.

Suppose one xes the entire random bit tape to some particular sequence in f0; 1g1. Then the counterfactual, as well as actual, behavior of a probabilistic simulation model is completely non-probabilistic. We de ne rst a basic language that allows us to express facts about such behavior. Then we will de ne the probability that a given probabilistic simulation model satis es a formula of this basic language. Our nal language L uses these probabilities|it thus expresses facts about the probabilities that counterfactual properties hold. In all logical expressions we help ourselves to these standard notational conventions: ! abbreviates : _ , and $ denotes ( ! ) ^ ( ! ). 2.2

The Basic Language

Syntax The basic, non-probabilistic language Lnon-prob is a propositional language over conditionals. Formally: De nition 2. Let X be a set of atoms fX1; X2; X3; : : : g representing the values of the memory tape variables and let Lprop be the propositional language formed by closing X o under conjunction, disjunction, and negation.

Let the intervention speci cation language Lint Lprop be the language of purely conjunctive, ordered formulas of unique literals,4 i.e., formulas of the form li1 ^ ^ lin for some n 0, where ij < ij+1 and each lij is either Xij or :Xij . > abbreviates the \empty intervention" formula with n = 0. Let Lcond be the conditional language of formulas of the form h i for 2 Lint; 2 Lprop.

The overall basic language Lnon-prob is the language formed by closing o the formulas of Lcond 5 under conjunction, disjunction, and negation. Every formula 2 Lint speci es an intervention I by giving a list of variables to x and which values they are to be xed to. Given a subjunctive conditional 4 The point being that such formulas are in one-to-one correspondence with speci cations of interventions, i.e., nite lists of variables along with the values each is to be held xed to. 5 Unlike [ 6 ], we do not admit the basic atoms X as atoms of L. There is no di culty extending the semantics to such atoms, but allowing them would needlessly complicate the proof of Theorem 1. formula h i 2 Lcond, we call the antecedent and the consequent. We use [ ] for the dual of h i, i.e., [ ] abbreviates :h i(: ). Note that hi' holds in a program if the unmodi ed program halts with a tape making ' true. Semantics The semantics of the basic language are de ned from considering a subjunctive conditional to be true in a simulation model when the program so intervened upon as to make its antecedent hold halts with such values of the tape variables as make its consequent hold. For example, consider a simple model that checks if the rst memory tape square X0 is 1 and if so writes a 1 into the second tape square X1, and otherwise simply halts. This program satis es the formulas hi:X0, hi:X1, but also the counterfactual formula hX0i(X0 ^ X1): holding the rst memory square xed to 1 causes a write of the value 1 into the second tape square, thus satisfying the consequent X0 ^ X1. Formally: De nition 3. Let T be a non-probabilistic simulation model. De ne T j=non-prob h i i I (T) halts with a memory tape whose variable assignment satis es . Now suppose T is probabilistic, and x values for all squares on the random bit tape to some sequence r 2 f0; 1g1. De ne T; r j= h i i I (T) when run with its random bit tape xed to r halts with a resultant memory tape satisfying . De ne (in both cases) satisfaction of arbitrary formulas of Lnon-prob in the familiar way by recursion.

In a sense, the validities of the non-probabilistic setting carry over to this setting, as we will now show. For ' 2 Lnon-prob, write j=non-prob ' if ' is valid in the class of all non-probabilistic simulation models. We will see that all such formulas are still valid for probabilistic simulation models, under De nition 3, once one xes the random bit tape to a particular sequence.

Lemma 1. j=non-prob ' if and only if, for all probabilistic simulation models T and all r 2 f0; 1g1, we have that T; r j= '.

Proof. Suppose j=non-prob '. Consider some probabilistic simulation model T and sequence r 2 f0; 1g1. ' is composed of Lcond-atoms, of the form h i . What is the behavior of I (T); r? Either I (T); r reads only a nite portion of r or reads an unbounded portion of r (in the latter case, it also does not halt). If only a nite portion is read, let N (a) be the maximal random bit tape square reached of r. Let N be the maximum of the N (a) for all atoms a in ', clearly existent as ' has nite length. Construct a Turing machine T0 from T that embeds the contents of r up to index N into its code, replacing any read from r with its value. This is possible in a nite amount of code as we only have to include values up to N in T0.

What if I (T); r ends up reading an unbounded portion of r? We note that it is possible to write code in T0 to check if the machine is being run under an - xing intervention|i.e., conditional code that runs under I (T0) and no other intervention.6 Add such code to T0, including an in nite loop conditional on an 6 For the precise details of this construction, see [ 6 ]. Brie y, if one wants to check if some Xi is being held xed by an intervention, one can try to toggle Xi; this attempt will be successful i Xi is not currently being xed by an intervention. -intervention for each case where I (T); r reads an unbounded portion of r. Now, for all atoms h i , T0 j=non-prob h i i T; r j= h i . As this holds for any atom of ', and j=non-prob ', we have that T; r j= ' as desired.

Now, suppose that T; r j= ' for all probabilistic T; r. We want to see that j=non-prob '. Given a non-probabilistic T, convert T to a probabilistic TM T0 that never reads from its random tape, and take any random tape r. Then T0; r j= ' so that T j=non-prob '. tu 2.3

Adding Probabilities

Syntax L is the language of linear inequalities over probabilities that formulas of Lnon-prob hold. More precisely: De nition 4. Let Lineq be the language of formulas of the form a1P('1) + for some n 2 N, and c; a1; : : : ; an 2 Z, '1; : : : ; 'n 2 Lnon-prob. Then L is the language of propositional formulas formed by closing o Lineq under conjunction, disjunction, and negation.

We sometimes write inequalities of a di erent form from (1) with the understanding that they can be readily converted into some L-formula. For example, an inequality with a > sign is a negation of a Lineq-formula.

Semantics Let T be a probabilistic simulation model. We will shortly de ne a probability PT : Lnon-prob ! [0; 1]. Now suppose a given ' 2 Lineq has the form (1). Then T j= ' i the inequality (1) holds when each P('i) factor takes the value PT('i). Satisfaction T j= ' for arbitrary ' 2 L is then de ned familiarly by recursion. Given ' 2 Lnon-prob, the probability PT(') is simply the (standard) measure of the set of in nite bit sequences r for which T; r j= '. More formally: let be the -algebra on f0; 1g1 generated by cylinder sets and be the standard measure de ned on .7 Now let S(') = fr 2 f0; 1g1 : T; r j= 'g. Then we de ne PT (') = (S(')). The following Lemma ensures that S(') is always measurable, so that this de nition is valid.

Lemma 2. For any ' 2 Lnon-prob, we have S(') 2 .

Proof. Proof by induction on the structure of '. If ' = : , then S(') is the complement of a set in and hence is in . The case of a conjunction or disjunction is similar since is closed under intersection and union. The base case is that of the atoms. Consider an atom of the form h i . If I (T) halts on x with random bit tape xed to r, then it does so reading only a nite portion of r. Thus S(h i ) is the union of cylinder sets extending nite strings on which I (T) halts with a result satisfying , and hence is in . tu 7 That is, as the product measure of Bernoulli(1=2) measures, as de ned in, e.g., [ 3 ]. This probability is coherent in the sense that it plays well with the logic of the basic language: Proposition 1. For any probabilistic T we have, 1. PT(') = 1 if j=non-prob ' for ' 2 Lnon-prob 2. PT(') PT( ) whenever j=non-prob ' ! 3. PT(') = PT(' ^ ) + PT(' ^ : ) for all '; for '; Proof. (1) holds since in this case, by Lemma 1, S(') = f0; 1g1. (2) holds since in this case, S(') S( ). Finally (3) holds by noting j=non-prob ' $ ((' ^ ) _ (' ^ : )), applying (2), and noting that S(' ^ ) and S(' ^ : ) are disjoint. tu A corollary of part (2) is that logical equivalents under j=non-prob preserve probability. 2.4

The Case of Almost-Surely Halting Simulations

An interesting special case is that of the simulation models that halt almostsurely, i.e., with probability 1 under every intervention. Call this class M#. Following the urging of [ 7 ] we have not restricted the de nition of probabilistic simulation model to such models. We will see that from a logical point of view, this # case is a natural probabilistic analogue of the class Mnon-prob of non-probabilistic simulation models that halt under every intervention. By this we mean that we may prove an analogue to Lemma 1. Write j=#non-prob ' if ' 2 Lnon-prob is valid # in Mnon-prob. Note that Lemma 1 does not hold if one merely changes all the preconditions to be halting/almost-surely halting: consider a probabilistic simulation model T that repeatedly reads random bits and halts at the rst 1 it discovers; this program is almost-surely halting. But if r is an in nite sequence of 0s, then T; r 6j= hi>, even though j=#non-prob hi>. Crucially, we must move to the perspective of probability and measure to see the analogy: Lemma 3. j=#non-prob ' if and only if, for all T 2 M#, we have T; r j= ' for all r 2 f0; 1g1 except on a set of measure 0.

Proof. Suppose j=#non-prob '. We claim that for all T 2 M# we have T; r j= ' for all r except on a set of measure 0. Again, consider an atom h i appearing in '. The set of r for which I (T); r does not halt has measure 0, given that T 2 M#. On each such r, the run of I (T); r must read in nitely many bits of r: otherwise, the intervened machine would have a nonzero probability of not halting. Thus, excluding such r, it is possible to repeat the construction of T0 from the proof of Lemma 1 for h i , and in doing this construction we are already ignoring all cases where an unbounded portion of r is read. This means that we do not have to include any in nite loops in T0, and T0 will be always-halting. If we exclude all the such r arising from all antecedents of atoms of ', then we only exclude a set of measure 0 since there are nitely many atoms. Except for such r, the construction works, and T0 has, as before, the same behavior as T. But since j=#non-prob ', we have that T; r j= ' except on the excluded set of measure 0.

For the opposite direction, let T 2 M#non-prob. We wish to show that T j=non-prob '. Convert T to an identical probabilistic simulation program T0 that never reads from its random tape. We have T0; r j= ' for all r but on a set of measure 0; in particular, for at least one r. This implies T j=non-prob '. tu 3

Axiomatic Systems

We will now give an axiomatic system for reasoning in L and prove that it is sound and complete with respect to probabilistic simulation models: it proves all (completeness) and only (soundness) the formulas of L that hold for all probabilistic simulation models. We will give an additional system that is sound and complete for validities with respect to the almost-surely halting simulation models M#.

De nition 5. Let AX be a set of rules and axioms formed by combining the following three modules. 1. PC: propositional reasoning (tautologies and modus ponens) over atoms of

L. 2. Prob: the following axioms:

NonNeg: P(')

0 Norm: P(>) = 1

Add: P(' ^ ) + P(' ^ : ) = P(')

Dist: P(') = P( ) whenever j=non-prob ' $ 3. Ineq, an axiomatization (see [ 2 ]) for reasoning about linear inequalities: Zero: (a1P('1) + Additionally, let AX# be the system formed in exactly the same way, but replacing j=non-prob with j=#non-prob.

Note that the non-probabilistic validities j=non-prob and j=#non-prob, appearing in Dist, have been completely axiomatized in [ 6 ]. The main result is: Theorem 1. AX (respectively, AX#) is sound and complete for the validities of L with respect to M (respectively, M#).

Proof. Soundness (of Prob) follows from Lemma 1, Proposition 1, and, for the almost-surely halting case, Lemma 3. For completeness, consider the general case of M rst. As usual, it su ces to show that any consistent ' 2 L is satis able by some probabilistic simulation model. We put ' into a normal form from which we construct a canonical model. By PC we may suppose ' is in disjunctive normal form. We may further suppose that it is a conjunction of Lineq-literals, as at least one (conjunctive) clause in the disjunctive normal form must be consistent. Let a1; : : : ; an 2 Lcond be the atoms that appear inside any probability P in ', and let 1; : : : ; 2n represent all the formulas of the form l1 ^ ^ ln that can be obtained by setting each li to either ai or :ai. We then have the following, which is a kind of normal form result: Lemma 4 (Lemma 2.3, [ 2 ]). ' is provably-in-AX equivalent to a conjunction (P( 1)

0) ^ (P( 1) + ^ (P( 2n )

0)^ + P( 2n ) = 1)^ (a1;1P( 1) +

+ a1;2n P( 2n ) (am;1P( 1) +

+ am;2n P( 2n ) (a01;1P( 1) + + a01;2n P( 2n ) > c01)^ c1)^ : : :^ cm)^ : : :^ (a0m0;1P( 1) + + a0m0;2n P( 2n ) > c0m0 ) (2) for some integer coe cients c1; : : : ; cm; c1; : : : ; c0m0 ; a1;1; : : : ; am;2n ; a01;1; : : : ; a0m0;2n . Proof. Let 2 Lnon-prob be any of the formulas appearing inside of a probability P in '. Note that P( ) = P( ^ l1) + P( ^ :l1) by Add. Moving on to l2, we have, provably, P( ^ l1) = P( ^ l1 ^ l2) + P( ^ l1 ^ :l2), and we may rewrite P( ^ :l1) similarly. Applying this process successively, we have P( ) = P( ^ 1) + + P( ^ 2n ). For any term in the right-hand side of this inequality, if ) i, propositional reasoning by Dist allows us to replace the term by P( i), and if not, by 0. Thus we always have that P( ) = b1P( 1) + + b2n P( 2n ) for some coe cients bi. Applying this process to each P-term in ' and using Ineq to rewrite the left-hand sides of the inequalities, and conjoining the (clearly provable) clauses that P( i) 0 for all 1 i 2n, and P( 1) + + P( 2n ) = 1, we obtain (2).

The conjunction (2) can be seen as a system of simultaneous inequalities over 2n unknowns, P( 1); : : : ; P( 2n ). Ineq is actually sound and complete for such systems (we refer the reader to Section 4 of [ 2 ] for the proof of this fact). So if ' is consistent with AX|which includes Ineq|this system must have a solution. Thus there are values P( i) solving (2). We will now construct a probabilistic simulation model having precisely these probabilities of satisfying each i. Note that for any i with j=non-prob ? $ i it is provable that P( i) = 0, and we may conjoin this to (2). Note also that i ^ j is unsatis able for any i 6= j. Given these two observations, the following Lemma implies the result.

Lemma 5. For any collection of satis able Lnon-prob-formulas '1; : : : ; 'n no two of which are jointly satis able, and any rational probabilities p1; : : : ; pn 0 such that p1 + + pn = 1, there is a probabilistic simulation model T such that PT('i) = pi for all i, 1 i n.

Proof. Since the 'i are satis able, there are non-probabilistic simulation models Tnon-prob;1; : : : Tnon-prob;n such that for all i = 1; : : : ; n, we have Tnon-prob;i j=non-prob 'i. Further, we may suppose the machines so constructed use only a bounded number of memory tape squares.8 Thus let the maximum index of a tape square used by any of the Tnon-prob;i be N . We now describe T informally. Suppose without loss of generality that for all i, pi = ai=b for some common denominator b. Let T draw a random number r from 1 up to b uniformly, and ensure that T does any auxiliary computations it might need only on squares with indices at least N + 1. Check whether r a1, and if so, let T branch into the code of Tnon-prob;1. If not, check if a1 + 1 r a1 + a2 and if so, branch into Tnon-prob;2. Repeat the process for p3; : : : ; pn. It's clear that the probability of branching into each Tnon-prob;i block is exactly pi, and the same is true under any relevant (i.e., involving only memory tape variables that appear in one of the 'i) intervention on T: we may suppose any auxiliary computations T might require use only memory tape squares with indices past N . After branching into the ith block, the behavior of T is exactly the same as that of Tnon-prob;i, meaning that any random bit tape xings that end up causing a branch into this block will belong to S('i). Another random bit tape xing that causes a branch into another block, say the jth, cannot belong to S('i) since 'i; 'j are jointly unsatis able. Thus, PT( i) = pi for all i. tu Finally, we must see that this model lies in M# if the original formula is consistent with AX#. [ 6 ] has shown that j=#non-prob [ ] ! h i . Then in the proof of Lemma 5, we may suppose that each Tnon-prob;i block contains only alwayshalting code,9 and hence that T does not contain any loops either: thus it almostsurely halts. tu 8 Why? Since 'i are satis able, they are consistent with the axiomatization for nonprobabilistic simulation models given by [ 6 ], and hence are satis ed by the canonical models given in [ 6 ]. These models use only boundedly many tape squares. 9 Since the canonical programs of [ 6 ] for Mnon-prob contain only such code.

# 4

Computational Complexity

Call the problem of deciding if a formula ' 2 L is satis able Prob-Sim-Sat('). Theorem 2 shows that solving this problem is no more complex than is propositional satis ability.

Theorem 2. Prob-Sim-Sat(') is NP-complete in j'j (where this length is computed standardly).

Proof. It's NP-hard since, given any propositional , the formula P(hi ) > 0 is satis able i is satis able (consider a machine that does nothing but write a satisfying memory tape assignment out). In order to show that the satis ability problem is in NP, we give the following nondeterministic satis ability algorithm: guess a program from a class of programs (that we will de ne shortly) that includes the program constructed in Lemma 5 |call this canonical program T'|and check (in polynomial time) if it satis es '. This algorithm decides satis ability since, by soundness, a satis able formula must be consistent, and hence has a canonical model of the form constructed in Lemma 5. For the remainder of the proof, by the \length of a number," we just mean the length of its computer (binary) representation. The \length of a rational" is the sum of the lengths of its numerator and its denominator.

What is the class of probabilistic simulation models that we may limit our guesses to? For some xed constants C; D 2 N, we will de ne a class M';C;D. We will then show that there exist C; D such that the canonical program of Lemma 5 belongs to M';C;D for all consistent '. Let M';C;D be the fragment of probabilistic simulation models whose code consists of the following: 1. Code to draw a random number uniformly between 1 and some N , such that

N has length at most Dj'j3. 2. At most n = Cj'j branches, that is, copies of: an if-statement with condition ` r u, whose body is a canonical program P i for some i 2 Lnon-prob, of the same form as the non-probabilistic canonical models (i.e., in the class de ned in the proof of Theorem 2 from [ 6 ]).

Letting `i; ui be the bounds for the ith copy in (2), we also require that `1 = 1, and that `i+1 = ui + 1 for all i, and that un = N . The following fact from linear algebra (we refer the reader to [ 2 ] for the proof) helps us to show that for all consistent ', the canonical program T' belongs to M';C;D for some C; D. Lemma 6. A system of m linear inequalities with integer coe cients of length at most ` that has a nonnegative solution has a nonnegative solution with at most m variables nonzero, and where the variables have length at most O(m` + m log m). tu Apply this lemma to (2). Each inequality in (2) originally came from ', so there are O(j'j) of them. Further, recall that each integer coe cient in (2) came from summing up a subset of 2n coe cients originally from ', with n is the number of atoms appearing anywhere inside P expressions in '. As this n is thus O(j'j)| and hence 2n is O(j'j) in length|and each original coe cient is also O(j'j) in length, each coe cient is O(j'j) in length as well (lengths of products add). Thus Lemma 6 shows that without loss of generality, we may suppose that the solutions for the P( i) of (2) have O(j'j2) length. The common denominator of these O(j'j) rationals hence has O(j'j3) length. The construction of Lemma 5 has one branch for each of them, and hence O(j'j) branches. This shows the existence of D for part (1) of the de nition of M';C;D and the existence of a C for part (2). We will abbreviate M' = M';C;D for some choice of C; D thus guaranteed.

It remains to show that given any program T 2 M', we can check if T j= ' in polynomial time. It su ces to show that checking if T j= for 2 Lineq is polynomial time: if we know whether T j= for every that ' is built out of, we can decide in linear time if T j= '. Thus suppose has the form a1P('1) + + anP('n) c. [ 6 ] shows that one may check if the P i in part (2) of the de nition of M' satisfy any formula of the basic language Lnon-prob in polynomial time. Then we can easily compute P('i) as simply the sum of the probabilities of each branch that satis es 'i. Doing the arithmetic to check if is satis ed is then certainly polynomial time, so we have our result. tu 5

Conclusion and Future Work

We have de ned and obtained foundational results concerning a very natural extension of counterfactual intervention on simulation models to the probabilistic case.

One critical operation in probability is conditioning, or updating probabilities given that some event is known to have occurred (in the subjective interpretation, updating a belief for known information). One may already de ne conditional probabilities in the usual way in the current framework, and our framework (without interventions) covers the conditional simulation approach to certain aspects of common-sense reasoning of [ 3 ]. In this approach, one limits oneself to the runs satisfying a certain query; the framework considered here would be equivalent for any queries expressible as formulas of Lnon-prob. [ 2 ] also give a logic for reasoning about conditional probabilities. Future work would involve extending this system to probabilistic simulation models and studying the complexity of reasoning in that setting.

As [ 8, 6 ] note, the simulation model approach invalidates many important logical principles that are valid in other approaches [ 5, 11, 9 ], such as cautious monotonicity : [A](B ^ C) ! [A ^ B]C. However the approach is otherwise quite general, and an important future direction would be to identify and characterize subclasses of of simulation models that validate this and other similar logical principles. We have begun investigating this extension. An interesting consequence it has is on the comparison of conditional probability with the probabilities of subjunctive conditionals: while these two probabilities are not in general equal in the classes M or M#, they are equal in certain restricted classes.

A nal direction we want to mention concerns \open-world" reasoning including rst-order reasoning about models with some domain, where counterfactual antecedents might alter how many individuals are being considered or which individuals fall under a property or bear certain relations to each other. Recursion and the tools of logic programming [ 4, 10 ] make this very natural for the simulation model approach, and we would like to understand the rst- and higher-order conditional logics that result in this approach, in both the non-probabilistic and probabilistic cases. We have also begun exploring this direction.

References

1. Chater , N. , Oaksford , M. : Programs as causal models: Speculations on mental programs and mental representation . Cognitive Science 37 ( 6 ), 1171 { 1191 ( 2013 )

2. Fagin , R. , Halpern , J.Y. , Megiddo , N.: A logic for reasoning about probabilities . Information and Computation 87 , 78 { 128 ( 1990 )

3. Freer , C.E. , Roy , D.M. , Tenenbaum , J.B. : Towards common-sense reasoning via conditional simulation: legacies of turing in arti cial intelligence . In: Downey, R . (ed.) Turing's Legacy: Developments from Turing's Ideas in Logic , Lecture Notes in Logic, vol. 42 , pp. 195 { 252 . Cambridge University Press ( 2014 )

4. Goodman , N.D. , Tenenbaum , J.B. , Gerstenberg , T. : Concepts in a probabilistic language of thought . In: Margolis, E. , Laurence , S. (eds.) The Conceptual Mind: New Directions in the Study of Concepts . MIT Press ( 2015 )

5. Halpern , J.Y.: Axiomatizing causal reasoning . Journal of AI Research 12 , 317 { 337 ( 2000 )

6. Ibeling , D. , Icard , T. : On the conditional logic of simulation models . Proc. 27th IJCAI ( 2018 )

7. Icard , T. : Beyond almost-sure termination . Proc. 39th CogSci ( 2017 )

8. Icard , T.F. : From programs to causal models . In: Cremers, A ., van Gessel, T. , Roelofsen , F . (eds.) Proceedings of the 21st Amsterdam Colloquium . pp. 35 { 44 ( 2017 )

9. Lewis , D. : Counterfactuals. Harvard University Press ( 1973 )

10. Milch , B. , Marthi , B. , Russell , S. , Sontag , D. , Ong , D.L. , Kolobov , A. : BLOG: Probabilistic models with unknown objects . In: Proc. 19th IJCAI . pp. 1352 { 1359 ( 2005 )

11. Pearl , J.: Causality. CUP ( 2009 )