(* Example of a construction of an ADJUNCTION - The TRANSITIVE CLOSURE of a graph as a FREE ALGEBRA *) (* The free algebra is constructed as a COUNTABLE COPRODUCT generated by a suitable functor F. Termination is determined by the first occurrence of an INITIAL OBJECT. Cocontinuity of F is assumed (at least initial objects and countable coproducts). This construction is applied to the category of graphs represented as parallel pairs of arrows in FinSet. The functor accumulates pairs of composable edges ensuring associativity by representing paths as lists of edges *) exception image_exn and iso_FinSet and iso_Graph; fun tail(nil) = nil | tail(a::s) = s; datatype ('o,'m)Parallel_Pair = pp of 'm * 'm; datatype ('o,'m)Parallel_Pair_Mor = pp_mor of ('o,'m)Parallel_Pair * 'm * ('o,'m)Parallel_Pair; fun Graph(C)(a) = cat( fn pp_mor(s,_,_) => s, fn pp_mor(_,_,t) => t, fn pp(f,g) => pp_mor( pp(f,g),identity(C)(source(C)(f)),pp(f,g)), fn (pp_mor(p,f,q),pp_mor(_,f',q')) => pp_mor(p,compose(C)(f,f'),q') ); fun P(C)(a) = ffunctor( Graph(C)(a), fn pp(f,g) => source(C)(f), fn pp_mor(pp(f,g),p,pp(f',g')) => p, C ); fun coapex(cocone(a,_,_)) = a; fun coapex_mor(cocone_mor(_,f,_)) = f; fun cat_of(cocomplete_cat(C,_)) = C; fun cocomplete_Graph(cC as cocomplete_cat(C,colimit))(a) = let val colim = fn (D as diagram(_,fN,_)) => let val D' = apply_Fun_Diag(P(C)(a),D); val (ccone',univ') = colimit(D'); val p = coapex_mor(univ' (cocone(a,D',fn n=>let val pp(f,g) = fN(n) in f end))) and q = coapex_mor(univ' (cocone(a,D',fn n=>let val pp(f,g) = fN(n) in g end))); val colim_cocone = cocone( pp(p,q), D, fn n => pp_mor(fN(n),sides(ccone')(n),pp(p,q)) ); val universal = fn c' => cocone_mor(colim_cocone, pp_mor(pp(p,q), coapex_mor(univ' (apply_Fun_CoCone(P(C)(a),c'))), coapex(c')), c') in (colim_cocone,universal) end in cocomplete_cat(Graph(C)(a),colim) end; val SetGraph = Graph(FinSet); val cocomplete_SetGraph = cocomplete_Graph(cocomplete_FinSet); datatype ('o,'m)IsoCat = iso_cat of ('o,'m)Cat * ('m -> bool) * ('m -> 'm); fun image_set(set_mor(a,f,b)) = f mapset a; val isoFinSet = let fun is_iso(fm as set_mor(a,f,b)) = (cardinal(a)=cardinal(b)) andalso (cardinal(b)=cardinal(image_set fm)); fun invert(set_mor(a,f,b)) = set_mor( b, fn x => let val y = element_of (a filtered_by (fn z => (f(z)=x))) in y end, a ) in iso_cat(FinSet,is_iso,invert) handle ? => raise iso_FinSet end; fun isoSetGraph(N) = let val iso_cat(_,is_iso,invert) = isoFinSet; fun is_graph_iso(pp_mor(g1,f,g2)) = is_iso(f); fun graph_invert(pp_mor(g1,f,g2)) = pp_mor(g2,invert(f),g1) in iso_cat(SetGraph(N),is_graph_iso,graph_invert) handle ? => raise iso_Graph end; type ('o,'m)Multiple_Coproduct = ('o list) * 'o * ('m list) -> ('o * ('m list) -> 'm); datatype ('o,'m)Multiple_Coproduct_Cat = multiple_coproduct_cat of ('o,'m)Cat * ('o,'m)Multiple_Coproduct; fun initial_coproduct(cC) = let val (i,i_mor) = initial(cC) in (([],i,[]),(fn (a,_) => i_mor(a))) end; fun add(cC)(a,((olist,a',mlist),univ)) = let val ((sum,inj1,inj2),cp_univ) = coproduct(cC)(a,a') in ( (a::olist,sum,inj1::map(fn f =>compose(cat_of cC)(f,inj2))(mlist)), fn (b,g::mlist') => cp_univ(b,g,univ(b,mlist')) ) end; fun iterated_coproduct(cC,iso_cat(C,is_iso,_))(F)(a) = let fun accumulate(aFn,sum) = if is_iso(initial_mor(cC)(aFn)) then sum else accumulate(F ofo aFn, add(cC)(aFn,sum)) in accumulate(a,initial_coproduct(cC)) end; fun free_algebra(cC,isoC)(F)(a) = let val ((_,aT,c),_) = iterated_coproduct(cC,isoC)(F)(a); val (_,univ) = iterated_coproduct(cC,isoC)(F)(F ofo a) in (aT,univ(aT,c)) end; fun edge_composition(lC as complete_cat(C,_))(G as pp(s,t)) = fn (H as pp(s',t')) => let val ((k1,k2),pb_univ) = pullback(lC)(t,s'); val _ = print("--- next iterate under computation --- ") in pp(compose(C)(k1,s),compose(C)(k2,t')) end; fun action_on_morphisms(lC as complete_cat(C,_))(G as pp(s,t)) = fn pp_mor(H as pp(s',t'),f,H1 as pp(s1',t1')) => let val ((k1,k2),pb_univ) = pullback(lC)(t,s'); val ((k1',k2'),pb_univ') = pullback(lC)(t,s1'); val u = pb_univ'(identity(C)(source(C)(s)),compose(C)(k2,f)) in pp_mor(edge_composition(lC)(G)(H),u,edge_composition(lC)(G)(H1)) end; fun Sigma(lC as complete_cat(C,_))(a)(G) = ffunctor( Graph(C)(a), edge_composition(lC)(G), action_on_morphisms(lC)(G), Graph(C)(a) ); fun transitive_close(G as pp(s,t)) = let val N = source(FinSet)(s); val S = Sigma(complete_FinSet)(N)(G) in free_algebra(cocomplete_SetGraph(N),isoSetGraph(N))(S)(G) end; val ex1 = let val E = set [ just("a"),just("b") ]; val N = set [ just("u"),just("v") ]; fun s(just("a")) = just("u") | s(just("b")) = just("u"); fun t(just("a")) = just("v") | t(just("b")) = just("v") in pp(set_mor(E,s,N),set_mor(E,t,N)) end; val ex2 = let val E = set [ just("a"),just("b") ]; val N = set [ just("u"),just("v"),just("w") ]; fun s(just("a")) = just("u") | s(just("b")) = just("v"); fun t(just("a")) = just("v") | t(just("b")) = just("w") in pp(set_mor(E,s,N),set_mor(E,t,N)) end; val ex3 = let val E = set [ just("a"),just("b"),just("c") ]; val N = set [ just("u"),just("v"),just("w"),just("x") ]; fun s(just("a")) = just("u") | s(just("b")) = just("v") | s(just("c")) = just("v"); fun t(just("a")) = just("v") | t(just("b")) = just("w") | t(just("c")) = just("x") in pp(set_mor(E,s,N),set_mor(E,t,N)) end; val ex4 = let val E = set [ just("a"),just("b"),just("c") ]; val N = set [ just("u"),just("v"),just("w"),just("x") ]; fun s(just("a")) = just("u") | s(just("b")) = just("v") | s(just("c")) = just("w"); fun t(just("a")) = just("v") | t(just("b")) = just("w") | t(just("c")) = just("x") in pp(set_mor(E,s,N),set_mor(E,t,N)) end; val example_graph = let val E = set [ just("a"),just("b"),just("c"),just("d"),just("e") ]; val N = set [ just("u"),just("v"),just("w"),just("x"),just("y") ]; fun s(just("a")) = just("u") | s(just("b")) = just("v") | s(just("c")) = just("w") | s(just("d")) = just("w") | s(just("e")) = just("v"); fun t(just("a")) = just("v") | t(just("b")) = just("w") | t(just("c")) = just("x") | t(just("d")) = just("y") | t(just("e")) = just("y") in pp(set_mor(E,s,N),set_mor(E,t,N)) end;