Recursive Definitions of Monadic Functions

TL;DR

This paper introduces a domain-theoretic fixed-point approach for defining recursive monadic functions, simplifying their formulation and automation in imperative programming contexts like Isabelle/HOL.

Contribution

It provides a novel method for defining recursive monadic functions using fixed-points, applicable to option and state-exception monads, with automatic derivation of recursion equations and induction principles.

Findings

Applicable to option and state-exception monads

Allows derivation of recursion equations without preconditions

Enables automatic generation of induction principles

Abstract

Using standard domain-theoretic fixed-points, we present an approach for defining recursive functions that are formulated in monadic style. The method works both in the simple option monad and the state-exception monad of Isabelle/HOL's imperative programming extension, which results in a convenient definition principle for imperative programs, which were previously hard to define. For such monadic functions, the recursion equation can always be derived without preconditions, even if the function is partial. The construction is easy to automate, and convenient induction principles can be derived automatically.