ProofProgram equivalence in the natural sciences
Introduction:
There is a general impression in the computational biology community that theories of computation are both difficult to understand and useless. I believe this situation is partly due to gaps in the general education of computational biologists. This may be filled by motivating theoretical neuroscience from a biological perspective [1] as well as reading a book on the history of computation where each advance is carefully justified.
However, for those computational biologists that would like a short introduction I prepared this article which focuses on insights and intuitions. Starting with function composition, which all scientists are familiar with, I show that proofprogram equivalence is a natural consequence. I then show that there is a direct correspondence between this functional approach to computation, from the perspective of a mathematician, and Turing Machines, developed from the perspective of a storedprogram computer.
A natural definition of computation:
If we define an approximate bijection between the sequence of mathematical operations \(f = \{f_i\}_{i=1}^n\) of a function \(f\) with \(\text{Dom}(f) = X\) and \(\text{Im}(f)=Y\), such that for any \(x_0 \in X\):
\begin{equation} x_1 = f_1 \circ x_0 \end{equation}
\begin{equation} x_2 = f_2 \circ x_1 \end{equation}
\begin{equation} f \circ x_0 = f_n \circ x_{n1} \end{equation}
and the sequence of mathematical operations \(g = \{g_i\}_{i=1}^n\) on a system state \(z_0 \in Z\), carried out by an engineered system:
\begin{equation} z_1 = g_1 \circ z_0 \end{equation}
\begin{equation} g \circ z_0 = g_n \circ z_{n1} \end{equation}
then we say that \(x_n\) is an encoding of \(z_n\), and \(g\) evaluated at \(z_0\) computes the operation \(f\) at \(x_0\).
We note that if the physical operation of the program halts at step \(n\), then the program returns its state at that instant:
\begin{equation} z_n = g_n \circ z_{n1} \end{equation}
and in this setting, a finite loop is a sequence of functions \(\{f_i\}_{i=1}^n\) where \(n < \infty\) and:
\begin{equation} \forall i,j \in [1,n], f_i \equiv f_j \end{equation}
At this point we may make a couple useful observations:

There are no infinite loops in a physical system as every physical computer runs on a finite amount of energy.

Biological systems address energy constraints via a complex combination of heuristics that are used for estimating the appropriate stopping time. In the real world, energy is a more important resource than time which is at most a proxy measure for energy. In any case, stopping criteria are an approximate solution to the halting problem in the real world [3].
Type theory and proofprogram equivalence:
Now, we note that the physical operation \(g_i\) and \(g_{i+1}\) compose with each other only if they share the same units so all physical equations define a type restriction:
\begin{equation} \text{Type}(\text{Im}(g_i)) \equiv \text{Type}(\text{Im}(g_{i+1})) \end{equation}
so \(g = \{g_i\}_{i=1}^n\) defines a path through a space of scientific units which may be modelled as a particular topological space [2].
For concreteness, let’s suppose we would like to perform a backoftheenvelope calculation to verify the proposition that the total mass of ants is approximately equal to the mass of humans:
\begin{equation} \text{P} := M_{\text{ants}} \approx M_{\text{humans}} \end{equation}
where approximate equality is defined as a difference of less than one order of magnitude:
\begin{equation} \frac{1}{10} \leq \frac{M_{\text{ants}}}{M_{\text{humans}}} \leq 10 \end{equation}
To perform a verification, i.e. the proof, we need a certain number of observables that are measurable(i.e. our assumptions).
\begin{equation} \text{Ant axioms} := \text{Number of ants}, \text{Average mass of an ant} \end{equation}
\begin{equation} \text{Homo sapiens axioms} := \text{Number of humans}, \text{Average mass of a human} \end{equation}
where we have distinct types for number(Integers) and mass(kilograms). It follows that we may define the input:
\begin{equation} z := (N_{\text{ants}}, N_{\text{humans}}, m_{\text{ant}}, m_{\text{human}}) \end{equation}
\begin{equation} g = g_2 \circ g_1 \end{equation}
\begin{equation} g_1 \circ z = \frac{N_{\text{ants}} \cdot m_{\text{ant}}}{N_{\text{humans}} \cdot m_{\text{human}}} \end{equation}
and using Boolean arithmetic we have:
\begin{equation} g_2 \circ g_1 = \text{Bool} \circ (g_1 \circ z \geq \frac{1}{10}) + \text{Bool} \circ (g_1 \circ z \leq 10) \end{equation}
and if we carry out the calculation, we find:
\begin{equation} g \circ z = 1 \end{equation}
So our constructive proof defines a program. It follows that within the realm of scientific computation(a subset of constructive mathematics) the notions of proof and program are equivalent.
Turing machines for simulating physical systems:
The functional perspective that has been introduced so far has been formalised as the Typed Lambda calculus which allows us to reason about the semantics of computation. This perspective is essential because computations are not observer independent. On the other hand, Turing Machines are an equally powerful model of computation that emerge naturally from the perspective of a storedprogram computer. They offer a complementary perspective as they allow us to reason about the mechanics of computation. To be precise, they allow us to analyse the computational complexity of algorithms. Moreover, a direct correspondence between the two perspectives is relatively simple to establish.
In order to simulate a finite sequence of mathematical operations \(\{f_i\}_{i=1}^n\) applied to \(x_0 \in X\)(our program) on a realistic computing device, let’s assume each state transition \(x_n = f_n \circ x_{n1}\) has a binary encoding each \(f_i\) has a binary encoding and each state \(x_i \in X\) has a binary encoding. It follows that we may refer to both functions and their variables \(x \in X\) as mathematical symbols.
As all physically realisable computers have a finite amount of memory and at any instant the sequence of operations only depends on the state \(x_{n1}\) and the function \(f_n\) being applied to it, we may model this process using a length of tape with countably many slots. We may imagine that each state transition is encoded by moving to the right on a finite length of tape and printing a sequence of ones and zeros with blank symbols(\(\emptyset\)) between adjacent encodings of mathematical symbols.
Likewise, in order to define the next statetransition \(f_{n+1} \circ x_n\), the computer must go back by moving to the left in order to replace the previous digits(our symbols) with new ones so the current sequence of symbols is in agreement with the binary encoding of \(f_{n+1} \circ x_n\). (This corresponds to what computer scientists call garbage collection, an automatic form of memory management.)
It follows that we generally need a finite set of mathematical symbols which is a subset of the set of binary sequences with the empty symbol(\(\emptyset\)):
\begin{equation} \Sigma \subset \{0,1\}^* \cup \emptyset \end{equation}
a set of states which in our case is a subset of the set of binary sequences as each statetransition \(f_n \circ x_{n1}\) is identifiable with a distinct state \(x_n\):
\begin{equation} X \subset \{0,1\}^* \end{equation}
an initial state:
\begin{equation} x_0 \in X \end{equation}
as well as final states i.e. termination criteria for the program:
\begin{equation} \bar{X} \subset X \end{equation}
and our sequence of functions may be replaced by the mechanicallyoperated transition function:
\begin{equation} \delta : (X \setminus \bar{X}) \times \Sigma \rightarrow X \times \Sigma \times \{\text{Left}, \text{Right}\} \end{equation}
where \(\delta\) is generally a partial function due to the fact that the Halting problem is undecidable. Now, we may make a couple useful observations.
First, given a particular discretetime dynamical system there exists a Turing Machine which may be used to simulate that system. Second, there are countably many Turing Machines. This means that if we can simulate \(n1\) discretetime dynamical systems with \(n1\) distinct Turing Machines then we may identify the nth Turing Machine with a computer which may be used to simulate any of the \(n1\) dynamical systems. By induction, there exists a Turing Machine which may be used to simulate all the other Turing Machines.
We may call such a Turing Machine the Universal Turing Machine and we may identify it with the Universe itself which is actively being used to simulate every physical process we observe [6]. In the Universe, garbage collection happens in real time via competition for finite resources.
Discussion:
Some scientists appear to struggle with the notion of an unbounded length of tape. But, I’d like to point out that this is not so different from an arbitrarily large envelope for backoftheenvelope calculations. More importantly, a good understanding of the ChurchTuring thesis is essential for all natural scientists because it defines the epistemological limits of the scientific method itself.
All physical systems at present are modelled within a mathematical framework that is consistent with Peano Arithmetic(PA) for combinatorics and algorithm design, first order logic for mathematical reasoning and proof verification, and a theory of types that is implicitly necessary for physical equations to make sense. This means that human scientists and the models they define operate within the confines of the ChurchTuring thesis.
On the other hand, if physicists reasoned within a mathematical framework that was inconsistent with PA then scientific induction would no longer be possible. So they might develop theories but they would not be testable. It follows that if computational neuroscientists build a testable model of the brain, this model must be within the Turing limit. In a very precise sense the limits of our language define the limits of our world, but the language of mathematics is also unmatched in its expressive power as observed by Wigner [4].
In order to transcend these epistemological limits we may need to build more powerful computers using principles of blackhole engineering [5]. In the nottoodistant future, this will allow scientists to use scientific methods that are beyond the Turinglimit and therefore strictly more powerful than the ones we currently use.
References:
 Hessameddin Akhlaghpour. An RNABased Theory of Natural Universal Computation. Arxiv. 2020.
 The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Princeton University. 2013.
 Thomas S. Ferguson. Who Solved the Secretary Problem? Statistical Science, Vol. 4, No. 3 (Aug., 1989), pp. 282289
 Eugene Wigner. The Unreasonable Effectiveness of Mathematics in the Natural Sciences. 1960.
 Hajnal Andréka et al. Closed Timelike Curves in Relativistic Computation. 2011.
 Aidan Rocke (https://cstheory.stackexchange.com/users/47594/aidanrocke), Understanding the Physical ChurchTuring thesis and its implications, URL (version: 20210222): https://cstheory.stackexchange.com/q/48450