LaTeX 中的双线下箭头（\Downarrow）

用途

输出向下的双线箭头，用于程序设计语言语义学中的大步求值。

操作语义学用 e \Downarrow v 表示在大步风格下表达式 e 求值为值 v，这是该符号最主要的技术用途。在图示和逻辑证明中，它可以标记竖直方向的推理步骤。与其他竖直箭头一样，\Downarrow 是定界符，因此 \Big\Downarrow 可以得到更高的版本。不要把它与 \downarrow 混淆，在同一套语义中后者可能表示终止。引入该判断时请说明你的约定。相比之下，小步语义用 \to 或 \longrightarrow 表示单步归约，用 \to^* 表示其自反传递闭包。

最小可编译示例

将其粘贴到空白 .tex 文件中，用 pdfLaTeX、XeLaTeX 或 LuaLaTeX 编译。

\documentclass{article}
\begin{document}
Down Arrow (Double): $\Downarrow$

\[ \frac{e_1 \Downarrow v_1 \quad e_2 \Downarrow v_2}{e_1 + e_2 \Downarrow v} \]
\end{document}

相关符号

• 左右箭头\leftrightarrow
• 双线长右箭头\Longrightarrow
• 长左右箭头\longleftrightarrow
• 双线长左箭头\Longleftarrow
• 上下箭头\updownarrow
• 双线上箭头\Uparrow

常见问题

如何在 LaTeX 中输入双线下箭头？

在数学模式中输入 \Downarrow，例如 $\frac{e_1 \Downarrow v_1 \quad e_2 \Downarrow v_2}{e_1 + e_2 \Downarrow v}$。无需加载任何宏包即可在标准 LaTeX 中使用。

\Downarrow 需要哪个宏包？

不需要。\Downarrow 是标准 LaTeX 的一部分，导言区只需文档类即可编译。

\Downarrow 能在文本模式中使用，还是只能用于数学模式？

只能用于数学模式。在 $...$ 之外，LaTeX 会报错 "Missing $ inserted"，所以在正文中请写 $\Downarrow$。 如果只需要在正文中显示该字形，可以直接粘贴 Unicode 字符 ⇓（需使用 XeLaTeX 或 LuaLaTeX 以及包含该字形的字体）。