the move relation
/ the turnstile symbol is read "yields" /
If an instantaneous description is a snapshot of the machine, the move relation is the rule that says which snapshot can come next. It is written with a turnstile symbol, often typed as |- and read 'yields' or 'moves to': one ID 'yields' another in a single legal step of the machine. It turns the static collection of snapshots into a moving film.
Precisely, one ID yields another when there is a transition in δ (delta) that justifies the change. If δ(q, a, X) allows the move (p, γ), then (q, a w, X β) yields (p, w, γ β): the machine consumed the input symbol a, changed from state q to p, and replaced the top stack symbol X with the string γ, leaving the rest of the input w and the rest of the stack β untouched. An ε-move does the same but consumes no input. Because a PDA is nondeterministic, a single ID may yield several different IDs. We also write the reflexive-transitive closure (|- with a star) to mean 'yields in zero or more steps' — the relation that captures a whole computation, not just one step.
This relation is the workhorse for definitions and proofs. Acceptance by final state is defined as: the start ID yields, in zero or more steps, some ID whose state is in F with all input consumed. Acceptance by empty stack is: the start ID yields some ID with all input consumed and an empty stack. Every theorem about PDAs — equivalence of the two acceptance modes, equivalence with grammars — is ultimately a statement about which IDs the move relation connects.
If δ(q0, a, Z0) = {(q0, X Z0)}, then (q0, ab, Z0) |- (q0, b, X Z0): the machine read a, stayed in q0, and pushed X above Z0. Chaining such single steps gives the whole run.
One ID |- another via a single transition; the starred version means zero-or-more steps.
The move relation is generally NOT a function: from one ID a nondeterministic PDA may yield several IDs at once. A computation is a path through this branching relation, and acceptance asks only that SOME path reaches an accepting ID.