Rewriting Implementation

[statusfailed]

Feature: Rewriting for Open Hypergraphs

Consider the following program using a (currently nonexistent) kernel language.

F32(M,N)
  ●----\            F32(M,N)                F32(M,N)
        [Map(add)]----●------[Map(negate)]------●
  ●----/
F32(M,N)

Interpret Map(f) as applying the kernel f to every element of each input array.
So add : f32 × f32 → f32 is the kernel, the Map(add) goes between arrays of f32.

We should be able to fuse the two "Map" kernels into one:

F32(M,N)
  ●----\                    F32(M,N)
        [Map(add ; negate)]----●
  ●----/
F32(M,N)

Where add : negate : f32 × f32 → f32 is the kernel x y → -(x+y)

Proposal: we do this by rewriting.
There are three parts to implement:

1. Identify a "match" (aka "LHS"): the region of the graph to rewrite (in example above, the two hyperedges Map(add), Map(negate), and their interfaces
2. Compute the result (aka "RHS"): in this case, the single op Map(add; negate)
3. Implement rewriting: replace LHS with RHS in the graph

Simple example

Here's a simpler example usable for testing. It corresponds to rewriting x + (-y) → x - y

----------------●----\                              ---●----\
                      [add]----●-----      ~>                [sub]----●-----
----●---[neg]---●----/                              ---●----/

This feature: a PR for open-hypergraphs

Assume both the match and RHS are known, so we only need to implement step (3) from above.
A rough sketch:

• Append the RHS into the graph
• Quotient the RHS interfaces with the match's interface
• Delete all non-interface data of the match

Acceptance criteria

• Propose API addition for rewriting in the lax module
• Datastructures for a Match in an open hypergraph
• Unit tests in the open hypergraphs library demonstrating successful rewrites;
  • Use evaluation to check rules like x + (-y) = x - y.

References/Glossary

• Open Hypergraphs library
• String Diagram Rewrite Theory paper series:
  • I
  • II
  • III