Skip to content

Commit

Permalink
Merge pull request #54 from AlgebraicJulia/attrvar_pushout_comp
Browse files Browse the repository at this point in the history 
New pushout complement for AttrVars
  • Loading branch information
@kris-brown
kris-brown authored Apr 19, 2024
2 parents 690fe70 + 79d9548 commit 2263d84
Show file tree
Hide file tree
Showing 8 changed files with 214 additions and 149 deletions.
104 changes: 52 additions & 52 deletions docs/literate/lotka_volterra.jl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,13 +7,14 @@ We start with importing some libraries.
=#

using Catlab, DataMigrations, AlgebraicRewriting
using Random, Test, StructEquality
using Luxor
using Random, Test
using Luxor # optional: makes the sequence of images via `view_traj` at the end

using Catlab.Graphics.Graphviz: Attributes, Statement, Node
using Catlab.Graphics.Graphviz

const hom = homomorphism

Random.seed!(123);

# # Ontology
Expand Down Expand Up @@ -335,11 +336,10 @@ view_sched(par_sched; names=N)

# #### Test rotation
begin
ex = @acset_colim yLV begin
e::E
s::Sheep
sheep_loc(s) == src(e)
sheep_dir(s) == :N
ex = @acset LV begin
E=1; Sheep=1; V=2
src=1; tgt=2; dir=:W; countdown = [0, 0]
sheep_loc=1; sheep_eng=100; sheep_dir=:N
end;

expected = copy(ex);
Expand Down Expand Up @@ -381,19 +381,16 @@ sheep_fwd = tryrule(RuleApp(:move_fwd, sheep_fwd_rule,

# #### Moving forward test

begin # test
ex = @acset_colim yLV begin
(e1, e2)::E; s::Sheep
sheep_loc(s) == tgt(e1); tgt(e1) == src(e2)
sheep_dir(s) == :N; dir(e1) == :N; dir(e2) == :N
sheep_eng(s) == 10
end
expected = @acset_colim yLV begin
(e1, e2)::E; s::Sheep
sheep_loc(s) == tgt(e2); tgt(e1) == src(e2)
sheep_dir(s) == :N; dir(e1) == :N; dir(e2) == :N
sheep_eng(s) == 9
begin
ex = @acset LV begin
V=3; E=2; Sheep=1;
countdown=[0,0,0]
src=[1,2]; tgt=[2,3]; dir=[:N,:W]
sheep_loc=1; sheep_dir=:N; sheep_eng = 10
end
expected = copy(ex);
expected[:sheep_loc] = 2
expected[:sheep_eng] = 9
@test is_isomorphic(expected, rewrite(sheep_fwd_rule, ex))
rewrite!(sheep_fwd_rule, ex)
@test is_isomorphic(ex, expected)
Expand All @@ -409,18 +406,17 @@ se_rule = Rule(S; expr=(Eng=[vs -> vs[1] + 4, vs -> 30],),
sheep_eat = tryrule(RuleApp(:Sheep_eat, se_rule, S));

# #### Sheep eating test
begin
ex = @acset_colim yLV begin
s::Sheep; e::E
sheep_loc(s) == tgt(e); sheep_eng(s) == 3
countdown(tgt(e)) == 0; countdown(src(e)) == 10
end
expected = @acset_colim yLV begin
s::Sheep; e::E
sheep_loc(s) == tgt(e); sheep_eng(s) == 7
countdown(tgt(e)) == 30; countdown(src(e)) == 10
begin
ex = @acset LV begin
E=1; V=2; Sheep=1;
src=1; tgt=2; dir=:S; countdown=[10, 0]
sheep_loc = 2; sheep_eng = 3; sheep_dir=:W
end

expected = copy(ex)
expected[2,:countdown] = 30
expected[1,:sheep_eng] = 7

@test is_isomorphic(expected, rewrite(se_rule, ex))
rewrite!(se_rule, ex)
@test is_isomorphic(ex, expected)
Expand All @@ -442,17 +438,15 @@ wolf_eat = tryrule(RuleApp(:Wolf_eat, we_rule, W));
begin
ex = @acset LV begin
Sheep=1; Wolf=1; V=3; E=2;
src=[1,2]; tgt=[2,3];
countdown=[9,10,11]; dir=[:N,:N];
src=[1,2]; tgt=[2,3]; countdown=[9,10,11]; dir=[:N,:N];
sheep_loc=2; sheep_eng=[3]; sheep_dir=[:N]
wolf_loc=[2]; wolf_eng=[16]; wolf_dir=[:S]
end
expected = @acset LV begin
Wolf=1; V=3; E=2;
src=[1,2]; tgt=[2,3];
countdown=[9,10,11]; dir=[:N,:N];
wolf_loc=[2]; wolf_eng=[36]; wolf_dir=[:S]
end

expected = copy(ex)
expected[1, :wolf_eng] = 36
rem_part!(expected, :Sheep, 1)

@test is_isomorphic(rewrite(we_rule,ex), expected)
rewrite!(we_rule, ex)
@test is_isomorphic(ex,expected)
Expand All @@ -469,13 +463,16 @@ sheep_starve = (RuleApp(:starve, sheep_die_rule,

# #### Sheep starvation test

begin # test
compile_rewrite(sheep_die_rule)
ex = @acset_colim yLV begin
s::Sheep; w::Wolf
sheep_eng(s) == 0; sheep_dir(s) == :W
begin
ex = @acset LV begin
V=1; Sheep=1; Wolf=1
countdown=20;
sheep_loc=1; sheep_eng=0; sheep_dir=:W
wolf_loc=1; wolf_eng=10; wolf_dir=:S
end
expected = @acset_colim yLV begin v::V; w::Wolf end
expected = copy(ex)
rem_part!(expected, :Sheep, 1)

@test is_isomorphic(rewrite(sheep_die_rule,ex), expected)
rewrite!(sheep_die_rule,ex)
@test is_isomorphic(ex, expected)
Expand All @@ -501,16 +498,19 @@ sheep_reprod = RuleApp(:reproduce, sheep_reprod_rule,
# #### Reproduction test

begin # test
ex = @acset_colim yLV begin
s::Sheep; w::Wolf; sheep_eng(s) == 10; sheep_dir(s) == :W
end
expected = @acset_colim yLV begin
(s1,s2)::Sheep; w::Wolf;
sheep_loc(s1) == sheep_loc(s2)
sheep_dir(s1) == sheep_dir(s2)
sheep_eng(s1) == sheep_eng(s2)
sheep_dir(s1) == :W; sheep_eng(s1) == 5;
ex = @acset LV begin
Sheep=1; Wolf=1; V=2;
countdown=[20,30]
sheep_loc=1; sheep_eng=10; sheep_dir=:W
wolf_loc=2; wolf_eng=5; wolf_dir=:N
end

expected = copy(ex)
add_part!(expected,:Sheep)
expected[:sheep_eng] = [5, 5]
expected[:sheep_loc] = [1, 1]
expected[:sheep_dir] = [:W, :W]

@test is_isomorphic(rewrite(sheep_reprod_rule,ex),expected)
rewrite!(sheep_reprod_rule,ex)
@test is_isomorphic(ex, expected)
Expand Down
115 changes: 77 additions & 38 deletions src/categorical_algebra/CSets.jl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ using CompTime
using Catlab
using Catlab.CategoricalAlgebra.FinSets: IdentityFunction, VarSet
using Catlab.CategoricalAlgebra.Chase: extend_morphism, extend_morphism_constraints
using Catlab.CategoricalAlgebra.CSets: unpack_diagram, type_components, abstract_attributes
using Catlab.CategoricalAlgebra.CSets: unpack_diagram, type_components, abstract_attributes, var_reference
import ..FinSets: pushout_complement, can_pushout_complement, id_condition
import ACSets: acset_schema
import Catlab.CategoricalAlgebra.FinSets: predicate
Expand All @@ -19,7 +19,7 @@ import Catlab.CategoricalAlgebra: is_natural, Slice, SliceHom, components,
using ACSets.DenseACSets: attrtype_type, datatypes, constructor
import ACSets: sparsify
import Base: getindex
using DataStructures: OrderedSet
using DataStructures: OrderedSet, DefaultDict, IntDisjointSets, find_root!
using StructEquality

# Morphism search
Expand Down Expand Up @@ -100,6 +100,47 @@ function check_pb(f,g,f_,g_)
end
end

# Non-monotonicity
##################

"""
Every morphism induces a partition of the parts of the domain. This function
finds every nontrivial partition (size greater than one element) for the objects
of the schema.
"""
fibers(f::ACSetTransformation) =
Dict(o => fibers(f[o]) for o in ob(acset_schema(dom(f))))

function fibers(f::FinFunction)
dic = DefaultDict{Int,Vector{Int}}(()->Int[])
for v in dom(f)
push!(dic[f(v)], v)
end
filter(xs->length(xs)>1, collect(values(dic)))
end

unions!(i::IntDisjointSets, xs::Vector{Int}) = if length(xs) > 1
[union!(i, x, y) for (x,y) in zip(xs, xs[2:end])]
end

getvalue(a::AttrVar) = a.val

"""Further induced equations between AttrVars, given a specific match morphism"""
function var_eqs(l::ACSetTransformation, m::ACSetTransformation)
I, L = dom(l), codom(l)
S = acset_schema(L)
eq_I = Dict(a => IntDisjointSets(nparts(I, a)) for a in attrtypes(S))
for (o, xss) in pairs(fibers(m)) # match induces equivalence of ob parts in L
for xsₗ in xss
xsᵢ = Vector{Int}(vcat(preimage.(Ref(l[o]), xsₗ)...))
for (f, _, at) in attrs(S; from=o)
unions!(eq_I[at], getvalue.(filter(x -> x isa AttrVar, I[xsᵢ, f])))
end
end
end
return eq_I
end

# Pushout complement
####################

Expand All @@ -111,45 +152,53 @@ this method will raise an error. If the dangling condition fails, the resulting
C-set will be only partially defined. To check all these conditions in advance,
use the function [`can_pushout_complement`](@ref).
Because Subobject does not work well with AttrVars, a correction is made
In the absence of AttrVars, K is a subobject of G. But we want to be able to
change the value of attributes. So any variables in I are not concretized by
the I->K map. However, AttrVars may be merged together if `m: L -> G` merges
parts together.
"""
function pushout_complement(pair::ComposablePair{<:ACSet, <:TightACSetTransformation})
p1,p2 = pair
I,G = dom(p1), codom(p2)
l, m = pair
I, G = dom(l), codom(m)
S = acset_schema(I)
all(at->nparts(G, at)==0, attrtypes(S)) || error("Cannot rewrite with AttrVars in G")
# Compute pushout complements pointwise in FinSet.
components = NamedTuple(Dict([o=>pushout_complement(ComposablePair(p1[o],p2[o]))
for o in types(S)]))
k_components, g_components = map(first, components), map(last, components)
components = NamedTuple(Dict(map(ob(S)) do o
o => pushout_complement(ComposablePair(l[o], m[o]))
end))
k_components = Dict{Symbol,Any}(pairs(map(first, components)))
g_components = Dict{Symbol,Any}(pairs(map(last, components)))

# Reassemble components into natural transformations.
g = hom(Subobject(G, NamedTuple(Dict(o=>g_components[o] for o in ob(S)))))
g = hom(Subobject(G, NamedTuple(Dict(o => g_components[o] for o in ob(S)))))
K = dom(g)

for at in attrtypes(S)
add_parts!(K, at, codom(k_components[at]).n)
end

for (a, d, at) in attrs(S)
# force k to be natural
for p in parts(I, d)
K[k_components[d](p),a] = k_components[at](I[p, a])
end
# force g to be natural
for p in parts(K, d)
gval = G[g_components[d](p), a]
preim = preimage(g_components[at], gval)
if !isempty(preim) && gval isa AttrVar
K[p,a] = AttrVar(only(preim))
var_eq = var_eqs(l, m) # equivalence class of attrvars

for at in attrtypes(S)
eq = var_eq[at]
roots = unique(find_root!.(Ref(eq), 1:length(eq)))
add_parts!(K, at, length(roots))
k_components[at] = map(parts(I, at)) do pᵢ
attrvar = AttrVar(findfirst(==(find_root!(eq, pᵢ)), roots))
for (a, d, _) in attrs(S; to=at)
for p in incident(I, AttrVar(pᵢ), a)
K[k_components[d](p), a] = attrvar
end
end
attrvar
end
end
T = Union{AttrVar, attrtype_type(G, at)}
g_components[at] = Vector{T}(map(parts(K, at)) do v
f, o, val = var_reference(K, at, v)
G[g_components[o](val), f]
end)
end

k = ACSetTransformation(I, K; k_components...)
g = ACSetTransformation(K, G; g_components...)

force(compose(k,g)) == force(compose(p1,p2)) || error("Square doesn't commute")
is_natural(k) || error("k unnatural")
force(compose(k,g)) == force(compose(l, m)) || error("Square doesn't commute")
is_natural(k) || error("k unnatural $k")
is_natural(g) || error("g unnatural")
return ComposablePair(k, g)
end
Expand Down Expand Up @@ -261,16 +310,6 @@ dangling_condition(pair::ComposablePair{<:DynamicACSet}) = let S = acset_schema(
results
end

# n_src = parts(codom(m), @ct(src_obj)) # BIG
# unmatched_vals = setdiff(n_src, collect(m[@ct(src_obj)]))
# unmatched_tgt = [codom(m)[x,@ct(morph)] for x in unmatched_vals]
# for unmatched_val in setdiff(n_src, collect(m[@ct(src_obj)])) # G/m(L) src
# unmatched_tgt = codom(m)[unmatched_val,@ct morph]
# if unmatched_tgt in dels[@ct(tgt_obj)]
# push!(results, (@ct(morph), unmatched_val, unmatched_tgt))
# end
# end

# Subobjects
############

Expand Down
31 changes: 0 additions & 31 deletions src/categorical_algebra/FinSets.jl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -46,37 +46,6 @@ function pushout_complement(pair::ComposablePair{<:FinSet{Int}})
return ComposablePair(k, g)
end

"""
This may not be the actual pushout complement in the relevant (Kleisli) category
l
L ← I
m ↓ ↓ k
G ← K
g
"""
function pushout_complement(pair::ComposablePair{<:VarSet{T}}) where {T}
l, m = pair
lm = compose(l,m)
I, G = dom(l), codom(m)
# Initialize I -> K with image of composite l⋅m
image_lm = unique([lm(AttrVar(i)) for i in I])

# Additionally, any vars not matched by m should be matched by g
unmatched = setdiff(AttrVar.(G), collect(m))
K = FinSet(length(image_lm) + length(unmatched))

# Construct I -> K
ik = VarFunction{T}([AttrVar(findfirst(==(lm(AttrVar(i))), image_lm))
for i in I], FinSet(length(K)))
# Construct K -> G
kg = VarFunction{T}(Union{T,AttrVar}[
[lm(AttrVar(findfirst(==(AttrVar(k)), collect(ik))))
for k in 1:length(image_lm)]..., unmatched...], FinSet(length(G)))
return ComposablePair(ik, kg)
end

can_pushout_complement(pair::ComposablePair{<:FinSet{Int}}) =
all(isempty, id_condition(pair))

Expand Down
Loading

0 comments on commit 2263d84

Please sign in to comment.