**2011.06.01** *Part of the library is updated to use universe polymorphism, and it now type checks with Agda 2.2.11. This is a temporary update yet to be finished. The unfinished parts are commented out in Everything.agda.*

An Agda library accompanying the paper Algebra of Programming in Agda: Dependent Types for Relational Program Derivation, developed in co-operation with Hsiang-Shang Ko and Patrik Jansson.

Dependent type theory is rich enough to express that a program satisfies an input/output relational specification, but it could be hard to construct the proof term. On the other hand, *squiggolists* know very well how to show that one relation is included in another by algebraic reasoning. The **AoPA** library allows one to encode Algebra of Programming style program derivation, both functional and relational, in Agda.

### Example

The following is a derivation of insertion sort in progress:

`isort-der : ∃ (\f → ordered? ○ permute ⊒ fun f )`

isort-der = (_ , (

⊒-begin

ordered? ○ permute

⊒⟨ (\vs -> ·-monotonic ordered? (permute-is-fold vs)) ⟩

ordered? ○ foldR combine nil

⊒⟨ foldR-fusion ordered? ins-step ins-base ⟩

foldR (fun (uncurry insert)) nil

⊒⟨ { foldR-to-foldr insert []}0 ⟩

{ fun (foldr insert [])

⊒∎ }1))

`isort : [ Val ] -> [ Val ]`

isort = proj₁ isort-der

The type of `isort-der`

is a proposition that there exists a function `f`

that is contained in `ordered ? ◦ permute`

, a relation mapping a list to one of its ordered permutations. The proof proceeds by derivation from the speciﬁcation towards the algorithm. The ﬁrst step exploits monotonicity of `◦`

and that `permute`

can be expressed as a fold. The second step makes use of relational fold fusion. The shaded areas denote interaction points — fragments of (proof ) code to be completed. The programmer can query Agda for the expected type and the context of the shaded expression. When the proof is completed, an algorithm `isort`

is obtained by extracting the witness of the proposition. It is an executable program that is backed by the type system to meet the speciﬁcation.

The complete program is in the Example directory of the code.

### The Code

The code consists of the following files and folders:

**AlgebraicReasoning**: a number of modules supporting algebraic reasoning. At present we implement our own because the`PreorderReasoning`

module in earlier versions of the Standard Library was not expressive enough for our need. We may adapt to the new Standard Library later.**Data**: defining relational fold, unfold, hylomorphism (using well-founded recursion), the greedy theorem, and the converse-of-a-function theorem, etc, for list and binary tree.**Examples**: currently we have prepared four examples: a functional derivation of the maximum segment sum problem, a relational derivation of insertion sort and quicksort (following the paper Functional Algorithm Design by Richard Bird), and solving an optimisation problem using the greedy theorem.**Relations**: modules defining various properties of relations.**Sets**: a simple encoding of sets, upon with**Relations**are built.

### Download

To grab the latest code, install darcs and check our the code from the repository:

`darcs get http://pc-scm.iis.sinica.edu.tw/repos/AoPA`

**AoPA** makes use of the Standard Library, to install which you will need darcs.