philzook58

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)

philzook58

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 )

philzook58

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# ZX calculus in Catlab"
   ]
  },
  {

philzook58

philzook58

philzook58

% Follow paper exactly.  https://arxiv.org/abs/1804.02452 See Appendix A
% Difference from unison model.mzn: Try not using integers. Try to use better minizinc syntax. Much simplified

include "globals.mzn";

%% ---------------------------------------
%% PARAMETERS
%% ---------------------------------------

% Type definitions

philzook58

(*|

I had a fun time giving a Z3 tutorial at Formal Methods for the Informal Engineer (FMIE) https://fmie2021.github.io/ (videos coming soon hopefully!). I got to be kind of the "fun dad" with the Z3 tutorial https://github.com/philzook58/z3_tutorial , while at times it felt a bit like Cody's Coq tutorial https://github.com/codyroux/broad-coq-tutorial was trying to feed the kids their vegetables. He knew it was going to be like this from the outset and had a fun little analogy of me downhill skiing while he was about to go on a cross country slog.

There are a number of factors to this. 
* I could use Z3's python bindings giving an air of familiarity, whereas everything was incredibly foreign in Coq.
* Z3 can actually be used to declaratively state problems and automatically calculate solutions to them with very little user help, which gives it a lot more "Wow" factor.
* Coq is a tool that requires significantly more background to even comprehend what the hell it is. I still think many aspects of it are tota

philzook58

using Pkg
Pkg.activate("metatheory")
Pkg.add(url="https://github.com/0x0f0f0f/Metatheory.jl.git")
using Metatheory
using Metatheory.EGraphs

cat_theory = @theory begin
	hom(hom(f, ob(a), ob(b)) ⋅ hom(id(ob(b)), ob(b), ob(b)), ob(a), ob(b)) == hom(f, ob(a), ob(b))
	hom(hom(id(ob(a)), ob(a), ob(a)) ⋅ hom(f, ob(a), ob(b)), ob(a), ob(b)) == hom(f, ob(a), ob(b))
	hom(hom(f, ob(a), ob(b)) ⋅ hom(hom(g, ob(b), ob(c)) ⋅ hom(h, ob(c), ob(d)), ob(b), ob(d)), ob(a), ob(d)) == hom(hom(hom(f, ob(a), ob(b)) ⋅ hom(g, ob(b), ob(c)), ob(a), ob(c)) ⋅ hom(h, ob(c), ob(d)), ob(a), ob(d))

philzook58

This is a simple script to convert Metatheory.jl https://github.com/0x0f0f0f/Metatheory.jl theories into an Egg https://egraphs-good.github.io/ query for comparison.

Get a rust toolchain https://rustup.rs/

Make a new project

cargo new my_project
cd my_project

philzook58

use egg::{*, rewrite as rw};
use wasm_bindgen::prelude::*;
use std::time::Duration;

define_language! {
    enum CatLanguage {
        // string variant with no children
        "id" = IdMorph(Id),
        "om" = OTimesM([Id; 2]),
        "oo" = OTimesO([Id; 2]),