diff --git a/src/categorical_algebra/CSets.jl b/src/categorical_algebra/CSets.jl index 9748bb7ed..ebbe84593 100644 --- a/src/categorical_algebra/CSets.jl +++ b/src/categorical_algebra/CSets.jl @@ -6,7 +6,8 @@ export ACSetTransformation, CSetTransformation, ACSetHomomorphismAlgorithm, BacktrackingSearch, HomomorphismQuery, components, force, is_natural, homomorphism, homomorphisms, is_homomorphic, isomorphism, isomorphisms, is_isomorphic, - generate_json_acset, parse_json_acset, read_json_acset, write_json_acset + generate_json_acset, parse_json_acset, read_json_acset, write_json_acset, + uncurry, curry, ACSetCat using Base.Iterators: flatten using Base.Meta: quot @@ -14,21 +15,24 @@ using AutoHashEquals using JSON using Reexport using Tables +using DataStructures: DefaultDict @reexport using ...CSetDataStructures using ...GAT, ...Present using ...Theories: Category, SchemaDescType, CSetSchemaDescType, attrtype, attrtype_num, attr, adom, acodom, acodom_nums import ...Theories: dom, codom, compose, ⋅, id, - ob, hom, meet, ∧, join, ∨, top, ⊤, bottom, ⊥ + ob, hom, meet, ∧, join, ∨, top, ⊤, bottom, ⊥, curry using ..FreeDiagrams, ..Limits, ..Subobjects, ..FinSets, ..FinCats import ..Limits: limit, colimit, universal, pushout_complement, can_pushout_complement import ..Subobjects: Subobject, SubobjectBiHeytingAlgebra, implies, ⟹, subtract, \, negate, ¬, non, ~ +import ..Categories: is_hom_equal import ..Sets: SetOb, SetFunction, TypeSet import ..FinSets: FinSet, FinFunction, FinDomFunction, force, predicate -import ..FinCats: FinDomFunctor, components, is_natural +import ..FinCats: FinDomFunctor, components, is_natural, FinTransformationMap, + FinDomFunctorMap # Sets interop ############## @@ -139,16 +143,24 @@ end const ACSetDomCat = FinCats.FinCatPresentation{ Symbol, Union{FreeSchema.Ob,FreeSchema.AttrType}, Union{FreeSchema.Hom,FreeSchema.Attr,FreeSchema.AttrType}} +const FinSetCat = TypeCat{SetOb,FinDomFunction{Int}} """ Wrapper type to interpret attributed C-set as a functor. """ @auto_hash_equals struct ACSetFunctor{ACS<:ACSet} <: - Functor{ACSetDomCat,TypeCat{SetOb,FinDomFunction{Int}}} + Functor{ACSetDomCat,FinSetCat} acset::ACS + eqs::Vector{Pair} end -FinDomFunctor(X::ACSet) = ACSetFunctor(X) +FinDomFunctor(X::ACSet; eqs=Pair[]) = ACSetFunctor(X, eqs) -dom(F::ACSetFunctor) = FinCat(Presentation(F.acset)) +function dom(F::ACSetFunctor) + p = Presentation(F.acset) + for (l,r) in F.eqs + add_equation!(p, l, r) + end + FinCat(p) +end codom(F::ACSetFunctor) = TypeCat{SetOb,FinDomFunction{Int}}() Categories.do_ob_map(F::ACSetFunctor, x) = SetOb(F.acset, x) @@ -159,9 +171,10 @@ Categories.do_hom_map(F::ACSetFunctor, f) = SetFunction(F.acset, f) function (::Type{ACS})(F::FinDomFunctor) where ACS <: ACSet X = if ACS isa UnionAll pres = presentation(dom(F)) - ACS{(eltype(ob_map(F, c)) for c in generators(pres, :AttrType))...}() + Base.invokelatest( + ACS{(eltype(ob_map(F, c)) for c in generators(pres, :AttrType))...}) else - ACS() + Base.invokelatest(ACS) end copy_parts!(X, F) return X @@ -236,6 +249,8 @@ end components(α::ACSetTransformation) = α.components force(α::ACSetTransformation) = map_components(force, α) +is_hom_equal(f::ACSetTransformation, g::ACSetTransformation) = + force(f) == force(g) """ Transformation between C-sets. @@ -385,6 +400,17 @@ function is_natural(α::ACSetTransformation{S}) where {S} return true end +function (C::Type{ACS})(F::FinTransformationMap) where ACS <: ACSet + Cd, CCd = C(dom(F)), C(codom(F)) + return CSetTransformation(Cd, CCd; components(F)...) +end + + +FinTransformationMap(f::ACSetTransformation; eqs=Pair[]) = + FinTransformationMap(components(f), + FinDomFunctor(dom(f); eqs=eqs), + FinDomFunctor(codom(f); eqs=eqs)) + # Category of C-sets #################### @@ -773,7 +799,7 @@ function limit(::Type{Tuple{ACS,Hom}}, diagram) where {S, ACS <: StructCSet{S}, Hom <: TightACSetTransformation} limits = map(limit, unpack_diagram(diagram)) Xs = cone_objects(diagram) - Y = ACS() + Y = Base.invokelatest(ACS) limit!(Y, diagram, Xs, limits) end @@ -818,7 +844,7 @@ function colimit(::Type{Tuple{ACS,Hom}}, diagram) where # Colimit of C-set without attributes. colimits = map(colimit, unpack_diagram(diagram)) Xs = cocone_objects(diagram) - Y = ACS() + Y = Base.invokelatest(ACS) for (c, colim) in pairs(colimits) add_parts!(Y, c, length(ob(colim))) end @@ -1134,6 +1160,120 @@ end end...)) end + +# Tensor-hom adjunction (currying of diagrams in C-Set) +####################################################### +const ACSetCat{S} = TypeCat{S, ACSetTransformation} + +""" curry(d::FinFunctor{D, ACSetCat{S}}) where {D,S} +Currying on objects of a functor category +""" +function curry(d::FinFunctor{D, ACSetCat{S}}) where {D,S} + shapelim = product([dom(d), FinCat(Presentation(S))]) + shape_ind, part_ind = legs(shapelim) + asl = apex(shapelim) + omap = Dict(map(ob_generators(asl)) do o + x = ob_map(shape_ind, o) + y = ob_map(part_ind, o) + o => FinSet(ob_map(d, x), Symbol(y)) + end) + + hmap = Dict(map(hom_generators(asl)) do o + x = hom_map(shape_ind, o) + y = hom_map(part_ind, o) + if x isa FreeSchema.Hom{:id} + o => FinFunction(ob_map(d, only(x.args)), Symbol(y)) + elseif y isa FreeSchema.Hom{:id} + o => hom_map(d, x)[Symbol(only(y.args))] + else + error("x $x y $y") + end + end) + + FinDomFunctor(omap,hmap,asl,FinSetCat()) +end + +""" +Uses an example FinDomFunctor (in the original uncurried format). +""" +function uncurry(d::FinDomFunctor{D1, FinSetCat}, + old_d::FinDomFunctor{D2, ACSetCat{S}}) where {D1,D2,S} + # Recover schema for d as a product, not just the apex + shapelim = product([dom(old_d), FinCat(Presentation(S))]) + asl = apex(shapelim) + shape_ind, part_ind = legs(shapelim) + + cset_type = typeof(first(old_d.ob_map)[2]) + omap = Dict(map(ob_generators(dom(old_d))) do o + x = Base.invokelatest(cset_type) + for o_ in ob_generators(asl) + if ob_map(shape_ind, o_) == o + add_parts!(x, Symbol(ob_map(part_ind, o_)), length(ob_map(d, o_))) + end + end + for h in hom_generators(asl) + h_ = hom_map(shape_ind, h) + if h_ == id(o) + set_subpart!(x, Symbol(hom_map(part_ind, h)), collect(hom_map(d, h))) + end + end + o => x + end) + hmap = Dict(map(hom_generators(dom(old_d))) do h + comps = Dict() + for h_ in hom_generators(asl) + if hom_map(shape_ind, h_) == h + comps[Symbol(only(hom_map(part_ind, h_).args))] = hom_map(d, h_) + end + end + dom_, codom_ = [omap[get(h)] for get in [dom, codom]] + h => ACSetTransformation(dom_,codom_; comps...) + end) + FinDomFunctor(omap,hmap,dom(old_d),ACSetCat{S}()) +end + +""" curry(d::FinFunctor{D, ACSetCat{S}}) where {D,S} +Currying on morphisms of a functor category with an ACSetCat as codom +""" +function curry(ϕ::FinTransformationMap{D, ACSetCat{S}}) where {D,S} + cur_d, cur_cd = curry.([dom(ϕ), codom(ϕ)]) + shapelim = product([dom(dom(ϕ)), FinCat(Presentation(S))]) + shape_ind, part_ind = legs(shapelim) + comps = Dict(map(ob_generators(apex(shapelim))) do o + oshape, opart = Symbol(shape_ind(o)), Symbol(part_ind(o)) + Symbol(o) => components(ϕ)[oshape][opart] + end) + FinTransformationMap(comps,cur_d,cur_cd) +end + +""" uncurry(d::FinTransformationMap, old_d::FinTransformationMap{D, ACSetCat{S}}) where {D, S} +Inverse to currying on morphisms of a functor category with an ACSetCat as codom +""" +function uncurry(d::FinTransformationMap, + old_d::FinTransformationMap{D, ACSetCat{S}}) where {D, S} + # Recover schema for d as a product, not just the apex + shapelim = product([dom(dom(old_d)), FinCat(Presentation(S))]) + shape_ind, part_ind = legs(shapelim) + + αcomps = Dict(o => DefaultDict{Symbol,Vector{Int}}(()->Int[]) + for o in keys(components(old_d))) + + for o in (ob_generators(apex(shapelim))) + dic = αcomps[Symbol(ob_map(shape_ind, o))] + dic[Symbol(ob_map(part_ind, o))] = collect(components(d)[Symbol(o)]) + end + + uc_d, uc_cd = [uncurry(get(d), get(old_d)) for get in [dom, codom]] + + α = Dict(map(collect(αcomps)) do (o, comps) + o => ACSetTransformation(ob_map(uc_d, o), + ob_map(uc_cd, o); comps...) + end) + + + FinTransformationMap(α, uc_d, uc_cd) +end + # Serialization ############### diff --git a/src/categorical_algebra/CategoricalAlgebra.jl b/src/categorical_algebra/CategoricalAlgebra.jl index 232ead2a5..5fc78820a 100644 --- a/src/categorical_algebra/CategoricalAlgebra.jl +++ b/src/categorical_algebra/CategoricalAlgebra.jl @@ -13,6 +13,7 @@ include("Matrices.jl") include("FinRelations.jl") include("CSets.jl") include("GraphCategories.jl") +include("Chase.jl") include("Diagrams.jl") include("CommutativeDiagrams.jl") include("CatElements.jl") @@ -32,6 +33,7 @@ include("Slices.jl") @reexport using .CSets @reexport using .CatElements +@reexport using .Chase @reexport using .Diagrams @reexport using .CommutativeDiagrams @reexport using .DataMigrations diff --git a/src/categorical_algebra/Chase.jl b/src/categorical_algebra/Chase.jl new file mode 100644 index 000000000..e0dedc62a --- /dev/null +++ b/src/categorical_algebra/Chase.jl @@ -0,0 +1,451 @@ +module Chase +export ED, chase, chase_crel, chase_step, to_c_rel, from_c_rel, crel_type, + egd, tgd, collage, pres_to_eds, pres_to_cset, extend_morphism + +using ...Theories, ...Present +using ..CSets +using ..FinSets +using ..FinCats +using ..Limits +using ..FreeDiagrams +import ...Theories: dom, codom +import ..Limits: universal + +using Reexport +@reexport using ...CSetDataStructures + +# EDs +##### + +""" +A morphism S->T, encoding an embedded dependency (or trigger). If the pattern S +is matched (via a homomorphism S->I), we demand there exist a morphism T->I (for +some database instance I) that makes the triangle commute in order to satisfy +the dependency (if this is not the case, then the trigger is 'active'). + +Homomorphisms can merge elements and introduce new ones. The former kind are +called "equality generating dependencies" (EGDs) and the latter "tuple +generating dependencies" (TGDs). Any homomorphism can be factored into EGD and +TGD components by, respectively, restricting the codomain to the image or +restricting the domain to the coimage. +""" +struct ED{Ob,Hom} + ST :: Hom#ACSetTransformation +end + +dom(e::ED) = dom(e.ST) +codom(e::ED) = codom(e.ST) +image(f) = equalizer(legs(pushout(f,f))...) +coimage(f) = coequalizer(legs(pullback(f,f))...) + +""" egd(e::ED) +Distill the component of a morphism that merges elements together +""" +egd(e::ED) = factorize(image(e.ST),e.ST) + +""" tgd(e::ED) +Distill the component of a morphism that adds new elements +""" +tgd(e::ED) = factorize(coimage(e.ST), e.ST) +no_change(f) = is_isomorphic(dom(f), codom(f)) # id up to isomorphism + +"""Split a list of EDs into two lists of EGDs and TGDs""" +function split_Σ(Σ::Dict{Symbol,ED{Ob,Hom}} + )::Pair{Dict{Symbol, Hom},Dict{Symbol, Hom}} where {Ob,Hom} + egds, tgds = [Dict{Symbol, Hom}() for _ in 1:2] + for (k, ed) in collect(Σ) + e, t = egd(ed), tgd(ed) + if !no_change(e) + egds[k] = e + end + if !no_change(t) + tgds[k] = t + end + end + egds => tgds +end + +""" +A collage of a functor is a schema encoding the data of the functor +It has the mapping data in addition to injections from the (co)domain. +""" +function collage(F::FinFunctor) + (dF, _) = Xs = [dom(F), codom(F)] + C = coproduct(Xs) + p = presentation(apex(C)) # inherit equations from dom and codom + # Add natural transformations + α = Dict(map(ob_generators(dF)) do o + o => add_generator!(p, Hom(Symbol("α_$o"), o, ob_map(F, o))) + end) + # Add naturality squares + for f in hom_generators(dF) + add_equation!(p, compose(α[dom(dF,f)], hom_map(F,f)), + compose(f, α[codom(dF,f)])) + end + + new_codom = FinCat(p) + ls = map(legs(C)) do l + FinFunctor(l.ob_map, l.hom_map, dom(l), new_codom) + end + Colimit(DiscreteDiagram(Xs), Multicospan(ls)) +end + +""" +Create constraints for enforcing a C-Set schema on a C-Rel instance. + +A presentation implies constraints of foreign keys being functional +(total and unique) in addition to any extra equations. +""" +function pres_to_eds(S::Presentation, name_::Symbol) + crt = crel_type(S, name_) + # Convert equations in presentation in EDs + eds = Dict{String, ACSetTransformation}( + map(enumerate(equations(S))) do (eqnum, (e1,e2)) + d, cd = Symbol.([dom(e1), codom(e1)]) + l, r1, r2 = [Base.invokelatest(crt) for _ in 1:3] + add_part!(l, d) + end1 = add_term!(l, e1) + end2 = add_term!(l, e2) + add_part!(r1, cd) + add_parts!(r2, cd, 2) + rr = homomorphism(r2, r1) + rl = ACSetTransformation(r2, l; Dict([cd => [end1,end2]])...) + "Eq$eqnum" => first(legs(pushout(rl, rr))) + end) + + # morphisms are functional + for f_ in S.generators[:Hom] + d, f, cd = Symbol.([dom(f_), f_, codom(f_)]) + sf, tf = add_srctgt(Symbol(f)) + unique_l, unique_r, total_l = [Base.invokelatest(crt) for _ in 1:3] + # uniqueness: [d d ⟶ cd] ==> [d ⟶ cd] + ld = add_part!(unique_l, d); lcd = add_parts!(unique_l, cd, 2) + add_parts!(unique_l, f, 2; Dict([sf=>[ld], tf=>collect(lcd)])...); + rd1 = add_part!(unique_r, d); rcd1 = add_part!(unique_r, cd) + add_part!(unique_r, f; Dict([sf=>rd1, tf=>rcd1])...); + if d == cd + uni = ACSetTransformation(unique_l, unique_r; + Dict(f=>[1,1], d=>[rd1, rcd1, rcd1])...) + eds["$(f_)_uni"] = uni + else + eds["$(f_)_uni"] = homomorphism(unique_l, unique_r;) + end + # totality: [d] ==> [d ⟶ cd] + add_part!(total_l, d) + tot = ACSetTransformation(total_l, unique_r; Dict(d=>[rd1])...) + eds["$(f_)_total"] = tot + end + + Dict([Symbol(k) => ED{crt, ACSetTransformation}(v) for (k,v) in collect(eds)]) +end + +""" +Modify C-Set representing a pattern to add a term. Assumes morphism begins from +index 1. +""" +function add_term!(t::StructACSet, args::Vector) + i = 1 + for fk in args + d, f, cd = Symbol.([dom(fk), fk, codom(fk)]) + fsrc, ftgt = add_srctgt(f) + new_i = add_part!(t, cd) + add_part!(t, f; Dict([fsrc=>i, ftgt=>new_i])...) + i = new_i + end + return i +end + +add_term!(t::StructACSet, p::HomExpr{:compose}) = add_term!(t, p.args) +add_term!(t::StructACSet, g::HomExpr{:generator}) = add_term!(t, [g]) +add_term!(t::StructACSet, ::HomExpr{:id}) = add_term!(t, []) + +""" +Convert a Presentation to a CSet type. Note this would be improved with +dynamic ACSets. +""" +function pres_to_cset(pres::Presentation, name_::Symbol) + edges = Symbol.(pres.generators[:Hom]) + expr = CSetDataStructures.struct_acset(name_, StructACSet, pres, index=edges) + eval(expr) + return eval(name_) +end + + +# C-Rel: note that (Span-C)-Set is our model for C-Rel +###################################################### + +# Convention for the names of span morphisms +add_srctgt(m) = Symbol("src_$m") => Symbol("tgt_$m") + +""" crel_type(x::StructACSet{S}) where S + +Convert an instance of a C-Set into an Span(C)-Set type. +""" +function crel_type(x::StructACSet{S}) where S + crel_type(Presentation(S), typeof(x).name.name) +end + +function crel_type(S::Presentation, n::Symbol) + name_ = Symbol("rel_$n") + pres = Presentation(FreeSchema) + edges = vcat(add_srctgt.(Symbol.(S.generators[:Hom]))...) + xobs = Dict(map([S.generators[:Ob]...,S.generators[:Hom]...]) do s + s => add_generator!(pres, Ob(FreeSchema, Symbol(s))) + end) + for h in S.generators[:Hom] + hs, ht = dom(h), codom(h) + s, t = add_srctgt(h) + add_generator!(pres, Hom(s, xobs[h], xobs[hs])) + add_generator!(pres, Hom(t, xobs[h], xobs[ht])) + end + expr = CSetDataStructures.struct_acset(name_, StructACSet, pres, index=edges) + eval(expr) + return eval(name_) +end + +""" to_c_rel(I::StructACSet{S}) where S +A functor C-Set -> C-Rel, on objects. Can be applied safely to C-sets with +undefined references. +""" +function to_c_rel(I::StructACSet{S}) where S + J = Base.invokelatest(crel_type(I)) + for o in ob(S) + add_parts!(J, o, nparts(I, o)) + end + for d in hom(S) + hs, ht = add_srctgt(d) + for (i, v) in filter(x->x[2] != 0, collect(enumerate(I[d]))) + n = add_part!(J, d) + set_subpart!(J, n, hs, i) + set_subpart!(J, n, ht, v) + end + end + return J +end + +""" to_c_rel(f::ACSetTransformation) +A functor C-Set -> C-Rel, on morphisms. It simply disregards the morphism data +in C-Rel that keeps track of the span apex objects. +""" +function to_c_rel(f::ACSetTransformation) + d, cd = to_c_rel.([dom(f), codom(f)]) + init = NamedTuple([k => collect(v) for (k, v) in pairs(components(f))]) + homomorphism(d, cd; initial=init) +end + + +""" from_c_rel(J::StructACSet,cset::StructACSet{S}) where S + +A partial functor C-Rel -> C-Set, on objects. + +This fails if a C-Rel morphism is non-unique and returns a C-set with +undefined references if the morphism isn't total (a return flag signals whether +this occured). +""" +function from_c_rel(J::StructACSet,cset::StructACSet{S}) where S + res = Base.invokelatest(typeof(cset)) + for o in ob(S) + add_parts!(res, o, nparts(J, o)) + end + total = true + for (m, s) in zip(hom(S), dom(S)) + msrc, mtgt = add_srctgt(m) + length(J[msrc]) == length(Set(J[msrc])) || error("non-unique $J") + total &= length(J[msrc]) != nparts(J, s) + for (domval, codomval) in zip(J[msrc], J[mtgt]) + set_subpart!(res, domval, m, codomval) + end + end + return res => total +end + +""" from_c_rel(f::ACSetTransformation,cset::StructACSet{S}) where S + +A functor C-Rel -> C-Set, on morphisms. +""" +function from_c_rel(f::ACSetTransformation,cset::StructACSet{S}) where S + (d, dsucc), (cd, cdsucc) = [from_c_rel(x, cset) for x in [dom(f), codom(f)]] + comps = Dict([k=>v for (k,v) in pairs(components(f)) if k ∈ ob(S)]) + ACSetTransformation(d, cd; comps...) => (dsucc && cdsucc) +end + +# Chase +####### + +""" chase(I::Ob, Σ::Dict{Symbol, ED{Ob,Hom}}, n::Int; verbose=false, viz::Union{Nothing, Function}=nothing) where {Ob, Hom} + +Chase a C-Set or C-Rel instance (attributes are tricky - TODO) given a list of +embedded dependencies. This may not terminate, so a bound `n` on the number of +iterations is required. + + [,] + ΣS ⟶ Iₙ +⊕↓ ⋮ (resulting morphism) + ΣT ... Iₙ₊₁ + +There is a copy of S and T for each active trigger. A trigger is a map from S +into the current instance. What makes it 'active' is that there is no morphism +from T to I that makes the triangle commute. + +Each iteration constructs the above pushout square. The result is a morphism, so +that one can keep track of the provenance of elements in the original CSet +instance within the chased result. + +If the initial instance and EDs are all C-sets, then the pushouts can take place +in C-Set (which is more memory efficient). Otherwise, everything is converted to +the Span(C) schema, which is sometimes necessary (for example, migrating data +forward into a cyclic schema). + +Whether or not the result is due to success or timeout is returned as a boolean +flag. + +TODO this algorithm could be made more efficient by keeping track which EDs have +been searched for over which subobjects, there is no need to search for the same +homomorphism again for an unchanging portion of the instance. +""" +function chase(I::Ob, Σ::Dict{Symbol, ED{Ob,Hom}}, n::Int; verbose=false, + viz::Union{Nothing, Function}=nothing) where {Ob, Hom} + Σ_e_t = split_Σ(Σ) + res = id(I) + + for i in 1:n + if verbose + println("\n\nIter $i\n") + show(stdout,"text/plain",(isnothing(viz) ? identity : viz)(codom(res))) + end + next_morphism = chase_step(codom(res), Σ_e_t; verbose=verbose) + if no_change(next_morphism) + return res => true + else + res = compose(res, next_morphism) + end + end + return res => false # failure +end + +""" +`chase` works when both `I` and `Σ` are in C-Set or both are in C-Rel. + +This function wraps `chase` and does the necessary conversions (computing in +C-Rel if *either* the initial instance or EDs are provided in C-Rel), returning +a result morphism in C-Set if the chase terminates. +""" +function chase_crel(I::Ob_, Σ::Dict{Symbol,ED{Ob,Hom}}, n::Int; + I_is_crel::Bool=false, Σ_is_crel::Bool=false, + cset_example::Union{StructACSet,Nothing}=nothing, + verbose=false) where {Ob_, Ob, Hom} + # Process inputs + is_crel = I_is_crel || Σ_is_crel + !(is_crel && isnothing(cset_example)) || error("Need CSet for conversion") + I_rel = (is_crel && !I_is_crel) ? to_c_rel(I) : I + Σ_rel = (is_crel && !Σ_is_crel) ? to_c_rel.(Σ) : Σ + + # Compute the chase + viz(x) = from_c_rel(x, cset_example) + res, succ = chase(I_rel, Σ_rel, n; verbose=verbose) + + # Postprocess results + if !succ + return res => false + end + return (is_crel ? from_c_rel(res, cset_example)[1] : res) => true +end + +""" +Naively determine active triggers of EDs (S->T) by filtering all triggers +(i.e. maps S->I) to see which are active (i.e. there exists no T->I such that +S->T->I = S->I). + +Optionally initialize the homomorphism search to control the chase process. +""" +function active_triggers(I::Ob, Σ::Dict{Symbol, Hom}; init::Union{NamedTuple, Nothing}, + verbose::Bool=false) where {Ob, Hom} + maps = Pair{Hom, Hom}[] + for (name,ed) in collect(Σ) + kw = Dict(isnothing(init) ? [] : [:initial=>init]) + for trigger in homomorphisms(dom(ed), I; kw...) + if isnothing(extend_morphism(trigger, ed)) + if verbose println("\tActive $name") end + push!(maps, trigger => ed) + end + end + end + return maps +end + +""" +Run a single chase step. +""" +function chase_step(I::Ob, Σ::Pair{Dict{Symbol, Hom},Dict{Symbol, Hom}}; + init::Union{NamedTuple, Nothing}=nothing, + verbose::Bool=false, viz::Union{Function,Nothing}=nothing + ) where {Ob,Hom} + Σegd, Σtgd = Σ + + # First fire one round of TGDs + ats = active_triggers(I, Σtgd; init=init, verbose=verbose) + res = isempty(ats) ? id(I) : fire_triggers(ats) # first: fire TGDs + if !isempty(ats) && verbose + println("\tPost TGD instance"); + show(stdout,"text/plain",(isnothing(viz) ? identity : viz)(codom(res))) + end + + # EGDs merely quotient, so this will terminate. + while true + if verbose println("\tEGDs") end + ats = active_triggers(codom(res), Σegd; init=init, verbose=verbose) + res_ = isempty(ats) ? id(codom(res)) : fire_triggers(ats) + if force(res_) == force(id(codom(res))) + return res + else + res = compose(res, res_) + end + end + en +end + +""" +Compute pushout of all EDs in parallel +""" +function fire_triggers(ats) + r_i_maps, r_s_maps = first.(ats), last.(ats) + # Combine each list of morphisms into a single one & take pushout + I_po = pushout(copair(r_i_maps), oplus(r_s_maps)) + return legs(I_po)[1] +end + + +""" extend_morphism(f::ACSetTransformation,g::ACSetTransformation,monic=false)::Union{Nothing, ACSetTransformation} + +Given a span of morphisms, we seek to find a morphism B → C that makes a +commuting triangle if possible. + + B + g ↗ ↘ ? + A ⟶ C + f +""" +function extend_morphism(f::ACSetTransformation, g::ACSetTransformation; + monic=false, many::Bool=false) + dom(f) == dom(g) || error("f and g are not a span: $jf \n$jg") + + init = Dict{Symbol, Dict{Int,Int}}() + for (ob, mapping) in pairs(components(f)) + init_comp = Pair{Int,Int}[] + for i in parts(codom(g), ob) + vs = Set(mapping(preimage(g[ob], i))) + if length(vs) == 1 + push!(init_comp, i => only(vs)) + elseif length(vs) > 1 # no homomorphism possible + return nothing + end + end + init[ob] = Dict(init_comp) + end + h = many ? homomorphisms : homomorphism + h(codom(g), codom(f); initial=NamedTuple(init), monic=monic) +end + + + +end # module \ No newline at end of file diff --git a/src/categorical_algebra/Diagrams.jl b/src/categorical_algebra/Diagrams.jl index 5a0a4ee3e..fb66d8f29 100644 --- a/src/categorical_algebra/Diagrams.jl +++ b/src/categorical_algebra/Diagrams.jl @@ -1,16 +1,24 @@ """ Diagrams in a category and their morphisms. """ module Diagrams -export Diagram, DiagramHom, id, op, co, shape, diagram, shape_map, diagram_map +export Diagram, DiagramHom, id, op, co, shape, diagram, shape_map, diagram_map, + leftkan, lk_universal -using ...GAT -import ...Theories: dom, codom, id, compose, ⋅, ∘, munit +using AutoHashEquals +using DataStructures: DefaultDict + +using ...GAT, ...Present +import ...Theories: dom, codom, id, compose, ⋅, ∘, munit, oplus, otimes using ...Theories: Category, composeH import ..Categories: ob_map, hom_map -using ..FinCats, ..FreeDiagrams -using ..FinCats: mapvals -import ..FinCats: force, collect_ob, collect_hom -import ..Limits: limit, colimit, universal +using ..FinCats, ..FreeDiagrams, ..Chase +using ..FinCats: mapvals, FinTransformationMap +using ..CSets, ..FinSets +import ..FinCats: force, collect_ob, collect_hom, is_natural +import ..Limits: limit, colimit, universal, equalizer, product, Limit, Colimit, + incl, proj, pullback, coproduct, coequalizer, copair, pushout, + AbstractLimit, Product, Coproduct, AbstractColimit, factorize, + create # TODO: Implement these functions more generally, and move elsewhere. @@ -166,6 +174,9 @@ function Base.show(io::IO, f::DiagramHom{T}) where T print(io, ")") end +is_natural(D::DiagramHom; verbose::Bool=false) = + is_functorial(shape_map(D)) && is_natural(diagram_map(D); verbose=verbose) + # Categories of diagrams ######################## @@ -278,4 +289,430 @@ function munit(::Type{DiagramHom{T}}, C::Cat, f; DiagramHom{T}([Pair(j, f)], d, d′) end +# Left Kan extensions of Diagrams in Set or C-set along FinFunctors +################################################################ + +""" leftkan(F::FinFunctor, I::StructACSet, cd::Symbol; n=15, verbose=false) + B +F ↗ η⇑ ↘ LanF(I) + A ⟶ C + I +Computes the left kan extension of I (a functor to Set) by F (a shape functor). +""" +function leftkan(F::FinFunctor, I::StructACSet, cd::Symbol; n=15, verbose=false) + # Assemble chase input using the collage of F as a schema + col = apex(collage(F)) + name, cname = Symbol("collage_F_$cd"), Symbol("cset_collage_F_$cd") + col_eds = pres_to_eds(presentation(col), name) + col_I = Base.invokelatest(crel_type(presentation(col), name)) + col_I_cset = Base.invokelatest(pres_to_cset(presentation(col), cname)) + copy_parts!(col_I, to_c_rel(I)) + + # Run the chase + chase_res_, check = chase_crel(col_I, col_eds, n; I_is_crel=true, + Σ_is_crel=true, cset_example=col_I_cset, verbose=verbose) + check || error("Chase failed to terminate") + chase_res = codom(chase_res_) + + # Project the codom portion of the collage and grab the α components + res = Base.invokelatest(pres_to_cset(presentation(codom(F)), + Symbol("rel_$cd"))) + copy_parts!(res, chase_res) + α = Dict(o=>FinFunction(chase_res, Symbol("α_$o")) + for o in ob_generators(dom(F))) + + # Return result as a DiagramHom{id} + ddom = Diagram(FinDomFunctor(I; eqs=equations(dom(F)))) + dcodom = Diagram(FinDomFunctor(res; eqs=equations(codom(F)))) + DiagramHom{id}(F, α, ddom, dcodom) +end + +""" +Reduce left kan of a functor to C-Set to a computation for a functor into FinSet +Convert result back to a functor into C-Set. +""" +function leftkan(F::FinFunctor{D,CD}, I::FinDomFunctor{D, ACSetCat{S}}, + cd::Symbol; n=15, verbose=false) where {D, CD, S} + Ic = curry(I) + ctype = pres_to_cset(presentation(dom(Ic)), Symbol("random_$cd")) + Ic_ = ctype(Ic) + + # Map from D x S -> CD x S based on map F: D->CD + domprod = product([dom(F), FinCat(Presentation(S))]) + domleg1, domleg2 = legs(domprod) + codomprod = product([codom(F), FinCat(Presentation(S))]) + Fc = universal(codomprod, Multispan([compose(domleg1, F), domleg2])) + + # Compute result for Functors to Set + curr_res = leftkan(Fc, Ic_, Symbol("random2_$cd"); n=n, verbose=verbose) + + # Create a meaningless FinFunctor from CD to the C-Set category for uncurry + cset_rep = last(first(ob_map(I))); cset_hom = id(cset_rep) + fakeob = Dict([o => cset_rep for o in ob_generators(codom(F))]) + fakehom = Dict([o => cset_hom for o in hom_generators(codom(F))]) + cd_finfun = FinDomFunctor(fakeob, fakehom, codom(F),codom(I)) + + # Uncurry result + ucodom = uncurry(diagram(codom(curr_res)), cd_finfun) + αcomps = Dict(o => DefaultDict{Symbol,Vector{Int}}(()->Int[]) + for o in ob_generators(dom(F))) + for o in ob_generators(apex(domprod)) + αcomps[ob_map(domleg1, o)][Symbol(ob_map(domleg2, o))] = collect(diagram_map(curr_res)[o]) + end + FU = compose(F, ucodom) + α = Dict(map(collect(αcomps)) do (o, comps) + o => ACSetTransformation(ob_map(I,o), ob_map(FU, o); comps...) + end) + return DiagramHom{id}(F, α, I, ucodom) +end + +""" +A left kan extension LanF(X) is an initial object in the category of extensions +of X along F (X & F viewed as morphisms in the category of diagrams w/ covariant +transformations). + B B +F ↗ η⇑ ↘ L F ↗ α⇑ ↘ M + A ⟶ C A ⟶ C + X + F⋅L ! + η ↗ ↘ + X ⟶ F⋅M where ∀ a ∈ A: η⋅! = α + α +We don't currently store data in the chase for computing the universal property. +This data is the provenance of each freely added element (for which morphism f +in B did the f_total trigger cause this element to be created?). Instead, we use +an iterative algorithm to recover this information after the fact. +""" +function lk_universal(η::DiagramHom{id,D,CD}, α::DiagramHom{id,D,CD} + ) where {D,CD} + ηα = [η, α] + L, M = diagram.(codom.(ηα)) + B, C = [only(Set(get.([L, M]))) for get in [dom, codom]] + X = only(Set(diagram.(dom.(ηα)))) + A = dom(X) + Fs = force.([x.shape_map for x in ηα]) + F = first(Fs) + all([F_==F for F_ in Fs]) || error("Fs must match") + codom(X) == C || error("bad codom") + + # Constraints on components of the natural transformation we wish to compute + init = Dict([bo => DefaultDict{Symbol,Dict{Int,Int}}( + ()->Dict{Int,Int}()) for bo in Symbol.(ob_generators(B))]) + # Each element a induces constraints + for a in ob_generators(A) + # We don't know ahead of time how many paths F(a)->b we will need to explore + # before we no longer get any new information, so we maintain a stack. + stack = [(Symbol(ob_map(F,a)), α.diagram_map[a], η.diagram_map[a])] + while !isempty(stack) + # Find constraints on a homomorphism codom(η[a]) ---> codom(α[a]) + # or, given : F(a)->b, we have constraints for η[a];F(f) and α[a];F(f) + b,f,g = pop!(stack) + changed = false + for (ob, mapping) in pairs(components(f)) + for i in parts(codom(g), ob) + for v in Set(mapping(preimage(g[ob], i))) + if haskey(init[b][ob],i) + init[b][ob][i] == v || error("Inconsistent") + else + init[b][ob][i] = v + changed |= true + end + end + end + end + if changed + for h in hom_generators(B) + if Symbol(dom(h)) == b + push!(stack, (Symbol(codom(h)), f⋅hom_map(M,h),g⋅hom_map(L,h))) + end + end + end + end + end + + σf = Dict(map(Symbol.(ob_generators(B))) do bo + i = NamedTuple(init[bo]) + hs = homomorphisms(ob_map(L,bo), ob_map(M,bo); initial=i) + Symbol(bo) => only(hs) + end) + + res = FinTransformation(L, M; σf...) + # is_natural(res; verbose=true) || error("res $res") + return res +end + +# (co)Limits in Category of Diagrams +#################################### + +""" +Product of diagrams in the same category. (coproduct for :op morphisms) +""" +function diagram_hom_product(Xs::AbstractVector{<: Diagram{T}}; kw...) where T + + # Collect / validate type information about the input + cod = codom(diagram(first(Xs))) # the category the diagrams are in + is_id = T == id + is_id || T == op || error("Diagrams of type $T not supported") + # Equality of typecat too strict, but in theory this should be checked + # cods = Set([codom(diagram(x)) for x in Xs]) + # length(cods) == 1 || error("Can't take product of diagrams in different cats") + + # Collect data about the product of the shape categories + P = product([dom(diagram(x)) for x in Xs]) + obs, homs = map([ob_map=>ob_generators, hom_map=>hom_generators]) do (F, gen) + [tuple([F(l, g) for l in legs(P)]...) for g in gen(apex(P))] + end; + + # Take (co)products of objects in the underlying category + omap, nat, base_prod = Dict(), Dict(), Dict() + for os in obs + lim = is_id ? product : coproduct + base_prod[os] = p = lim([ob_map(diagram(X), o) for (o, X) in (zip(os, Xs))]) + s = Symbol(os) + omap[s] = apex(p) + nat[s] = legs(p) + end + + hmap = Dict(map(homs) do hs + maps = [hom_map(diagram(X), o) for (o, X) in (zip(hs, Xs))] + Symbol(hs) => (is_id ? otimes : oplus)(maps) + end) + + # Assemble product diagram + apx = Diagram{T}(FinDomFunctor(omap, hmap, apex(P), cod)) + ls = map(enumerate(zip(legs(P), Xs))) do (i, (l, X)) + η = Dict([k=>v[i] for (k,v) in nat]) + src, tgt = is_id ? (apx, X) : (X, apx) + DiagramHom{T}(l, η, src, tgt) + end; + return P, base_prod, Vector{DiagramHom{T}}(ls) +end + +""" +Computes the equalizer (for id morphisms) / coequalizer (for op morphisms) +""" +function diagram_hom_equalizer(fs::AbstractVector{<: DiagramHom{T}}) where T + # Collect / validate type information about the input + X, Y = diagram.(only.(Set.([dom.(fs), codom.(fs)]))); + is_id = T == id + is_id || T == op || error("diagram hom of type $T not supported") + eq, eq_incl = is_id ? (equalizer, incl) : (coequalizer, proj) + cod = codom(diagram(dom(first(fs)))) + # Equality of typecat too strict, but in theory this should be checked + # cods = Set([codom(diagram(x)) for x in Xs]) + # cod = only(Set(vcat([codom.(diagram.([dom(x),codom(x)])) for x in fs]...))) + + # Shape level equalizer + shape_eq = equalizer(shape_map.(fs)) + Eshape = apex(shape_eq) + + # Underlying (co)equalizer on natural transformations + eqs = Dict(map(ob_generators(Eshape)) do o + o=>eq([diagram_map(f)[o] for f in fs]) + end) + η = Dict([o=>eq_incl(e) for (o,e) in collect(eqs)]) + + om_ = Dict([o=>apex(e) for (o,e) in collect(eqs)]) + hm_ = Dict(map(hom_generators(Eshape)) do h + h => compose(η[dom(h)], hom_map(is_id ? X : Y, h)) # TO CONFIRM: don't we need to factorize with η[codom(h)]? + end) + + # Assemble diagram morphism + E = Diagram{T}(FinDomFunctor(om_,hm_,Eshape, cod)) + src, tgt = is_id ? (diagram(E), X) : (Y, diagram(E)) + l = DiagramHom{T}(incl(shape_eq), η, src, tgt) + return shape_eq, eqs, l +end + + +""" +Coproduct of diagrams in the same category. (product for op morphisms) +""" +function diagram_hom_coproduct(Xs::AbstractVector{<: Diagram{T}}; kw...) where {T} + # Collect / validate type information about the input + is_id = T == id + is_id || T == op || error("Diagrams of type $T not supported") + cod = codom(diagram(first(Xs))) # the category the diagrams are in + # Equality of typecat too strict, but in theory this should be checked + # cod = only(Set([codom(diagram(x)) for x in Xs])) + + # Shape level coproduct + hcprod = coproduct(FinCatPresentation[dom(diagram(x)) for x in Xs]) + + # Inclusion of data in underlying category + obs, homs = Dict(), Dict() + for (l, X) in zip(legs(hcprod), Xs) + for (k,v) in ob_map(diagram(X)) + obs[ob_map(l, k)] = v + end + for (k,v) in hom_map(diagram(X)) + homs[hom_map(l, k)] = v + end + end + + # Assemble diagram morphism + apx = Diagram{T}(FinDomFunctor(obs,homs, apex(hcprod), cod)) + ls = map(zip(legs(hcprod), Xs)) do (l, X) + eta = Dict(k => id(v) for (k, v) in ob_map(diagram(X))) + src, tgt = diagram.(is_id ? [X, apx] : [apx, X]) + DiagramHom{T}(l, eta, src, tgt) + end; + return hcprod, Dict(), ls +end + +""" +Coequalizer of diagrams in the same category. (equalizer for op morphisms) +""" +function diagram_hom_coequalizer(fs::AbstractVector{<: DiagramHom{T}}; kw...) where {T} + X, Y = diagram.(only.(Set.([dom.(fs), codom.(fs)]))); + h = Symbol(string(hash(fs))[1:4]) + # Shape level coequalizer + shape_ceq = coequalizer(shape_map.(fs)) + H = proj(shape_ceq) + # Left kan extensions + κ = leftkan(H, Y, Symbol("H$h"); verbose=false) + FH = shape_map(first(fs))⋅H # F⋅H = G⋅H = ... + λ = leftkan(FH, X, Symbol("HF$h"); verbose=false) + αs = [lk_universal(λ, ϕ⋅κ) for ϕ in fs] + # Take coequalizer of universals, but need to convert them to CSet morphisms + # TODO: work out doing coequalizers pointwise without the currying/uncurrying + # This is important to return the coequalizer as a dictionary, + # which is important for implementing the universal property of coequalizers + curried = curry.(αs) + csettypes = [pres_to_cset(presentation(dom(dom(x))), Symbol("x$h")) + for x in curried] + csethoms = [αtype(αc) for (αtype, αc) in zip(csettypes, curried)] + ceq = coequalizer(csethoms) + γ = uncurry(FinTransformationMap(proj(ceq)), first(αs)) + KX = Diagram{T}(codom(γ)) + κγ = Dict([o=> compose(f, components(γ)[Symbol(ob_map(H, o))]) + for (o,f) in components(diagram_map(κ))]) + l = DiagramHom{T}(H, κγ, Diagram{T}(Y), KX) + return shape_ceq, Dict(nothing=>ceq), l +end + +@auto_hash_equals struct DiagLimit{ + Ob,Diagram,LimType<:Union{Limit,Colimit},Cone<:Multispan{Ob} + } <: AbstractLimit{Ob,Diagram} + diagram::Diagram + shapelim::LimType + baselim::Dict + cone::Cone +end + + +@auto_hash_equals struct DiagColimit{ + Ob,Diagram,LimType<:Union{Limit,Colimit},Cocone<:Multicospan{Ob} + } <: AbstractColimit{Ob,Diagram} + diagram::Diagram + shapelim::LimType + baselim::Dict + cocone::Cocone +end + +product(Xs::AbstractVector{<: Diagram{id}}; kw...) = + let r = diagram_hom_product(Xs) + DiagLimit(DiscreteDiagram(Xs), r[1], r[2], Multispan(r[3])) end + +coproduct(Xs::AbstractVector{<: Diagram{id}}; kw...) = + let (sl, dl, csp) = diagram_hom_coproduct(Xs) + DiagColimit(DiscreteDiagram(Xs), sl, dl, Multicospan(csp)) end + +product(Xs::AbstractVector{<: Diagram{op}}; kw...) = + let r = diagram_hom_coproduct(Xs) + DiagLimit(DiscreteDiagram(Xs), r[1], r[2], Multispan(r[3])) end + +coproduct(Xs::AbstractVector{<: Diagram{op}}; kw...) = + let r = diagram_hom_product(Xs) + DiagColimit(DiscreteDiagram(Xs), r[1], r[2], Multicospan(r[3])) end + +equalizer(fs::AbstractVector{<: DiagramHom{id}}) = + let r = diagram_hom_equalizer(fs) + DiagLimit(ParallelMorphisms(fs), r[1], r[2], Multispan([r[3]])) end + +coequalizer(fs::AbstractVector{<: DiagramHom{op}}) = + let r = diagram_hom_equalizer(fs) + DiagColimit(ParallelMorphisms(fs), r[1], r[2], Multicospan([r[3]])) end + +coequalizer(fs::AbstractVector{<: DiagramHom{id}}) = + let r = diagram_hom_coequalizer(fs) + DiagColimit(ParallelMorphisms(fs), r[1], r[2], Multicospan([r[3]])) end + +function pullback(fs::Multicospan{<:Diagram{T}, <: DiagramHom{T}}) where {T} + p = product(Diagram{T}[dom(f) for f in fs]) + equalizer(DiagramHom{T}[compose(l, f) for (l,f) in zip(legs(p), fs)]) +end + +function pushout(fs::Multispan{<:Diagram{T}, <: DiagramHom{T}}) where {T} + cp = coproduct(Diagram{T}[codom(f) for f in fs]) + coequalizer(DiagramHom{T}[compose(f,l) for (l,f) in zip(legs(cp), fs)]) +end + +function universal(p::DiagLimit{<:Diagram{id},<:DiscreteDiagram}, sp::Multispan) + a_p, a_sp = apex.([p, sp]) + s_map = universal(p.shapelim, Multispan(shape_map.(legs(sp)))) + d_map = Dict(map(ob_generators(dom(diagram(a_sp)))) do o + d_tgts = [diagram_map(l)[o] for l in sp] + tgts = tuple([ob_map(shape_map(l),o) for l in sp]...) + o => universal(p.baselim[tgts], Multispan(d_tgts)) + end) + DiagramHom{id}(s_map, d_map, a_sp, a_p) +end + + +function universal(p::DiagLimit{<:Diagram{op},<:DiscreteDiagram}, sp::Multispan) + a_p, a_sp = apex.([p, sp]) + s_map = universal(p.shapelim, Multicospan(shape_map.(legs(sp)))) + d_map = Dict() + for (spl, pl) in zip(legs(sp),legs(p)) + for (k,v) in components(diagram_map(spl)) + d_map[ob_map(shape_map(pl),k)] = v + end + end + DiagramHom{op}(s_map, d_map, a_sp, a_p) +end + +function universal(cp::DiagColimit{<:Diagram{id},<:DiscreteDiagram}, csp::Multicospan) + a_cp, a_csp = apex.([cp, csp]) + s_map = universal(cp.shapelim, Multicospan(shape_map.(legs(csp)))) + d_map = Dict() + for (cspl, cpl) in zip(legs(csp),legs(cp)) + for o in ob_generators(dom(diagram(dom(cpl)))) + d_map[Symbol(ob_map(shape_map(cpl), o))] = diagram_map(cspl)[o] + end + end + DiagramHom{id}(s_map, d_map, a_cp, a_csp) +end + +function universal(p::DiagColimit{<:Diagram{op},<:DiscreteDiagram}, sp::Multicospan) + a_p, a_sp = apex.([p, sp]) + s_map = universal(p.shapelim, Multispan(shape_map.(legs(sp)))) + d_map = Dict(map(ob_generators(dom(diagram(a_sp)))) do o + d_tgts = [diagram_map(l)[o] for l in sp] + tgts = tuple([ob_map(shape_map(l),o) for l in sp]...) + o => universal(p.baselim[tgts], Multicospan(d_tgts)) + end) + DiagramHom{op}(s_map, d_map, a_p, a_sp) +end + +function uni_eq(eq, fs) + f = only(fs) + a_eq = apex(eq) + s_map = universal(eq.shapelim, shape_map(f)) + d_map = Dict(map(collect(ob_map(shape_map(f)))) do (k, v) + k => factorize(eq.baselim[v], diagram_map(f)[k]) + end) + s_map, d_map, a_eq +end + +function universal(eq::DiagLimit{<:Diagram{id},<:ParallelMorphisms}, fs::SMultispan{1}) + s_map, d_map, a_eq = uni_eq(eq, fs) + DiagramHom{id}(s_map, d_map, dom(only(fs)), a_eq) +end + +function universal(eq::DiagColimit{<:Diagram{op},<:ParallelMorphisms}, fs::SMulticospan{1}) + s_map, d_map, a_eq = uni_eq(eq, fs) + DiagramHom{op}(s_map, d_map, a_eq, codom(only(fs))) +end + end diff --git a/src/categorical_algebra/FinCats.jl b/src/categorical_algebra/FinCats.jl index 7e0b612f2..0c262be23 100644 --- a/src/categorical_algebra/FinCats.jl +++ b/src/categorical_algebra/FinCats.jl @@ -13,7 +13,7 @@ module FinCats export FinCat, FinCatGraph, Path, ob_generators, hom_generators, equations, is_discrete, is_free, graph, edges, src, tgt, presentation, FinFunctor, FinDomFunctor, is_functorial, collect_ob, collect_hom, force, - FinTransformation, components, is_natural, is_initial + FinTransformation, components, is_natural, is_initial, FinCatPresentation using AutoHashEquals using Reexport @@ -24,10 +24,10 @@ using DataStructures: IntDisjointSets, in_same_set, num_groups using ...GAT, ...Present, ...Syntax import ...Present: equations using ...Theories: Category, Schema, ObExpr, HomExpr, AttrExpr, AttrTypeExpr -import ...Theories: dom, codom, id, compose, ⋅, ∘ +import ...Theories: dom, codom, id, compose, ⋅, ∘, FreeCategory, Ob, Hom using ...CSetDataStructures, ...Graphs import ...Graphs: edges, src, tgt, enumerate_paths -import ..Categories: ob, hom, ob_map, hom_map, component +import ..Categories: ob, hom, ob_map, hom_map, component, is_hom_equal # Categories ############ @@ -100,6 +100,8 @@ end edges(path::Path) = path.edges src(path::Path) = path.src tgt(path::Path) = path.tgt +src(C::FinCatGraph, i::Int) = src(graph(C), i) +tgt(C::FinCatGraph, i::Int) = tgt(graph(C), i) function Path(g::HasGraph, es::AbstractVector) !isempty(es) || error("Nonempty edge list needed for nontrivial path") @@ -293,8 +295,12 @@ function hom_map(F::FinDomFunctor{<:FinCatPathGraph}, path::Path) end ob_map(F::FinDomFunctor, x::GATExpr{:generator}) = ob_map(F, first(x)) +ob_map(F::FinDomFunctor) = Dict([k=>ob_map(F,k) for k in ob_generators(dom(F))]) + hom_map(F::FinDomFunctor, f::GATExpr{:generator}) = hom_map(F, first(f)) hom_map(F::FinDomFunctor, f::GATExpr{:id}) = id(codom(F), ob_map(F, dom(f))) +hom_map(F::FinDomFunctor) = Dict([ + k=>hom_map(F,k) for k in hom_generators(dom(F))]) function hom_map(F::FinDomFunctor, f::GATExpr{:compose}) D = codom(F) @@ -501,19 +507,31 @@ domains and codomains of the components are checked. See also: [`is_functorial`](@ref). """ -function is_natural(α::FinTransformation; check_equations::Bool=true) - F, G = dom(α), codom(α) +function is_natural(α::FinTransformation; check_equations::Bool=true, + verbose::Bool=false) +F, G = dom(α), codom(α) C, D = dom(F), codom(F) # == dom(G), codom(G) all(ob_generators(C)) do c α_c = α[c] - dom(D, α_c) == ob_map(F,c) && codom(D, α_c) == ob_map(G,c) + res = dom(D, α_c) == ob_map(F,c) && codom(D, α_c) == ob_map(G,c) + if !res && verbose + println("c $c\ndom(D, α_c) $(dom(D, α_c))\nob_map(F,c) $(ob_map(F,c))") + println("codom(D, α_c) $(codom(D, α_c))\nob_map(G,c) $(ob_map(G,c))") + end + res end || return false if check_equations all(hom_generators(C)) do f Ff, Gf = hom_map(F,f), hom_map(G,f) α_c, α_d = α[dom(C,f)], α[codom(C,f)] - is_hom_equal(D, compose(D, α_c, Gf), compose(D, Ff, α_d)) + res = is_hom_equal(D, compose(D, α_c, Gf), compose(D, Ff, α_d)) + if !res && verbose + println("f $f\nFf $Ff\nGf $Gf\nα_c $α_c\nα_d $α_d") + println("\tcompose(D, α_c, Gf) $(compose(D, α_c, Gf))") + println("\tcompose(D, Ff, α_d)) $(compose(D, Ff, α_d)))") + end + res end || return false end diff --git a/src/categorical_algebra/Limits.jl b/src/categorical_algebra/Limits.jl index df242f066..cd162db57 100644 --- a/src/categorical_algebra/Limits.jl +++ b/src/categorical_algebra/Limits.jl @@ -17,13 +17,15 @@ export AbstractLimit, AbstractColimit, Limit, Colimit, using AutoHashEquals using StaticArrays: StaticVector, SVector +using DataStructures: IntDisjointSets, find_root! -using ...GAT, ...Theories +using ...GAT, ...Theories, ...Graphs, ...Present import ...Theories: ob, terminal, product, proj1, proj2, equalizer, incl, initial, coproduct, coproj1, coproj2, coequalizer, proj, delete, create, pair, copair, factorize using ...CSetDataStructures, ..FinCats, ..FreeDiagrams import ..FreeDiagrams: apex, legs +import ..FinCats: FinCatPresentation # Data types for limits ####################### @@ -589,4 +591,335 @@ function universal(colim::BipartiteColimit, cocone::Multicospan) universal(colim, cocone) end +# Limits in category of diagrams +#------------------------------- +""" +Decompose a product morphism into a composition of canonical generators, i.e. +morphisms that have exactly one non-ID component + +Assumes we have a dictionary that takes us, e.g., from a tuple (f: A->B, idₓ) to +the product morphism (f,idₓ): A×X⟶B×X +""" +function product_decompose(f::Vector, hdict::Dict) + curr = id.(dom.(f)) + res, n = [], length(f) + for (i,m) in enumerate(f) + if (m isa HomExpr{:compose}) margs = m.args + elseif (m isa HomExpr{:generator}) margs = [m] + else margs = [] + end + for marg in margs + args = tuple([j == i ? marg : curr[j] for j in 1:n]...) + push!(res, hdict[args]) + end + curr[i] = id(codom(m)) + end + return compose(res) +end + +""" +Product of finitely-presented categories has the cartesian product of ob +generators as its objects. Its morphisms are generated by, for each morphism in +the underlying categories, taking the product of that morphism with the +identity morphism of all objects of all other categories. For example: + + h f g +X->Y multiplied by A->B<-C is: + + (f,idY) (g, idY) + YA -> YB <- YC + (h,idA) | |(h,idB) | (h,idC) + XA -> XB <- XC + (f,idX) (g, idX) + + +For any pair (e.g. f:A->B,h:X->Y), we get a naturality square + (f,idX) + A x X ----> B x X + | | + (id(A),h) | | (id(B),h) + A x Y ---> B x Y + (f,id(Y)) + +For any triple, we get a naturality cube (six naturality squares), and so on. +TODO: figure out whether or not we also require 8 path equations to go from one +corner of the cube to the other, or if that is derivable from the equalities on +the faces of the cube. My intuition is: yes we need these additional equations. +Currently we have no tests that fail due to this. +""" +function product(Xs::AbstractVector{<: FinCatPresentation}; kw...) + # Get cartesian product of obs and hosm + obs = collect(Iterators.product([ob_generators(x) for x in Xs]...))[:] + + homs = vcat(map(enumerate(Xs)) do (i,X) + vcat(map(hom_generators(X)) do h + p = Iterators.product([id.(ob_generators(Y)) for (j,Y) in enumerate(Xs) if j!=i]...) + map(collect.(collect(p)[:])) do hgens + tuple(insert!(Vector{Any}(hgens), i, h)...) + end + end...) + end...) + + obdict = Dict([v=>k for (k,v) in enumerate(obs)]) + + # Create new presentation with tuple-looking names + p = Presentation(FreeSchema) + + ogens = [Ob(FreeSchema, Symbol(o)) for o in obs] + map(ogens) do g add_generator!(p, g) end + hgens = Dict{Any,Any}(map(homs) do hs + src, tgt = map([dom, codom]) do get + ogens[obdict[tuple([get(X, h) for (h, X) in zip(hs,Xs)]...)]] + end + hs => add_generator!(p, Hom(Symbol(hs), src, tgt)) + end) + for (k,v) in zip(obs, ogens) + hgens[tuple(id.(k)...)] = id(v) + end + + # Add naturality squares + for i in 1:(length(Xs)-1) + hgi = hom_generators(Xs[i]) + for j in i+1:length(Xs) + hgj = hom_generators(Xs[j]) + fun(iarg, jarg, args) = map(1:length(Xs)) do k + if k==i iarg elseif k==j jarg else args[k] end end + for hij in Iterators.product(hgi, hgj) + hi, hj = hij + args = fun([nothing], [nothing], [id.(ob_generators(x)) for x in Xs]) + for hs in Iterators.product(args...) + (di, cdi), (dj, cdj) = [id.([dom(x), codom(x)]) for x in hij] + xs = [hi=>dj, cdi=>hj, di=>hj, hi=>cdj] # naturality square + a1,a2,b1,b2 = [product_decompose(fun(x1,x2,hs), hgens) for (x1,x2) in xs] + add_equation!(p, compose(a1,a2), compose(b1,b2)) + end + end + end + end + + # Add equations from base categories + for (i, X) in enumerate(Xs) + for lr in equations(X) + is = [j == i ? [nothing] : id.(ob_generators(x)) + for (j, x) in enumerate(Xs)] + for bkgrnd in Iterators.product(is...) + l_, r_ = map(lr) do t + comps = (t isa HomExpr{:id} || t isa HomExpr{:generator}) ? [t] : t.args + comps_ = map(comps) do comp + hgens[tuple([k==i ? comp : c for (k,c) in enumerate(bkgrnd)]...)] + end + compose(comps_) + end + add_equation!(p, l_, r_) + end + end + end + + # Create projection maps + apx = FinCat(p) + ls = map(enumerate(Xs)) do (i, x) + os, hs = map([obs, homs]) do oldgens + Dict([Symbol(o) => o[i] for o in oldgens]) + end + FinDomFunctor(os, hs, apx, x) + end + Limit(DiscreteDiagram(Xs), Multispan(ls)) +end + +""" +TODO: handle equations by filtering those including symbols not in osyms ∪ hsyms +""" +function equalizer(fs::AbstractVector{<:FinDomFunctor{<:FinCatPresentation}}) + # Check fs are parallel finfunctors + I, _ = only.(Set.([dom.(fs), codom.(fs)])) + + # identify things that maps make equal + Eo, Eh = map(zip([ob_generators, hom_generators], [ob_map, hom_map])) do (g, m) + [x for x in g(I) if length(Set([m(f, x) for f in fs])) == 1] + end + osyms, hsyms = Set.([Symbol.(Eo), Symbol.(Eh)]) + + # Create new sub-presentation of the domain + p = Presentation(FreeSchema) + for g in vcat(Eo,Eh) add_generator!(p, g) end + + # Create inclusion morphism + obs, homs = map([osyms,hsyms]) do syms + Dict{Symbol,Symbol}(s=>s for s in syms) + end + l1 = FinDomFunctor(obs, homs, FinCat(p), I) + Limit(ParallelMorphisms(fs), Multispan([l1])) +end + +""" +Preserves the original name of the inputs if it is unambiguous, otherwise +disambiguates with index in original input. E.g. (A,B)⊔(B,C) → (A,B#1,B#2,C) +""" +function coproduct(Xs::AbstractVector{<: FinCatPresentation}; kw...) + # Collect all generators and identify conflicting names + all_ob = vcat(ob_generators.(Xs)...) + all_hom = vcat(hom_generators.(Xs)...) + conflict_obs = Set([i for i in all_ob if count(==(i), all_ob) > 1]) + conflict_homs = Set([i for i in all_hom if count(==(i), all_hom) > 1]) + + # Create new disjoint union presentation + p = Presentation(FreeSchema) + ogens = Dict(vcat(map(enumerate(Xs)) do (i, X) + map(ob_generators(X)) do o + (i,o) => Ob(FreeSchema, Symbol("$o" * (o ∈ conflict_obs ? "#$i" : ""))) + end + end...)) + map(values(ogens)) do g add_generator!(p, g) end + + hgens = Dict(vcat(map(enumerate(Xs)) do (i, X) + map(hom_generators(X)) do h + n = Symbol("$h" * (h ∈ conflict_homs ? "#$i" : "")) + s, t = ogens[(i, dom(X,h))], ogens[(i, codom(X,h))] + (i,h) => add_generator!(p, Hom(n, s, t)) + end + end...)) + + # Create legs into equationless target to help us project the equations + for (i,x) in enumerate(Xs) + os, hs = map(zip([ob_generators,hom_generators], [ogens,hgens])) do (get, g) + Dict([Symbol(o) => Symbol(g[(i,o)]) for o in get(x)]) + end + l = FinDomFunctor(os, hs, x, FinCat(p)) + for (e1,e2) in equations(x) + add_equation!(p, hom_map(l, e1), hom_map(l, e2)) + end + end + + # Create legs into equationful target + ls = map(enumerate(Xs)) do (i,x) + os, hs = map(zip([ob_generators,hom_generators], [ogens,hgens])) do (get, g) + Dict([Symbol(o) => Symbol(g[(i,o)]) for o in get(x)]) + end + FinDomFunctor(os, hs, x, FinCat(p)) + end + + Colimit(DiscreteDiagram(Xs), Multicospan(ls)) +end + +""" +TODO: handle equations +""" +function coequalizer(fs::AbstractVector{<:FinDomFunctor{<:FinCatPresentation}}) + # Check inputs are parallel finfunctors + I, J = only.(Set.([dom.(fs), codom.(fs)])) + + # Generate equivalence class reps for the generators of codomain + f1 = first(fs) + og, hg = ob_generators, hom_generators + odict, hdict = map(zip([og, hg], [ob_map, hom_map])) do (gen, map_) + class = IntDisjointSets(length(gen(J))) + inds = Dict(v=>k for (k,v) in enumerate(gen(J))) + map(gen(I)) do o + map(fs) do f + union!(class, inds[map_(f1, o)], inds[map_(f, o)]) + end + end + Dict(o => gen(J)[find_root!(class, i)] for (i, o) in enumerate(gen(J))) + end + + # Create presentation from equivalence classes + p = Presentation(FreeSchema) + obs, homs = [Dict() for _ in 1:2] + for i in sort(collect(Set(values(odict))), by=string) + os = sort([string(k) for (k, v) in collect(odict) if v==i]) + g = add_generator!(p, Ob(FreeSchema, Symbol("[$(join(os,","))]"))) + for o in os + obs[Symbol(o)] = g + end + end + for i in sort(collect(Set(values(hdict))), by=string) + hs = sort([k for (k, v) in collect(hdict) if v==i], by=string) + s, t = map([dom, codom]) do get + obs[Symbol(get(J, first(hs)))] + end + g = add_generator!(p, Hom(Symbol("[$(join(string.(hs),","))]"), s, t)) + for h in hs + homs[Symbol(h)] = Symbol(g) + end + end + l1 = FinDomFunctor(obs, homs, J, FinCat(p)) + Colimit(ParallelMorphisms(fs), Multicospan([l1])) +end + + +""" +A generator a that is mapped to generators X,Y,... in the span is matched to the +ob generator (X, Y, ...) in the product. + +An edge f:a->b that is mapped to morphisms α,β,γ in the span is matched to a +composite of hom generators that yields the morphism (α,β,γ) in the product. +This composition sequence starts with (α, id(src(β)), id(src(γ))) and ends with +(id(tgt(α)), id(tgt(β)), γ) +""" +function universal(p::Product{<:FinCat}, sp::Multispan) + a_p, a_sp = apex.([p, sp]) + obs = Dict(map(ob_generators(a_sp)) do o + p_tgts = [ob_map(l, o) for l in legs(sp)] + for po in ob_generators(a_p) + if p_tgts == [ob_map(l, po) for l in legs(p)] + return o => po + end + end + error("o $o (w/ tgts $p_tgts) not found") + end) + homs = Dict(map(hom_generators(a_sp)) do h + doms, codoms = map([dom, codom]) do get + id.([get(codom(l), hom_map(l, h)) for l in legs(sp)]) + end + # Find the morphism generators we want to map to + h_comps = map(enumerate(legs(sp))) do (i, l) + # Identify morphism by what the product maps it to + h_tgt = map(1:length(legs(sp))) do j + if j < i codoms[j] + elseif j == i hom_map(l, h) + else doms[j] + end + end + """ + WARNING: if the hom map component is composite, it won't be found below. + Need to break up compose into components with `product_decompose` + """ + # Locate this morphism based on what it maps to + for ph in vcat(hom_generators(a_p), id.(ob_generators(a_p))) + if h_tgt == [hom_map(l, ph) for l in legs(p)] + return ph + end + end + error("h $h -> htgt $h_tgt not found") + end + h => compose(h_comps) + end) + FinFunctor(obs, homs, a_sp, a_p) +end + + +function universal(cp::Coproduct{<:FinCat}, csp::Multicospan) + a_cp, a_csp = apex.([cp, csp]) + obs, homs = Dict(), Dict() + for (cpl, cspl) in zip(legs(cp),legs(csp)) + for o in ob_generators(dom(cpl)) + obs[ob_map(cpl, o)] = ob_map(cspl, o) + end + for h in hom_generators(dom(cpl)) + homs[hom_map(cpl, h)] = hom_map(cspl, h) + end + end + FinFunctor(obs, homs, a_cp, a_csp) +end + +function universal(eq::Equalizer{<:FinCat}, f::FinDomFunctor) + FinFunctor(ob_map(f), hom_map(f), dom(f), apex(eq)) +end + +function universal(ceq::Coequalizer{<:FinCat}, f::FinDomFunctor) + obs = Dict([ob_map(proj(ceq), k) => v for (k,v) in ob_map(f)]) + homs = Dict([hom_map(proj(ceq), k) => v for (k,v) in hom_map(f)]) + FinFunctor(obs, homs, apex(ceq), codom(f)) +end + end diff --git a/src/core/Present.jl b/src/core/Present.jl index 926f664d3..d45672bbd 100644 --- a/src/core/Present.jl +++ b/src/core/Present.jl @@ -38,6 +38,10 @@ function Presentation{Name}(syntax::Module) where Name end Presentation(syntax::Module) = Presentation{Symbol}(syntax) +Base.hash(pres::Presentation{T,N}, h::UInt) where {T,N} = + hash(T, hash(N, hash(pres.syntax, hash(pres.generators, + hash(pres.equations, h))))) + function Base.:(==)(pres1::Presentation, pres2::Presentation) pres1.syntax == pres2.syntax && pres1.generators == pres2.generators && pres1.equations == pres2.equations diff --git a/test/categorical_algebra/CSets.jl b/test/categorical_algebra/CSets.jl index 108bd6edd..0ecc75a50 100644 --- a/test/categorical_algebra/CSets.jl +++ b/test/categorical_algebra/CSets.jl @@ -476,6 +476,46 @@ A = Subobject(S, X=[3,4,5]) @test ¬Subobject(ι₂) |> force == Subobject(ι₁) @test ~A |> force == ⊤(S) |> force +# FinFunctors +############# +const Grph = ACSetCat{Graph} +g1 = Graph(1) +ar = @acset Graph begin V=2; E=2; src=[1,2]; tgt=[2,2] end +t1 = apex(terminal(Graph)) +t1_ar = homomorphism(t1, ar) +_, g1_arr2 = homomorphisms(g1, ar) + +@present CSpanPres_(FreeSchema) begin + (C1, C2, C3)::Ob; c1::Hom(C1, C2); c2::Hom(C3,C2) +end +CSpan = FinCat(CSpanPres_) + +# Example FinFunctor into Grph +CG_t1ar = FinDomFunctor(Dict(:C1=>t1,:C2=>ar,:C3=>g1), + Dict(:c1=>t1_ar,:c2=>g1_arr2), + CSpan, Grph()); + +# FinFunctor to Grph -> FinFunctor to Set +cspan_graph_ex = curry(CG_t1ar); +# (reversible) +@test uncurry(cspan_graph_ex, CG_t1ar) == CG_t1ar + +"""Convert a FinCat to a CSet type""" +function cset_type(f::FinCat, name_::Symbol) + pres = presentation(f) + edges = Symbol.(pres.generators[:Hom]) + expr = CSetDataStructures.struct_acset(name_, StructACSet, pres, index=edges) + eval(expr) + return eval(name_) +end + +# FinFunctor to Set -> C-Set +cg = cset_type(dom(cspan_graph_ex), :cspangraph) +cg_cset = cg(cspan_graph_ex) + +# C-Set -> FinFunctor to Set -> FinFunctor to Grph +@test uncurry(FinDomFunctor(cg_cset), CG_t1ar) == CG_t1ar + # Serialization ############### diff --git a/test/categorical_algebra/CategoricalAlgebra.jl b/test/categorical_algebra/CategoricalAlgebra.jl index 76740371f..2f1044fea 100644 --- a/test/categorical_algebra/CategoricalAlgebra.jl +++ b/test/categorical_algebra/CategoricalAlgebra.jl @@ -59,5 +59,8 @@ end include("Slices.jl") end +@testset "Chase" begin + include("Chase.jl") +end end diff --git a/test/categorical_algebra/Chase.jl b/test/categorical_algebra/Chase.jl new file mode 100644 index 000000000..f1ae53d6c --- /dev/null +++ b/test/categorical_algebra/Chase.jl @@ -0,0 +1,135 @@ +module TestChase + +using Test +using Catlab.Graphs +using Catlab.CategoricalAlgebra.Chase +using Catlab.Present +using Catlab.Theories +using Catlab.CategoricalAlgebra +using Catlab.Graphs.BasicGraphs: TheoryGraph + +# Factorizing EDs +#---------------- +gED = ED{Graph, ACSetTransformation} + +# We can factor a ED that combines EGD and TGD aspects +etgd_s = path_graph(Graph, 3) +etgd_t = @acset Graph begin + V = 2; E=3; src=[1,1,2]; tgt=[1,2,1] +end +# cset common to both tgd and egd +core = @acset Graph begin V=2; E=2; src=[1,2]; tgt=[2,1] end + +# This adds a self loop to #1 and merges #1/#3 +etgd = gED(ACSetTransformation(etgd_s,etgd_t; V=[1,2,1], E=[2,3])) + +@test is_isomorphic(codom(egd(etgd)), core) # EGD has no extra self-edge +@test collect(egd(etgd)[:V]) == [1,2,1] # but it does merge vertices + +@test is_isomorphic(dom(tgd(etgd)), core) # TGD does not merge +@test codom(tgd(etgd)) == codom(etgd.ST) # but it does add the self edge + + +# School example +#--------------- +@present ThSchool(FreeSchema) begin + (TA, Student, Faculty, Person)::Ob + t_s::Hom(TA, Student) + t_f::Hom(TA, Faculty) + s_p::Hom(Student, Person) + f_p::Hom(Faculty, Person) + + compose(t_s, s_p) == compose(t_f, f_p) +end +@acset_type School(ThSchool) + +# Construct ED to enforce the path equality +ed1 = @acset School begin + TA = 1; Student = 1; Faculty = 1; Person = 2 + t_s = [1]; t_f = [1]; s_p = [1]; f_p = [2] +end +ed2 = @acset School begin + TA = 1 ;Student = 1 ;Faculty = 1 ;Person = 1 + t_s = [1] ;t_f = [1] ;s_p = [1] ;f_p = [1] +end +d = Dict([:TA=>[1], :Student=>[1], :Faculty=>[1], :Person=>[1,1]]) +sED = ED{School, ACSetTransformation} +ed = sED(ACSetTransformation(ed1, ed2; d...)) +# initializing db from an instance with 5 faculty, 4 students, and 2 TAs +# when we freely add elements due to functionality, we get 9 elements in Person +unchased = @acset School begin + TA = 2; Student = 4; Faculty = 5; Person = 9 + t_s = [1,2]; t_f = [1,2]; s_p = [1,2,3,4]; f_p = [5,6,7,8,9] +end +# Because the first two Faculty are the same people as the first two students +# We expect the result to have only 7 people and for f_p[1:2] == s_p[1:2] +expected = @acset School begin + TA = 2; Student = 4; Faculty = 5; Person = 7 + t_s = [1,2]; t_f = [1,2]; s_p = [1,2,3,4]; f_p = [1,2,5,6,7] +end + +chaseres, _ = chase(unchased, Dict(:R=>ed), 1) +@test is_isomorphic(expected, codom(chaseres)) + +# Symmetric digraph example +#-------------------------- + +# Construct ED that symmetrizes arrows +pg = path_graph(Graph, 2) # 1 --> 2 +biarr = deepcopy(pg) # 1 <-> 2 +add_edge!(biarr, 2, 1) +ed = gED(ACSetTransformation(pg, biarr, V=[2,1], E=[2])) + +# Initial instance +tri = path_graph(Graph, 3) +add_edge!(tri, 3, 1) + +# Expected result +sym_tri = deepcopy(tri) +add_edges!(sym_tri, [2,3,1],[1,2,3]) + +# terminates in one step +@test is_isomorphic(sym_tri, codom(first(chase(tri, Dict(:R=>ed), 3)))) +# terminates instantly +@test biarr == codom(first(chase(biarr, Dict(:R=>ed), 3))) + +# Chases that require computation in C-Rel +#----------------------------------------- + +@present ThLoop(FreeSchema) begin + X::Ob + x::Hom(X, X) + compose(x, x, x) == compose(x, x) +end +@acset_type Loop(ThLoop) +LoopRel = crel_type(ThLoop, :Loop) +lED = ED{LoopRel, ACSetTransformation} + +# Constraints to encode that x is a function +unique_l = @acset LoopRel begin X=3; x=2; src_x=[1,1]; tgt_x=[2,3] end +unique_r = @acset LoopRel begin X=2; x=1; src_x=[1]; tgt_x=[2] end +ED_unique = homomorphism(unique_l, unique_r) +total_l = @acset LoopRel begin X=1 end +ED_total = homomorphism(total_l, unique_r) +# x-path of length 3 = x-path of length 2 +three_two_l = @acset LoopRel begin + X=6; x=5; src_x=[1,2,3,1,5]; tgt_x=[2,3,4,5,6] end +three_two_r = @acset LoopRel begin + X=5; x=5; src_x=[1,2,3,1,5]; tgt_x=[2,3,4,5,4] end +ED_three_two = ACSetTransformation(three_two_l, three_two_r; + X=[1,2,3,4,5,4], x=[1,2,3,4,5]) +ΣX = lED.([ED_unique,ED_total,ED_three_two]) + +loop_eds = pres_to_eds(ThLoop, :Loop) # autogenerate from schema +@test loop_eds[:Eq1].ST == ED_three_two +@test loop_eds[:x_total].ST == ED_total +@test loop_eds[:x_uni].ST == ED_unique + +# Compute the chase +res, succ = chase_crel(total_l, loop_eds, 5; I_is_crel=true, Σ_is_crel=true, + cset_example=Loop(), verbose=false) +@test succ +@test codom(res) == @acset Loop begin X=3; x=[2,3,3] end + + +end # module diff --git a/test/categorical_algebra/Diagrams.jl b/test/categorical_algebra/Diagrams.jl index f093774da..c2185b0f9 100644 --- a/test/categorical_algebra/Diagrams.jl +++ b/test/categorical_algebra/Diagrams.jl @@ -3,6 +3,8 @@ using Test using Catlab.Theories, Catlab.Graphs, Catlab.CategoricalAlgebra using Catlab.Graphs.BasicGraphs: TheoryGraph, TheorySymmetricGraph +using Catlab.Present +import Catlab.CategoricalAlgebra.FinCats: is_natural const SchSGraph = TheorySymmetricGraph @@ -77,4 +79,341 @@ d = munit(Diagram{id}, C, :V) f = munit(DiagramHom{id}, C, :src) @test only(components(diagram_map(f))) == TheoryGraph[:src] +# Left Kan +########## + +# Left Kan of diagram in Set (see example docs in test/Chase.jl) +#--------------------------------------------------------------- +@present ThSchool′(FreeSchema) begin + (TA′, Student′, Faculty′)::Ob + t_s′::Hom(TA′, Student′) + t_f′::Hom(TA′, Faculty′) +end + +@present ThSchool(FreeSchema) begin + (TA, Student, Faculty, Person)::Ob + t_s::Hom(TA, Student) + t_f::Hom(TA, Faculty) + s_p::Hom(Student, Person) + f_p::Hom(Faculty, Person) + + compose(t_s, s_p) == compose(t_f, f_p) +end + +SchoolC, SchoolC′ = FinCat.([ThSchool, ThSchool′]) +@acset_type School′(ThSchool′) +@acset_type School(ThSchool) + +F = FinFunctor(Dict(:TA′=>:TA, :Faculty′=>:Faculty, :Student′=>:Student), + Dict(:t_s′=>:t_s,:t_f′=>:t_f), SchoolC′, SchoolC) + +I = @acset School′ begin + TA′=2; Student′=4; Faculty′=5 + t_s′=[1,2]; t_f′=[1,2] +end + +lk = leftkan(F, I, :School) +@test is_natural(lk) + +expected = @acset School begin + TA = 2; Student = 4; Faculty = 5; Person = 7 + t_s = [1,2]; t_f = [1,2]; s_p = [1,2,3,4]; f_p = [1,2,5,6,7] +end + +@test is_isomorphic(expected, School(diagram(codom(lk)))) + +# Left kan of Diagrams in Grph +#----------------------------- + +const Grph = ACSetCat{Graph} + +# Set up example shape categories +@present ThArr(FreeSchema) begin + (A,B)::Ob; f::Hom(A,B) +end +@present ThArr2(FreeSchema) begin + (C,D)::Ob; m::Hom(C,D); n::Hom(D, C); compose(m,n) == id(C) +end +@present ThInv(FreeSchema) begin + (Y)::Ob; f::Hom(Y,Y); compose(f,f) == id(Y) +end +@present ThOne(FreeSchema) begin + (X)::Ob end + +@present ThInv2(FreeSchema) begin + (Y)::Ob; f::Hom(Y,Y); compose(f,f) == f +end + +pres_to_eds(ThInv2, :Inv2) # example of an equation with a :generator term + + +Arr, Arr2, One, Inv = FinCat.([ThArr, ThArr2, ThOne, ThInv]) + +# Set up graph data +two = path_graph(Graph, 2) +ar = @acset Graph begin V=2; E=2; src=[1,2]; tgt=[2,2] end +h1, h2 = homomorphisms(two, ar) # don't send both vertices to #2, or do that + +# Freely adding a right inverse to a C-set transformation: f: A->B +#----------------------------------------------------------------- +F = FinFunctor(Dict(:A=>:C, :B=>:D), Dict(:f=>:m), Arr, Arr2) +# This may require adding things to A. These must then be mapped to B in a +# distinct place, thereby adding to B, too. +I = FinDomFunctor(Dict(:A=>two,:B=>ar),Dict(:f=>h1),Arr,Grph()) +lk = diagram(codom(leftkan(F, I, :X; verbose=false))) +# This homomorphism is injective on vertices. Those can be easily inverted. +# However, V2 in the codomain has a self loop not present in V2 of the domain. +# Therefore the domain has an extra loop added to it. +@test ob_map(lk, :C) == ar +# The new edge ISN'T forced to match to the self loop in the codomain, though +@test ob_map(lk, :D) == @acset Graph begin V=2; E=3; src=[1,2,2]; tgt=2 end + +# This homomorphism sends V1 and V2 to V2 of the codomain. +I = FinDomFunctor(Dict(:A=>two,:B=>ar),Dict(:f=>h2),Arr,Grph()) +lk2 = diagram(codom(leftkan(F, I, :X2; verbose=false))) +@test is_isomorphic(ob_map(lk2, :C), ar) +# TODO: rationalize why this is the result, if it's correct +@test ob_map(lk2, :D) == @acset Graph begin V=3; E=3; src=[1,3,2]; tgt=3 end + +# Freely adding an involution +#---------------------------- +F = FinFunctor(Dict(:X=>:Y),nothing,One,Inv) +# creates a copy of the starting graph, and the involution is a swap function. +I = FinDomFunctor(Dict(:X=>two), nothing, One, Grph()) +lk3_ = leftkan(F, I, :XF; verbose=false) +lk3 = diagram(codom(lk3_)) +@test ob_map(lk3, :Y) == two ⊕ two +@test collect(hom_map(lk3, :f)[:V]) == [3,4,1,2] +@test collect(hom_map(lk3, :f)[:E]) == [2,1] + +otherF = FinDomFunctor(Dict(:Y=>two), Dict(:f => id(two)), Inv, Grph()) +otherD = DiagramHom(F, Dict(:X=>id(two)), Diagram(I), Diagram(otherF)) +phi = lk_universal(lk3_, otherD) +@test is_natural(phi) + +# Limits of diagrams +######################### + +# Nontrivial Examples +#-------------------- + +# FinCats +@present ArrPres_(FreeSchema) begin + (A1, A2)::Ob; a::Hom(A1, A2) +end +@present CSpanPres_(FreeSchema) begin + (C1, C2, C3)::Ob; c1::Hom(C1, C2); c2::Hom(C3,C2) +end +@present LoopPres_(FreeSchema) begin + L::Ob; l::Hom(L,L) +end +@present ThFSet(FreeSchema) begin + X::Ob +end + +@acset_type FSet(ThFSet) + +Arr, CSpan, Loop, FS = FinCat.([ArrPres_, CSpanPres_, LoopPres_, ThFSet]) + +# ACSet Cats +const Grph = ACSetCat{Graph} +const Finset = ACSetCat{FSet} + +# FinFunctors +FS_CS = FinDomFunctor(Dict(:X=>:C2), nothing, FS, CSpan) +FS_A = FinDomFunctor(Dict(:X=>:A2), nothing, FS, Arr) +F_AC = FinDomFunctor(Dict(:A1=>:C1, :A2=>:C2), Dict(:a=>:c1), Arr, CSpan) +G_AC = FinDomFunctor(Dict(:A1=>:C3, :A2=>:C2), Dict(:a=>:c2), Arr, CSpan) +A_L = FinDomFunctor(Dict(:A1=>:L,:A2=>:L), Dict(:a=>:l), Arr, Loop) +H_CA = FinDomFunctor(Dict(:C1=>:A1, :C2=>:A2, :C3=>:A1), + Dict(:c1=>:a, :c2=>:a), CSpan, Arr) + +# Graphs/Finsets +g0,g1,g2 = Graph.([0,1,2]) +t1 = apex(terminal(Graph)) +arr = path_graph(Graph, 2) +ar = @acset Graph begin V=2; E=2; src=[1,2]; tgt=[2,2] end +f1,f2,f3,f4 = fs = [@acset FSet begin X=i end for i in 1:4] + +ig1,it1 = id.([g1,t1]) +if1,if2 = id.([f1,f2]) +g1_arr1, g1_arr2 = homomorphisms(g1, ar) +harr = homomorphisms(arr,ar)[2] +g1arr = homomorphisms(g1,arr)[1] +gt1_arr1 = homomorphism(g1 ⊕ t1, ar) +t1_plus = homomorphism(t1, g1 ⊕ t1) +t1_ar = homomorphism(t1, ar) +g12a, g12b = homomorphisms(g1, g2) +g1_gt1,g1_gt1_2 = homomorphisms(g1, g1 ⊕ t1) +ar_t1 = homomorphism(ar, t1) +g1_t1= homomorphism(g1, t1) +g21 = homomorphism(g2, g1) +g01 = homomorphism(g0, g1) +g2_t1 = homomorphism(g2, t1) +ar_ar = homomorphisms(ar,ar)[2] +f12 = homomorphism(f1,f2) +f21 = homomorphism(f2,f1) +f32 = homomorphism(f3,f2) +f31 = homomorphism(f3,f1) +f22_1 = ACSetTransformation(f2,f2;X=[1,1]) +f23 = ACSetTransformation(f2,f3; X=[2,2]) +f13_2 = ACSetTransformation(f1,f3;X=[2]) + +# Diagrams to Grph or FinSet +AG_g1 = FinDomFunctor(Dict(:A1=>g1,:A2=>g1), Dict(:a=>ig1), Arr, Grph()); + +CG_g1t1ar = FinDomFunctor(Dict(:C1=>g1 ⊕ t1,:C2=>ar, :C3=>g1), + Dict(:c1=>gt1_arr1, :c2=>g1_arr2), + CSpan, Grph()); +AG_g12 = FinDomFunctor(Dict(:A1=>g2,:A2=>g1), + Dict(:a=>homomorphism(g2,g1)), + Arr, Grph()); +AG_t1 = FinDomFunctor(Dict(:A1=>t1,:A2=>t1), Dict(:a=>it1), Arr, Grph()); +CG_g1 = FinDomFunctor(Dict(:C1=>g1,:C2=>g1,:C3=>g1), + Dict(:c1=>ig1,:c2=>ig1), + CSpan, Grph()); +CG_t1ar = FinDomFunctor(Dict(:C1=>t1,:C2=>ar,:C3=>g1), + Dict(:c1=>t1_ar,:c2=>g1_arr2), + CSpan, Grph()); +FS_ar = FinDomFunctor(Dict(:X=>ar), FS, Grph()); +LG_g2 = FinDomFunctor(Dict(:L=>f2), Dict(:l=>if2), Loop, Finset()); +LG_g1 = FinDomFunctor(Dict(:L=>f1), Dict(:l=>if1), Loop, Finset()); +A_12 = FinDomFunctor(Dict(:A1=>f1,:A2=>f2), Dict(:a=>f12), Arr, Finset()); +A_13 = FinDomFunctor(Dict(:A1=>f1,:A2=>f3), Dict(:a=>f13_2), Arr, Finset()); +A_01 = FinDomFunctor(Dict(:A1=>g0,:A2=>g1), Dict(:a=>g01), Arr, Grph()); + +ds = [AG_g1, CG_g1t1ar, AG_g12, CG_g1, CG_t1ar, LG_g2, LG_g1, A_12, A_13, A_01, AG_t1] +AGg1, CGg1t1ar, AGg12, CGg1, CGt1ar, LGg2, LGg1, A12, A13, A01, AGt1 = Diagram.(ds) + +# Diagram morphisms +F_AAg1 = DiagramHom(id(Arr), Dict(:A1=>g12a,:A2=>ig1), AG_g1, AG_g12); +G_AAg1 = DiagramHom(id(Arr), Dict(:A1=>g12b, :A2=>ig1), AG_g1, AG_g12); +H_CAg1 = DiagramHom(H_CA, Dict(:C1=>g12a, :C2=>ig1,:C3=>g12b), CG_g1, AG_g12); +F_2 = DiagramHom(F_AC, Dict(:A1=>g1_gt1, :A2=>g1_arr1), AGg1, CGg1t1ar); +G_2 = DiagramHom(G_AC, Dict(:A1=>ig1, :A2=>g1_arr2), AGg1, CGg1t1ar); +H_2 = DiagramHom(id(Arr), Dict(:A1=>g1_t1, :A2=>g1_t1), AGg1, AGt1) +AA_02 = DiagramHom(id(Arr), Dict(:A1=>g01, :A2=>ig1), A01, AGg1); +# ACop1 = DiagramHom{op}(H_CA, Dict(:C1=>g21,:C2=>ig1, :C3=>g21), AG_g12, CG_g1) +# ACop2 = DiagramHom{op}(H_CA, Dict(:C1=>g2_t1,:C2=>g1_arr2, :C3=>g21), +# AG_g12, CG_t1ar) +Fop = DiagramHom{op}(F_AC, Dict(:A1=>it1, :A2=>ar_t1), CG_t1ar, AG_t1); +Gop = DiagramHom{op}(G_AC, Dict(:A1=>g1_t1,:A2=>ar_t1), CG_t1ar, AG_t1); +Hop = DiagramHom{op}(FS_CS, Dict(:X=>ar_ar), CG_t1ar, FS_ar); +Qop = DiagramHom{op}(FS_A, Dict(:X=>t1_ar), AG_t1, FS_ar) + +AL1 = DiagramHom(A_L, Dict(:A1=>if1,:A2=>f31), A_13, LG_g1); +AL2 = DiagramHom(A_L, Dict(:A1=>f12, :A2=>f32), A_13, LG_g2); +ALop1 = DiagramHom{op}(A_L, Dict(:A1=>f21,:A2=>f22_1), LG_g2, A_12); +ALop2 = DiagramHom{op}(A_L, Dict(:A1=>f21,:A2=>f23), LG_g2, A_13) + +ALop1 = DiagramHom{op}(A_L, Dict(:A1=>f21,:A2=>f22_1), LG_g2, A_12); +ALop2 = DiagramHom{op}(A_L, Dict(:A1=>f21,:A2=>f23), LG_g2, A_13) +ALop3 = DiagramHom{op}(A_L, Dict(:A1=>if1,:A2=>f13_2), LG_g1, A_13) +CA1 = DiagramHom(H_CA, Dict(:C1=>ig1, :C2=>ig1, :C3=>ig1), CGg1, AGg1) +CC1 = DiagramHom(id(CSpan), Dict(:C1=>g1_gt1_2, :C2=>g1_arr2, :C3=>ig1), + CGg1, CGg1t1ar); + +# Limits +#------- + +p1 = product([AGg1, CGg1t1ar, AGg12, CGg1, CGt1ar]); +p2 = product([LGg1, LGg2]); +e1 = equalizer(DiagramHom{id}[F_AAg1,G_AAg1]); +e2 = equalizer(DiagramHom{id}[F_2,G_2]); +pb = pullback(Multicospan([G_AAg1,H_CAg1])); + +map([p1, p2, e1, e2, pb]) do lim + @test is_functorial(diagram(apex(lim))) + @test all(is_natural.(legs(lim))) +end + +u = universal(p2, Multispan([AL1, AL2])) +@test is_natural(u) + +u = factorize(e1, AA_02) +@test is_natural(u) + +# Limits(op) +#----------- +p1 = product(Diagram{op}.([A_12,A_13])); +p2 = product(Diagram{op}.([AG_g1, CG_g1t1ar, AG_g12, CG_g1, CG_t1ar])); + +# e = equalizer() NOT SUPPORTED - requires Kan +# pb = pullback()) NOT SUPPORTED - requires Kan + +map([p1, p2]) do lim + @test is_functorial(diagram(apex(lim))) + @test all(is_natural.(legs(lim))) +end + +u = universal(p1, Multispan([ALop1, ALop2])) +@test is_natural(u) + +# Colimits +#---------- +cp1 = coproduct(Diagram{id}[AGg1, CGg1]); +cp2 = coproduct(Diagram{id}[AGg1, CGg1t1ar, AGg12, CGg1, CGt1ar]); + +ceq = coequalizer(DiagramHom{id}[F_2,G_2]) +po = pushout(Multispan([F_2,H_2])) + +""" Worked out pushout for two diagram homs in Grph: + +Pushout at shape level is id(•) +. Arrow = Arrow. If we plug in the graphs: + + •↦ V₁ + (l1) V₁₂ ↦ V₂ + {[•]} ⇒ {[•₁ → •₂] ⟶ [•₁ → •₂↺]} + •↦ V₁ (l2)⇓ + {[•₁ → •₂↺]} + +This results in a diagram with shape •→•. The first graph is the same as +before with an extra l2 component glued onto V₁, while the second graph has the +l2 component glued onto V₂. Result: + + •₂ V₁₂ ↦ V₂ + ↑ V₃ ↦ V₃ + •₁ → •₃↺ ⟶ •₁ → •₃↺ → •₃↺ +""" +l1_ = Diagram(FinDomFunctor(Dict(:A1=>arr,:A2=>ar),Dict(:a=>harr),Arr,Grph())) +l2_ = Diagram(FinDomFunctor(Dict(:X=>ar), nothing, FS, Grph())); +FS_A = FinDomFunctor(Dict(:X=>:A1), nothing, FS, Arr) +apx = Diagram(FinDomFunctor(Dict(:X=>g1), nothing, FS, Grph())) +l1 = DiagramHom(FS_A,Dict(:X=>g1arr),apx,l1_) +l2 = DiagramHom(id(FS),Dict(:X=>g1_arr1),apx,l2_) +po2 = pushout(Multispan([l1,l2])); + +expected_a1 = @acset Graph begin V=3;E=3; src=[1,1,3]; tgt=[2,3,3] end +expected_a2 = @acset Graph begin V=3;E=4; src=[1,2,2,3]; tgt=[2,2,3,3] end +@test is_isomorphic(ob_map(apex(po2), Symbol("[A1,X]")), expected_a1) +@test is_isomorphic(ob_map(apex(po2), Symbol("[A2]")), expected_a2) + + +map([cp1, cp2, ceq, po, po2]) do clim + @test is_functorial(diagram(apex(clim))) + @test all(is_natural.(legs(clim))) +end + +u = universal(cp1, Multicospan([F_2,CC1])) +@test is_natural(u) + +# Colimits(op) +#------------ +cp1 = coproduct(Diagram{op}.([LG_g1, LG_g2])); +cp2 = coproduct(Diagram{op}.([CG_g1, CG_t1ar])); +ce = coequalizer([Fop, Gop]); +po = pushout(Multispan([ALop1, ALop2])); + +map([cp1, cp2, ce, po]) do clim + @test is_functorial(diagram(apex(clim))) + @test all(is_natural.(legs(clim))) +end + +u = universal(cp1, Multicospan([ALop3, ALop2])) +@test is_natural(u) + +u = factorize(ce, Qop) +@test is_natural(u) + +end # module diff --git a/test/categorical_algebra/FinCats.jl b/test/categorical_algebra/FinCats.jl index 28aa8f0e3..36c89f635 100644 --- a/test/categorical_algebra/FinCats.jl +++ b/test/categorical_algebra/FinCats.jl @@ -234,4 +234,75 @@ F5 = FinFunctor([1,2,3], [1,2,3], T, T2) @test !is_initial(F4) @test !is_initial(F5) +# Define examples for limits and colimits +#---------------------------------------- +@present I_(FreeSchema) begin (I1, I2)::Ob; i::Hom(I1, I2) end +@present M_(FreeSchema) begin (M1, M2)::Ob; m::Hom(M1, M2) end +@present N_(FreeSchema) begin (N1, N2)::Ob; n::Hom(N1, N2) end +@present J_(FreeSchema) begin + (J1, J2, J3)::Ob; j1::Hom(J1, J2); j2::Hom(J3,J2) +end +@present K_(FreeSchema) begin + K::Ob; k::Hom(K,K) + compose(k,k) == k +end + +I, J, K, M, N = FinCat.([I_,J_,K_,M_,N_]); +(i,),(j1,j2),(k_,) = hom_generators.([I,J,K]) + +F_IJ = FinDomFunctor(Dict(:I1=>:J1, :I2=>:J2), Dict(:i=>:j1), I, J) +G_IJ = FinDomFunctor(Dict(:I1=>:J3, :I2=>:J2), Dict(:i=>:j2), I, J) +F_IK = FinDomFunctor(Dict(:I1=>:K, :I2=>:K), Dict(:i=>:k), I, K) +J_I = FinDomFunctor(Dict(:J1=>:I1, :J2=>:I2, :J3 => :I1), + Dict(:j1=>:i, :j2=>:i), J, I) + +# Limits +#------- +p = product([I, J, K]); +e = equalizer([F_IJ, G_IJ]) +e2 = equalizer([F_IJ, F_IJ]) + +map([p, e, e2]) do lim + @test all(is_functorial.(legs(lim))) +end + +u = universal(p, Multispan([id(I), F_IJ, F_IK])) +@test is_functorial(u) +ij1k,i2j1k,i2j2k = [h for h in hom_generators(apex(p)) if h.args[1] in Symbol.( + ["(i, id(J1), id(K))","(id(I2), j1, id(K))","(id(I2), id(J2), k)"])] +@test hom_map(u, :i) == compose(ij1k, i2j1k, i2j2k) + +u = universal(e2, J_I) +@test is_functorial(u) + +# encode a graph homomorphism as a FinCat. It is •→• ⟶ Grph +# by curry adjunction, the shape is the product of •→• and •⇉• +P = apex(product([I, FinCat(TheoryGraph)])) +@test length(equations(P)) == 2 # the two naturality squares +P = apex(product([I,M,N])) # multidimensional +@test length(equations(P)) == 6 +P = apex(product([I,K])) # base equation in K gets multiplied by 2 +@test length(equations(P)) == 3 # also have one naturality square + + +# Colimits +#--------- +cp = coproduct([I, I, J]); +@test length(ob_generators(apex(cp))) == 7 +cp2 = coproduct([K, K]) +@test length(equations(apex(cp2))) == 2 +ce1 = coequalizer([G_IJ, G_IJ]); +ce2 = coequalizer([F_IJ, G_IJ]); +map([cp, ce1, ce2]) do colim + @test all(is_functorial.(legs(colim))) +end + +u = universal(cp, Multicospan([F_IJ, G_IJ, id(J)])) +@test is_functorial(u) +@test ob_map(u, Symbol("I1#1")) == ob_generators(J)[1] +@test ob_map(u, Symbol("I1#2")) == ob_generators(J)[3] + +u = universal(ce1, J_I) +@test is_functorial(u) + end