Read-back: Def_mm_path

Throughout, $V$ is an arbitrary finite type with decidable equality, and $P$ is an arbitrary $V \times V$ matrix of real numbers — no assumption is made anywhere in this file that $P$ is stochastic, nonnegative, or otherwise probability-like. A "path of length $t$" below means a function $\omega : \{0, 1, \dots, t\} \to V$ assigning a state to each of the $t+1$ time indices; the sums below range over all such functions.

pathWeight. Given the matrix $P$, a natural number $t$ (implicit), and a path $\omega : \{0,\dots,t\} \to V$, the path weight is defined as the product of the matrix entries along the consecutive steps of the path:

$$w_P(\omega) = \prod_{i=0}^{t-1} P\big(\omega(i),\, \omega(i+1)\big).$$

When $t = 0$ (a path consisting of a single state), this is the empty product and equals $1$, regardless of $P$ or $\omega$. Since $P$ is not assumed nonnegative, the weight may be any real number.

avoidHitProb. Given $P$, three states $x, z, y \in V$ (not assumed distinct), and $t \in \mathbb{N}$, this is the real number

$$\sum_{\omega : \{0,\dots,t\} \to V} w_P(\omega) \cdot \mathbf{1}\Big[\,\omega(0) = x \;\wedge\; \big(\forall i \in \{1,\dots,t\},\ \omega(i) \neq z\big) \;\wedge\; \omega(t) = y\,\Big],$$

i.e. the sum of path weights over all length-$t$ paths that start at $x$, end at $y$ at time $t$, and avoid $z$ at every time index except possibly time $0$ (the starting state is exempt from the avoidance requirement, so $x = z$ is allowed; but the final index $t$ is not exempt when $t \ge 1$, so for $t \ge 1$ and $y = z$ every summand vanishes). Degenerate case $t = 0$: the only time index is $0$, the avoidance condition is vacuous, and the value is $1$ if $x = y$ and $0$ otherwise (in particular it is $1$ when $x = y = z$).

avoidTailProb. Given $P$, states $x, z \in V$, and $t \in \mathbb{N}$, this is

$$\sum_{\omega : \{0,\dots,t\} \to V} w_P(\omega) \cdot \mathbf{1}\Big[\,\omega(0) = x \;\wedge\; \big(\forall i \in \{1,\dots,t\},\ \omega(i) \neq z\big)\,\Big],$$

the sum of weights of all length-$t$ paths that start at $x$ and avoid $z$ at every time index from $1$ through $t$ inclusive; time $0$ is again exempt, so $x = z$ is permitted. No condition is placed on the endpoint. Degenerate case $t = 0$: the condition reduces to $\omega(0) = x$, so the value is $1$ (the weight of the single one-point path at $x$).

expHitTimePos. Given $P$ and states $x, z \in V$, this is the value of the infinite series

$$\sum_{t=0}^{\infty} \texttt{avoidTailProb}(P, x, z, t),$$

where the sum is a topological sum over $\mathbb{N}$: if the family $\big(\texttt{avoidTailProb}(P,x,z,t)\big)_{t \ge 0}$ is not (unconditionally) summable, this expression is by convention equal to $0$, not $+\infty$. Note the series starts at $t = 0$, and the $t = 0$ term always equals $1$.

expReturnTime. Given $P$ and a state $x \in V$, this is literally $\texttt{expHitTimePos}(P, x, x)$: the (topological) sum over $t \ge 0$ of the total weight of length-$t$ paths that start at $x$ and do not visit $x$ at any time in $\{1, \dots, t\}$. Again, if the series is not summable the value is $0$ by convention.

firstHitBeforeProb. Given $P$, states $x, a, b \in V$ (not assumed distinct), and $t \in \mathbb{N}$, this is

$$\sum_{\omega : \{0,\dots,t\} \to V} w_P(\omega) \cdot \mathbf{1}\Big[\,\omega(0) = x \;\wedge\; \omega(t) = a \;\wedge\; \big(\forall i \neq t,\ \omega(i) \neq a\big) \;\wedge\; \big(\forall i \in \{0,\dots,t\},\ \omega(i) \neq b\big)\,\Big],$$

the sum of weights of all length-$t$ paths that start at $x$, are at $a$ at time $t$ but at no earlier time (including time $0$, so for $t \ge 1$ this forces $x \neq a$), and never equal $b$ at any time, including time $0$ and time $t$. Consequences of the literal reading: if $x = b$ every summand is $0$ (the constraints $\omega(0) = x$ and $\omega(0) \neq b$ conflict); if $a = b$ every summand is $0$ (the constraints $\omega(t) = a$ and $\omega(t) \neq b$ conflict). Degenerate case $t = 0$: the "no earlier visit to $a$" condition is vacuous and the value is $1$ if $x = a$ and $x \neq b$, else $0$.

hitBeforeProb. Given $P$ and states $x, a, b \in V$, this is the topological sum

$$\sum_{t=0}^{\infty} \texttt{firstHitBeforeProb}(P, x, a, b, t),$$

with the same convention: the value is $0$ if the family of terms is not summable.

setAvoidTailProb. Given $P$, a state $x \in V$, a finite subset $S \subseteq V$, and $t \in \mathbb{N}$, this is

$$\sum_{\omega : \{0,\dots,t\} \to V} w_P(\omega) \cdot \mathbf{1}\Big[\,\omega(0) = x \;\wedge\; \big(\forall i \in \{0,\dots,t\},\ \omega(i) \notin S\big)\,\Big],$$

the sum of weights of all length-$t$ paths that start at $x$ and avoid the set $S$ at every time index, including time $0$ — unlike avoidTailProb, the starting state is not exempt here, so if $x \in S$ the value is $0$ for every $t$. $S$ may be empty, in which case the avoidance condition is vacuous. Degenerate case $t = 0$: the value is $1$ if $x \notin S$ and $0$ if $x \in S$.

expSetHitTime. Given $P$, a state $x \in V$, and a finite subset $S \subseteq V$, this is the topological sum

$$\sum_{t=0}^{\infty} \texttt{setAvoidTailProb}(P, x, S, t),$$

equal by convention to $0$ whenever the family of terms is not summable. If $x \in S$, every term of the series is $0$ and the sum is $0$.