LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-09-12

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Accepting computation histories can be encoded by modified-PCP domino matches

Statement

For every coded deterministic one-tape Turing machine $M$ and every input word $w$ , one can effectively construct a modified-PCP instance $P_{M, w}$ such that $P_{M, w}$ has a match if and only if $M$ has an accepting computation history on $w$ . The construction may be chosen so that every match spells a separator-delimited accepting history before its forced cleanup suffix and uses only start, copier, local-transition, boundary-extension, accepting-cleanup, and terminal tiles.

Facts & Assumptions

Given: A coded deterministic one-tape Turing machine $M$ and an input word $w$ .

[L1]

A modified-PCP solution is a PCP match that starts with the designated first domino, by The modified Post correspondence problem.

[L2]

$M$ accepts $w$ exactly when $M$ has an accepting computation history on $w$ , by Finite computation histories, halting computations, and divergence.

[L3]

The chosen machine coding is effective and gives one finite transition table and one chosen start configuration for the pair $(M, w)$ , by A fixed effective binary encoding of deterministic one-tape Turing machines.

[L4]

For a fixed machine-input pair, accepting computation histories admit an effective configuration coding and form a decidable language, by For a fixed machine and input, valid accepting computation histories form a decidable language.

Proof

technique · direct

1.1

For a concrete version of the effective configuration coding in [L4], tag the finite state and tape alphabets disjointly. For $C = (q, h, t)$ and any padding bound $r \geq \max ({h} \cup supp (t))$ , put $a_{i} : = t (i)$ and encode the padded representative as ${\tilde{C}}^{(r)} : = ▹ a_{0} \dots a_{h - 1} q a_{h} \dots a_{r},$ where $▹$ is a fresh left-end marker. This word contains exactly one state symbol and decodes unambiguously to $C$ even when some final $a_{i}$ are blank; different amounts of trailing blank padding may represent the same configuration. We also permit the right-blank abbreviation $▹ a_{0} \dots a_{h - 1} q$ when $t (h) = ⊔$ and every cell from $h$ onward is blank; it records the same configuration with the scanned blank left implicit. Adjoin a second fresh symbol # as a block separator. Starting with the least explicit bound for $C_{0}$ , the intended history prefix has the form $# {\tilde{C}}_{0}^{(r_{0})} # {\tilde{C}}_{1}^{(r_{1})} # \dots # {\tilde{C}}_{t}^{(r_{t})} # .$

L3L4givenconstruct

2.1

Write a domino as $(u, v)$ with top word $u$ and bottom word $v$ . Let $P_{M, w}$ contain the designated start domino $(#, # {\tilde{C}}_{0}^{(r_{0})} #) .$ Add copier dominoes $(c, c)$ for $c \in Γ \cup {▹, #}$ , but not for state symbols. For every transition $δ (q, a) = (r, b, R)$ add $(q a, b r)$ . Add the boundary-padding domino $(#, ⊔ #)$ : it supplies the newly scanned blank when a right move passes the last displayed tape cell, and otherwise merely permits one additional trailing blank in the next padded representative. For every $δ (q, a) = (r, b, L)$ and $c \in Γ$ add $(c q a, r c b)$ , and add the separate clamped-left domino $(▹ q a, ▹ r b)$ . Finally, for each $c \in Γ \cup {▹}$ add the accepting-cleanup dominoes $(c q_{a c c}, q_{a c c})$ and $(q_{a c c} c, q_{a c c})$ , and add the terminal domino $(q_{a c c} # #, #)$ . These are finitely many pairs of nonempty words and are computed directly from the finite alphabet, transition table, and start configuration in [L3].

L1L3step 1.1construct

3.1

If $M$ has an accepting history $C_{0}, C_{1}, \dots, C_{t}$ , choose padding bounds recursively. Having chosen $r_{j}$ , keep the same bound for $C_{j + 1}$ unless a right move from cell $r_{j}$ requires $r_{j + 1} = r_{j} + 1$ ; in particular, retain a now-trailing blank when a left move erases the last nonblank cell. Begin with the start domino. For each $C_{j} ⊢_{M} C_{j + 1}$ , use copier dominoes up to the head window, the unique right-, interior-left-, or clamped-left transition domino from step 2.1 at that window, copier dominoes after it, and then $(#, #)$ if $r_{j + 1} = r_{j}$ or $(#, ⊔ #)$ if $r_{j + 1} = r_{j} + 1$ . At every separator the top row has thereby copied ${\tilde{C}}_{j}^{(r_{j})} #$ while the bottom row has appended ${\tilde{C}}_{j + 1}^{(r_{j + 1})} #$ , so the bottom remains exactly one padded configuration block ahead. In the final accepting block, repeated whole-block passes use copiers together with $(c q_{a c c}, q_{a c c})$ to delete the symbol immediately left of the accepting state, or with $(q_{a c c} c, q_{a c c})$ to delete the symbol immediately right of it. These passes eventually leave the one-block lag $q_{a c c} #$ , which the terminal domino closes because its top is $q_{a c c} # #$ and its bottom is #. The two full concatenations are then equal, giving a modified-PCP match.

L1L2step 1.1step 2.1construct

3.2

Conversely, let a modified-PCP match be given. Its first domino is the designated start domino by [L1], so the unmatched bottom suffix initially is exactly ${\tilde{C}}_{0}^{(r_{0})} #$ . Induct over the separators subsequently matched by the top row. Copier dominoes cannot copy a state symbol. Before $q_{a c c}$ appears, the unique state symbol in the current block must therefore be consumed by one transition domino from step 2.1. The symbol immediately before it distinguishes an interior left move from the special $▹$ -boundary move. All other tape symbols are copied, while the choice between $(#, #)$ and $(#, ⊔ #)$ either preserves the displayed length or adds one trailing blank. If a right move has put a nonaccepting state just beyond the last displayed cell, choosing $(#, #)$ would leave that state immediately before the separator, where no transition or cleanup top can consume it, so a complete match must choose the boundary-padding tile. If the new state is $q_{a c c}$ , the shorter choice is precisely the right-blank abbreviation from step 1.1. Consequently every pre-cleanup bottom block decodes to the unique configuration $C_{j + 1}$ with $C_{j} ⊢_{M} C_{j + 1}$ , although its harmless trailing-blank padding need not be unique. Cleanup dominoes contain $q_{a c c}$ and cannot begin this suffix before an accepting block has been reached; after they begin, their shorter bottom words and the terminal anchor can remove the remaining offset. Hence every match has a prefix decoding to an accepting computation history of the original machine $M$ on $w$ .

L1L2step 1.1step 2.1induction

4.1

Steps 3.1 and 3.2 prove that $P_{M, w}$ has a match if and only if $M$ has an accepting computation history on $w$ . Step 2.1 constructs its finite domino list effectively from $(M, w)$ .

step 2.1step 3.1step 3.2∎

Depends on

Used by

Dependency tree · two levels

13 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

MIT OpenCourseWare, Lecture 10: Computation History Method (standard reference, not scraped)
John Watrous, Introduction to the Theory of Computing (standard reference, not scraped)
Chris Pollett, CS 154: PCP and Rice's Theorem (standard reference, not scraped)