496
E. Bartocci et al.
yˆ2 characterizing the first and second moments of all loop variables of Figure 1. Further, the loop updates of Figure 1 are rewritten by MORA into equations over expected
values, as follows:
E[x
k (n + 1)] = E[1/2 · (x(n) − u(n + 1))
k + 1/2 · (x(n) + u(n + 1))
k ]
E[y
k (n + 1)] = E[(y(n) + x(n + 1) + g(n + 1))
k ]
, (2)
where n ≥ 0 is the loop counter of Figure 1, x(n) denotes the value of x at the nth loop
iteration, and E[expr] is the expected value of an expression expr.
MORA – Core. After rewriting probabilistic loop updates into equations over expected
values, MORA rewrites these equations into non-probabilistic recurrences over so-called
E-variables, with the loop counter n being the recurrence index. E-variables are simply
variables created from monomials over original variables. Thanks to the restrictions
defining PPs to be Prob-solvable, the resulting recurrences are linear recurrences with
constant coefficients, that is C-finite recurrences, whose closed forms can always be
computed [8]. MORA solves these recurrences by calling its Solver module.
Using the equations (2) over expected values, the non-probabilistic recurrences of
Figure 1 generated by MORA are as follows, using the MORA synthax:
y = x + y
g ∗ ∗2 = 1
x = x
u = b/2
x ∗ ∗2 = b ∗ ∗2/3 + x ∗ ∗2
u ∗ ∗2 = b ∗ ∗2/3
y ∗ ∗2 = b ∗ ∗2/3 + x ∗ ∗2 + 2 ∗ x ∗ y + y ∗ ∗2 + 1
g = 0
x ∗ y = b ∗ ∗2/3 + x ∗ ∗2 + x ∗ y
(3)
The left-hand sides of these equations represent values of E-variables at iteration n + 1,
while monomials over original variables on the right-hand side represent E-variables at
iteration n. For example, the first equation of (3) stands for E[y(n + 1)] = E[x(n)] +
E[y(n)]. On the other hand, the fourth equation of (3) represents E[x(n + 1)
2 ] =
b
2
3 + E[x(n)
2 ], as b is a constant parameter and x ** k in python denotes the kth
power of x.
Solver. In this module, MORA extracts and solves recurrences from the non-probabilistic
equations over E-variables computed by its Core module. By exploiting the structure
of Prob-solvable programs, MORA also optimizes the order in which recurrences are
solved, e.g. independent recurrences are solved first. Partial solutions can be used to
reduce the complexity of the latter recurrences. MORA then uses the diofant library
to handle and solve single recurrences.
For Figure 1, using the E-variable equations of (3), the following closed form solutions are computed by MORA:
E. Bartocci et al.
yˆ2 characterizing the first and second moments of all loop variables of Figure 1. Further, the loop updates of Figure 1 are rewritten by MORA into equations over expected
values, as follows:
E[x
k (n + 1)] = E[1/2 · (x(n) − u(n + 1))
k + 1/2 · (x(n) + u(n + 1))
k ]
E[y
k (n + 1)] = E[(y(n) + x(n + 1) + g(n + 1))
k ]
, (2)
where n ≥ 0 is the loop counter of Figure 1, x(n) denotes the value of x at the nth loop
iteration, and E[expr] is the expected value of an expression expr.
MORA – Core. After rewriting probabilistic loop updates into equations over expected
values, MORA rewrites these equations into non-probabilistic recurrences over so-called
E-variables, with the loop counter n being the recurrence index. E-variables are simply
variables created from monomials over original variables. Thanks to the restrictions
defining PPs to be Prob-solvable, the resulting recurrences are linear recurrences with
constant coefficients, that is C-finite recurrences, whose closed forms can always be
computed [8]. MORA solves these recurrences by calling its Solver module.
Using the equations (2) over expected values, the non-probabilistic recurrences of
Figure 1 generated by MORA are as follows, using the MORA synthax:
y = x + y
g ∗ ∗2 = 1
x = x
u = b/2
x ∗ ∗2 = b ∗ ∗2/3 + x ∗ ∗2
u ∗ ∗2 = b ∗ ∗2/3
y ∗ ∗2 = b ∗ ∗2/3 + x ∗ ∗2 + 2 ∗ x ∗ y + y ∗ ∗2 + 1
g = 0
x ∗ y = b ∗ ∗2/3 + x ∗ ∗2 + x ∗ y
(3)
The left-hand sides of these equations represent values of E-variables at iteration n + 1,
while monomials over original variables on the right-hand side represent E-variables at
iteration n. For example, the first equation of (3) stands for E[y(n + 1)] = E[x(n)] +
E[y(n)]. On the other hand, the fourth equation of (3) represents E[x(n + 1)
2 ] =
b
2
3 + E[x(n)
2 ], as b is a constant parameter and x ** k in python denotes the kth
power of x.
Solver. In this module, MORA extracts and solves recurrences from the non-probabilistic
equations over E-variables computed by its Core module. By exploiting the structure
of Prob-solvable programs, MORA also optimizes the order in which recurrences are
solved, e.g. independent recurrences are solved first. Partial solutions can be used to
reduce the complexity of the latter recurrences. MORA then uses the diofant library
to handle and solve single recurrences.
For Figure 1, using the E-variable equations of (3), the following closed form solutions are computed by MORA: