In the definition of conditional semimeasure is not correct. See below.
In the definition of conditional semimeasure is not correct. It should say “A conditional semimeasure ν takes a sequence of actions a_{1:∞} as input and returns a semimeasure ν( · || a_{1:∞}) over E^{♯}.”
Thanks to Daniel Filan.
In Theorem 4, Q needs to be absolutely continuous with respect to P on cylinder sets. In Theorem 6, Corollary 7, Corollary 8, and Corollary 13, P needs to have perpetual entropy. Please see the technical report for details.
Example 5 has two errors:
a, b := b, a + 1
.The nontermination argument is incorrect, it should be as follows.
x_0 = (7, 7.5)
x_1 = (7, 7.5)
y = (0.5, 0.5)
lambda = 1
Example 7 does in fact have multiphase ranking function. Thanks to Samir Genaim for pointing this out. Please see the LMCS version of the paper for a correct example.
In the last sentence of Chapter 3 is missing a ‘not’. It should say “Decidability of termination does not hold for integer domains if the lasso program’s coefficients allow real numbers [3].”
Lemma 2 needs the additional condition that the constraints are integral. Thanks to Amir Ben-Amram.