Abstract

This entry defines the Boustrophedon transform, which can be seen as either a transformation of a sequence of numbers or, equivalently, an exponential generating function. We define it in terms of the Seidel triangle, a number triangle similar to Pascal’s triangle, and then prove the closed form B(f) = (sec + tan)f.

We also define several related sequences, such as: the zigzag numbers, the Entringer numbers, the secand and tangent numbers, and the Euler numbers and Euler polynomials. Various relationships between these sequences are shown.

Reasonably efficient executable algorithms to compute the Boustrophedon transform and the above sequences are also given, including imperative ones for the tangent and secant numbers using Imperative HOL.

BibTeX

@article{Boustrophedon_Transform-AFP,
  author  = {Manuel Eberl},
  title   = {The {B}oustrophedon Transform, the {E}ntringer Numbers, and Related Sequences},
  journal = {Archive of Formal Proofs},
  month   = {October},
  year    = {2024},
  note    = {\url{https://isa-afp.org/entries/Boustrophedon_Transform.html},
             Formal proof development},
  ISSN    = {2150-914x},
}