Solution (source code)

= Solution

A <Turing machine> has a finite control, an unbounded tape divided into cells over a finite tape <alphabet> including a blank symbol, and a head that reads one cell at a time. For a deterministic <Turing machine>, the current state and scanned symbol determine the replacement symbol, a head move one cell left or right, and the next state. The input occupies finitely many cells initially; all other cells are blank. Distinguished halting states report acceptance or rejection.

A <formal language> is a <decidable language> if some <Turing machine> halts on every input <string>, accepting exactly the members and rejecting all nonmembers:
$$
\boxed{L\text{ is decidable}\iff\exists M\ \forall w,\ M(w)\text{ halts and accepts exactly when }w\in L.}
$$
Halting on the nonmembers is part of the requirement; a machine that merely runs forever on some nonmembers need not decide the <formal language>.