Do "Type-2" Turing machines with infinite length inputs have more computational power? Certain idealizations of a Turing machine yield an increase in computational power, such as an inductive Turing machine, which can (trivially) solve the halting problem if it has an infinite amount of time to run.

A related variation is the "type-2 Turing machine" defined by Weihrauch, which (if I understand correctly) is basically a Turing machine with an infinite-length input, and a write-only output tape for which previous outputs cannot be changed. Such models are useful for describing real computation.

Does this model of computation have more computational power than a standard Turing machine, similar to the inductive one?

I would naively guess yes, since the theory of "type-2 computability" and "type-2 recursion" seems to be distinct from the ordinary theory of computability, and it seems intuitive that anything which is "type-1 computable" should also be "type-2 computable" (but not the other way around). However, I am unsure of all this.

Burgin (2004) seems to suggest this as a model of hypercomputation in his book on "super-recursive algorithms," but as he does not offer a proof of such, I may be misinterpreting.
Type-2 Turing machines are not more powerful than ordinary Turing machines in the sense that any map $\mathbb{N} \to \mathbb{N}$ that can be computed by a type-2 machine can also be computed by an ordinary machine. To see this, suppose a type-2 Turing machine $T$ computes a function $f : \mathbb{N} \to \mathbb{N}$. We can convert $T$ to an ordinary machine by modifying it so that it stops as soon as it writes $f(n)$ on the output (and we can tell when this happens because the output is a single finite number, so it cannot take forever for the machine to produce it).

It is far more interesting to go up one level and compare computability of functionals, which are maps
$$F : \mathbb{N}^\mathbb{N} \to \mathbb{N}$$
that take an infinite sequence of numbers as an input and output a number. Now there is a difference between type 1 and type 2.

Say that a functional $F$ is type-2 computable if there exists a type-2 Turing machine $T$ such that, for any sequence $\alpha \in \mathbb{N}^\mathbb{N}$, when $\alpha$ is written on the input tape and machine $T$ is run, it writes $F(\alpha)$ on the output tape (and terminates).

Say that a functional $F$ is type-1 computable if there exists a type-1 Turing machine $T$ (i.e., an ordinary one), such that, for any computable sequence $\alpha \in \mathbb{N}^\mathbb{N}$, if we write onto the input tape the encoding $n$ of a machine that computes $\alpha$, then $T(n)$ writes $F(\alpha)$ on the output tape (and terminates).

Notice that a type-1 computable functional only accepts computable inputs, whereas a type-2 computable functional accepts all inputs. If we write $\mathcal{R}$ for the set of all computable sequences of numbers (i.e., the total computable functions), then a type-1 computable functional is a map $F : \mathcal{R} \to \mathbb{N}$ computed by some type-1 machine, whereas a type-2 computable functional is a map $F : \mathbb{N}^\mathbb{N} \to \mathbb{N}$ computed by some type-2 machine.

Because $\mathcal{R} \subseteq \mathbb{N}^\mathbb{N}$, we can convert any type-2 functional to a type-1 functional by simply feeding it only computable inputs. We have:


  Theorem: When a type-2 computable functional is restricted to computable inputs, it becomes a type-1 computable functional.


Proof. The theorem is not a complete triviality. The input is presented to a type-2 functional as a sequence, whereas to a type-1 functional it is presented as a description of a Turing machine computing the sequence. So, suppose $F$ is a type-2 functional computed by a type-2 machine~$T$. We convert $T$ to a type-1 machine as follows: when given an input $n$ which described a machine $M$ that computes some $\alpha \in \mathcal{R}$, we simulate an input type for $T$ so that whenever $T$ wants the $k$-th cell of the input, we run $M(k)$ to compute $\alpha(k)$ and give $T$ the answer. $\Box$

Can we go in the other direction? Suppose $F : \mathcal{R} \to \mathbb{N}$ is computed by a type-1 machine $T$. Perhaps we can extend $F$ to all of $\mathbb{N}^\mathbb{N}$ to get a computable $\overline{F} : \mathbb{N}^\mathbb{N} \to \mathbb{N}$ which agrees with $F$ on $\mathcal{R}$? The anwser is negative! (See Exercise 15-40 in H. Rogers Jr. "Theory of Recursive Functions and Effective Computability".)

The moral of the story is this (as I have often repeated on these forums): all known notions of computability of functions from numbers to numbers agree, but notions of computability of functionals do not, and they are incomparable in general.