A Relational Derivation of a Functional Program
Graham Hutton · 1992
This article is an introduction to the use of relational calculi in deriving programs. We present a derivation in a relational language of a functional program that adds one bit to a binary number. The resulting program is unsurprising, being the standard ‘column of half–adders’, but the derivation illustrates a number of points about working with relations rather than functions. 1 Ruby Our derivation is made within the relational calculi developed by Jones and Sheeran [14, 15]. Their language, called Ruby, is designed specifically for the derivation of ‘hardware–like ’ programs that denote finite networks of simple primitives. Ruby has been used to derive a number of different kinds of hardware–like programs [13, 22, 23, 16]. Programs in Ruby are built piecewise from smaller programs using a simple set of combining forms. Ruby is not meant as a programming language in its own right, but as a tool for developing and explaining algorithms. Fundamental to Ruby is the use of terse notation; most formulae fit onto a single line. Having compact formulae makes it