Cardinal Register Machines A cardinal register machine is like an ordinal register machine but with branching based on cardinal equality rather than ordinal equality.  What is the complexity of the halting problem for cardinal register machines (with finite initial values in the registers)?
Is the complexity independent of whether
- at limits, the internal state is set to the initial state versus liminf (the registers always use liminf as ordinals)
- we can test for ordinal equality in addition to cardinal equality
- we have a copy instruction that allows copying register A into register B (without it, we may have to zero B first which affects liminf)?
Also, what if computations were restricted to countable length?
Ordinal register machines are a model of transfinite computation with a finite set of internal states and a finite set of registers that can store arbitrary ordinals.  They are explored in "Computing the Recursive Truth Predicate on Ordinal Register Machines" by Peter Koepke and Ryan Siders.
For readers unfamiliar with ordinal register machines or wondering why we would want the restrictions above, the answer is that cardinal register machines have a natural definition that scarcely makes any use of set theory.
(Mostly) nontechnical definition:
A cardinal register machine is like a finite register machine:
* Finite internal state (i.e. finite set of internal states).
* Finite set of registers.
* The ability to
   - halt
   - zero a register
   - increment: add a new element to a register
   - test whether two registers have the same number of elements
but with a twist:
* The machine can run for a transfinite time. At limit steps,
   - the internal state is set to the initial state
   - each register keeps the elements added since the supremum of times it was zeroed.
Thus, each register stores a set of elements, with the ability to add a new element (elements are never repeated), remove all elements, and test whether two registers have the same (cardinal) number of elements.  At every stage, an element is in a register iff it was added but not removed.
Now, if we label each increment with the ordinal stage when it occurred, then
- the order type of the set of increments in a register equals the ordinal for that register.
- adding an element increments that ordinal
- liminf behavior follows. Since we do not have a copy instruction, the only discontinuity is that if a register was zeroed cofinally often, it is zero in the limit.
This question is in Q/A format as I was able to solve it before posting (with countable length added later), but feel free to contribute additional answers.  For example, an additional answer could have:
* More on bounded time computations.
* The minimum number of registers (and what happens with fewer registers).
* The spectrum of complexities of $Σ_1(\mathrm{Card})$ without the large cardinal assumption.
 A: Unbounded Computations
Independent of the restrictions, the halting problem is $Σ_1(\mathrm{Card})$-complete, where $\mathrm{Card}$ is the cardinality function (and $Σ_1$ is $Σ^V_1$).  Also, there are universal machines: For every $Σ_1(\mathrm{Card})$-predicate $P$ on $ℕ$, there is a cardinal register machine that halts iff $P(n)$ holds, where $n$ is the initial value in the first register.  The minimum number of registers might depend on the restrictions.
To start, we can test whether a condition occurred cofinally often (before the last limit state) by keeping a register nonzero most of the time, but setting it 0 and then 1 when the condition is met.  Thus, we can assume the more conventional liminf internal state at limit ordinals (and allowing that directly may cut down on the required number of registers).
Without an ordinal equality test, the machine will not notice if a register value is replaced with another ordinal of the same cardinality -- even if we replace multiple registers countably many times (without zeroing), and even if we have a copy instruction.
However, we can still simulate ordinal register machines with a predicate for cardinals (initial ordinals), with an ordinal $ω+α$ coded by $ω_α$ (which does not affect finite ordinals).  To convert $ω_α$ into $ω_{α+1}$, copy the register and keep incrementing the register until the copy and the register are no longer equal.  To check whether $α$ is a cardinal given a register $ω_α$: Copy $ω_α$ into register A, using register B to check when |A| has incremented, counting increments in register C, using register D to detect when C becomes a successor cardinal, and also checking whether C became a successor cardinal cofinally often.
Ordinal register machines can simulate arbitrary ordinal computation (without needing a copy/transfer instruction).  See "Computing the Recursive Truth Predicate on Ordinal Register Machines" by Peter Koepke and Ryan Siders.  While the paper does not state it explicitly, their reduction shows that given an oracle (a class of ordinals) $F$, the halting problem for ordinal register machines with $F$ is $Σ_1(F)$-complete.
Thus, the halting problem for cardinal register machines is $Σ_1(\mathrm{Card})$-complete.  If $V=L$, this is $Σ_2$ complete, but under moderate large cardinal axioms, the complexity is in $Δ^1_3$.  Specifically, using the argument in this question, $Σ_1(\mathrm{Card})$ corresponds to $Σ_2$ theory of the minimal inner model with a proper class of measurable cardinals if the sharp for this model exists.
Note: For models where the sharp does not exist, natural questions include whether $Σ_1(\mathrm{Card})$ captures the $Σ_2$ theory of K, and whether in some generic extension of V, it is $Σ_2$-complete.
Countable Length Computations
For countable length computations, there are three possibilities depending on the model.


*

*If we can test for ordinal equality, then these are just ordinal register machines, with $Σ^1_2$ complete halting problem.

*If we can test just for cardinal equality, then with a copy instruction, the complexity is equivalent to Infinite Time Register Machines, defined here.  That paper sets infinite liminf to 0, but that does not affect the expressiveness.  ITRM can compute $Π^1_1$ truth and more.  There are no universal machines; machine with more registers are more powerful.  As far as I know, which complexity class corresponds to ITRM is unknown.

*If we can test just for cardinal equality, then without a copy instruction, the complexity is exactly arithmetical (without universal machines).  While a copy instruction is not needed for unbounded ordinal/cardinal registers, its lack here prevents us from simulating a stack that resets at limits to unchanged variables rather than to 0.
Proof sketch of arithmetical complexity: In one direction, arithmetical formulas can be evaluated recursively, with essentially one register per variable.  In the other direction, for a halting computation, at limit ordinals, at least one register will be $ω$ or 0, at limits of limit ordinals -- two registers, and so on, thus halting before $ω^ω$.  Because the state can be coded by an integer with the transition at the limits arithmetical, if time evolution over $α$-steps has an arithmetic formula, then so does time evolution over $αω$ steps.
