Monads, Indexes and Transformations

The specification and derivation of substitution for the de Bruijn representation of - terms is used to illustrate programming with a function-sequence monad. The resulting program is improved by interactive program transformation methods into an efficient implementation that uses primitive machine arithmetic. These transformations illustrate new techniques that assist the discovery of the arithmetic structure of the solution. Introduction Substitution is one of many problems in computer science that, once understood in one context, is understood in all contexts. Why, then, must a different substitution function be written for every abstract syntax implemented? This paper shows how to define substitution once and use the monadic structure of the definition to instantiate it on different abstract syntax structures. It also shows how to interactively derive an efficient implementation of substitution from this very abstract definition. Formal methods that support reasoning about free a..