I ended up giving *Baire space (computability)* its (minimal) stand-alone entry after all

I had created a stub for *effective topological space* and cross-linked with *equilogical space*. Added some pointers to the literature, but otherwise no real content yet.

started something at *Church-Turing thesis*, please see the comments that go with this in the thread on ’computable physics’.

This is clearly just a first step, to be expanded. For the moment my main goal was to record the results about physical processes which are not type-I computable but are type-II computable.

]]>For completenss and clarification I created a brief entry *exact real computer arithmetic* and cross-linked with all the entries on mathematical type-II computability.

And now I need to turn away from this computability business…

]]>I gather the following is true and is shown in Battenfield-Schröder-Simpson (pdf), but I haven’t really fully absorbed yet how $AdmRep$ is actually embedded in $RT(\mathcal{K}_2)$.

The subcategory on the effectively computable morphisms of the function realizability topos $RT(\mathcal{K}_2)$ is the Kleene-Vesley topos $KV$. The category of “admissible representations” $AdmRep$ (whose morphisms are computable functions (analysis), see there) is a reflective subcategory of $RT(\mathcal{K}_2)$ (BSS) and the restriction of that to $KV$ is $AdmRep_{eff}$

$\array{ AdmRep_{eff} &\hookrightarrow& KV \\ \downarrow && \downarrow \\ AdmRep &\hookrightarrow& RT(\mathcal{K}_2) }$

This is currently stated this way in the entry function ralizability and computable function (analysis), but please criticize/handle with care, I’ll try to further fine-tune as need be.

]]>Am starting an entry *computable physics*. For the moment this is essentialy a glorified lead-in for

- Thomas Streicher,
*Computability Theory for Quantum Theory*, talk at Logic Seminar Univ. Utrecht in July 2012 (pdf)

I had had the feeling that most previous literature on computability in physics is suffering from being not well informed of the relevant mathematical concepts, but then I found

- Matthew Szudzik,
*The Computable Universe Hypothesis*(arXiv:1003.5831) published as*A Computable Universe*, World Scientific, 2013, pp. 479-523

which seems to be sober, well-informed and sensible. The main drawback seems to be, to me, that the author looks only at type-I computability and not really seriously at quantum physics. Both of this is what Streicher’s note above aims to do!

If anyone has more pointers to decent literature on this topic, please drop me a note.

Here is what it currently has in the entry text *computable physics*:

The following idea or observation or sentiment has been expressed independently by many authors. We quote from Szudzik 10, section 2:

The central problem is that physical models use real numbers to represent the values of observable quantities, $[...]$ Careful consideration of this problem, however, reveals that the real numbers are not actually necessary in physical models. Non-negative integers suffice for the representation of observable quantities because numbers measured in laboratory experiments necessarily have only finitely many digits of precision.

Diverse conclusions have been drawn from this. One which seems useful and well-informed by the theory of computability in mathematics is the following (further quoting from Szudzik 10, section 2)

So, we suffer no loss of generality by restricting the values of all observable quantities to be expressed as non-negative integers — the restriction only forces us to make the methods of error analysis, which were tacitly assumed when dealing with real numbers, an explicit part of each model.

In type-I computability the computable functions are partial recursive functions and in view of this some authors conclude (and we still quote Szudzik 10, section 2) for this:

To show that a model $[$ of physics $]$ is computable, the model must somehow be expressed using recursive functions.

However, in computability theory there is also the concept type-II computable functions used in the field of “constructive analysis”, “computable analysis”. This is based on the idea that for instance for specifying computable real numbers as used in physics, an algorithm may work not just on single natural numbers, but indefinitely on sequences of them, producing output that is in each step a finite, but in each next step a more accurate approximation.

!include computable mathematics – table

This concept of type-II computability is arguably closer to actual practice in physics.

Of course there is a wide-spread (but of course controversial) vague speculation (often justified by alluding to expected implications of quantum gravity on the true microscopic nature of spacetime and sometimes formalized in terms of cellular automata, e.g. Zuse 67) that in some sense the observable universe is fundamentally “finite”, so that in the end computability is a non-issue in physics as one is really operating on a large but finite set of states.

However, since fundamental physics is quantum physics and since quantum mechanics with its wave functions, Hilbert spaces and probability amplitudes invokes (functional) analysis and hence non-finite mathematics even when describing the minimum of a physical system with only two possible configurations (a “qbit”) a strict finitism perspective on fundamental physics runs into severe problems and concepts of computable analysis would seem to be necessary for discussing computability in physics.

This issue of computable *quantum* physics has only more recently been considered in (Streicher 12), where it is shown that at least a fair bit of the Hilbert space technology of quantum mechanics/quantum logic sits inside the function realizability topos $RT(\mathcal{K}_2)$.

I have started something at *computability*.

Mainly I was after putting some terms in organized context. That has now become

which I have included under “Related concepts” in the relevant entries.

]]>created a minimum at *computable real number*, for the moment just so as to record the references with section numbers as given there.