-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
A TOOL FOR RELATIONAL PROGRAMMERS
---------------------------------
Graham Hutton Erik Meijer Ed Voermans
Chalmers University Utrecht University Eindhoven University
graham@cs.chalmers.se erik@cs.ruu.nl wsinedv@win.tue.nl
21st January, 1994
This note describes an implementation of a decision procedure for
provable equality of terms in an allegory with products. A number of
relational programming languages can be viewed as being founded on
such an algebraic structure, e.g. Ruby [JS92], the Spec calculus
[BVvdW92], and the calculus of Bird and de Moor [BdM92]. The tool is
implemented in Gofer [J92], and is based upon a soundness/completeness
result of Brown and Hutton [BH94]. The Gofer code was originally
developed as a bit of fun, but seems to be practically useful, so we
are making it available to other relational programmers. It is our
hope that the tool will be a useful concrete aid when first learning
about allegories, and of practical use by researchers in verifying
simple allegorical equations without the labour of axiomatic proofs.
This note does not stand alone from [FS90] and [BH94], but is addressed
to those that already have some knowledge of these texts. Feel free
to modify or extend the system for your own use, but we would ask that
you let us know before distributing any modified system.
ALLEGORIES WITH PRODUCTS
------------------------
We briefly recall the algebraic setting of [BH94]. Allegories were
introduced by Freyd in [FS90]. An allegory is a category equipped
with two extra operators (reciprocation and intersection):
R : A -> B, S : B -> C
------------- -----------------------
id_A : A -> A R ; S : A -> C
R : A -> B R : A -> B, S : A -> B
------------ -----------------------
R' : B -> A R n S : A -> B
These operators are subject to a number of axioms (see Appendix).
A partial ordering <= on arrows is defined by R <= S iff R n S = R.
We assume a fixed allegory such that for any two objects A and B,
there is a maximal arrow top_{A,B} in the poset hom(A,B), and that the
maximal arrow is tabulated by a pair of arrows p0_{A,B} and p1_{A,B}
(see Appendix); we write AxB for the source of p0 and p1. These extra
conditions imply pre-tabularity of the allegory.
------------------ ------------------- -------------------
top_{A,B} : A -> B p0_{A,B} : AxB -> A p1_{A,B} : AxB -> B
We also adopt four derived operators (split, product, dom and rng)
R : A -> B, S : A -> C R : A -> B, S : C -> D
----------------------- -----------------------
: A -> BxC RxS : AxC -> BxD
R : A -> B R : A -> B
--------------- ---------------
dom(R) : A -> A rng(R) : B -> B
defined by
= (R ; p0') n (S ; p1') RxS =
dom(R) = id_A n (R ; top_{B,A}) rng(R) = dom(R')
THE THEORY
----------
The basis of the decision procedure is a mapping from terms to
networks. Briefly, a network is made up of nodes and names. A name
is either a basic name (e.g. x,y,z,...) or a pair (x,y) of names.
Basic names are typed, and pairs of names have product types (if x:A
and y:B then (x,y):AxB.) A node is a triple (R,x,y), where R : A -> B
is a primitive arrow, and x:A and y:B are names for the left and right
sides of R. A network is a triple (N,x,y) where N is a set of nodes,
and x and y are the left/right names for the net. A translation
function that maps terms to networks is described in [BH94].
A homomorphism h : (N,x,y) -> (M,a,b) between networks (with sets of
basic names X and Y respectively) is a type preserving function h : X
-> Y (extended to pairs of names) such that hx=a, hy=b, and for each
node (R,l,r) in N there is a node (R,hl,hr) in M.
The main result of [BH94] is a soundness/completeness theorem: two
allegorical terms R and S are provably equal using the axioms if and
only if the nets represented by R and S are mutually homomorphic.
This gives a decision procedure for provable equality: translate the
two terms to networks, and exhaustively search for homomorphisms in
both directions between the two networks. Since terms are finite, the
networks they represent are finite, and hence the search terminates,
although it takes time exponential in the number of names in the
networks. In practice, however, most of the terms of interest are
small, and searching for homomorphisms takes just a few seconds. Lazy
evaluation also helps speed things up, by automatically discarding a
candidate homomorphism when it first fails to work.
THE PRACTICE
------------
The input to the Gofer program is an equation, syntax as follows:
e ::= t = t equality
| t <= t inclusion
| t >= t subsumption
t ::= R | S | T | ... primitives
| id | top | p0 | p1 wiring cells
| t' | t ; t | t n t | (t) allegorical ops
| | t x t | dom t | rng t derived ops
Any sequence of upper-case letters is acceptable as a primitive.
Operator precedence (from highest to lowest) is reciprocation, dom and
rng, product, composition, and intersection. Hence R ; dom S x T' n U
is parsed as (R ; ((dom S) x T')) n U. Both ; and n are associative.
For parsing, x is assumed to associate to the right, e.g. RxSxT is
parsed as Rx(SxT). White-space can be used freely in terms.
The Gofer program does no type checking or type inference on terms:
type subscripts can't be placed on id, top, p0 and p1, and there is no
option to supply the types of primitives R,S,T etc. Sensible results
are only guaranteed for well-typed input. (See next section.)
The system is loaded as follows:
> gofer allegories.gs
Gofer Version 2.28 Copyright (c) Mark P Jones 1991-1993
Reading script file "/usr/pd/lib/Gofer/standard.prelude":
Reading script file "allegories.gs":
Equations are proved using the function "prove":
? prove " ; p0 = R"
net 1 : ([(R,0,1),(S,0,2)],0,1)
net 2 : ([(R,0,1)],0,1)
homo 1-2 : []
homo 2-1 : [(0,0),(1,1)]
Only the inclusion ( ; p0) <= R is TRUE
In the output from prove, net 1 is the network for the left-hand term
of the equation (connector names are numbers 0,1,2,...), net 2 is the
network for the right-hand term, homo 1-2 is a homomorphism from net 1
to net 2 (the empty list [] means that there is no such), and homo 2-1
is a homomorphism from net 2 to net 1 (a homomorphism is shown as a
list of pairs, a pair (a,b) meaning that a is mapped to b.)
Here's an another example (a simple property of dom):
? prove "dom(R) ; R = R"
net 1 : ([(R,0,1),(R,0,2)],0,2)
net 2 : ([(R,0,1)],0,1)
homo 1-2 : [(0,0),(1,1),(2,1)]
homo 2-1 : [(0,0),(1,2)]
The equation (dom R ; R) = R is TRUE
If we try and prove an inclusion (for example, the modular law), then
a homomorphism is only searched for in one direction:
? prove "R;S n T <= (R n T;S') ; S"
net 1 : ([(R,0,1),(S,1,2),(T,0,2)],0,2)
net 2 : ([(R,0,1),(T,0,2),(S,1,2),(S,1,3)],0,3)
homo 2-1 : [(0,0),(1,1),(2,2),(3,2)]
The inclusion ((R ; S) n T) <= ((R n (T ; S')) ; S) is TRUE
Here's an example of an invalid equation:
? prove "R;S = S;R"
net 1 : ([(R,0,1),(S,1,2)],0,2)
net 2 : ([(S,0,1),(R,1,2)],0,2)
homo 1-2 : []
homo 2-1 : []
The equation (R ; S) = (S ; R) is FALSE
PRODUCT TYPES
-------------
If you use primitives that involve product types (e.g. id_{AxB} or R :
AxB -> C), you sometimes have to be careful. For example, even though
id_A x id_B = id_{AxB}, the system can't prove this, because it
doesn't know that the right-hand identity is used on products:
? prove "id x id = id"
net 1 : ([],(0,1),(0,1))
net 2 : ([],0,0)
homo 1-2 : []
homo 2-1 : []
The equation (id x id) = id is FALSE
Consider the inclusion T <= . This is provable from the
axioms, provided T : AxB -> C, i.e. that T takes pairs as input. When
tried on the Gofer system, only the T's in the network for
are forced to return pairs (by being composed with projections), and
so the system is not able to prove the inclusion:
? prove "T <= "
net 1 : ([(T,0,1)],0,1)
net 2 : ([(T,0,(1,2)),(T,0,(3,4))],0,(1,4))
homo 2-1 : []
The inclusion T <= <(T ; p0),(T ; p1)> is FALSE
The solution is to post-compose the remaining T with id x id. Then all
the T's are forced to return pairs, and the inclusion can be proved:
? prove "T ; id x id <= "
net 1 : ([(T,0,(1,2))],0,(1,2))
net 2 : ([(T,0,(1,2)),(T,0,(3,4))],0,(1,4))
homo 2-1 : [(0,0),(1,1),(2,2),(3,1),(4,2)]
The inclusion (T ; (id x id)) <= <(T ; p0),(T ; p1)> is TRUE
Here's another example where the id x id trick is used:
? prove "rng = id x id"
net 1 : ([],(0,0),(0,0))
net 2 : ([],(0,1),(0,1))
homo 1-2 : []
homo 2-1 : [(0,0),(1,0)]
Only the inclusion rng <= (id x id) is TRUE
USER DEFINED OPERATORS
----------------------
This section can be omitted on first reading.
Suppose we are interested in feedback loops. Then we might define a
new operator: given R : AxB -> B, the arrow feed(R) : A -> B obtained
by connecting the output of R to its second input is defined by
feed(R) = p0' ; (R n p1). One approach to handling such new
operators is to modify the parser for terms in the Gofer program. You
need to know about combinator parsers and grammars to do this.
An approach that avoids modifying the parser is to directly construct
values in the datatype "Term" used by the program. For example, the
definition feed t = Wok Exl `Comp` (t `Cap` Exr) appears at the end of
the source code. Details of the type Term can be found at the
beginning of the source. The function "tprove" takes two terms and
tries to prove that they are equal. When using tprove, the
abbreviations r = Cell "R", s = Cell "S", and t = Cell "T" (defined in
the source) are useful. Here is a proof of the modular law using
terms built directly using the constructors of Term.
? tprove ((r `Comp` s) `Cap` t) ((r `Cap` (t `Comp` Wok s)) `Comp` s)
net 1 : ([(R,0,1),(S,1,2),(T,0,2)],0,2)
net 2 : ([(R,0,1),(T,0,2),(S,1,2),(S,1,3)],0,3)
homo 1-2 : []
homo 2-1 : [(0,0),(1,1),(2,2),(3,2)]
Only the inclusion ((R ; S) n T) <= ((R n (T ; S')) ; S) is TRUE
Using the function termify :: String -> Term, some parts of a term can
be built using constructors and other parts can be parsed:
? tprove (feed (termify "'")) Id
net 1 : ([],0,0)
net 2 : ([],0,0)
homo 1-2 : [(0,0)]
homo 2-1 : [(0,0)]
The equation (p0' ; (' n p1)) = id is TRUE
POSSIBLE EXTENSIONS
-------------------
A key aspect of the Gofer program is a function "compile" that maps
terms to networks. We have also implemented a network decompiler,
that maps a network to an allegorical term that represents that
network. The existence of such a mapping proves that the compiler is
surjective, i.e. that every network can be represented as a term.
At present, the program only proves isolated equations. Many
equations that we want to prove have pre-conditions, e.g. that a
primitive R is simple or entire. Such pre-conditions are typically
expressed themselves as allegorical equations; e.g. simplicity of R :
A -> B is expressed by R ; R' <= id_A. If the present system could
be extended to prove Horn formulae (logical formulae of the form
A_1 ^ A_2 ^ ... ^ A_n => A_0, where each A_i is an allegorical
equation), its usefulness would be greatly increased.
Relational languages intended for programming typically provide more
operators on terms than just those of an allegory with products
(e.g. union, disjoint sum, residuation, catamorphisms, etc.) It is a
subject for future research whether the decision procedure can be
extended to handle a larger class of operators.
Type inference on terms is essential for a robust system.
ACKNOWLEDGEMENTS
----------------
Utrecht University funded a visit by Hutton for November '93; the
Gofer program was implemented during this time. Lambert Meertens
suggested a definition for a network decompiler; it was programming
this in Gofer that lead to the idea of building the present tool.
Thanks to Johan Jeuring for careful proof-reading of the manual.
APPENDIX: THE AXIOM SYSTEM
--------------------------
(For all arrows R,S,T of appropriate type)
id_A ; R = R R'' = R
R ; id_B = R (R ; S)' = S' ; R'
R ; (S ; T) = (R ; S) ; T (R n S)' = R' n S'
R n R = R R ; (S n T) <= (R ; S) n (R ; T)
R n S = S n R (R ; S) n T <= (R n (T ; S')) ; S
R n (S n T) = (R n S) n T
R <= top_{A,B}
p0_{A,B}' ; p0_{A,B} = id_A
p1_{A,B}' ; p1_{A,B} = id_B
p0_{A,B}' ; p1_{A,B} = top_{A,B}
(p0_{A,B} ; p0_{A,B}') n (p1_{A,B} ; p1_{A,B}') = id_{AxB}
REFERENCES
----------
[J92] Mark Jones. Introduction to Gofer 2.20. Programming
Research Group, Oxford 1992.
[FS90] Peter Freyd and Andre Scedrov. Categories, Allegories.
North-Holland, 1990.
[BH94] Carolyn Brown and Graham Hutton. Categories, Allegories and
Circuit Design. Proc LICS 1994.
[JS92] Geraint Jones and Mary Sheeran. Designing Arithmetic Circuits
by Refinement in Ruby. In Proc. Second International Conference
on Mathematics of Program Construction, LNCS. Springer-Verlag, 1992.
[BVvdW92] Roland Backhouse, Ed Voermans, and Jaap van der Woude. A
Relational Theory of Datatypes. In Proc. STOP Summer School on
Constructive Algorithmics, Ameland, The Netherlands, September 1992.
[BdM92] Richard Bird and Oege de Moor. From Dynamic Programming to
Greedy Algorithms. In Proc. STOP Summer School on Constructive
Algorithmics, Ameland, The Netherlands, September 1992.
-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=