3

I am interested in reproducing this style of stepwise exposition:

From Bird and de Moor

This particular example is from Bird and de Moor's Algebra of Programming. This style seems to be common in theoretical computer science papers.

I don't know the name of this style, so I can't effectively search for a package that implements it already.

I've been trying solutions with the tabular, alignat and flalign environments, but I'm not really getting anything I like. My biggest issue is that there seem to be two sets of tabs that alternate from line to line.

I'm using amsmath with fleqn.

Advice would be appreciated.

Improve this question

2 Answers 2

Reset to default
2

You can use calculation (provided you fix a couple of things) or define your own environment.

\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}

The error of calculation is to set \mathindent before \begin{document}, whereas amsmath sets it at that point. The code has the necessary fix to make the calculation environment to respect the fleqn math indent.

The showframe package is only used to add a frame around the text block.

enter image description here

Improve this answer
2
  • I realize now that I should have chosen a simpler example. I'm sorry to have made you type it all out. Thank you. Commented Aug 26, 2018 at 20:44
  • 1
    @Timtro It was a good occasion for suggesting a few tricks (\mathit, mainly). Commented Aug 26, 2018 at 20:50
0

It's apparently the style of Wim Feijen. It is implemented in the calculation package as the calculation environment.

Improve this answer

You must log in to answer this question.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.