Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{ | |
"cells": [ | |
{ | |
"cell_type": "markdown", | |
"metadata": {}, | |
"source": [ | |
"# ZX calculus in Catlab" | |
] | |
}, | |
{ |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
class IntOrderCat(): | |
def __init__(self, dom, cod): | |
assert(dom <= cod) | |
self.cod = cod | |
self.dom = dom | |
self.f = () | |
def idd(n): | |
return IntOrderCat(n,n) | |
def compose(f,g): | |
assert( f.dom == g.cod ) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
import numpy as np | |
import scipy | |
import scipy.linalg | |
# https://docs.scipy.org/doc/numpy/user/basics.subclassing.html | |
class FinVect(np.ndarray): | |
def __new__(cls, input_array, info=None): | |
# Input array is an already formed ndarray instance | |
# We first cast to be our class type | |
obj = np.asarray(input_array).view(cls) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
from collections import Counter | |
class FinSet(): | |
def init(self, dom ,cod , f): | |
''' In order to specify a morphism, we need to give a python set that is the domain, a python set | |
that is the codomain, and a dictionary f that encodes a function between these two sets. | |
We could by assumption just use f.keys() implicitly as the domain, however the codomain is not inferable from just f. | |
In other categories that domain might not be either, so we chose to require both symmettrically. | |
''' | |
assert( dom == set(f.keys())) # f has value for everything in domain | |
assert( all( [y in cod for y in f.value()] )) # f has only values in codomain |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
def matrix_to_eqs(m): | |
nrows, ncols = m.shape | |
gens = [sy.Dummy() for i in range(ncols)] | |
eqs = m @ sy.Matrix(gens) | |
return eqs, gens | |
def eqs_to_matrix(eqns, gens): | |
return sy.Matrix( [[ eq.coeff(g) for g in gens] for eq in eqns]) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
def controller(Cat,pend_step, pos, vel): | |
acc = Cat.idd(3) | |
for i in range(10): | |
acc = acc @ pend_step | |
init = Cat.const(pos) * Cat.const(vel) * Cat.idd(1) | |
return acc @ init |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
from z3 import * | |
def compare_and_swap_z3(x,y): | |
x1, y1 = FreshInt(), FreshInt() | |
c = If(x <= y, And(x1 == x, y1 == y) , And(x1 == y, y1 == x) ) | |
return x1, y1, c | |
# predicates of interest | |
def sorted_list(x): # list is sorted | |
return And([x <= y for x,y in zip(x , x[1:])]) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
T = 10 # total number of time steps as a global parameter | |
class PetriCat(): | |
def compose(f,g): | |
def res(): | |
a, b , fcon = f() | |
b1, c, gcon = g() | |
return a, c, fcon + gcon + [b == b1] | |
def idd(): | |
def res() | |
x = cvx.Variable((T-1,1), integer = True) |