用户:CaffeineP/笔记/Types and Programming Languages (Benjamin C. Pierce)

3 Untyped Arithmetic Expressions

3.2 Syntax

3.2.4 concrete definition of terms

3.2.5 the sets S_i are cumulative

$\begin{matrix} 𝑡 𝑟 𝑢 𝑒 & \Leftrightarrow {\begin{matrix} 𝑡 𝑟 𝑢 𝑒 \Leftrightarrow \emptyset \subseteq {𝗍 𝗋 𝗎 𝖾, 𝖿 𝖺 𝗅 𝗌 𝖾, 0} \Leftrightarrow S_{0} \subseteq S_{1} \\ \forall i \in ℕ (\begin{matrix} S_{i} \subseteq S_{i + 1} & \Rightarrow \forall t \in S_{i + 1} {\begin{matrix} \begin{matrix} t \in {𝗍 𝗋 𝗎 𝖾, 𝖿 𝖺 𝗅 𝗌 𝖾, 0} & \lor \exists t_{1} \in S_{i} t \in {𝗌 𝗎 𝖼 𝖼 t_{1}, 𝗉 𝗋 𝖾 𝖽 t_{1}, 𝗂 𝗌 𝗓 𝖾 𝗋 𝗈 t_{1}} \\ \lor \exists t_{1} \in S_{i}, t_{2} \in S_{i}, t_{3} \in S_{i} t = 𝗂 𝖿 t_{1} 𝗍 𝗁 𝖾 𝗇 t_{2} 𝖾 𝗅 𝗌 𝖾 t_{3} \end{matrix} \\ \forall t_{1} \in S_{i} (𝑡 𝑟 𝑢 𝑒 \Leftrightarrow t_{1} \in S_{i + 1} \Rightarrow {𝗌 𝗎 𝖼 𝖼 t_{1}, 𝗉 𝗋 𝖾 𝖽 t_{1}, 𝗂 𝗌 𝗓 𝖾 𝗋 𝗈 t_{1}} \subseteq S_{i + 2}) \\ \forall t_{1} \in S_{i}, t_{2} \in S_{i}, t_{3} \in S_{i} (𝑡 𝑟 𝑢 𝑒 \Leftrightarrow {t_{1}, t_{2}, t_{3}} \subseteq S_{i + 1} \Rightarrow (𝗂 𝖿 t_{1} 𝗍 𝗁 𝖾 𝗇 t_{2} 𝖾 𝗅 𝗌 𝖾 t_{3}) \in S_{i + 2}) \end{matrix} \\ \Rightarrow S_{i + 1} \subseteq S_{i + 2} \end{matrix}) \end{matrix} \\ \Rightarrow \forall i \in ℕ S_{i} \subseteq S_{i + 1} \end{matrix}$

3.3 Induction on Terms

3.3.4 induction on terms

sketch of proofs:

induction on depth

$\begin{matrix} \forall s \in S (\forall r \in S (𝑑 𝑒 𝑝 𝑡 ℎ r < 𝑑 𝑒 𝑝 𝑡 ℎ s \Rightarrow P r) \Rightarrow P s) & \Leftrightarrow \forall n \in ℕ^{*} (\forall r \in S (𝑑 𝑒 𝑝 𝑡 ℎ r < n \Rightarrow P r) \Rightarrow \forall s \in S (𝑑 𝑒 𝑝 𝑡 ℎ s = n \Rightarrow P s)) \\ \Leftrightarrow \forall n \in ℕ^{*} (\forall m \in ℕ^{*}, m < n, s \in S (𝑑 𝑒 𝑝 𝑡 ℎ s = m \Rightarrow P s) \Rightarrow \forall s \in S (𝑑 𝑒 𝑝 𝑡 ℎ s = n \Rightarrow P s)) \\ \Rightarrow \forall n \in ℕ^{*}, s \in S (𝑑 𝑒 𝑝 𝑡 ℎ s = n \Rightarrow P s) \Leftrightarrow \forall s \in S P s \end{matrix}$

induction on size

$\begin{matrix} \forall s \in S (\forall r \in S (𝑠 𝑖 𝑧 𝑒 r < 𝑠 𝑖 𝑧 𝑒 s \Rightarrow P r) \Rightarrow P s) & \Leftrightarrow \forall n \in ℕ^{*} (\forall r \in S (𝑠 𝑖 𝑧 𝑒 r < n \Rightarrow P r) \Rightarrow \forall s \in S (𝑠 𝑖 𝑧 𝑒 s = n \Rightarrow P s)) \\ \Leftrightarrow \forall n \in ℕ^{*} (\forall m \in ℕ^{*}, m < n, s \in S (𝑠 𝑖 𝑧 𝑒 s = m \Rightarrow P s) \Rightarrow \forall s \in S (𝑠 𝑖 𝑧 𝑒 s = n \Rightarrow P s)) \\ \Rightarrow \forall n \in ℕ^{*}, s \in S (𝑠 𝑖 𝑧 𝑒 s = n \Rightarrow P s) \Leftrightarrow \forall s \in S P s \end{matrix}$

structural induction

$\forall s \in S (\forall r (r is a subterm of s \Rightarrow P r) \Rightarrow P s) \Rightarrow \forall i \in ℕ (\forall j \in ℕ, j < i, s \in S_{j} P s \Rightarrow \forall s \in S_{i} P s) \Rightarrow \forall i \in ℕ, s \in S_{i} P s \Rightarrow \forall s \in S P s$