Diagram rewriting

from discopy import Ty, Box, Id, Diagram

folder = lambda file: '../_static/imgs/' + file
params = dict(
    aspect='auto',
    loop=True,
    draw_type_labels=False)

A simple circuit

x = Ty('x')
copy, add = Box('copy', x, x @ x), Box('add', x @ x, x)
CX = copy @ Id(x) >> Id(x) @ add
XC = Id(x) @ copy >> add @ Id(x)
diagram = CX @ XC >> XC @ CX
rewrite_steps = diagram.normalize()

diagram.to_gif(*rewrite_steps,
               path=folder('simple-rewrite.gif'), **params)

Asymptotic worst-case

def spiral(n_cups):
    """
    Implements the asymptotic worst-case
    for normal_form, see arXiv:1804.07832.
    """
    x = Ty('x')
    unit, counit = Box('unit', Ty(), x), Box('counit', x, Ty())
    cup, cap = Box('cup', x @ x, Ty()), Box('cap', Ty(), x @ x)
    result = unit
    for i in range(n_cups):
        result = result >> Id(x ** i) @ cap @ Id(x ** (i + 1))
    result = result >> Id(x ** n_cups) @ counit @ Id(x ** n_cups)
    for i in range(n_cups):
        result = result >>\
            Id(x ** (n_cups - i - 1)) @ cup @ Id(x ** (n_cups - i - 1))
    return result


diagram = spiral(3)
diagram.to_gif(*diagram.normalize(),
               path=folder('spiral.gif'),
               **dict(params, draw_box_labels=False, loop=True, aspect='equal'))

Snake removal

snake = Box('f', x @ x, x @ x)\
    .transpose(left=True).transpose(left=True)\
    .transpose().transpose()

snake.to_gif(*snake.normalize(), **params,
             path=folder('snake-removal.gif'))