Computability

The one-state binary incrementer of the lesson starts on the least significant bit of $10111$ (twenty-three). How many steps does it take before it halts?

A Turing machine has $3$ states and the two symbols $0, 1$. Each of its $3 \times 2 = 6$ table entries chooses a symbol to write, a direction (L or R) and a next state, which is one of the $3$ states or halt. How many different tables are there?

Which of these sets are recursively enumerable? (Select all that apply.)

In the proof that $K$ is undecidable we assumed a machine computing the total function $h$. Suppose instead we only had a semi-decider $s$ for $K$: it halts with output $1$ when $\varphi_e(e)\!\downarrow$ and runs forever otherwise. Build $D$ as before (on input $x$: run $s(x)$; if it outputs $1$, loop forever; otherwise halt). What happens?

You want to prove that a new set $B$ is undecidable, using the undecidability of $K$. Which do you need to show?

For which of these properties of an index $e$ does Rice's theorem show that the set of $e$ with the property is undecidable? (Select all that apply.)

In Mathlib, c.eval n is the (partial) result of running program c : Nat.Partrec.Code on input n, and (c.eval n).Dom says that it halts. Which Lean statement says that halting on input n is undecidable?

Write run(machine, max_steps) that simulates a two-symbol Turing machine started in state 0 on a blank tape. machine is a dict mapping (state, symbol) to (write, move, next_state), with move in (-1, 1) and next_state equal to None for halt. Return ("halt", steps, ones) if it halts within max_steps steps (counting the halting step) and ("running", max_steps, ones) otherwise, where ones is the number of 1s on the tape at that moment.

We want to prove for all $n \ge 0$ that the incrementer, started on the binary expansion of $n$ with the head on the last bit, halts with $n + 1$ on the tape after $t(n) + 1$ steps, where $t(n)$ is the number of trailing $1$s. Which induction works?