This paper is a contribution to the meta-theory of systems featuring
syntax with bindings, such as 𝜆-calculi and logics. It provides a
general criterion that targets inductively defined rule-based systems,
enabling for them inductive proofs that leverage Barendregt’s variable
convention of keeping the bound and free variables disjoint. It improves
on the state of the art by (1) achieving high generality in the style of
Knaster–Tarski fixed point definitions (as opposed to imposing syntactic
formats), (2) capturing systems of interest without modifications, and
(3) accommodating infinitary syntax and non-equivariant predicates.
Formal reasoning about the time complexity of algorithms and data
structures is usually done in interactive theorem provers like
Isabelle/HOL. This includes reasoning about amortized time
complexity which looks at the worst case performance over a
series of operations. However, most programs are not written
within a theorem prover and thus use the data structures of the
production language. To verify the correctness it is necessary to
translate the data structures from the production language into the
language of the prover. Such a translation step could introduce errors,
for example due to a mismatch in features between the two languages.
We show how to prove amortized complexity of data structures directly
in Haskell using LiquidHaskell. Besides skipping the translation step,
our approach can also provide a didactic advantage. Learners do not have
to learn an additional language for proofs and can focus on the new
concepts only. For this paper, we do not assume prior knowledge of
amortized complexity as we explain the concepts and apply them in our
first case study, a simple stack with multipop. Moving to more
complicated (and useful) data structures, we show that the same
technique works for binomial heaps which can be used to implement a
priority queue. We also prove amortized complexity bounds for Claessen’s
version of the finger tree, a sequence-like data structure with
constant-time cons/uncons on either end. Finally we discuss the current
limitations of LiquidHaskell that made certain versions of the data
structures not feasible.