Equilibrium in a Halting Game Consider the following 2-player game:


Nature randomly picks a program
Each player plays a number in [0, infinity] inclusive in response to nature's move
Take the minimum of the players’ numbers, and run the program for (up to) that many steps (unless both players chose infinity)
If the program halts, the player who played the minimum number gains 1 point. If the program does not halt, that player loses 1 point. Any player who played a non-minimum number receives 0 points, and both players receive 0 if they both play infinity.


(Corner cases may be handled in whatever way best preserves the spirit of the problem - e.g. upper semicontinuity may be helpful.)

The question: does this game possess a computable Nash equilibrium?

Without the computability requirement, each player just plays the exact number of steps in which the program halts (or infinity, if it does not halt). 

If you try the usual diagonalization argument for the halting problem, you'll find that an equilibrium exists in mixed strategies, so the obvious approach does not immediately work. Maybe there's some way to tweak it?

On the other hand, the equivalence of real closed fields means that finite games with computable payoffs have computable equilibria. This game is not finite, but the strategy space is closed and the payoffs computable, so maybe the same trick could be applied with Glicksberg's Theorem or something in that vein? The problem is, without the computability requirement, the equilibrium is in pure strategies, so any attempt to prove existence of a computable equilibrium using existence of a maybe-computable equilibrium has to explain why the equilibrium is downgraded from pure to mixed.

This seems like the sort of problem where people may not have addressed this exact question before, but might have looked at something similar. I haven't been able to turn up much, but if anyone knows of something in spirit, please let me know!

Motivation: there's a common intuition that self-reference is the main block to computability - i.e., that any uncomputable problem somehow embeds self-reference. If a game roughly like this has a computable Nash equilibrium, it would provide evidence for that intuition.

UPDATE: To clarify, the equilibrium should be "computable" in the sense of computable real numbers: the probabilities describing the mixed strategy distribution should be computable to arbitrary precision. (Note that only finitely many probabilities will be above any particular precision cutoff.) This also means that we can sample from an arbitrarily close approximation of the equilibrium strategy.
Even if you have a one-player game there is no computable equilibrium. Consider nature putting probability $1/2^i$ on program $i$. Any computable strategy will achieve some value strictly less than one or you could use it to solve the halting problem. But you can achieve any value less than one by the strategy that for some fixed sufficiently large $t$, simulates nature's program $j$ for $t$ steps and outputs the number of steps it takes program $j$ to halt if $j$ halts in $t$ steps, infinity otherwise.