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