Diagram#

class discopy.rigid.Diagram(dom, cod, boxes, offsets, layers=None)[source]#

Bases: Diagram

Implements diagrams in the free rigid monoidal category.

>>> I, n, s = Ty(), Ty('n'), Ty('s')
>>> Alice, jokes = Box('Alice', I, n), Box('jokes', I, n.r @ s)
>>> boxes, offsets = [Alice, jokes, Cup(n, n.r)], [0, 1, 0]
>>> d = Diagram(Alice.dom @ jokes.dom, s, boxes, offsets)
>>> print(d)
Alice >> Id(n) @ jokes >> Cup(n, n.r) @ Id(s)

>>> d.draw(figsize=(3, 2),
...        path='docs/_static/imgs/rigid/diagram-example.png')

foliate(yield_slices=False)[source]#

>>> x = Ty('x')
>>> f = Box('f', x, x)
>>> gen = (f @ Id(x) >> (f @ f)).foliate()
>>> print(next(gen))
f @ Id(x) >> Id(x) @ f >> f @ Id(x)

static cups(left, right)[source]#

Constructs nested cups witnessing adjointness of x and y.

>>> a, b = Ty('a'), Ty('b')
>>> assert Diagram.cups(a, a.r) == Cup(a, a.r)
>>> assert Diagram.cups(a @ b, (a @ b).r) ==\
...     Id(a) @ Cup(b, b.r) @ Id(a.r) >> Cup(a, a.r)

>>> Diagram.cups(a @ b, (a @ b).r).draw(figsize=(3, 1),\
... margins=(0.3, 0.05), path='docs/_static/imgs/rigid/cups.png')

static caps(left, right)[source]#

Constructs nested cups witnessing adjointness of x and y.

>>> a, b = Ty('a'), Ty('b')
>>> assert Diagram.caps(a, a.l) == Cap(a, a.l)
>>> assert Diagram.caps(a @ b, (a @ b).l) == (Cap(a, a.l)
...                 >> Id(a) @ Cap(b, b.l) @ Id(a.l))

static spiders(n_legs_in, n_legs_out, typ)[source]#: Constructs spiders with compound types.

static fa(left, right)[source]#: Forward application.

static ba(left, right)[source]#: Backward application.

static fc(left, middle, right)[source]#: Forward composition.

static bc(left, middle, right)[source]#: Backward composition.

static fx(left, middle, right)[source]#: Forward crossed composition.

static bx(left, middle, right)[source]#: Backward crossed composition.

static curry(diagram, n_wires=1, left=False)[source]#: Diagram currying.

transpose(left=False)[source]#

>>> a, b = Ty('a'), Ty('b')
>>> double_snake = Id(a @ b).transpose()
>>> two_snakes = Id(b).transpose() @ Id(a).transpose()
>>> double_snake == two_snakes
False
>>> *_, two_snakes_nf = monoidal.Diagram.normalize(two_snakes)
>>> assert double_snake == two_snakes_nf
>>> f = Box('f', a, b)

>>> a, b = Ty('a'), Ty('b')
>>> double_snake = Id(a @ b).transpose(left=True)
>>> snakes = Id(b).transpose(left=True) @ Id(a).transpose(left=True)
>>> double_snake == two_snakes
False
>>> *_, two_snakes_nf = monoidal.Diagram.normalize(
...     snakes, left=True)
>>> assert double_snake == two_snakes_nf
>>> f = Box('f', a, b)

normal_form(normalizer=None, **params)[source]#: Implements the normalisation of rigid monoidal categories, see arxiv:1601.05372, definition 2.12.

normalize(left=False)#

Return a generator which yields normalization steps.

>>> from discopy.rigid import *
>>> n, s = Ty('n'), Ty('s')
>>> cup, cap = Cup(n, n.r), Cap(n.r, n)
>>> f, g, h = Box('f', n, n), Box('g', s @ n, n), Box('h', n, n @ s)
>>> diagram = g @ cap >> f[::-1] @ Id(n.r) @ f >> cup @ h
>>> for d in diagram.normalize(): print(d)  
g... >> Cup(n, n.r) @ Id(n)...
g >> f[::-1] >> Id(n) @ Cap(n.r, n) >> Cup(n, n.r) @ Id(n) >> f >> h
g >> f[::-1] >> f >> h

id#: alias of Id

Diagram

Contents

Diagram#