May 07, 2026
Causal models, also known as Structural Equation Models (SEM), are a well-known formalism for representing and reasoning about causal dependencies between events. In this paper, we show that Temporal SEMs (TSEMs), which extend SEMs to support causal reasoning in temporal settings, can be interpreted as a model of computation. We prove that TSEMs can encode Linear Bounded Automata, and thus causal settings representable in context sensitive languages. We also prove that TSEMs with countably many variables are Turing complete. These results establish a formal connection between causal reasoning and classical models of computation, enabling the integration of counterfactual reasoning techniques from causal inference into the theory of computation.
Causal models in the form of Structural Equation Models (SEM) [1]–[3] have become the dominant AI framework for representing and analysing causal relations between events of interest. These models represent events as the assignment of values to variables, and encode causal dependencies between variables using structural equations which define how the value of each variable depends on the values of other variables. Being a relatively simple yet powerful formalism, they have found multiple applications in different disciplines, including Economics [4], Medicine [5] and Machine Learning [6].
Causal frameworks can also be used to causally model and understand the temporally extended behaviour of natural systems or temporally extended processes. In many applications we are interested in reasoning about not only whether “event A causes event B" but also whether”event A happening at time \(t_1\) causes event B at time \(t_2\)", and a range of approaches to integrating temporal and causal reasoning have been proposed, based both on SEMs e.g., [7]–[11], and on alternative frameworks, e.g., [12]–[16].
In this paper we argue that temporal causal models are not only an effective tool for reasoning about causal structures underlying physical, biological or social processes, but can also be viewed as a useful formalism for representing computing devices. Although other temporal formalisms, for example extensions of the logic LTL [17], can be used to reason about computations, temporal causal models allow us to use techniques specifically developed for causal inference, e.g., counterfactual reasoning, to model and understand the dynamics of program behaviour. We show that Temporal Structural Equation Models (TSEM) [10] can encode Linear Bounded Automata and thus causal settings representable in context sensitive languages. We also prove that TSEMS with countably many variables are Turing complete, and sufficiently expressive for reasoning about computations in both deterministic and non-deterministic settings.
Understanding the causal evolution of computational processes over time is important for computability theory, and we argue that TSEMs provide a useful framework to represent not only the sequence of computational states, but also the causal dependencies between state transitions. This allows us to analyse how specific inputs or intermediate steps causally affect computational outcomes. For example, TSEMs may be used to augment formal verification techniques to determine why certain errors occurred in a system, and what could prevent them.
The contributions of this paper are as follows:
We introduce a non-deterministic extension of TSEMs and define interventions on TSEMs in Section 2.
We prove that TSEMs are as expressive as Linear Bounded Automata in Section 3.
We prove that TSEMs with countably many variables are as expressive as Turing machines in Section 4.
We discuss how interventions on TSEMs can be used to answer computational questions in Section 5.
In this section, we introduce the main components of Temporal Structural Equation Models (TSEM). As we aim to encode nondeterministic Linear Bounded Automata and nondeterministic Turing Machines, we focus on nondeterministic causal models in which a set of events may result in more than one outcome.
Let \(\mathcal{V}= \{X_1, X_2, \dots\}\) be a finite set of variables. A range function \(\mathcal{R}\) associates with every variable \(X_i\in \mathcal{V}\) a non-empty finite set \(\mathcal{R}(X_i)=\{x_1, \dots, x_k\}\) of possible values. The values of variables may change over time, and these changes are governed by temporal structural equations which describe how the current value of each \(X_i\in \mathcal{V}\) depends on the previous values of variables in \(\mathcal{V}\). A domain function \(\mathcal{D}: \mathcal{V}\longrightarrow 2^{\mathcal{V}}\) maps each variable \(Y \in \mathcal{V}\) to a finite subset of variables, intuitively those variables whose values determine the possible next values of \(Y\).
A causal model \(\mathcal{M}\) over a signature \(\mathcal{S}= (\mathcal{V}, \mathcal{R}, \mathcal{D})\) consists of a set of structural equations \(\mathcal{F}= \{\mathcal{F}_Y\mid Y\in \mathcal{V}\}\) specifying how the next values of \(Y\) depends on the previous values of the variables in its domain \(\mathcal{D}(Y)\). Formally:
Definition 1 (Temporal Structural Equation Model). A (nondeterministic) Temporal Structural Equation Model (TSEM), over a signature \(\mathcal{S}\) is a tuple \(\mathcal{M}= (\mathcal{S}, \mathcal{F})\), where \(\mathcal{F}\) associates with every variable \(Y \in \mathcal{V}\) a function \[\mathcal{F}_Y:\prod\limits_{X \in \mathcal{D}(Y)}\mathcal{R}(X)\longrightarrow 2^{\mathcal{R}(Y)}\] which defines the structural equation describing how the (next) value of \(Y\) depends on the (previous) values of the variables in its domain \(\mathcal{D}(Y)\).1 A TSEM is deterministic if all structural equations always return a single value.
The changes in the values of variables induced by a set of structural equations are described by a computation. A computation \(\mathcal{C}\) is a tree of configurations of \(\mathcal{M}\), i.e., complete assignments of values to variables \(\mathcal{V}\). We denote a complete assignment to \(\mathcal{V}\) by \(\vec{v}\), and use \(\vec{v}^{|X}\) to denote \(\vec{v}\) restricted to \(X \in \mathcal{V}\); we also denote \(\vec{v}\) restricted to the variables in the domain of \(Y\) as \(\vec{v}^{|\mathcal{D}(Y)}\). Let \(\mathit{Conf}^{CM}(\mathcal{M})\) be the set of all possible configurations of a causal model \(\mathcal{M}\).
Definition 2 (Computation). A computation \(\mathcal{C}\) for a TSEM \(\mathcal{M}\) with initial assignment \(\vec{v_0}\) is a tree \(\mathcal{T}^{\mathcal{C}}\), whose nodes are elements of \(\mathit{Conf}^{CM}(\mathcal{M})\) with root node \(\vec{v_0}\), and \(\vec{v_1} \twoheadrightarrow_{\mathcal{M}} \vec{v_2}\) iff\(\forall X\in\mathcal{V}, \vec{v_2}^{|X}\in \mathcal{F}_X(\vec{v_1}^{|\mathcal{D}(X)})\).
As a simple illustration, consider a model \(\mathcal{M}\) with a single variable \(X\): \(\mathcal{V}=\{X\}\), such that \(\mathcal{R}(X)= \{0, \dots, 9\}\), \(\mathcal{D}(X) = \{ X \}\), and a single structural equation defined as follows: \[\mathcal{F}_X (X=x)=\begin{cases} 9, \text{ if } x=9\\ \{0, x+1\}, \text{ if } x\neq 9\\ \end{cases}\] If the value of \(X\) on the previous step of the computation is equal to 9, it remains so on the current step. However, if the previous value \(x\) of \(X\) is less than 9, \(\mathcal{F}_X\) makes a non-deterministic choice: either to continue counting and increase the value of \(X\) to \(x+1\) or to reset \(X\) to 0.
One of the key features of causal models is that they allow counterfactual reasoning, that is, they allow us to reason not only about the actual sequence of events, but also about hypothetical counterfactual sequences of events by means of so-called interventions. An intervention is an operation on causal model.
An atomic intervention is denoted by \(do(Y^n\gets y)\), where \(Y\in\mathcal{V}, n\in\mathbb{N}, y\in\mathcal{R}(Y)\), says that the value of the variable \(Y\) must be fixed to \(y\) at the \(n\)th step of the computation. An intervention \(do(\vec{Y}^{\vec{n}}\leftarrow \vec{y}) = do(Y_1^{n_1}\gets y_1, \dots, Y_i^{n_j}\gets y_i)\) is a vector of atomic interventions. Here we assume that if \(Y_k^n\gets y_k\) and \(Y_l^n\gets y_l\) occur in \(\vec{Y}^{\vec{n}}\leftarrow \vec{y}\), then \(Y_k\neq Y_l\). This intervention results in an updated computation tree \(\mathcal{C}^{\vec{Y}^{\vec{n}}\leftarrow \vec{y}}\), defined for each computation branch as follows. Given a default assignment \(\vec{v}_0\), let \(\vec{v}^{I}_0\) under intervention \(I=do(\vec{Y}^{\vec{n}}\leftarrow \vec{y})\) be an assignment of \(\mathcal{V}\), which agrees with \(\vec{v}_0\) everywhere, except the variables \(Y_i\), such that \(Y_i^0\leftarrow y\) occurs in \(\vec{Y}^{\vec{n}}\leftarrow \vec{y}\). The values of those variables in \(\vec{v}^{I}_0\) are set according to \(\vec{Y}^{\vec{n}}\leftarrow \vec{y}\). We write \(\mathcal{C}(i)|_X\) to refer to \(X\)’s value at the \(i\)’th step of \(\mathcal{C}\). This means that we set a value of \(X\) on all branches of \(\mathcal{C}\).
Definition 3 (Intervention). Given an intervention \(I=do(\vec{Y}^{\vec{n}}\leftarrow \vec{y})\) and \((\mathcal{M}, \vec{v_0})\), an updated* computation tree \(\mathcal{C}^{I}\) is defined as, for every branch \(\mathcal{C}_b\) in the tree, \(\mathcal{C}^{I}_b(0)=\vec{v_0}^{I}\), and \(\forall i>0,\, \forall X\in \mathcal{V}\): \[\mathcal{C}^{I}_b(i)|_X=\begin{cases} x', \text{ if } X^i\gets x' \in \vec{Y}^{\vec{n}}\leftarrow \vec{y}\\ \mathcal{F}_X(\mathcal{C}^{I}_b(i-1))^{|\mathcal{D}(X)}, \text{ otherwise} \end{cases}\]*
Interventions can be used to define a cause of a particular state of affairs. Since we consider a temporal setting, as in [10], we focus on the notion of a cause at step \(n\) rather than cause in general. Since we are in non-deterministic setting, we follow [18] to define a cause in the strong sense that the outcome could have been prevented on all branches of the computation tree.
Definition 4. Given a TSEM \(\mathcal{M}\), its initial configuration \(\vec{v}_0\) and two assignments of variables \(\vec{X}^{\vec{t}}=\vec{x} = (X_1^{t_1}=x_1, \dots, X_n^{t_n}=x_n)\) and \(\vec{Y}^{\vec{t'}}=\vec{y} = (Y_1^{t_1'}=y_1, \dots, Y_k^{t_k'}=y_k')\) at the corresponding time steps
\(t_1, \dots, t_n\) and \(t_1', \dots, t_k'\). We say that \(\vec{X}^{\vec{t}}=\vec{x}\) is the cause* of \(\vec{Y}^{\vec{t'}}=\vec{y}\) in \((\mathcal{M}, \vec{v}_0)\) iff
(1) both \(\vec{X}^{\vec{t}}=\vec{x}\) and \(\vec{Y}^{\vec{t'}}=\vec{y}\) hold in \(\mathcal{C}\) for \((\mathcal{M},
\vec{v}_0)\);
(2) there exists an intervention \(I = do(\vec{X}^{\vec{t}}\gets \vec{x}')\) with \(\vec{x}\neq \vec{x'}\), such that \(\vec{Y}^{\vec{t'}}=\vec{y}\) does not hold on any branch in \(\mathcal{C}^I\);
(3) no proper subset of \(\vec{X}^{\vec{t}}=\vec{x}\) satisfies condition (2).*
The definition of causal models we present here differs from the standard definition of static SEM, e.g., [3], where a signature usually contains two types of variables: exogenous variables (whose values are determined outside of the model) and endogenous variables (whose values depend on the values of other variables). However, this distinction is not required in our setting, and we treat all the variables as endogenous.
Following [10], we also interpret structural equations as temporal (or time-lagged), and call these models temporal SEMs. While in general TSEMs allow equations with arbitrary long delays (time lags) [19], to simplify notation we restrict consideration to TSEMs with 1-step delays as these are sufficient for the proofs presented below. Lastly, while non-deterministic extensions of static SEMs have been considered in [18], [20] and [21], to the best of our knowledge, temporal extensions of non-deterministic SEMs have not been studied before.
In this section, we show how TSEMs can be used to encode Linear Bounded Automata.
A linear bounded automaton (LBA) is a restricted form of a Turing Machine in which the tape is finite and bounded by left and right endmarkers, and where transitions may not overwrite the endmarkers or to move to the left of the left endmarker or to the right of the right endmarker. Non-deterministic LBAs accept the class of context-sensitive languages, that is, problems which can be expressed in a context sensitive grammar [22]. An LBA accepts a grammar if for each string in the language it accepts with a tape that is bounded by a linear function of the length of the input string.
There are several definitions of LBAs in the literature. The definition below is based on that in [23] as it allows a simpler encoding as a causal model.
Definition 5 (LBA). A (nondeterministic) LBA is a tuple \(\mathcal{A}= (Q, q_0, F, \Sigma, \Gamma, \delta)\), where
\(Q\) is a finite set of states with \(q_0\in Q\) the initial state;
\(F\subset Q\) is the set of final (or accepting) states;
\(\Sigma\) is a finite set of input symbols;
\(\Gamma = \Sigma \cup \{\#, \triangleright, \triangleleft\}\) is the finite set of tape symbols, where \(\#\) is the blank symbol, \(\triangleright\) and \(\triangleleft\) the left and right endmarkers, and \(\{\#, \triangleright, \triangleleft\} \cap \Sigma = \emptyset\);
\(\delta: (Q\setminus F)\times \Gamma \times Q\times\Gamma \times \{-1, 0, 1\}\) is a transition relation mapping a state \(q\in (Q\setminus F)\) and a symbol \(\gamma\in \Gamma\) to a set of tuples \((q', \gamma', d)\), where \(q'\) is the next state, \(\gamma' \in \Gamma\) is the symbol written in the current cell and \(d\in \{-1,0, 1 \}\) is the direction in which the head moves (\(-1\) indicates the head moves to the left etc.).
The transition relation \(\delta\) is constrained such that, if \(\gamma\) is \(\triangleright\) then \(\gamma' = \triangleright\) and \(d \not = -1\) and if \(\gamma\) is \(\triangleleft\) then \(\gamma' = \triangleleft\) and \(d \not = 1\), i.e., the endmarkers cannot be overwritten and transitions cannot move to the left of the left endmarker or to the right of the right endmarker. Note also that \(\delta\) is defined only for states in \(Q \setminus F\), i.e., computation stops when a final state is reached.
We say that an LBA has tape of length \(n\) if the number of cells between \(\triangleright\) and \(\triangleleft\), not including the cells with the endmarkers, is \(n\). We represent a configuration of an LBA with a tape of length \(n\) as a string \[\lambda = C_{0} C_{1} \ldots q C_i \ldots C_{n} C_{n + 1}\] where \(q\) is the state of the LBA, the tape head is above cell \(C_i\), \(C_{0}=\triangleright\), \(C_{n + 1}=\triangleleft\), and each \(C_k, 1 \leq k \leq n\) represents a symbol written in the \(k\)-th cell of the tape. Without loss of generality, we assume that, in the initial configuration, the head is above cell \(C_0\), and the string of input symbols \(s = \sigma_1, \ldots, \sigma_k\) are in the cells \(C_1, \ldots C_{k}\).
Definition 6. Let \(\mathit{Conf}^{LBA}({\cal A})\) be the set of all possible configurations of an LBA \({\cal A}\). Then, a run of \({\cal A}\) on input \(s\) is a tree \(\mathcal{T}\). The nodes of \(\mathcal{T}\) are elements of \(\mathit{Conf}^{LBA}({\cal A})\) with a root node \(\lambda_s\) representing the initial configuration of \(\cal A\) for input \(s\), and \(\lambda \twoheadrightarrow_{\cal A}\lambda' \in \mathcal{T}\) iff \(\lambda'\) is a possible result of transition from \(\lambda\) according to \(\delta\).
An LBA accepts a string \(s\) iff the computation tree \(\mathcal{T}\) for the input \(s\) contains a sequence of valid transitions \(\lambda_s \twoheadrightarrow_{\cal A} \dots \twoheadrightarrow_{\cal A}\lambda'\) from the root node \(\lambda_s\) to some accepting configuration \(\lambda' = C_{0} \ldots q^F \ldots C_{n + 1}\) where the LBA is in a final state (i.e., \(q^F \in F\)).
We now show how to construct a TSEM which we call a Causal Calculator that simulates an LBA. For a given LBA \(\mathcal{A}\) with a tape of length \(n\) we are going to build an LBA causal calculator \(\mathcal{M}^{\mathcal{A}}\) parameterised by \(n\) such that \(\mathcal{A}\) accepts a string iff \(\mathcal{M}^{\mathcal{A}}\) has an accepting computation on the corresponding input. To simplify the construction, we introduce a transition relation \(\delta^{F}\) which is deterministic for final states of the LBA: \[\delta^{F}(q, \gamma) = \begin{cases} \{ \langle q', \gamma', d \rangle \mid \langle q, \gamma, q', \gamma', d \rangle \in \delta(q, \gamma) \} \text{ if } q \not\in F \\ \{ \langle q, \gamma, 0 \rangle \} \text{ if } q\in F \end{cases}\] where \(d \in \{-1, 0, 1\}\).
We first explain the intuition and then give the formal definition. As the LBA transition relation \(\delta\) is non-deterministic, we cannot update the state, symbol and the direction in which the head moves separately in the configuration of \(\mathcal{M}^{\mathcal{A}}\). We therefore use a special variable \(X_0\) whose value is a 3-tuple where the first element is the current state of the LBA, the second is the symbol written at the last LBA transition, and the third is the direction the head moved to arrive at the current LBA configuration. In addition, to allow interventions on LBA transitions, instead of an encoding where a variable \(X_i\) holds the symbol in the \(i\)th cell of the LBA, the index of the variable holding the symbol in \(C_i\) is relative to the last position of the head. In effect, we shift the representation of the LBA tape in the causal model left or right depending on the movement of the head. This requires twice the number of variables in the causal model as there are cells in the tape of the LBA, from \(X_{-(n+1)}\) to \(X_{n+1}\). At any given time, a contiguous set of these variables correspond to \(C_0,\ldots,C_{n + 1}\) but shifted by at most \(n+1\) compared to the LBA cells, depending on the past movements of the head. For example, if at time \(t - 1\) the head was over \(C_{n+1}\), at time \(t\) the second element of \(X_0\) is \(\triangleleft\) and \(C_0\) in the LBA corresponds to the variable \(X_{-(n+1)}\).
Definition 7. Given an LBA \(\mathcal{A}= (Q, q_0, F, \Sigma, \Gamma, \delta)\) with tape of length \(n\), an LBA Causal Calculator* is a tuple \(\mathcal{M}^{{\cal A}} = (\mathcal{S}^{\cal A}, \mathcal{F}^{\cal A})\), with signature \(\mathcal{S}^{\cal A} = (\mathcal{V}, \mathcal{R}, \mathcal{D})\), where*
\(\mathcal{V}= \{X_i\mid -(n + 1) \leq i \leq (n + 1)\}\);
\(\mathcal{R}(X_0) = Q \times \Gamma \times \{-1, 0, 1\}\),
\(\mathcal{R}(X_{i \in [-(n + 1), n + 1] \setminus \{0\}}) = \Gamma\);
\(\mathcal{D}(X_{i \in [-n, n]})=\{X_0, X_{i-1}, X_i, X_{i+1}\}\),
\(\mathcal{D}(X_{-(n + 1)}) = \{ X_0, X_{-(n + 1)}, X_{-n} \}\),
\(\mathcal{D}(X_{n + 1}) = \{ X_0, X_{n} X_{n + 1} \}\);
and equations \(\mathcal{F}^{\mathcal{A}}\): \[\begin{align} &\mathcal{F}_{X_0} ( X_0 = \langle q, \gamma, d \rangle, X_{d} = \gamma' ) = &&\\ &\qquad \{ \langle q', \gamma'', d' \rangle \mid \langle q', \gamma'', d' \rangle \in \delta^{F}(q, \gamma') \} &&\\ &\mathcal{F}_{X_{i \in [-(n + 1), n] \setminus \{0\}}} ( X_{0} = \langle q, \gamma, d \rangle, X_{i+d} = \gamma' ) = \gamma' && \end{align}\]
In the initial configuration \(\vec{v_0}\), \(X_0 = \langle q_0, \triangleright, 0 \rangle\), \(X_{n + 1} = \triangleleft\), \(X_{i \in [1, k]} = \sigma_i\), where \(\sigma_1, \ldots, \sigma_k\) is the input, and \(X_{i} = \#\) for \(-n \leq i < 0\) and \(k+1 \leq i \leq n\).
Informally, the first equation updates the value of \(X_0\) and the second equation updates the value of all other variables \(X_{i \in [-n, n + 1] \setminus \{0\}}\).
For \(X_0\), if the head did not move at \(t - 1\) (this includes the initial configuration), the value of \(X_0\) is updated with the LBA transition \((q', \gamma'', d') = \delta^F(q, \gamma')\) at \(t\), where \(\gamma' = \gamma\). If the head moved left at the last transition, then \(X_0\) is updated with \((q', \gamma'', d') = \delta^F(q, \gamma')\), where \(\gamma'\) is the symbol in \(X_{- 1}\) (i.e., the symbol currently under the head). If the head moved right at the last transition, then \(X_0\) is updated with \((q', \gamma'', d') = \delta^F(q, \gamma')\), where \(\gamma'\) is the symbol in \(X_{1}\).
For \(X_{i \in [-n, n + 1] \setminus \{0\}}\), if the head did not move the value of \(X_i\) is updated with \(\gamma' = \gamma\), i.e., remains the same. If the head moved left, the value of \(X_i\) is updated to be the value in \(X_{i - 1}\), i.e., it shifts the representation of the LBA tape in the causal model to the right. (To simplify the presentation, we abuse notation and assume that in the case where \(X_{i - 1} = X_0\), \(\gamma'\) is the second element of the tuple in \(X_0\).) If the head moved right, the value of \(X_i\) is updated to be the value in \(X_{i + 1}\).
We say that an LBA causal calculator accepts a string \(s\) iff the computation tree \(\mathcal{C}^{\mathcal{M}^{\mathcal{A}}}\) for the input \(s\) contains a sequence of valid transitions \(\vec{v_0} \twoheadrightarrow_{\mathcal{M}^{\cal A}} \dots \twoheadrightarrow_{\mathcal{M}^{\cal A}}\vec{v_m}\) from the root node \(\vec{v_0}\) to some accepting configuration \(\vec{v_m}\) such that \(\vec{v_{i}} \in \mathit{Conf}^{CM}, 0 \leq i \leq m\). A configuration \(\vec{v_m} = X_{-(n+1)}\ldots\) \(X_{0} \ldots X_{n+1}\) is accepting iff \(X_0 = \langle q^F \in F, \gamma, 0 \rangle\), i.e., the state is final.
Theorem 1. An LBA \(\cal A\) accepts a string if, and only if, it is accepted by the corresponding causal calculator \(\mathcal{M}^{{\cal A}}\).
Proof. In order to prove this we show that there is a bisimulation relation between the nodes of the computation tree of \(\cal A\), \(\mathcal{T}\), and of computation tree of \(\mathcal{M}^{{\cal A}}\), \(\mathcal{C}\), where bisimilar nodes have the same states and tape contents. If \(\lambda\) and \(\vec{v}\) are bisimilar, and \(\lambda \twoheadrightarrow_{\cal A} \lambda'\), then there is a transition \(\vec{v} \twoheadrightarrow_{\mathcal{M}^{\cal A}} \vec{v'}\) such that \(\lambda'\) and \(\vec{v'}\) are bisimilar, and vice versa. This will imply that a configuration with an accepting state is reachable in one tree if and only if it is reachable in another.
Since the variables of \(\mathcal{M}^{\cal A}\) correspond to different tape cells at different steps, the notion of bisimulation is non-trivial and depends on the history of the computation so far. We will say that a transition \(\lambda \twoheadrightarrow_{\cal A} \lambda'\) is by \((q,\gamma,q', \gamma', d)\) if this was the element of \(\delta^F\) used for this transition, and label this edge in \(\mathcal{T}\) by \(d\). Similarly, we say that a transition \(\vec{v} \twoheadrightarrow_{\mathcal{M}^{\cal A}} \vec{v'}\) is by \((q,\gamma,q', \gamma', d)\) if the value of \(X_0\) in \(\vec{v}\) is \((q,\gamma,-)\) and the value of \(X_0\) in \(\vec{v'}\) is \((q',\gamma',d)\), and we label this edge in \(\mathcal{C}\) by \(d\).
Finally, we say that two nodes \(\lambda\) and \(\vec{v}\) at step \(t\) are \(d_1,\ldots, d_t\) bisimilar if (i) the path from the root node to each of them is labelled \(d_1,\ldots, d_t\), (ii) the state in \(\lambda\) is the same as the state component in the value of \(X_0\) in \(\vec{v}\), (iii) the symbol in \(C_k\) in \(\lambda\) is the same as the symbol in \(X_{k-o_t}\) (the symbol in \(X_0 = (-,\gamma,-)\) is \(\gamma\)), where \(o_t = \Sigma^{i=t}_{i=0} d_i - d_t\). Observe that \(j=\Sigma^{i=t}_{i=0} d_i\) is the position of the head in \(\lambda\). (Note that the offset \(o_t\) can also be calculated using the index of the variable containing \(\triangleright\), but this more general approach also works for non-deterministic TMs.)
Clearly, \(\lambda_0\) and \(\vec{v_0}\) are \(\epsilon\)-bisimilar, where \(\epsilon\) is an empty path.
For the inductive step, assume that \(\lambda\) and \(\vec{v}\) at step \(t-1\) are \(d_1,\ldots, d_{t-1}\) bisimilar. We
need to show that
\((\mathcal{T}\rightarrow \mathcal{C})\) if there is a transition from \(\lambda\) to \(\lambda'\) by \((q,\gamma,q',
\gamma', d)\), then there is a transition from \(\vec{v}\) to \(\vec{v'}\) by \((q,\gamma,q', \gamma', d)\), and \(\lambda'\) and \(\vec{v'}\) are \(d_1,\ldots, d_{t-1},d\) bisimilar;
\((\mathcal{C}\rightarrow \mathcal{T})\) if there is a transition from \(\vec{v}\) to \(\vec{v'}\) by \((q,\gamma,q',
\gamma', d)\), then there is a transition from \(\lambda\) to \(\lambda'\) by \((q,\gamma,q', \gamma', d)\), and \(\lambda'\) and \(\vec{v'}\) are \(d_1,\ldots, d_{t-1},d\) bisimilar.
We prove those conditions for \(d=1\). The proofs for \(d=-1\) and \(d=0\) are similar.
\((\mathcal{T}\rightarrow \mathcal{C})\) Let \(\lambda = C_0\ldots q C_j\ldots C_{n+1}\), that is, the head is over \(C_j\) and the state is \(q\). By the inductive hypothesis, \(X_0=(q,C_{j-d_{t-1}},d_{t-1})\), and the symbol that the head is reading is in \(X_{j-o_{t-1}}\). Let the transition from
\(\lambda\) be by some \((q,\gamma,q',\gamma',1)\) where \(\gamma\) is in \(C_j\). The resulting \(\lambda' = C_0\ldots C_j=\gamma' q'C_{j+1}\ldots C_{n+1}\). The successor of \(\vec{v}\) by \((q,\gamma,q',\gamma',1)\) is (i) reachable from
the root by the same sequence \(d_1,\ldots, d_{t-1},1\) as \(\lambda'\), (ii) has the same state \(q'\) due to the equation for \(X_0\), (iii) the symbol that was held in \(X_i\) is now held in \(X_{i-1}\) because of the equation for \(X_i\), which maintains
the correspondence with LBA cells since the offset has increased by \(d=1\).
\((\mathcal{C}\rightarrow \mathcal{T})\) Let \(X_0\) in \(\vec{v}\) have value \((q,\chi,d_{t-1})\). Assume that transition
in \(\mathcal{M}^{\cal A}\) is to \(\vec{v'}\) by \((q,\gamma,q',\gamma',1)\) where \(\gamma\) is the symbol in
\(X_{d_{t-1}}\) (which by the inductive hypothesis is the symbol the head is reading in \(\lambda\)). Since \(\vec{v}\) and \(\lambda\) have the same state \(q\) and the head position in \(\lambda\) is over \(\gamma\), \({\cal
A}\) can make a transition to \(\lambda' = C_0\ldots C_j=\gamma' q' C_{j+1}\ldots C_{n+1}\). The argument that \(\vec{v'}\) is \(d_1,\ldots,
d_{t-1},1\) bisimilar to \(\lambda'\) is the same as above. ◻
In this section we show that TSEMs with a countable set of variables \(\mathcal{V}\) are Turing complete. For a simpler construction, we consider the case of deterministic Turing Machines, since they are known to be as powerful as non-deterministic ones. We begin by recalling the definition of a Turing Machine [22].
Definition 8 (Turing machine). A Turing Machine (TM) is a tuple \(T = (Q, q_0, F, \Sigma, \Gamma, \delta)\), where
\(Q\) is a finite set of states with \(q_0\in Q\) the initial state;
\(F\subset Q\) is the set of final (or accepting) states;
\(\Sigma\) is a finite set of input symbols;
\(\Gamma = \Sigma \cup \{\# \}\) is the finite set of tape symbols, where \(\# \not \in \Sigma\) is the blank symbol;
\(\delta: Q\setminus F\times \Gamma \longrightarrow Q\times\Gamma \times \{-1, 1\}\) is a function mapping a state \(q\in (Q\setminus F)\) and a symbol \(\gamma\in \Gamma\) to a tuple \(\delta(q, \gamma) = (q', \alpha, d)\), where \(q'\) is the next state, \(\alpha\in \Gamma\) is a symbol that must be written in the cell and \(d\in \{-1, 1\}\) is the direction in which the head moves (\(-1\) indicates the head moves to the left).
To simplify notation we will write \(d=Dir(q, \gamma)\) (for direction), \(\sigma = Sym(q, \gamma)\) (for symbol) and \(q' = Out(q, \gamma)\) (for outcome).
We assume that all cells on the tape are indexed with integers relative to the head. So, the current cell always has index \(0\), its right-side cells have positive indexes, and left-side cells have negative ones. We represent a configuration of a TM as \[\lambda = C_{-i}\dots C_{-2}C_{-1}qC_0C_1C_2\dots C_{j}\] where \(q\) is the state of the TM, the head is (always) scanning a cell indexed 0, and each \(C_k\) represents a symbol written in the \(k\)-th cell of the tape. Note that only blank symbol \(\#\) may occur on the tape on left of \(-i\)’s and on the right of \(j\)’s cells.
Definition 9. Let \(Conf^{TM}(T)\) be the set of all possible configurations of a TM \(T\). Then, a run of \(T\) on input \(I\) is a sequence \(\lambda_0 \twoheadrightarrow_{T} \lambda_1 \twoheadrightarrow_{T} \dots\) of elements of \(Conf^{TM}(T)\), where \(\lambda_0\) is the initial configuration of \(T\) for input \(I\), and each \(\lambda_i\) yields \(\lambda_{i+1}\) in one step.
A TM \(T\) accepts a string \(s\) iff the run \(\lambda_s \twoheadrightarrow_{T} \lambda_1 \twoheadrightarrow_{T} \dots \twoheadrightarrow_{T} \lambda'\) of \(T\) starting in the initial configuration \(\lambda_s\) terminates in an accepting configuration \(\lambda' = C_{-i}\dots C_{-2}C_{-1}q^FC_0C_1C_2\dots C_{j}\) where the TM is in a final state (i.e., \(q^F \in F\)).
Now we will construct a causal calculator \(\mathcal{M}^T\) simulating a TM \(T\). Since a TM has an infinite tape, a causal calculator has to work with an input of arbitrary length. So, in contrast to Definition 1, we assume that \(\mathcal{V}\) contains countably many variables, however ranges and domains of all variables remain finite. The extension to infinitely many variables does not create any technical difficulties and the definitions of a computation \(\mathcal{C}\) (Definition 2) remains unchanged. Causal models with infinitely many variables have previously been studied in [24].
Definition 10. Given a TM \(T = (Q, q_0, F, \Sigma, \Gamma, \delta)\), a TM causal calculator is a tuple \(\mathcal{M}^T = (\mathcal{S}^T, \mathcal{F}^T)\), with a signature \(\mathcal{S}^T = (\mathcal{V}, \mathcal{R}, \mathcal{D})\), where
\(\mathcal{V}= \{S\} \cup \{X_i\mid i\in\mathbb{Z}\}\);
\(\mathcal{R}(X_i) = \Gamma\) and \(\mathcal{R}(S) = Q\);
\(\mathcal{D}(S) = \{S, X_0\}\)
\(\mathcal{D}(X_i)=\{X_0, S, X_{i-1}, X_i, X_{i+1}\}\) for \(i\in\mathbb{Z}\);
Structural equations \(\mathcal{F}\) are defined as follows.
\(\mathcal{F}_S(S=q, X_0=\gamma)= \begin{cases} q', \text{ if } q'\in Out(q, \gamma)\\ q, \text{ if } q\in F \end{cases}\)
For \(\vec{v}^{|\mathcal{D}(X_{i})}=(X_0=\alpha, X_{i-1}=\beta, X_i=\gamma, X_{i+1}=\delta, S=q)\):
\(\mathcal{F}_{X_i\notin \{-1, 1\}}(\vec{v}^{|\mathcal{D}(X_{i})}) = \begin{cases} \beta, \text{ if } -1= Dir(q, \alpha)\\ \delta, \text{ if } 1= Dir(q, \alpha)\\ \gamma, \text{ if } q\in F \end{cases}\)
For \(\vec{v}^{|\mathcal{D}(_{X_{-1}})}=(X_0=\alpha, X_{-1}=\beta, X_{-2}=\gamma, S=q)\):
\(\mathcal{F}_{X_{-1}}(\vec{v}^{|\mathcal{D}(X_{-1})}) = \begin{cases} \gamma, \text{ if } -1= Dir(q, \alpha)\\ Sym(q, \alpha), \text{ if } 1= Dir(q, \alpha) \\ \beta, \text{ if } q\in F \end{cases}\)
For \(\vec{v}^{|\mathcal{D}(X_{1})}=(X_0=\alpha, X_1=\beta, X_{2}=\gamma, S=q)\):
\(\mathcal{F}_{X_{1}}(\vec{v}^{|\mathcal{D}(X_{1})}) = \begin{cases} Sym(q, \alpha), \text{ if } -1= Dir(q, \alpha)\\ \gamma, \text{ if } 1= Dir(q, \alpha)\\ \beta, \text{ if } q\in F \end{cases}\)
Variable \(S\) represents the state of the TM, and \(X_i\)’s represent corresponding cells on the tape. So, the range of \(S\) is the set of states \(Q\) of the TM, and the range of each \(X_i\) is the tape alphabet \(\Gamma\). Finally, domains \(\mathcal{D}\) demonstrate which variables are causally related. Thus, the value of the current state \(S\) depends on the previous value of itself and a current symbol \(X_0\). And the value of any variable \(X_i\) depends on itself, \(X_0, S\), and its left- and right-most cells \(X_{i-1}\) and \(X_{i+1}\). The structural equations are defined as follows. For \(S\), if the previous value \(q_1\) of \(S\) is a final state of the TM (\(q_1\in F\)), then the current value of \(S\) remains \(q_1\). Otherwise, \(S\) gets value \(q_2\), which is the result of the transition \(\delta(q_1, \alpha)\) in the TM. Next, for any cell variable \(X_i\), except \(X_1\) and \(X_{-1}\), and any possible input \(\vec{v}^{|\mathcal{D}(X_{i})}=(X_0=\alpha, X_{i-1}=\beta, X_i=\gamma, X_{i+1}=\delta, S=q)\) of \(\mathcal{F}_{X_i}\), it is defined as follows. In case the TM’s head moves to the left (\(-1= Dir(q, \alpha)\)), \(\mathcal{F}_{X_i}\) gets the value of \(X_{i-1}\); if it moves to the right (\(1= Dir(q, \alpha)\)) then \(\mathcal{F}_{X_i}\) gets the value of \(X_{i+1}\); and if the state \(q\) is final, \(\mathcal{F}_{X_i}\) inherits its own value from the previous step. This allows us to simulate the movements of the head in TM taking into account that the numeration of the tape cells is attached to the head. Thus, at any step of the computation \(\mathcal{C}\), the value of \(X_i\) corresponds to the current symbol written in \(i\)’s cell on the tape of the TM. Finally, \(X_{-1}\) and \(X_1\) are two special cases, because TM rewrites the symbol in the current cell (indexed 0) with a new symbol \(Sym(q, \alpha)\) on each step, which propagates to either \(X_{-1}\) or \(X_1\) depending on the direction of the next movement. Thus, for \(X_{-1}\) and input \(\vec{v}^{|\mathcal{D}(X_{-1})}=(X_0=\alpha, X_{-1}=\beta, X_{-2}=\gamma, S=q)\), if the head moves left in \(\delta(q, \alpha)\), then \(\mathcal{F}_{X_{-1}}\) gets the value of \(X_{-2}\); if the head moves right in \(\delta(q, \alpha)\), then \(\mathcal{F}_{X_{-1}}\) gets a symbol \(Sym(q, \alpha)\) that has been written on the tape before the movement; and if \(q\) is the final state, the value of \(X_{-1}\) remains the same. The case for \(X_1\) is symmetric.
Now it is straightforward to define a translation between the configurations of \(T\) and \(\mathcal{M}^T\). Given a configuration \(\lambda = C_{-i}\dots C_{-2}C_{-1}qC_0C_1C_2\dots C_{j}\) of \(T\), the corresponding configuration of \(\mathcal{M}\) is \(\vec{v}_{\lambda} = (S=q) \cup \{(X_k=C_k)\mid -i \leq k \leq j\} \cup \{(X_n=\#)\mid n\in \mathbb{Z}\setminus [-i, j] \}\).
We say that a TM causal calculator accepts a string \(s\) iff the computation \(\mathcal{C}^{\mathcal{M}^{T}}\) for the input \(s\) contains a sequence of valid transitions \(\vec{v_0} \twoheadrightarrow_{\mathcal{M}^{T}} \dots \twoheadrightarrow_{\mathcal{M}^{T}}\vec{v_m}\) from the initial configuration \(\vec{v_0}\) to some accepting configuration \(\vec{v_m}\) such that \(\vec{v_{i}} \in \mathit{Conf}^{CM}, 0 \leq i \leq m\). A configuration \(\vec{v_m}\) is accepting iff \((S = q^F)\in \vec{v_m}\), i.e., it contains the final state.
We want to show that for any initial configuration \(\lambda\) of \(T\) we can take a corresponding initial configuration \(\vec{v} = \tau(\lambda)\) of \(\mathcal{M}^T\) and generate a computation \(\mathcal{C}\) which will simulate a computation of \(T\) in a step-wise manner.
Lemma 1. For any \(\lambda_1, \lambda_2\in Conf^{TM}\), it holds that \[\lambda_1\twoheadrightarrow_{T}\lambda_2, \text{ iff } \vec{v}_{\lambda_1}\twoheadrightarrow_{\mathcal{M}_T}\vec{v}_{\lambda_2}\]
Proof. Given a configuration \[\lambda_1 = C_{-i}\dots C_{-2}C_{-1}qC_0C_1C_2\dots C_{j}\] of the TM, there are three possible cases for the \[\lambda_2 = C_{-i}'\dots C_{-2}'C_{-1}'q'C_0'C_1'C_2'\dots C_{j}'\]
Case \(q\in F\)2. If the current state in \(\lambda_1\) is final, then \(\lambda_2=\lambda_1\). The construction of \(\mathcal{M}^T\) also guarantees that for any \(Y\in \mathcal{V}\) and any \(\vec{v}\), s.t. \((S=q^F)\in \vec{v}\) it holds that \(\mathcal{F}_Y(\vec{v}^{|\mathcal{D}(Y)})=\vec{v}^{|Y}\). So, \(\vec{v}_{\lambda_1}\twoheadrightarrow_{\mathcal{M}_T}\vec{v}_{\lambda_1}\), and thus \(\vec{v}_{\lambda_1}\twoheadrightarrow_{\mathcal{M}_T}\vec{v}_{\lambda_2}\).
Case \(-1= Dir(q, C_0)\). In this case the head moves to the left after writing symbol \(\zeta\): \(\delta(q, C_0)=(q', \zeta, -1)\). The construction of \(\mathcal{M}^T\) guarantees that (a) \(\mathcal{F}_S(\vec{v}_{\lambda_1}^{|\mathcal{D}(S)}) = q'\) iff \(q'=Out(q, C_0)\), (b) \(\mathcal{F}_{X_1}(\vec{v}_{\lambda_1}^{|\mathcal{D}(X_1)}) = \zeta\) iff \(\zeta = Sym(q, C_0)\) (i.e. iff \(C_1'=\zeta\)), and (c) for \(i\neq 1\), \(\mathcal{F}_{X_i}(\vec{v}_{\lambda_1}^{|\mathcal{D}(X_i)})=\beta\) iff \(\vec{v}_{\lambda_1}^{|X_{i-1}}=\beta\) (i.e. iff \(C_{i-1}=\beta\)). Thus, \(\lambda_1\twoheadrightarrow_{T}\lambda_2\) iff \(\vec{v}_{\lambda_1}\twoheadrightarrow_{\mathcal{M}_T}\vec{v}_{\lambda_2}\).
Case \(1= Dir(q, X_0)\). The argument is symmetric to the previous case. ◻
The next result follows immediately.
Theorem 2. A TM accepts a string if, and only if, it is accepted by the corresponding causal calculator.
As we mentioned before, it is a well-known fact that any non-deterministic TM \(T^*\) can be simulated by a deterministic TM \(T\) 3. So, Theorem 2 implies that TSEMs can also simulate \(T^*\) by simulating the corresponding \(T\). However, such a procedure exponentially increases the computation time of \(T\) (and thus of \(\mathcal{M}^T\)) with respect to \(T^*\). But since in general case TSEMs admit non-deterministic structural equations, they are capable of simulating an NTM in a stepwise manner, with no additional computing time. This can be demonstrated using a slightly modified construction of the LBA causal calculator from Definition 7 that does not contain tape bounds.
Theorem 3. An NTM accepts a string if, and only if, it is accepted by the corresponding causal calculator.
Proof. The detailed proof is presented in Technical Appendix. ◻
The key feature of causal models is that they are specifically designed for counterfactual reasoning. Causal models contain enough information to represent not only the actual sequence of events that occurred, but also hypothetical counterfactual alternatives. This capability aligns closely with theoretical concerns in computability theory, when we are interested in reasoning not only about what happened in the actual computation, but also what would have happened if a different computational path had been taken. TSEMs provide sufficient expressive power to analyse both the actual computation and its counterfactual variations enabling new forms of reasoning about temporally extended processes by means of the interventions introduced in Section 2.
Interventions allow us to alter value of some variable(s) at a given time step and observe how this might change the overall outcome of a computation. For example, interventions allow us to ask questions such as “Which part of the input had causal influence on the output?" or”Had the random bit at step \(t\) been flipped, would the output remain unchanged?" to analyse the internal causal structure that governs a computing device to arrive at a given result.
One possible application is the analysis of the causal influence of alternating bits of input, because interventions provide a straightforward way to explore how local changes in the input propagate through the computation. As a simple example, consider a Turing machine that accepts binary strings if the input contains an alternating pattern of 0s and 1s, e.g.”\(0101\dots\)" or “\(1010\dots\)". A causal analysis of such a computation may reveal not only when the machine accepts or rejects the input, but also how individual bits contribute to the machine’s decision. Suppose the machine halts and accepts the input”0101”, which may be represented as the initial assignment of a canonical causal calculator (Definition 10) \(\vec{v_0}=(X_0=0,X_1=1,X_3=0,X_5=1\)). Then, by systematically intervening on each bit, changing 0 to 1 or vice versa (in our notation \(do(X_i^0\gets 1)\)), we can identify which bits are causally necessary for acceptance. For example, the intervention \(do(X_1^0\gets 0)\) disrupts the alternation pattern and causes the machine to reject, indicating that this bit \(X_1\) has a critical causal link to the outcome of the computation. Conversely, if altering a bit leaves the outcome unchanged, we can classify it as causally inert or redundant.
At the same time, we may be interested in intervening not only on the input bits (intervening at time step \(t=0\)), but also in analysing the role of some random bit alternation at an arbitrary step \(t'\). This allows reasoning about computations with corrupted or faulty memory, for example. One potential application of such counterfactual reasoning is the analysis of so-called soft errors [25]. A soft error is a type of a computer system fault that alters data or logic states without causing permanent damage to the hardware. It is typically caused by external factors like cosmic rays or radioactive decay, which can flip a bit in memory or logic circuits, leading to incorrect computational behaviour. A recent example of this kind of error is the Airbus incident, where intense solar radiation was claimed to corrupt data critical to the functioning of flight controls, which resulted in a recall of 6000 aircraft [26]. By systematically intervening on different values in arbitrary steps of the computation and exploring the causal consequences of these changes, we can study the fault tolerance of a system and develop methods to mitigate the effects of soft errors in critical computational applications.
We conclude this section by commenting on the decision problems involved, namely establishing causality. In Definition 3, as time indexes are fixed for all variables, the decision problem of whether some variable values are the cause of other variable values at a fixed step is decidable for both LBA and TM causal calculators. However, if we would like to represent the outcome in a richer language, for example using an LTL temporal operator eventually \(\mathsf{F}\), e.g. \(\mathsf{F}(\vec{Y}=\vec{y})\) instead of \(\vec{Y}^{\vec{t}}=\vec{y}\), then the problem becomes undecidable for the case of TM causal calculator, because the formula \(\mathsf{F} (S=q^F)\) basically encodes the halting problem for Definition 10.
In reasoning about computation, we are usually interested in answering questions like whether a given function is computable, how long it takes to compute, or how much resources it requires. However, we typically lack a formal framework for asking why a computation led to a specific outcome, or what would have happened if a particular input or step had been different.
In this paper, we used temporal causal models to address this gap and to analyse the internal dynamics of computations in a causally meaningful way. We introduced a temporal causal framework with non-deterministic structural equations and defined interventions for this setting. We then proved that TSEMs can simulate Linear Bounded Automata and TSEMs with countably many variables are Turing complete. Finally, we discussed potential applications of interventions for counterfactual reasoning about computations. We believe our results can enrich the field of formal verification with TSEM-based techniques for reasoning about safety, fault tolerance and explainability of computational systems.
In future work we would like to explore other notions of interventions that make sense for computations. For example, we could consider atomic structure interventions, \(do(Y^n(\vec{X}=\vec{x})\gets y\)), where \(\vec{X}=\mathcal{D}(Y), \vec{x}\in\mathcal{R}(\vec{X})\), says that at time \(n\) the structural equation \(\mathcal{F}_Y\) for \(Y\) must be rewritten so that \(\mathcal{F}_X(\vec{X}=\vec{x}) = y\). As before, a structure intervention \(do(\vec{Y}^{\vec{n}}(\vec{X}=\vec{x})\gets \vec{y})\) is a vector of atomic interventions.
Definition 11 (Structure Intervention). Given a TSEM \(\mathcal{M}\) and a structure intervention \(I=do(\vec{Y}^{\vec{n}}(\vec{X}=\vec{x})\gets \vec{y})\), let dynamic structural equations \(\mathcal{F}^i\) be defined as follows. For any \(Y\in \mathcal{V}, \vec{X}=\mathcal{D}(Y)\) and \(\vec{x}=\mathcal{R}(\vec{X})\), \(\mathcal{F}^0_Y(\vec{X}=\vec{x})= y'\) if \(Y^0(\vec{X}=\vec{x})\gets y' \in I\) and \(\mathcal{F}^0_Y(\vec{X}=\vec{x})= \mathcal{F}(\vec{X}=\vec{x})\) otherwise. For any \(i>0\), \[\mathcal{F}^i_Y(\vec{X}=\vec{x})= \begin{cases} y', \text{ if } Y^i(\vec{X}=\vec{x})\gets y' \in I\\ \mathcal{F}_Y^{i-1}(\vec{X}=\vec{x}), \text{ otherwise} \end{cases}\] Finally, the computation is defined as \[\mathcal{C}^{I}(i) = \prod\limits_{X\in \mathcal{V}} \mathcal{F}_X^{i-1}\bigl(\mathcal{C}^{I}(i-1)^{|\mathcal{D}(X)}\bigr) \text{ for i>0}\]
Note that structure interventions are not expressible in terms of standard interventions. Consider the model \(\mathcal{V}=\{X\}\), \(\mathcal{R}(X)=\{0,1\}\) and \(\mathcal{F}_X (X=x)=1\) for any \(x\). So, whatever the initial assignment of \(X\) is, starting from step \(i>0, (X=1)\in C(i)\). With a structure intervention, we can turn the equation into a constant function returning 0 instead of 1: \(\mathcal{F}_X (X=x)=0\) for any \(x\). So, we can enforce that for \(i>0, (X=0)\in C(i)\). Standard interventions allow changing the value of \(X\) only on the steps specified in the intervention. So, we can enforce \(X=0\) on an arbitrary long but finite interval of the computation. Thus, an infinite sequence of \(X=0\) cannot be achieved by changing the value of \(X\) at a finite sequence of steps. Structure interventions would enable us to talk about changing transition rules in a computing device rather than a particular value, enabling us to model e.g. software patches.
Formal reasoning about structure interventions will require a richer syntax (being able to say that a particular equation is the cause of a state of affairs). We can also enrich the syntax with temporal operators, to express that some value is reachable in principle.
Further variations of causality problems for TSEMs may also be developed besides the extension with a richer syntax. Firstly, for non-deterministic computations it may be important to check if some \(C\) is the cause of some outcome \(O\) on all or only some branches of the computation tree. Secondly, we presented the simplest form of the definition of a cause, called but-for cause, however several alternative approaches to actual causality have been developed, e.g., [3], [20], [27]. The adaptation of these approaches to temporal settings and validating whether arguments against but-for definition hold for TSEM framework as well as extending existing formal verification techniques, e.g., [28], [29] to temporal setting are important directions for future research.
Finally, the canonical causal calculators constructed in Sections 3–4 have a specific structure since they are specifically designed to simulate LBA and TMs. However, other architectures of causal models (e.g. a more distributed structures with multiple ‘inner’ variables) may be more suitable in some applications. In this context, an important question to ask is whether two structurally different causal models execute the same computational behaviour under various interventions. We believe that recent work on the notions of causal model equivalence [10], [30] as well as on the notions of an abstraction or a transformation of one causal model into another [31]–[33] can bring new formal techniques initially developed for causal reasoning to analysis of computation and enrich the field.
Here we demonstrate how to extend the construction of the LBA causal calculator from Section 3 to simulate a non-deterministic TM (NTM) is stepwise manner and prove Theorem 3. The overall argument is very similar to Section 3, except the numeration of the tape cells. We start with a definition of NTM [22].
Definition 12. A non-deterministic Turing Machine (NTM) is a tuple \(T^* = (Q, q_0, F, \Sigma, \Gamma,\delta^*)\), in which all elements except \(\delta^*\) are identical to TM (Definition 8), and the transition function is replaced with a relation \[\delta^*\subseteq \bigl(Q\setminus F\times \Gamma\bigr) \times \bigl(Q\times\Gamma \times \{-1, 0, 1\}\bigr)\footnote{Here for technical reasons we assume that d=\{-1, 0, 1\} rather than \{-1, 1\}. }\]
Following Section 4, we represent a configuration of an NTM as a string \[\lambda = C_{-i}\dots C_{-2}C_{-1}qC_0C_{1}C_{2}\dots C_{j}\] where \(q\) is the state of the TM, the tape head is scanning a symbol indexed \(i\), and each \(C_l\), \(-i \leq l \leq j\) represents a symbol written in the \(l\)-th cell of the tape. Note that only the blank symbol \(\#\) may occur in cells to the left of \(-i\) and to the right of \(j\). We use \(\mathit{Conf}^{TM}(T^*)\) to denote the set of all configurations of \(T^*\).
Definition 13. A run of an NTM \(T^*\) on input \(I\) is a tree \(\mathcal{T}\). The nodes of \(\mathcal{T}\) are elements of \(\mathit{Conf}^{TM}(T^*)\) with a root node \(\lambda_0\) representing the initial configuration of \(T^*\) for input \(I\), and \(\lambda \twoheadrightarrow_{T^*}\lambda' \in \mathcal{T}\) iff \(\lambda'\) is a possible result of transition from \(\lambda\) according to \(\delta^*\).
Similarly to Section 3, to simplify the construction, we introduce a transition relation \(\delta^{F}\) which is deterministic for final states of the NTM: \[\delta^{F}(q, \gamma) = \begin{cases} \{ \langle q', \gamma', d \rangle \mid \langle q, \gamma, q', \gamma', d \rangle \in \delta^*(q, \gamma) \} \text{ if } q \not\in F \\ \{ \langle q, \gamma, 0 \rangle \} \text{ if } q\in F \end{cases}\] where \(d \in \{-1, 0, 1\}\).
An NTM accepts a string \(s\) iff the computation tree \(\mathcal{T}\) for the input \(s\) contains a sequence of valid transitions \(\lambda_s \twoheadrightarrow_{T^*} \dots \twoheadrightarrow_{T^*}\lambda'\) from the root node \(\lambda_s\) to some accepting configuration \(\lambda'\), such that \(q^F\in \lambda'\).
Definition 14. Given a non-deterministic TM \(T^* = (Q, q_0, F, \Sigma, \Gamma, \delta^*)\), a non-deterministic canonical causal calculator is a tuple \(\mathcal{M}^{T^*} = (\mathcal{S}^{T^*}, \mathcal{F}^{T^*})\) with signature \(\mathcal{S}^{T^*} = (\mathcal{V}, \mathcal{R}, \mathcal{D})\) where
\(\mathcal{V}= \{X_i\mid i\in \mathbb{Z}\}\);
\(\mathcal{R}(X_0) = Q \times \Gamma \times \{-1, 0, 1\}\),
\(\mathcal{R}(X_{i \neq 0}) = \Gamma\);
\(\mathcal{D}(X_{i})=\{X_0, X_{i-1}, X_{i+1}\}\);
and equations \(\mathcal{F}^{T^*}\): \[\begin{align} &\mathcal{F}_{X_0} ( X_0 = \langle q, \gamma, d \rangle, X_{d} = \gamma' ) = &&\\ &\qquad \{ \langle q', \gamma'', d' \rangle \mid \langle q', \gamma'', d' \rangle \in \delta^{F}(q, \gamma') \} &&\\ &\mathcal{F}_{X_{i\neq 0}} ( X_{0} = \langle q, \gamma, d \rangle, X_{i+d} = \gamma' ) = \gamma' && \end{align}\]
This construction is similar to Definition 7, except the numeration on the tape and the absence of end-marker symbols since the NTM’s tape is unbounded. So, in the initial configuration \(\vec{v_0}\), \(X_0 = \langle q_0, \alpha, 0 \rangle\), where \(C_0=\alpha\), \(X_{k\in [-i, j]\setminus \{0\}} = C_k\), and \(X_{l} = \#\) for \(l<-i\) and \(l>j\).
For \(X_0\), if the head did not move at \(t - 1\) (this includes the initial configuration), the value of \(X_0\) is updated with the NTM transition \((q', \gamma'', d') = \delta^F(q, \gamma')\) at \(t\), where \(\gamma' = \gamma\). If the head moved left at the last transition, then \(X_0\) is updated with \((q', \gamma'', d') = \delta^F(q, \gamma')\), where \(\gamma'\) is the symbol in \(X_{- 1}\) (i.e., the symbol currently under the head). If the head moved right at the last transition, then \(X_0\) is updated with \((q', \gamma'', d') = \delta^F(q, \gamma')\), where \(\gamma'\) is the symbol in \(X_{1}\).
For \(X_{i\neq 0}\), if the head did not move the value of \(X_i\) is updated with \(\gamma' = \gamma\), i.e., remains the same. If the head moved left, the value of \(X_i\) is updated to be the value in \(X_{i - 1}\) (To simplify the presentation, we abuse notation and assume that in the case where \(X_{i - 1} = X_0\), \(\gamma'\) is the second element of the tuple in \(X_0\).) If the head moved right, the value of \(X_i\) is updated to be the value in \(X_{i + 1}\).
We say that an NTM causal calculator accepts a string \(s\) iff its computation tree \(\mathcal{C}\) for the input \(s\) contains a sequence of valid transitions \(\vec{v_0} \twoheadrightarrow_{\mathcal{M}^{T^*}} \dots \twoheadrightarrow_{\mathcal{M}^{T^*}}\vec{v_m}\) from the root node \(\vec{v_0}\) to some accepting configuration \(\vec{v_m}\) such that \(\vec{v_{i}} \in \mathit{Conf}^{CM}, 0 \leq i \leq m\). A configuration \(\vec{v}\) is accepting iff \((X_0 = \langle q^F \in F, \gamma, 0 \rangle)\in \vec{v}\), i.e., if it contains the final state.
An NTM accepts a string if, and only if, it is accepted by the corresponding causal calculator.
Proof. Following the proof of Theorem 1, we will show that there is a bisimulation relation between the nodes of the computation tree of \(T^*\), \(\mathcal{T}\), and of computation tree of \(\mathcal{M}^{{T^*}}\), \(\mathcal{C}\). If \(\lambda\) and \(\vec{v}\) are bisimilar, and \(\lambda \twoheadrightarrow_{\cal A} \lambda'\), then there is a transition \(\vec{v} \twoheadrightarrow_{\mathcal{M}^{T^*}} \vec{v'}\) such that \(\lambda'\) and \(\vec{v'}\) are bisimilar, and vice versa. This will imply that a configuration with an accepting state is reachable in one tree if and only if it is reachable in another.
We say that a transition \(\lambda \twoheadrightarrow_{T^*} \lambda'\) is by \((q,\gamma,q', \gamma', d)\) if this was the element of \(\delta\) used for this transition, and label this edge in the tree by \(d\). Similarly, we say that a transition \(\vec{v} \twoheadrightarrow_{\mathcal{M}^{T^*}} \vec{v'}\) is by \((q,\gamma,q', \gamma', d)\) if the value of \(X_0\) in \(\vec{v}\) is \((q,\gamma,-)\) and the value of \(X_0\) in \(\vec{v'}\) is \((q',\gamma',d)\), and we label this edge in the tree by \(d\).
Finally, we say that two nodes \(\lambda\) and \(\vec{v}\) at step \(t\) are \(d_1,\ldots, d_t\) bisimilar if (i) the path from the root node to each of them is labelled \(d_1,\ldots, d_t\), (ii) the state in \(\lambda\) is the same as the state component in the value of \(X_0\) in \(\vec{v}\), (iii) the symbol in \(C_k\) in \(\lambda\) is the same as the symbol in \(X_{k+d_t}\) (the symbol in \(X_0 = (-,\gamma,-)\) is \(\gamma\)).
Clearly, \(\lambda_0\) and \(\vec{v_0}\) are \(\epsilon\)-bisimilar.
For the inductive step, assume that \(\lambda\) and \(\vec{v}\) at step \(t-1\) are \(d_1,\ldots, d_{t-1}\) bisimilar. We
need to show that
\((\mathcal{T}\rightarrow \mathcal{C})\) if there is a transition from \(\lambda\) to \(\lambda'\) by \((q,\gamma,q',
\gamma', d)\), then there is a transition from \(\vec{v}\) to \(\vec{v'}\) by \((q,\gamma,q', \gamma', d)\), and \(\lambda'\) and \(\vec{v'}\) are \(d_1,\ldots, d_{t-1},d\) bisimilar;
\((\mathcal{C}\rightarrow \mathcal{T})\) if there is a transition from \(\vec{v}\) to \(\vec{v'}\) by \((q,\gamma,q',
\gamma', d)\), then there is a transition from \(\lambda\) to \(\lambda'\) by \((q,\gamma,q', \gamma', d)\), and \(\lambda'\) and \(\vec{v'}\) are \(d_1,\ldots, d_{t-1},d\) bisimilar.
We prove the back and forth conditions for \(d=1\). The proofs for \(d=-1\) and \(d=0\) are similar.
\((\mathcal{T}\rightarrow \mathcal{C})\) Let \(\lambda = C_{-i}\dots C_{-1}qC_0C_{1}\dots C_{j}\). By the inductive hypothesis, \(X_0=(q,C_{-d_{t-1}},d_{t-1})\), and the symbol that the head is reading is in \(X_{d_{t-1}}\). Let the transition from \(\lambda\) be by some \((q,\gamma,q',\gamma',1)\) where \(\gamma\) is in \(C_0\). The resulting \(\lambda' = C_{-i-1}\dots
C_{-1}qC_0=\gamma'C_{1}\dots C_{j-1}\). The successor of \(\vec{v}\) by \((q,\gamma,q',\gamma',1)\) is (i) reachable from the root by the same sequence \(d_1,\ldots, d_{t-1},1\) as \(\lambda'\), (ii) has the same state \(q'\) due to the equation for \(X_0\), (iii) the
symbol that was held in \(X_i\) is now held in \(X_{i-1}\) because of the equation for \(X_i\), which maintains the correspondence with LBA cells since the
offset has changed by \(d=1\).
\((\mathcal{C}\rightarrow \mathcal{T})\) Let \(X_0\) in \(\vec{v}\) have value \((q,\chi,d_{t-1})\). Assume that transition
in \(\mathcal{M}^{T^*}\) is to \(\vec{v'}\) by \((q,\gamma,q',\gamma',1)\) where \(\gamma\) is the symbol in
\(X_{d_{t-1}}\) (which by the inductive hypothesis is the symbol the head is reading in \(\lambda\)). Since \(\vec{v}\) and \(\lambda\) have the same state \(q\) and the head position in \(\lambda\) is over \(\gamma\), \({T^*}\) can make a transition to \(\lambda' = C_{-i}\ldots C_{-1} q'C_0=\gamma' C_{1}\ldots C_{j}\), where \(C_k\) from \(\lambda'\) is equal to \(X_{k+1}\) from \(\vec{v'}\). The argument that \(\vec{v'}\) is \(d_1,\ldots, d_{t-1},1\) bisimilar to \(\lambda'\) is the same as above. ◻
Recall that the construction of the LBA causal calculator in Section 3 uses twice as many variables as the number of LBA cells. However, one can use even simpler construction with a single variable, whose values represent all possible configurations of the LBA.
Definition 15 (LBA Causal Calculator). Given an LBA \({\cal A} = (Q, q_0, F, \Sigma, \Gamma, \delta)\) with tape of length \(n\), an LBA causal calculator* is a tuple \(\mathcal{M}^{{\cal A}} = (\mathcal{S}^{\cal A}, \mathcal{F}^{\cal A})\), with a signature \(\mathcal{S}^{\cal A} = (\mathcal{V}, \mathcal{R}, \mathcal{D})\), where*
\(\mathcal{V}= \{V\}\) where \(V\) represents a configuration \(S H X_0 X_{1}X_{2}\ldots X_{n} X_{n+1}\)
\(\mathcal{R}(V) = Q \times \{0,\ldots,n+1\} \times \{\triangleright\} \times \Gamma \times \ldots \Gamma \times \{\triangleleft\}\)
\(\mathcal{D}(V) = \{V\}\)
The structural equations \(\mathcal{F}\) are defined as follows:
\(\mathcal{F}_V (q,j,\triangleright, \gamma_1,\ldots,\gamma_j,\ldots,\gamma_n,\triangleleft)=\)
\(\{(q',j',\triangleright, \gamma_1,\ldots,\gamma'_j,\ldots,\gamma_n,\triangleleft) \mid j' = j+d, (q,\gamma_j,q',\gamma'_j, d) \in \delta\}\)
Given a configuration \(\lambda\) of the LBA \(\cal A\), we denote a corresponding configuration of \(\mathcal{M}^{\cal A}\) as \((V=\lambda)\). For any initial configuration \(\lambda_0\), let \(\mathcal{T}_{\mathcal{A}}\) and \(\mathcal{C}_{\mathcal{M}^{\mathcal{A}}}\) be computation trees for the LBA \(\mathcal{A}\) and the causal calculator \(\mathcal{M}^A\) on inputs \(\lambda_0\) and \(\vec{v_0} = (V=\lambda_0)\) respectively. It is now straightforward to prove that the construction of \(\mathcal{M}^{\cal A}\) guarantees that \((V=\lambda)\twoheadrightarrow_{\mathcal{M}^{\mathcal{A}}} (V=\lambda') \in \mathcal{C}_{\mathcal{M}^{\mathcal{A}}}\) iff \(\lambda \twoheadrightarrow_{\cal A}\lambda' \in \mathcal{T}_{\mathcal{A}}\). Thus, \(\mathcal{T}_{\mathcal{A}}\) is isomorphic to \(\mathcal{C}_{\mathcal{M}^{\mathcal{A}}}\).
However, this construction does not allow us to intervene on e.g. the symbol read by the head or on the next transition of the LBA.
We abuse notation and interpret elements of \(\prod\limits_{X\in \{X_1, \dots, X_k\}}\mathcal{R}(X)\) both as vectors of values \((x_1,\dots,x_k)\) and as vectors of assignments \((X_1=x_1,\dots,X_k=x_k)\).↩︎
Here for simplicity of the proof we assume that for any final configuration \(\lambda\), \(\lambda\twoheadrightarrow_{T}\lambda\).↩︎
Recall that in a non-deterministic TM \(T^*\) the transition function \(\delta\) is replaced with a relation \(\delta^*\subseteq \bigl(Q\setminus F\times \Gamma\bigr) \times \bigl(Q\times\Gamma \times \{-1, 1\}\bigr)\)↩︎