理论 CS 风格数学步骤

Question

我感兴趣的是重现这种逐步阐述的风格：

这个特殊的例子来自 Bird 和 de Moor 的《编程代数》。这种风格似乎在理论计算机科学论文中很常见。

我不知道这种风格的名字，所以我无法有效地搜索已经实现它的包。

我一直在尝试使用tabular、alignat和flalign环境的解决方案，但并没有得到我想要的结果。我最大的问题是似乎有两组制表符在行与行之间交替出现。

我正在amsmath使用fleqn。

非常感谢您的建议。

Answer 1

您可以使用calculation（只要您修复了几个问题）或定义您自己的环境。

\documentclass[fleqn]{article}
\usepackage{amsmath}
\usepackage{stmaryrd}
\usepackage{calculation}

\usepackage{showframe}

% generic command
\newcommand{\catam}[1]{\llparenthesis#1\rrparenthesis}

% for csproof
\newenvironment{csproof}
 {\begin{equation*}\begin{aligned}}
 {\end{aligned}\end{equation*}}
\newcommand{\pline}[1]{&#1\\}
\newcommand{\eline}[1]{{=}\quad&\quad\{\text{#1}\}\\}

% for calculation
\renewcommand{\Hsep}{0pt}
\makeatletter % fix the error of the package
\AtBeginDocument{\calc@indent\mathindent}
\makeatother

\begin{document}

This equation can be verified as follows:
\begin{csproof}
\pline{\langle\catam{h},\catam{k}\rangle\cdot\alpha}
\eline{split fusion}
\pline{\langle\catam{h}\cdot\alpha,\catam{k}\cdot\alpha\rangle}
\eline{catamorphisms}
\pline{\langle h\cdot\mathsf{F}\catam{h},k\cdot\mathsf{F}\catam{k}\rangle}
\eline{split cancellation (backwards)}
\pline{\langle
  h\cdot\mathsf{F}(\mathit{outl}\cdot\langle\catam{h},\catam{k}\rangle,
  k\cdot\mathsf{F}(\mathit{outr}\cdot\langle\catam{h},\catam{k}\rangle
\rangle}
\eline{$\mathsf{F}$ functor}
\pline{\langle
  h\cdot\mathsf{F}\mathit{outl}\cdot\mathsf{F}\langle\catam{h},\catam{k}\rangle,
  k\cdot\mathsf{F}\mathit{outr}\cdot\mathsf{F}\langle\catam{h},\catam{k}\rangle
\rangle}
\eline{split fusion (backwards)}
\pline{\langle h\cdot\mathsf{F}\mathit{outl},k\cdot\mathsf{F}\mathit{outr}\rangle
  \cdot\langle\catam{h},\catam{k}\rangle}
\end{csproof}

This equation can be verified as follows:
\begin{calculation}
\langle\catam{h},\catam{k}\rangle\cdot\alpha
\step{split fusion}
\langle\catam{h}\cdot\alpha,\catam{k}\cdot\alpha\rangle
\step{catamorphisms}
\langle h\cdot\mathsf{F}\catam{h},k\cdot\mathsf{F}\catam{k}\rangle
\step{split cancellation (backwards)}
\langle
  h\cdot\mathsf{F}(\mathit{outl}\cdot\langle\catam{h},\catam{k}\rangle,
  k\cdot\mathsf{F}(\mathit{outr}\cdot\langle\catam{h},\catam{k}\rangle
\rangle
\step{$\mathsf{F}$ functor}
\langle
  h\cdot\mathsf{F}\mathit{outl}\cdot\mathsf{F}\langle\catam{h},\catam{k}\rangle,
  k\cdot\mathsf{F}\mathit{outr}\cdot\mathsf{F}\langle\catam{h},\catam{k}\rangle
\rangle
\step{split fusion (backwards)}
\langle
  h\cdot\mathsf{F}\mathit{outl},k\cdot\mathsf{F}\mathit{outr}\rangle
  \cdot\langle\catam{h},\catam{k}
\rangle
\end{calculation}

\end{document}

的错误calculation在于\mathindent在 之前设置\begin{document}，而 则amsmath在该点设置它。代码有必要的修复，以使calculation环境尊重fleqn数学缩进。

该showframe包仅用于在文本块周围添加框架。

Answer 2

这显然是 Wim Feijen 的风格。它被实现在计算包作为calculation环境。