Skip to content
Algebra of Programming in Agda: Dependent Types for Relational Program Derivation
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
AlgebraicReasoning
Data Fix for Agda 2.5.1. Jul 11, 2016
Examples Some quick, temporary fix to get Examples.MSS to work. Jun 24, 2015
Relations Use agda-stdlib PreorderReasoning. May 30, 2016
typeintype Repository migrated from darcs. Jan 7, 2015
.gitignore Made _←_ more level-polymorphic. Apr 1, 2015
Everything.agda
FixedPoint.agda Unique of halo (in progress). May 25, 2015
Makefile Repository migrated from darcs. Jan 7, 2015
README.md Editing README.md. May 18, 2016
Relations.agda Added `foldR-universal-⇐-≑`, `foldR-fun`, `foldR-fold`. Jun 13, 2015
Sets.agda Use agda-stdlib PreorderReasoning. May 30, 2016
aopa.agda-lib

README.md

Algebra of Programming in Agda: Dependent Types for Relational Program Derivation

The AoPA library allows one to encode Algebra of Programming (BdM97) style program derivation, both functional and relational, in Agda.

Since the 90s, the program derivation community has been exploring moving from functions to a relational theory of program calculation, culminating in the work of Bird and de Moor. A problem is specified as a relation that maps inputs to outputs, which allows us not to be over specific about which output to choose when they are equally good, leaving the choices to implementations. The task is to refine the specification into a functional implementation, using algebraic properties.

Meanwhile, the programming language community has been moving toward more reliance on machine-aided program verification. Complex theorems are considered "proved" only if the proof is verified by a theorem prover or a proof assistant.

AoPA allows us to to develop relational proofs, in Agda, in the style of Bird and de Moor. Elements of the relational theory of programs are modelled in the type system of Agda. Calculations are expressed as program terms that, if type-checked, is guaranteed to be correct. In the end of a calculation one may extract a functional program that is proved to respect the relational specification.

Quick 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 specification towards the algorithm. The first 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 specification.

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

Files

The library currently consists of the following folders:

  • Relations: modules defining various relational operators and their properties. These include relational factors, minimum and maximum, monotype factor, Galois connections, and the "shrink" operator of Oliveira (MO11).

  • AlgebraicReasoning: a number of modules supporting algebraic reasoning. We are in the progress of integrating this with the PreorderReasoning module in the Agda Standard Library.

  • Data: defining relational fold, unfold, hylomorphism (using well-founded recursion), the greedy theorem, and the converse-of-a-function theorem, etc, for lists, binary trees, and generic datatypes using polynomial base functors.

  • 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.

History

The earliest version of AoPA was developed by Shin-Cheng Mu, Hsiang-Shang Ko, and Patrik Jansson, accompanying their papers (MKJ08) (MKJ09). The development is currently picked up by Yu-Hsi Chiang and Shin-Cheng Mu. New additions include universe polymorphism, generic datatypes with polymorphic base functors, and theories for developing algorithms from Galois connections (MO11) (CM15).

References

You can’t perform that action at this time.