PDA 七元組（seven-tuple）
一旦掌握了直覺——有限控制加上一個堆疊——就把整台機器精確寫成一份七部分的配方。下推自動機是一個七元組 (Q, Σ, Γ, δ, q0, Z0, F)。和 DFA 的五個部分相比，PDA 恰好多加了描述堆疊的兩項材料，這很令人滿意：新的能力正來自兩個新零件，僅此而已。
逐一讀這七個部分：Q 是狀態的有限集合（即控制）；Σ（Sigma）是輸入字母表，即機器讀取的字母；Γ（Gamma）是堆疊字母表，即它可推入與彈出的符號；δ（delta）是轉移函數，這份規則手冊規定：給定一個狀態、一個輸入符號（或 ε）、以及堆疊最上面的符號，允許哪些動作；q0 ∈ Q 是起始狀態；Z0 ∈ Γ 是開始時就在堆疊上的起始堆疊符號；而 F 是 Q 的子集，即接受（終止）狀態的集合，在機器以終止狀態接受時使用。前五項與 DFA 相對應；Γ 與 Z0 是真正新增的堆疊材料，而 δ 升級為會查看並改寫堆疊頂端。
為什麼非要這個形式化元組不可？因為精確才能讓我們「證明」事情——證明 PDA 恰好辨識上下文無關語言、兩種接受模式等價、文法可轉成 PDA。要留意一個形狀細節：δ 回傳的是動作的「集合」（PDA 一般是非確定性的），而每個動作是一對（下一個狀態，要推入的堆疊符號串）。那個串可以為空（純彈出）、為單一符號（替換），或為數個（彈出後再推入更多）。
一台 a^n b^n 的 PDA：Q = {q0, q1}，Σ = {a, b}，Γ = {X, Z0}，起始 q0，起始堆疊符號 Z0，F = {q0}（輸入讀完且回到 q0 時接受）。δ 在 q0 對每個 a 推入 X，在 q1 對每個 b 彈出 X，依此類推。
(Q, Σ, Γ, δ, q0, Z0, F)：DFA 的五個部分，再加上堆疊字母表 Γ 與起始堆疊符號 Z0。
終止狀態集合 F 只在「以終止狀態接受」時才重要；在「以空堆疊接受」時 F 常為空集或被忽略。相較於 DFA，多出的兩項正是 Γ 與 Z0。