Theorem Proving For Catlab 2: Let’s Try Z3 This Time. Nope.

Welp, you win some, you lose some.

As I had left off last time, I had realized that my encoding of the equations of Catlab was unsound.

As an example, look at the following suggested axioms.

fof( axiom2, axiom, ![Varf, VarA, VarB]: constcompose(Varf, constid(VarB)) = Varf).
fof( axiom3, axiom, ![Varf, VarA, VarB]: constcompose(constid(VarA), Varf) = Varf).

It is a theorem from these axioms that compose(id(A),id(B)) = id(A) = id(B), which should not be a theorem. Evan made the interesting point that this is the standard proof that shows the identity of a group is unique, so we’re reducing our magnificent category into a pitiful monoid. How sad. And inspecting the trace for some “proofs” returned by eprover shows that the solver was actually using this fact. Oh well.

An approach that I feel more confident in being correct is using “type guards” as preconditions for the equations. In the very useful paper https://people.mpi-inf.mpg.de/~jblanche/mono-trans.pdf this technique is described as well known folklore, albeit in a slightly different context. The type guard is an implication clause that holds the necessary typing predicates from the typing context required for the equation to even make sense. For example composition associativity look like forall A B C D f g h, (type(f) = Hom A B /\ type(g) = Hom B C /\ type(h) = Hom C D /\ type(A) = Ob /\ type(B) = Ob /\ type(C) = Ob /\ type(C) = Ob) => compose(f (g, h)) = compose( compose(f,g),h).

Adding the guards seems to work, but slows the provers to a crawl for fairly trivial queries. My running example is pair(proj1(A,B), proj2(A,B)) = otimes(id(A),id(B)). In Catlab proj1, proj2, and pair, are defined in terms of mcopy and delete, which makes this theorem not as trivial as it would appear. Basically it involves unfolding the definitions, and then applying out of nowhere some identities involving braiding.

I decided to give Z3, an SMT solver, a go since I’m already familiar with it and its python bindings. There are native Julia bindings https://github.com/ahumenberger/Z3.jl which may be useful for a more high performance situation, but they don’t appear to have quantifier support yet.

Julia has the library PyCall https://github.com/JuliaPy/PyCall.jl which was a shear joy to use. I actually could copy and paste some python3 z3 code and run it with very few modifications and I couldn’t imagine going into and out of Julia data types being more seemless.

Z3 does a better job than I expected. I thought thus problem was more appropriate to eprover or vampire, but z3 seemed to consistently out perform them.

At first I tried using a single z3 sort z3.DeclareSort("Gat") , but eventually I switched to a multisorted representation z3.DeclareSort("Ob") and z3.DeclareSort("Hom") as this gets a step closer to accurately representation the types of the GATs in the simply sorted smtlib language. Which of these sorts to use can be determined by looking at the head symbol of the inferred Catlab types. I wrote a custom type inference just so I could try stuff out, but after asking in the zulip, apparently catlab has this built in also.

Some Z3 debugging tips:

I tend to make my z3 programs in python, dump the s.sexpr() in a file and then run that via the z3 command line. It’s easier to fiddle with the smtlib2 file to try out ideas fast. Take stuff out, put stuff in, make simpler questions, etc. Be aware most ideas do not work.

Z3 appears to be inferring pretty bad triggers. The main way z3 handles quantifiers is that it looks for patterns from the quantified expression in the currently known assertion set and instantiates the quantified expression accordingly. Hence I kind of think of quantified expressions as a kind of macro for formulas. This is called E-matching https://rise4fun.com/z3/tutorialcontent/guide#h28. Running z3 with a -v:10 flag let’s you see the triggers. Z3 tries to find very small pieces of expressions that contain the quantified variables. I think we don’t really want any equations instantiated unless it finds either the full right or left hand side + context types. In addition, the triggers inferred for the type inference predicates were not good. We mostly want z3 to run the typing predicate forward, basically as a type inference function. So I tried adding all this and I think it helped, but not enough to actually get my equation to prove. Only simpler problems.


(assert (forall ((A Ob)) (! (= (typo (id A)) (Hom A A)) :pattern ((id A)))))
(assert (forall ((A Ob) (B Ob) (C Ob) (f Hom) (g Hom))
  (! (=> (and (= (typo f) (Hom A B)) (= (typo g) (Hom B C)))
         (= (typo (compose f g)) (Hom A C)))
     :pattern ((compose f g) (Hom A B) (Hom B C)))))
(assert (forall ((A Ob) (B Ob)) (! (= (typo (otimes A B)) Ob) :pattern ((otimes A B)))))
(assert (forall ((A Ob) (B Ob) (C Ob) (D Ob) (f Hom) (g Hom))
  (! (=> (and (= (typo f) (Hom A B)) (= (typo g) (Hom C D)))
         (= (typo (otimes f g)) (Hom (otimes A C) (otimes B D))))
     :pattern ((otimes f g) (Hom A B) (Hom C D)))))
;(assert (forall ((A Ob) (B Ob) (C Ob) (D Ob) (f Hom) (g Hom))
;  (! (=> (and (= (typo f) (Hom A B)) (= (typo g) (Hom C D)))
;         (= (typo (otimes f g)) (Hom (otimes A C) (otimes B D))))
;     :pattern ((= (typo f) (Hom A B)) (= (typo g) (Hom C D))))))
(assert (= (typo munit) Ob))
(assert (forall ((A Ob) (B Ob))
  (! (= (typo (braid A B)) (Hom (otimes A B) (otimes B A)))
     :pattern ((braid A B)))))
(assert (forall ((A Ob))
  (! (= (typo (mcopy A)) (Hom A (otimes A A))) :pattern ((mcopy A)))))
(assert (forall ((A Ob)) (! (= (typo (delete A)) (Hom A munit)) :pattern ((delete A)))))
(assert (forall ((A Ob) (B Ob) (C Ob) (f Hom) (g Hom))
  (! (=> (and (= (typo f) (Hom A B)) (= (typo g) (Hom A C)))
         (= (typo (pair f g)) (Hom A (otimes B C))))
     :pattern ((pair f g) (Hom A B) (Hom A C)))))
(assert (forall ((A Ob) (B Ob))
  (! (= (typo (proj1 A B)) (Hom (otimes A B) A)) :pattern ((proj1 A B)))))
(assert (forall ((A Ob) (B Ob))
  (! (= (typo (proj2 A B)) (Hom (otimes A B) B)) :pattern ((proj2 A B)))))

I tried the axiom profiler to give me any insight. http://people.inf.ethz.ch/summersa/wiki/lib/exe/fetch.php?media=papers:axiomprofiler.pdf https://github.com/viperproject/axiom-profiler I do see some quantifiers that have an insane number of instantiations. This may be because of my multipattern approach of using the Hom type and separately the term as patterns. It will just randomly fire the trigger on Homs unrelated to the one their connected to. That’s awful. The associativity axioms also seem to be triggering too much and that is somewhat expected.

Z3 debugging is similar to prolog debugging since it’s declarative. https://www.metalevel.at/prolog/debugging Take out asserts. Eventually, if you take out enough, an unsat problem should turn sat. That may help you isolate problematic axiom

Another thing I tried was to manually expand out each step of the proof to see where z3 was getting hung up. Most simple step were very fast, but some hung, apparently due to bad triggers? Surprisingly, some things I consider 1 step trivial aren’t quite. Often this is because single equations steps involves associating and absorbing munit in the type predicates. The interchange law was difficult to get to fire for this reason I think.

Trimming the axioms available to only the ones needed really helps, but doesn’t seem practical as an automated thing.

Code

Here’s the Julia code I ended up using to generate the z3 query from the catlab axioms. It’s very hacky. My apologies. I was thrashing.

# here we're trying to use Z3 sorts to take care of some of the typign
using Catlab
using Catlab.Theories
using PyCall
z3 = pyimport("z3")

# my ersatz unnecessary type inference code for Cartesian category terms

function type_infer(x::Symbol; ctx = Dict())
    if x == :Ob
        return :TYPE
    elseif x == :munit
        return :Ob
    else 
        return ctx[x]
    end 
    
end
    
function type_infer(x::Expr; ctx = Dict())
        @assert x.head == :call
        head = x.args[1]
        if head == :compose
            t1 = type_infer(x.args[2], ctx=ctx)
            @assert t1.args[1] == :Hom
            obA = t1.args[2] 
            t2 = type_infer(x.args[3], ctx=ctx)
            @assert t2.args[1] == :Hom
            obC = t2.args[3] 

            if t1.args[3] != t2.args[2]
               #println("HEY CHECK THIS OUT ITS WEIRD")
            #println(t1)
            #println(t2)
        end

            return :(Hom($obA, $obC))
        elseif head == :otimes
            t1 = type_infer(x.args[2], ctx=ctx)
            #@assert t1.args[1] == :Hom
            if t1 isa Symbol && t1 == :Ob
                return :Ob
            end
            @assert t1.args[1] == :Hom
            obA = t1.args[2] 
            obC = t1.args[3] 
            t2 = type_infer(x.args[3], ctx=ctx)
            @assert t2.args[1] == :Hom
            obB = t2.args[2] 
            obD = t2.args[3] 
            return :(Hom(otimes($obA,$obB),otimes($obC, $obD)))
        elseif head == :pair
            t1 = type_infer(x.args[2], ctx=ctx)
            @assert t1.args[1] == :Hom
            obA = t1.args[2] 
            obB = t1.args[3] 
            t2 = type_infer(x.args[3], ctx=ctx)
            @assert t2.args[1] == :Hom
            obC = t2.args[3] 
            @assert t1.args[2] == t2.args[2]
            return :(Hom($obA, otimes($obB,$obC)))
        elseif head == :mcopy
            ob = x.args[2]
            return :(Hom($ob, otimes($ob,$ob)))
        elseif head == :id
            ob = x.args[2]
            return :(Hom($ob, $ob))
        elseif head == :delete
            ob = x.args[2]
            return :(Hom($ob, munit))
        elseif head == :proj1
            obA = x.args[2]
            obB = x.args[3]
            return :(Hom(otimes($obA, $obB), $obA))
        elseif head == :proj2
            obA = x.args[2]
            obB = x.args[3]
            return :(Hom(otimes($obA, $obB), $obB))
        elseif head == :braid
            obA = x.args[2]
            obB = x.args[3]
            return :(Hom(otimes($obA, $obB), otimes($obB, $obA)))
        elseif head == :Hom
            return :TYPE
        elseif head == :munit
            return :Ob
        else
            println(x, ctx)
            @assert false
        end
end

TYPE = z3.DeclareSort("TYPE")

# sortify takes a type expression, grabs the head, and returns the corresponding Z3 sort.
function sortify(ty) 
    if ty isa Symbol
        return z3.DeclareSort(String(ty))
    elseif ty isa Expr
        @assert ty.head == :call
        return z3.DeclareSort(String(ty.args[1]))
    end
end

# z3ify take an Expr or Symbol in a dictionary typing context and returns the z3 equivalent
z3ify( e::Symbol , ctx) = z3.Const(String(e), sortify(type_infer(e,ctx=ctx)))

function z3ify( e::Expr , ctx)
    @assert e.head == :call
    out_sort = sortify(type_infer(e,ctx=ctx))
    z3.Function(e.args[1], [sortify(type_infer(x,ctx=ctx)) for x in e.args[2:end]]..., out_sort)(map(x -> z3ify(x,ctx), e.args[2:end])...)
end

# typo is a helper routine that takes an Expr or Symbol term and returns the Z3 function typo applied to the z3ified term
function typo(x, ctx)
    f = z3.Function("typo" , sortify(type_infer(x,ctx=ctx))  , TYPE ) 
    f(z3ify(x,ctx))
end

# a helper function to z3ify an entire context for the implication
function build_ctx_predicate(ctx)
    map( kv-> begin
        #typo = z3.Function("typo" , sortify(typ)  , TYPE ) 
        typo(kv[1], ctx) == z3ify(kv[2], ctx)
        end
        
        , filter( kv -> kv[2] isa Expr , # we don't need to put typo predicates about simple types like Ob 
             collect(ctx)))

end

# converts the typing axioms of a GAT into the equivalent z3 axioms
# This is quite close to unreadable I think
function build_typo_z3(terms)
    map(myterm ->  begin
                ctx = myterm.context
                conc =  length(myterm.params) > 0  ?  Expr(:call, myterm.name, myterm.params...) : myterm.name
                 preconds = build_ctx_predicate(myterm.context) 
                    if length(myterm.context) > 0 && length(preconds) > 0
                        z3.ForAll( map(x -> z3ify(x,ctx), collect(keys(myterm.context))) ,
                            z3.Implies( z3.And(preconds)  , 
                                     typo(conc,myterm.context) == z3ify(myterm.typ, myterm.context)),
                  patterns = [ z3.MultiPattern(z3ify(conc,ctx),  
                               [ z3ify(x ,ctx ) for x in collect(values(myterm.context)) if x isa Expr]...) # not super sure this is a valid way of filtering generally
                             ],
                  )
                elseif length(myterm.context) > 0
                        z3.ForAll( map(x -> z3ify(x,ctx), collect(keys(myterm.context))) ,
                                     typo(conc,myterm.context) == z3ify(myterm.typ, myterm.context),
                         patterns = [z3ify(conc,ctx)])
                    else
                        typo(conc,myterm.context) == z3ify(myterm.typ, myterm.context)
                    end
            end
              
    , terms)
end

# convert the equations axioms of a GAT into the equivalent z3 terms
function build_eqs_z3(axioms)
        map(axiom -> begin
            @assert axiom.name == :(==)
            ctx = axiom.context
            l = z3ify(axiom.left, axiom.context)
            r = z3ify(axiom.right, axiom.context)
            preconds= build_ctx_predicate(axiom.context) 
            ctx_patterns = [ z3ify(x ,ctx ) for x in collect(values(axiom.context)) if x isa Expr]
            println([z3.MultiPattern( l , ctx_patterns...  ) , z3.MultiPattern( r , ctx_patterns...  ) ])
            if length(axiom.context) > 0 && length(preconds) > 0
                    try
                    z3.ForAll( map(x -> z3ify(x,ctx), collect(keys(axiom.context))) , 
                    z3.Implies(  z3.And( preconds) ,   l == r),
                patterns = [z3.MultiPattern( l , ctx_patterns...  ) , z3.MultiPattern( r , ctx_patterns...  ) ])
                    catch e
                      println(e)
                       z3.ForAll( map(x -> z3ify(x,ctx), collect(keys(axiom.context))) , 
                        z3.Implies(  z3.And( preconds) ,   l == r))
                end
                elseif length(axiom.context) > 0  && length(preconds) == 0
                    z3.ForAll( map(x -> z3ify(x,ctx), collect(keys(axiom.context))) , l == r, patterns = [l,r])
                
                else
                    l == r
                end
            end,
        axioms)
end

# jut trying some stuff out
sortify( :Ob )
sortify( :(Hom(a,b)))
ctx = Dict(:A => :Ob, :B => :Ob)
z3ify(:(id(A)) , ctx)
#=typing_axioms = build_typo_z3(theory(CartesianCategory).terms)
eq_axioms = build_eqs_z3(theory(CartesianCategory).axioms)

s = z3.Solver()
s.add(typing_axioms)
s.add(eq_axioms)
#print(s.sexpr())
=#

inferall(e::Symbol, ctx) = [typo(e,ctx) == z3ify(type_infer(e,ctx=ctx),ctx)]
inferall(e::Expr, ctx) = Iterators.flatten([[typo(e,ctx) == z3ify(type_infer(e,ctx=ctx),ctx)], Iterators.flatten(map(z -> inferall(z,ctx), e.args[2:end]))])


function prove(ctx, l,r; pr = false)
    typing_axioms = build_typo_z3(theory(CartesianCategory).terms)
    eq_axioms = build_eqs_z3(theory(CartesianCategory).axioms)
    s = z3.Solver()
    s.add(typing_axioms)
    s.add(eq_axioms)
    s.add(collect(inferall(l,ctx)))
    s.add(collect(inferall(r,ctx)))
    s.add(z3.Not( z3ify(l,ctx) == z3ify(r,ctx)))
    #println("checking $x")
    #if pr
    println(s.sexpr())
     #else
    #println(s.check())
    #end
end
ctx =  Dict(:A => :Ob, :B => :Ob)
prove( ctx, :(pair(proj1(A,B), proj2(A,B))), :(otimes(id(A),id(B))))

The returned smtlib2 predicate with a (check-sat) manually added at the end

(declare-sort Ob 0)
(declare-sort TYPE 0)
(declare-sort Hom 0)
(declare-fun id (Ob) Hom)
(declare-fun Hom (Ob Ob) TYPE)
(declare-fun typo (Hom) TYPE)
(declare-fun compose (Hom Hom) Hom)
(declare-fun otimes (Ob Ob) Ob)
(declare-fun Ob () TYPE)
(declare-fun typo (Ob) TYPE)
(declare-fun otimes (Hom Hom) Hom)
(declare-fun munit () Ob)
(declare-fun braid (Ob Ob) Hom)
(declare-fun mcopy (Ob) Hom)
(declare-fun delete (Ob) Hom)
(declare-fun pair (Hom Hom) Hom)
(declare-fun proj1 (Ob Ob) Hom)
(declare-fun proj2 (Ob Ob) Hom)
(declare-fun B () Ob)
(declare-fun A () Ob)
(assert (forall ((A Ob)) (! (= (typo (id A)) (Hom A A)) :pattern ((id A)))))
(assert (forall ((A Ob) (B Ob) (C Ob) (f Hom) (g Hom))
  (! (=> (and (= (typo f) (Hom A B)) (= (typo g) (Hom B C)))
         (= (typo (compose f g)) (Hom A C)))
     :pattern ((compose f g) (Hom A B) (Hom B C)))))
(assert (forall ((A Ob) (B Ob)) (! (= (typo (otimes A B)) Ob) :pattern ((otimes A B)))))
(assert (forall ((A Ob) (B Ob) (C Ob) (D Ob) (f Hom) (g Hom))
  (! (=> (and (= (typo f) (Hom A B)) (= (typo g) (Hom C D)))
         (= (typo (otimes f g)) (Hom (otimes A C) (otimes B D))))
     :pattern ((otimes f g) (Hom A B) (Hom C D)))))
(assert (= (typo munit) Ob))
(assert (forall ((A Ob) (B Ob))
  (! (= (typo (braid A B)) (Hom (otimes A B) (otimes B A)))
     :pattern ((braid A B)))))
(assert (forall ((A Ob))
  (! (= (typo (mcopy A)) (Hom A (otimes A A))) :pattern ((mcopy A)))))
(assert (forall ((A Ob)) (! (= (typo (delete A)) (Hom A munit)) :pattern ((delete A)))))
(assert (forall ((A Ob) (B Ob) (C Ob) (f Hom) (g Hom))
  (! (=> (and (= (typo f) (Hom A B)) (= (typo g) (Hom A C)))
         (= (typo (pair f g)) (Hom A (otimes B C))))
     :pattern ((pair f g) (Hom A B) (Hom A C)))))
(assert (forall ((A Ob) (B Ob))
  (! (= (typo (proj1 A B)) (Hom (otimes A B) A)) :pattern ((proj1 A B)))))
(assert (forall ((A Ob) (B Ob))
  (! (= (typo (proj2 A B)) (Hom (otimes A B) B)) :pattern ((proj2 A B)))))
(assert (forall ((A Ob) (B Ob) (C Ob) (D Ob) (f Hom) (g Hom) (h Hom))
  (! (=> (and (= (typo f) (Hom A B))
              (= (typo g) (Hom B C))
              (= (typo h) (Hom C D)))
         (= (compose (compose f g) h) (compose f (compose g h))))
     :pattern ((compose (compose f g) h) (Hom A B) (Hom B C) (Hom C D))
     :pattern ((compose f (compose g h)) (Hom A B) (Hom B C) (Hom C D)))))
(assert (forall ((A Ob) (B Ob) (f Hom))
  (! (=> (and (= (typo f) (Hom A B))) (= (compose f (id B)) f))
     :pattern ((compose f (id B)) (Hom A B))
     :pattern (pattern f (Hom A B)))))
(assert (forall ((A Ob) (B Ob) (f Hom))
  (! (=> (and (= (typo f) (Hom A B))) (= (compose (id A) f) f))
     :pattern ((compose (id A) f) (Hom A B))
     :pattern (pattern f (Hom A B)))))
(assert (forall ((A Ob) (B Ob) (C Ob))
  (! (= (otimes (otimes A B) C) (otimes A (otimes B C)))
     :pattern ((otimes (otimes A B) C))
     :pattern ((otimes A (otimes B C))))))
(assert (forall ((A Ob))
  (! (= (otimes A munit) A) :pattern ((otimes A munit)) :pattern (pattern A))))
(assert (forall ((A Ob))
  (! (= (otimes munit A) A) :pattern ((otimes munit A)) :pattern (pattern A))))
(assert (forall ((A Ob) (B Ob) (C Ob) (X Ob) (Y Ob) (Z Ob) (f Hom) (g Hom) (h Hom))
  (! (=> (and (= (typo f) (Hom A X))
              (= (typo g) (Hom B Y))
              (= (typo h) (Hom C Z)))
         (= (otimes (otimes f g) h) (otimes f (otimes g h))))
     :pattern ((otimes (otimes f g) h) (Hom A X) (Hom B Y) (Hom C Z))
     :pattern ((otimes f (otimes g h)) (Hom A X) (Hom B Y) (Hom C Z)))))
(assert (forall ((A Ob)
         (B Ob)
         (C Ob)
         (X Ob)
         (Y Ob)
         (Z Ob)
         (f Hom)
         (h Hom)
         (g Hom)
         (k Hom))
  (! (=> (and (= (typo f) (Hom A B))
              (= (typo h) (Hom B C))
              (= (typo g) (Hom X Y))
              (= (typo k) (Hom Y Z)))
         (= (compose (otimes f g) (otimes h k))
            (otimes (compose f h) (compose g k))))
     :pattern ((compose (otimes f g) (otimes h k))
               (Hom A B)
               (Hom B C)
               (Hom X Y)
               (Hom Y Z))
     :pattern ((otimes (compose f h) (compose g k))
               (Hom A B)
               (Hom B C)
               (Hom X Y)
               (Hom Y Z)))))
(assert (forall ((A Ob) (B Ob))
  (! (= (id (otimes A B)) (otimes (id A) (id B)))
     :pattern ((id (otimes A B)))
     :pattern ((otimes (id A) (id B))))))
(assert (forall ((A Ob) (B Ob))
  (! (= (compose (braid A B) (braid B A)) (id (otimes A B)))
     :pattern ((compose (braid A B) (braid B A)))
     :pattern ((id (otimes A B))))))
(assert (forall ((A Ob) (B Ob) (C Ob))
  (! (= (braid A (otimes B C))
        (compose (otimes (braid A B) (id C)) (otimes (id B) (braid A C))))
     :pattern ((braid A (otimes B C)))
     :pattern ((compose (otimes (braid A B) (id C)) (otimes (id B) (braid A C)))))))
(assert (forall ((A Ob) (B Ob) (C Ob))
  (! (= (braid (otimes A B) C)
        (compose (otimes (id A) (braid B C)) (otimes (braid A C) (id B))))
     :pattern ((braid (otimes A B) C))
     :pattern ((compose (otimes (id A) (braid B C)) (otimes (braid A C) (id B)))))))
(assert (forall ((A Ob) (B Ob) (C Ob) (D Ob) (f Hom) (g Hom))
  (! (=> (and (= (typo f) (Hom A B)) (= (typo g) (Hom C D)))
         (= (compose (otimes f g) (braid B D))
            (compose (braid A C) (otimes g f))))
     :pattern ((compose (otimes f g) (braid B D)) (Hom A B) (Hom C D))
     :pattern ((compose (braid A C) (otimes g f)) (Hom A B) (Hom C D)))))
(assert (forall ((A Ob))
  (! (= (compose (mcopy A) (otimes (mcopy A) (id A)))
        (compose (mcopy A) (otimes (id A) (mcopy A))))
     :pattern ((compose (mcopy A) (otimes (mcopy A) (id A))))
     :pattern ((compose (mcopy A) (otimes (id A) (mcopy A)))))))
(assert (forall ((A Ob))
  (! (= (compose (mcopy A) (otimes (delete A) (id A))) (id A))
     :pattern ((compose (mcopy A) (otimes (delete A) (id A))))
     :pattern ((id A)))))
(assert (forall ((A Ob))
  (! (= (compose (mcopy A) (otimes (id A) (delete A))) (id A))
     :pattern ((compose (mcopy A) (otimes (id A) (delete A))))
     :pattern ((id A)))))
(assert (forall ((A Ob))
  (! (= (compose (mcopy A) (braid A A)) (mcopy A))
     :pattern ((compose (mcopy A) (braid A A)))
     :pattern ((mcopy A)))))
(assert (forall ((A Ob) (B Ob))
  (! (let ((a!1 (compose (otimes (mcopy A) (mcopy B))
                         (otimes (otimes (id A) (braid A B)) (id B)))))
       (= (mcopy (otimes A B)) a!1))
     :pattern ((mcopy (otimes A B)))
     :pattern ((compose (otimes (mcopy A) (mcopy B))
                        (otimes (otimes (id A) (braid A B)) (id B)))))))
(assert (forall ((A Ob) (B Ob))
  (! (= (delete (otimes A B)) (otimes (delete A) (delete B)))
     :pattern ((delete (otimes A B)))
     :pattern ((otimes (delete A) (delete B))))))
(assert (= (mcopy munit) (id munit)))
(assert (= (delete munit) (id munit)))
(assert (forall ((A Ob) (B Ob) (C Ob) (f Hom) (g Hom))
  (! (=> (and (= (typo f) (Hom C A)) (= (typo g) (Hom C B)))
         (= (pair f g) (compose (mcopy C) (otimes f g))))
     :pattern ((pair f g) (Hom C A) (Hom C B))
     :pattern ((compose (mcopy C) (otimes f g)) (Hom C A) (Hom C B)))))
(assert (forall ((A Ob) (B Ob))
  (! (= (proj1 A B) (otimes (id A) (delete B)))
     :pattern ((proj1 A B))
     :pattern ((otimes (id A) (delete B))))))
(assert (forall ((A Ob) (B Ob))
  (! (= (proj2 A B) (otimes (delete A) (id B)))
     :pattern ((proj2 A B))
     :pattern ((otimes (delete A) (id B))))))
(assert (forall ((A Ob) (B Ob) (f Hom))
  (! (=> (and (= (typo f) (Hom A B)))
         (= (compose f (mcopy B)) (compose (mcopy A) (otimes f f))))
     :pattern ((compose f (mcopy B)) (Hom A B))
     :pattern ((compose (mcopy A) (otimes f f)) (Hom A B)))))
(assert (forall ((A Ob) (B Ob) (f Hom))
  (=> (and (= (typo f) (Hom A B))) (= (compose f (delete B)) (delete A)))))
(assert (= (typo (pair (proj1 A B) (proj2 A B))) (Hom (otimes A B) (otimes A B))))
(assert (= (typo (proj1 A B)) (Hom (otimes A B) A)))
(assert (= (typo A) Ob))
(assert (= (typo B) Ob))
(assert (= (typo (proj2 A B)) (Hom (otimes A B) B)))
(assert (= (typo A) Ob))
(assert (= (typo B) Ob))
(assert (= (typo (otimes (id A) (id B))) (Hom (otimes A B) (otimes A B))))
(assert (= (typo (id A)) (Hom A A)))
(assert (= (typo A) Ob))
(assert (= (typo (id B)) (Hom B B)))
(assert (= (typo B) Ob))
(assert (not (= (pair (proj1 A B) (proj2 A B)) (otimes (id A) (id B)))))
(check-sat)

Other junk

One could use z3 as glue for simple steps of proofs as is, but it doesn’t appear to scale well to even intermediately complex proofs. Maybe this could be used for a semi-automated (aka interactive) proof system for catlab? This seems misguided though. You’re better off using one of the many interactive proof assistants if that’s the way you wanna go. Maybe one could generate the queries to those system?

I tried the type tagging version, where every term t is recursively replaced with tag(t, typo_t). This allows us to avoid the guards and the axioms of the GAT take the form of pure equations again, albeit ones of complex tagged terms. This did not work well. I was surprised. It’s kind of interesting that type tagging is in some sense internalizing another piece of Catlab syntax into a logic, just like how type guards internalized the turnstile as an implication and the context as the guard. In this case we are internalizing the inline type annotations (f::Hom(A,B)) into the logic, where I write the infix notation :: as the function tag().

Notebook here https://github.com/philzook58/thoughtbooks/blob/master/catlab_gat.ipynb

file:///home/philip/Downloads/A_Polymorphic_Intermediate_Verification_Language_D.pdf The 3.1 method. If we have an extra argument to every function for the type of that argument inserted, then quantifier instantiation can only work when the

We could make it semi interactive (I guess semi interactive is just interactive though

https://hal.inria.fr/hal-01322328/document TLA+ encoding. Encoding to SMT solvers is a grand tradition

Wait, could it be that id really is the only problem? It’s the only equation with a raw variable in an equality. And that poisons all of Hom. Fascinating. I thought the problem was compose, but it’s id?

https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7324017/ vampire now supports polymorphism.

I realized that things that felt like a single step, were in fact not. This is because

Asserting the types of all subexpressions helped the solver sometimes and sometime hurt.

Solvers often use a heuristic where they want to look at the oldest generated inferences first. This means that the deeper you make your proof, the hard it is to for the solver to find it (well that’s true anyway). Making the proof depth harder for trivial type inference purposes is foolish.

Of course, taken to some extreme, at a certain point we’re asserting so many derived facts to the solver we have written a fraction of a solver ourselves.

I wonder what the recent burst of higher order capabilities of zipperposition, eprover, and vampire might do for me? The thing is we’re already compiling to combinators. That’s what categories are. https://matryoshka-project.github.io/

Functor example http://page.mi.fu-berlin.de/cbenzmueller/papers/J22.pdf THF is higher order format of tptp.

Exporting to Isabelle in particular is a viable approach, as it is well known to have good automation. I mean, I’m reading the sledgehammer guy’s papers for tips. Also, exporting to an interactive theorem prover of any kind seems kind of useful.

Notes on Synthesis and Equation Proving for Catlab.jl

Catlab is a library and growing ecosystem (I guess the ecosystem is called AlgebraicJulia now) for computational or applied category theory, whatever that may end up meaning.

I have been interested to see if I could find low hanging fruit by applying off the shelf automated theorem proving tech to Catlab.jl.

There area couple problems that seem like some headway might be made in this way:

  • Inferring the type of expressions. Catlab category syntax is pretty heavily annotated by objects so this is relatively easy. (id is explicitly tagged by the object at which it is based for example)
  • Synthesizing morphisms of a given type.
  • Proving equations

In particular two promising candidates for these problems are to use eprover/vampire style automated theorem provers or prolog/kanren logic programming.

Generalized Algebraic Theories (GATs)

Catlab is built around something known as a Generalized Algebraic Theory. https://algebraicjulia.github.io/Catlab.jl/dev/#What-is-a-GAT? In order to use more conventional tooling, we need to understand GATs in a way that is acceptable to these tools. Basically, can we strip the GAT down to first order logic?

I found GATs rather off putting at first glance. Who ordered that? The nlab article is 1/4 enlightening and 3/4 obscuring. https://ncatlab.org/nlab/show/generalized+algebraic+theory But, in the end of the day, I think it it’s not such a crazy thing.

Because of time invested and natural disposition, I understand things much better when they are put in programming terms. As seems to be not uncommon in Julia, one defines a theory in Catlab using some specialized macro mumbo jumbo.

@theory Category{Ob,Hom} begin
  @op begin
    (→) := Hom
    (⋅) := compose
  end

  Ob::TYPE
  Hom(dom::Ob, codom::Ob)::TYPE

  id(A::Ob)::(A → A)
  compose(f::(A → B), g::(B → C))::(A → C) ⊣ (A::Ob, B::Ob, C::Ob)

  (f ⋅ g) ⋅ h == f ⋅ (g ⋅ h) ⊣ (A::Ob, B::Ob, C::Ob, D::Ob,
                                f::(A → B), g::(B → C), h::(C → D))
  f ⋅ id(B) == f ⊣ (A::Ob, B::Ob, f::(A → B))
  id(A) ⋅ f == f ⊣ (A::Ob, B::Ob, f::(A → B))
end

Ok, but this macro boils down to a data structure describing the syntax, typing relations, and axioms of the theory. This data structure is not necessarily meant to be used by end users, and may change in it’s specifics, but I find it clarifying to see it.

Just like my python survival toolkit involves calling dir on everything, my Julia survival toolkit involves hearty application of dump and @macroexpand on anything I can find.

We can see three slots for types terms and axioms. The types describe the signature of the types, how many parameters they have and of what type. The terms describe the appropriate functions and constants of the theory. It’s all kind of straightforward I think. Try to come up with a data structure for this and you’ll probably come up with something similar

I’ve cut some stuff out of the dump because it’s so huge. I’ve placed the full dump at the end of the blog post.

>>> dump(theory(Category))

Catlab.GAT.Theory
  types: Array{Catlab.GAT.TypeConstructor}((2,))
    1: Catlab.GAT.TypeConstructor
      name: Symbol Ob
      params: Array{Symbol}((0,))
      context: OrderedCollections.OrderedDict{Symbol,Union{Expr, Symbol}}
        slots: Array{Int32}((16,)) Int32[0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
        keys: Array{Symbol}((0,))
        vals: Array{Union{Expr, Symbol}}((0,))
        ndel: Int64 0
        dirty: Bool false
      doc: String " Object in a category "
    2: ... More stuff
  terms: Array{Catlab.GAT.TermConstructor}((2,))
    1: Catlab.GAT.TermConstructor
      name: Symbol id
      params: Array{Symbol}((1,))
        1: Symbol A
      typ: Expr
        head: Symbol call
        args: Array{Any}((3,))
          1: Symbol Hom
          2: Symbol A
          3: Symbol A
      context: OrderedCollections.OrderedDict{Symbol,Union{Expr, Symbol}}
        slots: Array{Int32}((16,)) Int32[0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
        keys: Array{Symbol}((1,))
          1: Symbol A
        vals: Array{Union{Expr, Symbol}}((1,))
          1: Symbol Ob
        ndel: Int64 0
        dirty: Bool true
      doc: Nothing nothing
    2: ... More stuff
  axioms: Array{Catlab.GAT.AxiomConstructor}((3,))
    1: Catlab.GAT.AxiomConstructor
      name: Symbol ==
      left: Expr
        head: Symbol call
        args: Array{Any}((3,))
          1: Symbol compose
          2: Expr
            head: Symbol call
            args: Array{Any}((3,))
              1: Symbol compose
              2: Symbol f
              3: Symbol g
          3: Symbol h
      right: Expr
        head: Symbol call
        args: Array{Any}((3,))
          1: Symbol compose
          2: Symbol f
          3: Expr
            head: Symbol call
            args: Array{Any}((3,))
              1: Symbol compose
              2: Symbol g
              3: Symbol h
      context: OrderedCollections.OrderedDict{Symbol,Union{Expr, Symbol}}
        slots: Array{Int32}((16,)) Int32[5, 0, 0, 0, 1, 0, 4, 0, 2, 7, 0, 6, 0, 0, 0, 3]
        keys: Array{Symbol}((7,))
          1: Symbol A
          2: Symbol B
          3: Symbol C
          4: Symbol D
          5: Symbol f
          6: Symbol g
          7: Symbol h
        vals: Array{Union{Expr, Symbol}}((7,))
          1: Symbol Ob
          2: Symbol Ob
          3: Symbol Ob
          4: Symbol Ob
          5: Expr
            head: Symbol call
            args: Array{Any}((3,))
              1: Symbol Hom
              2: Symbol A
              3: Symbol B
          6: Expr
            head: Symbol call
            args: Array{Any}((3,))
              1: Symbol Hom
              2: Symbol B
              3: Symbol C
          7: Expr
            head: Symbol call
            args: Array{Any}((3,))
              1: Symbol Hom
              2: Symbol C
              3: Symbol D
        ndel: Int64 0
        dirty: Bool true
      doc: Nothing nothing
    2: ... More stuff
  aliases: ... Stuff

This infrastructure is not necessarily for category theory alone despite being in a package called Catlab. You can describe other algebraic theories, like groups, but you won’t need the full flexibility in typing relations that the “Generalized” of the GAT gets you. The big hangup of category theory that needs this extra power is that categorical composition is a partial function. It is only defined for morphisms whose types line up correctly, whereas any two group elements can be multiplied.

@theory Group(G) begin

  G::TYPE

  id()::G
  mul(f::G, g::G)::G
  inv(x::G)::G

  mul(mul(f, g), h) == mul(f,  mul(g , h)) ⊣ ( f::G, g::G, h::G)
   # and so on
end

Back to the first order logic translation. If you think about it, the turnstile ⊣ separating the context appearing in the Catlab theory definition is basically an implication. The definition id(A)::Hom(A,A) ⊣ (A::Ob) can be read like so: for all A, given A has type Ob it implies that id(A) has type Hom(A,A). We can write this in first order logic using a predicate for the typing relation. \forall A,  type(A,Ob) \implies type(id(A), Hom(A,A)).

The story I tell about this is that the way this deals with the partiality of compose is that when everything is well typed, compose behaves as it axiomatically should, but when something is not well typed, compose can return total garbage. This is one way to make a partial function total. Just define it to return random trash for the undefined domain values or rather be unwilling to commit to what it does in that case.

Even thought they are the same thing, I have great difficulty getting over the purely syntactical barrier of _::_ vs type(_,_). Infix punctuation never feels like a predicate to me. Maybe I’m crazy.

Turnstiles in general are usually interchangeable with or reflections of implication in some sense. So are the big horizontal lines of inference rules for that matter. I find this all very confusing.

Everything I’ve said above is a bold claim that could be actually proven by demonstrating a rigorous correspondence, but I don’t have enough interest to overcome the tremendous skill gap I’m lacking needed to do so. It could very easily be that I’m missing subtleties.

Automated Theorem Provers

While the term automated theorem prover could describe any theorem prover than is automated, it happens to connote a particular class of first order logic automated provers of which the E prover and Vampire are canonical examples.

In a previous post, I tried axiomatizing category theory to these provers in a different way https://www.philipzucker.com/category-theory-in-the-e-automated-theorem-prover/ , with a focus on the universal properties of categorical constructions. Catlab has a different flavor and a different encoding seems desirable.

What is particularly appealing about this approach is that these systems are hard wired to handle equality efficiently. So they can handle the equational specification of a Catlab theory. I don’t currently know to interpret to proofs it outputs into something more human comprehensible.

Also, I wasn’t originally aware of this, but eprover has a mode --conjectures-are-questions that will return the answers to existential queries. In this way, eprover can be used as a synthesizer for morphisms of a particular type. This flag gives eprover query capabilities similar to a prolog.

eprover cartcat.tptp --conjectures-are-questions --answers=1 --silent

One small annoying hiccup is that TPTP syntax takes the prolog convention of making quantified variables capitalized. This is not the Catlab convention. A simple way to fix this is to append a prefix of Var* to quantified objects and const* to constant function symbols.

All of the keys in the context dictionary are the quantified variables in an declaration. We can build a map to symbols where they are prefixed with Var

varmap = Dict(map(kv -> kv[1] => Symbol("Var$(kv[1])")  , collect(myterm.context )))

And then we can use this map to prefixify other expressions.

prefixify(x::Symbol, varmap) = haskey(varmap,x) ?  varmap[x] : Symbol( "const$x")
prefixify(x::Expr, varmap) = Expr(x.head, map(y -> prefixify(y, varmap),  x.args)... )

Given these, it has just some string interpolation hackery to port a catlab typing definition into a TPTP syntax axiom about a typing relation

function build_typo(terms)
    map(myterm ->  begin
                varmap = Dict(map(kv -> kv[1] => Symbol("Var$(kv[1])")  , collect(myterm.context )))
                prefix_context = Dict(map(kv -> kv[1] => prefixify(kv[2] , varmap) , collect(myterm.context )))
                context_terms = map( kv -> "typo($(varmap[kv[1]]), $(kv[2]))", collect(prefix_context))
                conc = "typo( const$(myterm.name)($(join(map(p -> prefixify(p,varmap) , myterm.params), ", "))) , $(prefixify(myterm.typ, varmap)) )"
                if length(myterm.context) > 0
                    "
                    ![$(join(values(varmap),","))]: 
                        ($conc <=
                            ($(join( context_terms , " &\n\t"))))"
                else # special case for empty context
                    "$conc"
                end
                    end
    , terms)
end

You can spit out the axioms for a theory like so

query = join(map(t -> "fof( axiom$(t[1]) , axiom, $(t[2]) ).", enumerate(build_typo(theory(CartesianCategory).terms))), "\n")
fof( axiom1 , axiom, 
![VarA]: 
    (typo( constid(VarA) , constHom(VarA, VarA) ) <=
        (typo(VarA, constOb))) ).
fof( axiom2 , axiom, 
![Varf,VarA,VarB,Varg,VarC]: 
    (typo( constcompose(Varf, Varg) , constHom(VarA, VarC) ) <=
        (typo(Varf, constHom(VarA, VarB)) &
	typo(VarA, constOb) &
	typo(VarB, constOb) &
	typo(Varg, constHom(VarB, VarC)) &
	typo(VarC, constOb))) ).
fof( axiom3 , axiom, 
![VarA,VarB]: 
    (typo( constotimes(VarA, VarB) , constOb ) <=
        (typo(VarA, constOb) &
	typo(VarB, constOb))) ).
fof( axiom4 , axiom, 
![Varf,VarA,VarD,VarB,Varg,VarC]: 
    (typo( constotimes(Varf, Varg) , constHom(constotimes(VarA, VarC), constotimes(VarB, VarD)) ) <=
        (typo(Varf, constHom(VarA, VarB)) &
	typo(VarA, constOb) &
	typo(VarD, constOb) &
	typo(VarB, constOb) &
	typo(Varg, constHom(VarC, VarD)) &
	typo(VarC, constOb))) ).
fof( axiom5 , axiom, typo( constmunit() , constOb ) ).
fof( axiom6 , axiom, 
![VarA,VarB]: 
    (typo( constbraid(VarA, VarB) , constHom(constotimes(VarA, VarB), constotimes(VarB, VarA)) ) <=
        (typo(VarA, constOb) &
	typo(VarB, constOb))) ).
fof( axiom7 , axiom, 
![VarA]: 
    (typo( constmcopy(VarA) , constHom(VarA, constotimes(VarA, VarA)) ) <=
        (typo(VarA, constOb))) ).
fof( axiom8 , axiom, 
![VarA]: 
    (typo( constdelete(VarA) , constHom(VarA, constmunit()) ) <=
        (typo(VarA, constOb))) ).
fof( axiom9 , axiom, 
![Varf,VarA,VarB,Varg,VarC]: 
    (typo( constpair(Varf, Varg) , constHom(VarA, constotimes(VarB, VarC)) ) <=
        (typo(Varf, constHom(VarA, VarB)) &
	typo(VarA, constOb) &
	typo(VarB, constOb) &
	typo(Varg, constHom(VarA, VarC)) &
	typo(VarC, constOb))) ).
fof( axiom10 , axiom, 
![VarA,VarB]: 
    (typo( constproj1(VarA, VarB) , constHom(constotimes(VarA, VarB), VarA) ) <=
        (typo(VarA, constOb) &
	typo(VarB, constOb))) ).
fof( axiom11 , axiom, 
![VarA,VarB]: 
    (typo( constproj2(VarA, VarB) , constHom(constotimes(VarA, VarB), VarB) ) <=
        (typo(VarA, constOb) &
	typo(VarB, constOb))) ).

% example synthesis queries
%fof(q , conjecture, ?[F]: (typo( F, constHom(a , a) )  <=  ( typo(a, constOb)  )   ) ).
%fof(q , conjecture, ?[F]: (typo( F, constHom( constotimes(a,b) , constotimes(b,a)) )  <=  ( typo(a, constOb) & typo(b,constOb) )   ) ).
%fof(q , conjecture, ?[F]: (typo( F, constHom( constotimes(a,constotimes(b,constotimes(c,d))) , d) )  <=  ( typo(a, constOb) & typo(b,constOb) & typo(c,constOb) & typo(d,constOb) )   ) ). % this one hurts already without some axiom pruning

For dealing with the equations of the theory, I believe we can just ignore the typing relations. Each equation axiom preserves well-typedness, and as long as our query is also well typed, I don’t think anything will go awry. Here it would be nice to have the proof output of the tool be more human readable, but I don’t know how to do that yet. Edit: It went awry. I currently think this is completely wrong.

function build_eqs(axioms)
        map(axiom -> begin
            @assert axiom.name == :(==)
            varmap = Dict(map(kv -> kv[1] => Symbol("Var$(kv[1])")  , collect(axiom.context )))
            l = prefixify(axiom.left, varmap)
            r = prefixify(axiom.right, varmap)
            "![$(join(values(varmap), ", "))]: $l = $r" 
            end,
        axioms)
end

t = join( map( t -> "fof( axiom$(t[1]), axiom, $(t[2]))."  , enumerate(build_eqs(theory(CartesianCategory).axioms))), "\n")
print(t)
fof( axiom1, axiom, ![Varf, VarA, VarD, VarB, Varh, Varg, VarC]: constcompose(constcompose(Varf, Varg), Varh) = constcompose(Varf, constcompose(Varg, Varh))).
fof( axiom2, axiom, ![Varf, VarA, VarB]: constcompose(Varf, constid(VarB)) = Varf).
fof( axiom3, axiom, ![Varf, VarA, VarB]: constcompose(constid(VarA), Varf) = Varf).
fof( axiom4, axiom, ![Varf, VarA, VarB, Varg, VarC]: constpair(Varf, Varg) = constcompose(constmcopy(VarC), constotimes(Varf, Varg))).
fof( axiom5, axiom, ![VarA, VarB]: constproj1(VarA, VarB) = constotimes(constid(VarA), constdelete(VarB))).
fof( axiom6, axiom, ![VarA, VarB]: constproj2(VarA, VarB) = constotimes(constdelete(VarA), constid(VarB))).
fof( axiom7, axiom, ![Varf, VarA, VarB]: constcompose(Varf, constmcopy(VarB)) = constcompose(constmcopy(VarA), constotimes(Varf, Varf))).
fof( axiom8, axiom, ![Varf, VarA, VarB]: constcompose(Varf, constdelete(VarB)) = constdelete(VarA)).

% silly example query
fof( q, conjecture, ![Varf, Varh, Varg, Varj ]: constcompose(constcompose(constcompose(Varf, Varg), Varh), Varj) = constcompose(Varf, constcompose(Varg, constcompose(Varh,Varj)) )).

It is possible and perhaps desirable fully automating the call to eprover as an external process and then parsing the results back into Julia. Julia has some slick external process facilities https://docs.julialang.org/en/v1/manual/running-external-programs/

Prolog and Kanrens

It was an interesting revelation to me that the typing relations for morphisms as described in catlab seems like it is already basically in the form amenable to prolog or a Kanren. The variables are universally quantified and there is only one term to the left of the turnstile (which is basically prolog’s :-) This is a Horn clause.

In a recent post I showed how to implement something akin to a minikanren in Julia https://www.philipzucker.com/yet-another-microkanren-in-julia/ I built that with this application in mind

Here’s an example I wrote by hand in in minikaren

(define (typo f t)
(conde
  [(fresh (a) (== f 'id) (== t `(hom ,a ,a))) ]
  [(== f 'f) (== t '(hom a c))]
  [(fresh (a b) (== f 'snd) (== t `(hom ( ,a ,b) ,b)))]
  [(fresh (a b) (== f 'fst) (== t `(hom ( ,a ,b) ,a)))]
  [(fresh (g h a b c) (== f `(comp ,g ,h))
                       (== t `(hom ,a ,c)) 
                       (typo g `(hom ,a ,b ))
                       (typo h `(hom ,b ,c)))]
  [ (fresh (g h a b c) (== f `(fan ,g ,h))
                       (== t `(hom ,a (,b ,c))) 
                       (typo g `(hom ,a ,b ))
                       (typo h `(hom ,a ,c)))  ]
  )
  )

;queries
; could lose the hom
;(run 3 (q) (typo  q '(hom (a b) a)))
;(run 3 (q) (typo  q '(hom ((a b) c) a)))
(run 3 (q) (typo  q '(hom (a b) (b a))))

And here is a similar thing written in my Julia minikanren. I had to depth limit it because I goofed up the fair interleaving in my implementation.

function typo(f, t, n)
    fresh2( (a,b) -> (f ≅ :fst) ∧ (t  ≅ :(Hom(tup($a,$b),$a)))) ∨
    fresh2( (a,b) -> (f ≅ :snd) ∧ (t  ≅ :(Hom(tup($a,$b),$b)))) ∨
    freshn( 6, (g,h,a,b,c,n2) -> (n ≅ :(succ($n2))) ∧ (f ≅ :(comp($g, $h)))  ∧ (t  ≅ :(Hom($a,$c))) ∧ @Zzz(typo(g, :(Hom($a,$b)), n2))  ∧ @Zzz(typo(h, :(Hom($b,$c)), n2))) ∨
    fresh(a -> (f ≅ :(id($a))) ∧ (t  ≅ :(Hom($a,$a))))
end


run(1, f ->  typo( f  , :(Hom(tup(a,tup(b,tup(c,d))),d)), nat(5)))

Bits and Bobbles

Discussion on the Catlab zulip. Some interesting discussion here such as an alternative encoding of GATs to FOL https://julialang.zulipchat.com/#narrow/stream/230248-catlab.2Ejl/topic/Automatic.20Theorem.20Proving/near/207919104

Of course, it’d be great it these solvers were bullet proof. But they aren’t. They are solving very hard questions more or less by brute force. So the amount of scaling they can achieve can be resolved by experimentation only. It may be that using these solvers is a dead end. These solvers do have a number of knobs to turn. The command line argument list to eprover is enormous.

These solvers are all facing some bad churn problems

  • Morphism composition is known to be a thing that makes dumb search go totally off the rails.
  • The identity morphism can be composed arbitrary number of times. This also makes solvers churn
  • Some catlab theories are overcomplete.
  • Some catlab theories are capable are building up and breaking down the same thing over and over (complicated encodings of id like pair(fst,snd))).

use SMT? https://github.com/ahumenberger/Z3.jl SMT is capable of encoding the equational problems if you use quantifiers (which last I checked these bindings do not yet export) . Results may vary. SMT with quantifiers is not the place where they shine the most. Is there anything else that can be fruitfully encoded to SMT? SAT?

Custom heuristics for search. Purely declarative is too harsh a goal. Having pure Julia solution is important here.

GAP.jl https://github.com/oscar-system/GAP.jl has facilities for knuth-bendix. This might be useful for finitely presented categories. It would be interesting to explore what pieces of computational group theory are applicable or analogous to computational category theory

>>> dump(theory(Category))

Catlab.GAT.Theory
  types: Array{Catlab.GAT.TypeConstructor}((2,))
    1: Catlab.GAT.TypeConstructor
      name: Symbol Ob
      params: Array{Symbol}((0,))
      context: OrderedCollections.OrderedDict{Symbol,Union{Expr, Symbol}}
        slots: Array{Int32}((16,)) Int32[0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
        keys: Array{Symbol}((0,))
        vals: Array{Union{Expr, Symbol}}((0,))
        ndel: Int64 0
        dirty: Bool false
      doc: String " Object in a category "
    2: Catlab.GAT.TypeConstructor
      name: Symbol Hom
      params: Array{Symbol}((2,))
        1: Symbol dom
        2: Symbol codom
      context: OrderedCollections.OrderedDict{Symbol,Union{Expr, Symbol}}
        slots: Array{Int32}((16,)) Int32[0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 2, 0, 0]
        keys: Array{Symbol}((2,))
          1: Symbol dom
          2: Symbol codom
        vals: Array{Union{Expr, Symbol}}((2,))
          1: Symbol Ob
          2: Symbol Ob
        ndel: Int64 0
        dirty: Bool true
      doc: String " Morphism in a category "
  terms: Array{Catlab.GAT.TermConstructor}((2,))
    1: Catlab.GAT.TermConstructor
      name: Symbol id
      params: Array{Symbol}((1,))
        1: Symbol A
      typ: Expr
        head: Symbol call
        args: Array{Any}((3,))
          1: Symbol Hom
          2: Symbol A
          3: Symbol A
      context: OrderedCollections.OrderedDict{Symbol,Union{Expr, Symbol}}
        slots: Array{Int32}((16,)) Int32[0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
        keys: Array{Symbol}((1,))
          1: Symbol A
        vals: Array{Union{Expr, Symbol}}((1,))
          1: Symbol Ob
        ndel: Int64 0
        dirty: Bool true
      doc: Nothing nothing
    2: Catlab.GAT.TermConstructor
      name: Symbol compose
      params: Array{Symbol}((2,))
        1: Symbol f
        2: Symbol g
      typ: Expr
        head: Symbol call
        args: Array{Any}((3,))
          1: Symbol Hom
          2: Symbol A
          3: Symbol C
      context: OrderedCollections.OrderedDict{Symbol,Union{Expr, Symbol}}
        slots: Array{Int32}((16,)) Int32[4, 0, 0, 0, 1, 0, 0, 0, 2, 0, 0, 5, 0, 0, 0, 3]
        keys: Array{Symbol}((5,))
          1: Symbol A
          2: Symbol B
          3: Symbol C
          4: Symbol f
          5: Symbol g
        vals: Array{Union{Expr, Symbol}}((5,))
          1: Symbol Ob
          2: Symbol Ob
          3: Symbol Ob
          4: Expr
            head: Symbol call
            args: Array{Any}((3,))
              1: Symbol Hom
              2: Symbol A
              3: Symbol B
          5: Expr
            head: Symbol call
            args: Array{Any}((3,))
              1: Symbol Hom
              2: Symbol B
              3: Symbol C
        ndel: Int64 0
        dirty: Bool true
      doc: Nothing nothing
  axioms: Array{Catlab.GAT.AxiomConstructor}((3,))
    1: Catlab.GAT.AxiomConstructor
      name: Symbol ==
      left: Expr
        head: Symbol call
        args: Array{Any}((3,))
          1: Symbol compose
          2: Expr
            head: Symbol call
            args: Array{Any}((3,))
              1: Symbol compose
              2: Symbol f
              3: Symbol g
          3: Symbol h
      right: Expr
        head: Symbol call
        args: Array{Any}((3,))
          1: Symbol compose
          2: Symbol f
          3: Expr
            head: Symbol call
            args: Array{Any}((3,))
              1: Symbol compose
              2: Symbol g
              3: Symbol h
      context: OrderedCollections.OrderedDict{Symbol,Union{Expr, Symbol}}
        slots: Array{Int32}((16,)) Int32[5, 0, 0, 0, 1, 0, 4, 0, 2, 7, 0, 6, 0, 0, 0, 3]
        keys: Array{Symbol}((7,))
          1: Symbol A
          2: Symbol B
          3: Symbol C
          4: Symbol D
          5: Symbol f
          6: Symbol g
          7: Symbol h
        vals: Array{Union{Expr, Symbol}}((7,))
          1: Symbol Ob
          2: Symbol Ob
          3: Symbol Ob
          4: Symbol Ob
          5: Expr
            head: Symbol call
            args: Array{Any}((3,))
              1: Symbol Hom
              2: Symbol A
              3: Symbol B
          6: Expr
            head: Symbol call
            args: Array{Any}((3,))
              1: Symbol Hom
              2: Symbol B
              3: Symbol C
          7: Expr
            head: Symbol call
            args: Array{Any}((3,))
              1: Symbol Hom
              2: Symbol C
              3: Symbol D
        ndel: Int64 0
        dirty: Bool true
      doc: Nothing nothing
    2: Catlab.GAT.AxiomConstructor
      name: Symbol ==
      left: Expr
        head: Symbol call
        args: Array{Any}((3,))
          1: Symbol compose
          2: Symbol f
          3: Expr
            head: Symbol call
            args: Array{Any}((2,))
              1: Symbol id
              2: Symbol B
      right: Symbol f
      context: OrderedCollections.OrderedDict{Symbol,Union{Expr, Symbol}}
        slots: Array{Int32}((16,)) Int32[3, 0, 0, 0, 1, 0, 0, 0, 2, 0, 0, 0, 0, 0, 0, 0]
        keys: Array{Symbol}((3,))
          1: Symbol A
          2: Symbol B
          3: Symbol f
        vals: Array{Union{Expr, Symbol}}((3,))
          1: Symbol Ob
          2: Symbol Ob
          3: Expr
            head: Symbol call
            args: Array{Any}((3,))
              1: Symbol Hom
              2: Symbol A
              3: Symbol B
        ndel: Int64 0
        dirty: Bool true
      doc: Nothing nothing
    3: Catlab.GAT.AxiomConstructor
      name: Symbol ==
      left: Expr
        head: Symbol call
        args: Array{Any}((3,))
          1: Symbol compose
          2: Expr
            head: Symbol call
            args: Array{Any}((2,))
              1: Symbol id
              2: Symbol A
          3: Symbol f
      right: Symbol f
      context: OrderedCollections.OrderedDict{Symbol,Union{Expr, Symbol}}
        slots: Array{Int32}((16,)) Int32[3, 0, 0, 0, 1, 0, 0, 0, 2, 0, 0, 0, 0, 0, 0, 0]
        keys: Array{Symbol}((3,))
          1: Symbol A
          2: Symbol B
          3: Symbol f
        vals: Array{Union{Expr, Symbol}}((3,))
          1: Symbol Ob
          2: Symbol Ob
          3: Expr
            head: Symbol call
            args: Array{Any}((3,))
              1: Symbol Hom
              2: Symbol A
              3: Symbol B
        ndel: Int64 0
        dirty: Bool true
      doc: Nothing nothing
  aliases: Dict{Symbol,Symbol}
    slots: Array{UInt8}((16,)) UInt8[0x01, 0x00, 0x00, 0x00, 0x00, 0x01, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00]
    keys: Array{Symbol}((16,))
      1: Symbol ⋅
      2: #undef
      3: #undef
      4: #undef
      5: #undef
      ...
      12: #undef
      13: #undef
      14: #undef
      15: #undef
      16: #undef
    vals: Array{Symbol}((16,))
      1: Symbol compose
      2: #undef
      3: #undef
      4: #undef
      5: #undef
      ...
      12: #undef
      13: #undef
      14: #undef
      15: #undef
      16: #undef
    ndel: Int64 0
    count: Int64 2
    age: UInt64 0x0000000000000002
    idxfloor: Int64 1
    maxprobe: Int64 0