On the one hand, PlanOut is straightforward and should be easy to reason about: the language does not permit user-defined functions and none of the operators use loops or recursion. Experiments are designed to provide apples-to-apples comparisons between two or more equivalent treatment groups, yet PlanOut programs are able to assign individuals to treatment groups using any number of users characteristics or complex logic. To analyze such experiments, one therefore needs to be able to determine what kinds of contrasts between the variables which define a treatment (the experimental contrasts), and the propensity to receive a treatment (the propensity scores).
What makes reasoning about PlanOut scripts tricky is that free variables may sit around unevaluated: we may have some expression such that there is no way to simplify it down to a base value without further information from the system. This post describes how the analyzer interprets expressions in the presence of unknown values.
Boolean expressions are fairly easy to reason about because of the relationship between truth values and boolean operators. When boolean literals take on truth values, we are guaranteed to be able to simplify their expressions because each truth value either absorbs or dominates the connective. For example, we know that in the expression , if evaluates down to
false, then the truth value of the expression is completely determined by the truth value of ; in this case,
false is the absorbing value for disjunction. Conversely, if evaluates down to
true, then the whole expression evaluates down to
true is the dominating value for disjunction.
Evaluation for truth values is trivial:
If a variable has a value in the context, then we just look up the value. However, if it does not have a value, then the variable is external. We annotate the variable with
+ to denote that its value is unknown statically.
The unary not operator behaves as expected:
Wolog, if the first variable in a disjunction evaluates down to true, then the whole expression is true. If the first variable evaluates down to false, then the second variable fully determines the value of the expression.
The rules for conjunction are similar. We can apply deMorgan’s laws to evaluate as much of the expression as possible:
Arithmetic expressions operate similarly, but the analogue of disjunction is summation (subtraction) and the analogue of conjunction is multiplication (division).
We flatten the parse tree by distributing the operations so that becomes .
The commutativity of addition allows us to rearrange the expression and evaluate down the expression down to two components – the first part is a number, and the second is a set of terms (summands) that are a series of products, each of which have at least one external term.