Calculating a backtracking algorithm: an exercise in monadic program derivation

TL;DR

This paper presents a derivation of a backtracking algorithm for monadic programs, specifically using equational reasoning to handle state and non-determinism, demonstrated through solving the n-queens puzzle.

Contribution

It develops theorems for transforming scanl to foldr with the state monad and constructs hylomorphisms, aiding monadic program derivation.

Findings

Derived a backtracking algorithm for monadic unfold-based specifications

Developed theorems for converting scanl to foldr with state monad

Successfully applied the method to solve the n-queens puzzle

Abstract

Equational reasoning is among the most important tools that functional programming provides us. Curiously, relatively less attention has been paid to reasoning about monadic programs. In this report we derive a backtracking algorithm for problem specifications that use a monadic unfold to generate possible solutions, which are filtered using a $\mathit{scanl}$-like predicate. We develop theorems that convert a variation of $\mathit{scanl}$ to a $\mathit{foldr}$ that uses the state monad, as well as theorems constructing hylomorphism. The algorithm is used to solve the $n$-queens puzzle, our running example. The aim is to develop theorems and patterns useful for the derivation of monadic programs, focusing on the intricate interaction between state and non-determinism.