AlgebraicJulia / AlgebraicJulia/Catlab.jl
Taking Operad Expression Syntax Seriously
- Vorherrschende Sprache
- Julia
- Sterne
- 724
- Forks
- 73
- PR-Merge-Kennzahlen
- Keine gemergten PRs in 30 T.
Beschreibung
## Summary
I'd like to get serious about expressing the substitutions in operads that we need for operating on *hypergraph algebras* without converting them to morphisms in a hypergraph category. Since, context free grammars present free operads, they seem like the natural starting point for implementing syntax data structure. Of course CFGs are implemented as syntax trees like `Expr` in Julia.
## Problem
We currently don't have a way to express operads at the syntactic level. We have several instances of Operad(FinSetCosp) floating around (aka hypergraph algebras) including UWDs and RelationalPrograms, but no syntax for working at the symbolic level in a particular operad. In order to implement compositional computations without forcing hypergraph algebras into DWDs or GATExprs in a hypergraph Category (see #288), we need syntactic expressions that don't rely on being morphisms in a category, which forces an arbitrary choice of inputs and outputs, when we want to operate on *ports*.
## Proposed Solution
It seems like we should take in a Backus-Nauer Form (BNF) description of a grammar and generate the free operad for it, then we could define additional axioms to declare which expressions are equal. The syntactic expressions are then stored in regular ASTs like Expr or a new type `OExpr{Function}(head, args...)` which would be more tailorable and allow for using dispatch[1](#myfootnote1).
Operads have data structures that represent the equivalence classes of the `FreeOperad(Generators)/Relations` like in [Spivak2015, Modular Systems](http://math.mit.edu/~dspivak/informatics/talks/ModularSystems.pdf). So we would want to have an algorithm for doing that normalizing by computing that data structure from the expression. This would allow us to replicate our Theory, Syntax, Instance structure from Categories but for Operads.
I think this illustration is helpful

We could store the diagrams as the cospans with signature
`f = UWD(Ports --junctions--> Junctions <--outer_junctions-- OuterPorts)` where `Ports = Coproduct(ports(b) for b in Boxes)`
then substitution (port plugging) becomes the composing cospans by pushout of the overlapping span.

Translating to our notation of P is for Ports of the big diagram, Phat is the ports of the smaller diagrams, OP is the outer ports, J is for Junctions. The indexing set for the coproducts is Box.

## Questions
1. Do we need to go through the existing GAT infrastructure or is that more trouble than it is worth? If there is not standard approach to describing Operads as GATs, then let's just use BNF for the generators and a list of axioms for the relations.
2. How do we encode operad functors for specifying operad algebras?
3. How do we present `Operad(FinSetCosp)`?
4. Can we implement the cospan composition above for using colimits in Categorical algebra? (see #288) for context on why that would be appealing for implementing arbitrary OperadAlgebras for FinSetCosp.
1 : Let's avoid the `invoke_term` design this time.
Beitragsleitfaden
Bewertung
Dieses Issue wurde noch nicht bewertet.