Module for linear algebra

epatters commented 4 years ago

ACT has a nice story to tell about linear algebra, through at least two paths:

Graphical linear algebra and the category of linear relations
Tensor algebra and categorical quantum mechanics

The Catlab standard library should include an implementation of these ideas. Besides its intrinsic interest, it may help newcomers who are puzzled about what Catlab actually does.

epatters commented 4 years ago

@jpfairbanks has a start on this in PR #64.

jpfairbanks commented 4 years ago

Based on our last discussion it makes sense to have a signature called LinearAlgebra that has both the tensor product monoidal product and the direct sum monoidal product. In this doctrine, how would we handle the fact that there are generators for every scalar (1x1 matrix). Would this be a generator parameterized by a Val{T<:Number}? For symbolic calculations present in must (numerical) linear algebra textbooks, it would be beneficial to have generators indexed by a symbol (variable name) so that you can talk about matrices

A = [ a b ]
    [ c d ]

or bidiagonal matrices

B = [ a1 b1          ]
    [    a2 b2       ]
    [       a3 b3    ]
    [          a4 b4 ]

This type of notation is really common in numerical linear algebra for describing matrix algorithms.

The bidiagonal matrices satisfy this recursive construction

@present Bidiagonal(FreeBicategoryRelations) begin
    R::Ob
    b::Hom(R,R)
    a::Hom(R,R)
    B::Hom(R⊗R, R⊗R)
    add::Hom(R⊗R, R)
end

R,b,a,B = map(x->generator(Bidiagonal,x), [:R, :b, :a, :B])
bidiag_recursion = (B⊗mcopy(R))⋅(id(R⊗R)⊗b⊗a)⋅(id(R)⊗mmerge(R)⊗id(R))

Handling the named scalars and the recursive definitions seems like important parts of getting GLA implemented in a useful way.

jpfairbanks commented 4 years ago

What I mean by recursive construction is that when B:R^n-1 --> R^n-1 is a bidiagonal matrix, then for any scalars a,b\in R, (B⊗mcopy(R))⋅(id(R⊗R)⊗b⊗a)⋅(id(R)⊗mmerge(R)⊗id(R)) will also be bidiagonal.

jpfairbanks commented 4 years ago

Just appending things to the GLA todo list.

The syntax / signature for LinearRel should support:

[ ] homs with scalars in them ie. mult(5)::Hom(R, R)
[ ] homs with symbolic scalars in them ie. mult(:a)::Hom(R, R)
[ ] homs with matrices in them ie. mult([1 -1; -1 1])::Hom(otimes(R,R), otimes(R,R))
[ ] homs with symbolic matrices in them ie. mult(:A)::Hom(otimes(R,R), otimes(R,R))
[ ] the isomorphism between a single wire carrying an object of type otimes(R,R,R,R) and four parallel wires carrying objects of type R. This might require introducing a new object constructor like vec(n::Int)::Ob with the axiom that vec(n) = otimes(R for i in 1:n)
[ ] constructors for types of matrices with special properties such as unitary(A::Symbol)::Ob which satisfies the axiom that compose(adjoint(unitary(A)), unitary(A)) = id(codom(A)) and compose(unitary(A), adjoint(unitary(A))) = id(dom(A)) or lower and upper triangular matrices which satisfy lower(A)::Ob; upper(A)::Ob with adjoint(lower(A))::upper; adjoint(upper)::lower

Jutho commented 4 years ago

Hi all;

I am trying to learn a bit about this very nice package, and noticed this second bullet point in this issue:

Tensor algebra and categorical quantum mechanics

So, over at TensorKit.jl, I've been working on a package for dealing with tensors, the building blocks of which are also based on the theory of monoidal categories. My knowledge of category theory is rather specific, and pertains to that part of category theory you need to understand quantum physics and topological order in condensed matter physics (it is essentially summarized here).

So TensorKit.jl has two important type (hierarchies). The first is a type hierarchy starting with the abstract type VectorSpace, which really should have been called LinearMonoidalCategory{𝕜}, as instances thereof represent objects in a 𝕜-linear monoidal category. In most cases, this is the category Vec, but there are actually parts of TensorKit.jl which go beyond the setting of Vec (most of the support so-far is for dagger pre-fusion categories, where objects are isomorphic to a direct sum of a finite family of simple objects, and there is a dagger operation, i.e. the setting of quantum mechanics, however this includes typical fusion categories like Fib(onacci), which have a non-symmetric braiding and are not subcategories of Vec.)

The second important type hierarchy (Abstract)TensorMap represents the corresponding morphisms. They have a domain and codomain which are VectorSpace objects, and there is a whole bunch of operations defined for them.

It seems like TensorKit.jl and Catlab.jl have much syntax in common (not a surprise), like domain, codomain, ⊗, ...

Now it certainly seems like some nice interface between Catlab.jl and TensorKit.jl are feasible (it seems like I could make the objects in TensorKit.jl a particular @instance of a certain @theory; and I could certainly benefit from the nice tools you have built to create, manipulate and visualize wiring diagrams. So far, in the community of tensor networks, when dealing with the category Vec, we use a flavor of string diagrams which is somewhat sloppy: we do not really care about inputs versus outputs, line crossings (braidings), etc, since all of the evaluation, coevaluation, braiding, ... maps are trivial for vector spaces. Essentially, then, you can encode the string diagram into just specifying which indices are connected with which using Einstein summation convention, and this has given rise to e.g. the @tensor macro in TensorOperations.jl.

However, for these more general categories, where in particular the braiding is not trivial, a properly formatted string diagram is what would be needed, and I currently don't have any support in my packages to deal with this.

One specific question: I noticed you have a SymmetricMonoidalCategory theory where you define a braid. But a general braid is not symmetric, correct? Symmetric means that compose(σ_{A,B} , σ_{B,A}) = munit(A ⊗ B) which need not be true.

Anyway, I will probably give this a try, but might need some help, so I am reaching out to see if you are interested in this and have thoughts to share?

jpfairbanks commented 4 years ago

Yes, we would really appreciate any help on implementing an instance of SMC or HypergraphCategory for TensorKit.

we use a flavor of string diagrams which is somewhat sloppy: we do not really care about inputs versus outputs, line crossings (braidings), etc, since all of the evaluation, coevaluation, braiding, ... maps are trivial for vector spaces.

The fact that you can get normalize out all the inputs/output/braiding/ caps/cups/idsfrom a these string diagrams is because they form a HyperGraph Category

Hypergraph Categories have undirected wiring diagrams, which are currently implemented to support categories of relations like FinRel the category of relations between finite sets. So if you make sure that your @theory inherits from HypergraphCategory then you should have all the term constructors that you need to use the undirected wiring diagrams.

We are currently organizing around the idea that there is a standard library of categories built out of the Julia Standard Libraries that ship with Catlab, and anything that requires a heavyweight dependency is in another package like the AlgebraicPetri.jl package which depends on DiffEQs.jl. If you want TensorKit to depend on Catlab, then you could add these features to TensorKit directly. Let us know if you need any help getting started.

Jutho commented 4 years ago

Thanks for the quick response.

The fact that you can get normalize out all the inputs/output/braiding/ caps/cups/idsfrom a these string diagrams is because they form a HyperGraph Category

Hypergraph Categories have undirected wiring diagrams, which are currently implemented to support categories of relations like FinRel the category of relations between finite sets. So if you make sure that your @theory inherits from HypergraphCategory then you should have all the term constructors that you need to use the undirected wiring diagrams.

Well, actually most of the vector spaces / objects in TensorKit.jl have dual( ... ) objects which are not equal to them self, and so the corresponding wiring diagram should have orientations/directions. The only exception would be what I've called CartesianSpace, the vector spaces over the reals with a euclidean inner product; the typical ℝ^n from classical physics; these are naturally isomorphic to their dual space.

So even in the case of a Euclidean space over the complex numbers, your typical ℂ^n (which is valid TensorKit.jl syntax), I do distinguish between the space and its dual, though most of my colleagues do indeed not use orientations, i.e. undirected wiring diagrams in that case. But you definitely need the orientations once you start to talk about tensors which have some symmetry (technically, which are morphisms in the category Rep{G} of some group G).

jpfairbanks commented 4 years ago

oh yeah, I was only thinking of R^n. You definitely need the orientations and such in that case so "sloppy" would be an appropriate characterization.

epatters commented 2 years ago

Closing because we now have a linear algebra module and also because we will likely spin off this module into its own package.

AlgebraicJulia / Catlab.jl

Module for linear algebra #65