| { | |
| "cells": [ | |
| { | |
| "cell_type": "markdown", | |
| "metadata": {}, | |
| "source": [ | |
| "# ZX calculus in Catlab" | |
| ] | |
| }, | |
| { |
| 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]) |
| % 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 |
| 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)) |
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
| 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]), |
| struct IntDisjointMap | |
| parents::Vector{Int64} | |
| values::Vector{Any} | |
| merge_fun | |
| end | |
| IntDisjointMap(merge_fun) = IntDisjointMap(Vector{Int64}[], [], merge_fun) | |
| Base.length(x::IntDisjointMap) = length(x.parents) |
| (*| | |
| A data structure that I've been more and more interested in recently is the disjoint set datastructure or union-find. | |
| https://en.wikipedia.org/wiki/Disjoint-set_data_structure It's used in egraphs, unification, prolog, and graph connectivity. | |
| I realized a cute representation that is easy to use and prover stuff about, although very inefficient compared to the usual version of disjoint set. It uses a simple functional representation based off the observation that the preimages of a function form disjoint sets. This representation is somewhat analogous to using functions to represent Maps in Coq like in Software Foundations. https://softwarefoundations.cis.upenn.edu/lf-current/Maps.html | |
| The nice thing about this is that it really avoids any termination stickiness. Termination of the `find_root` operation of a union find in an explicit array or tree is not at all obvious and requires side proof or a refined type. | |
| The termination ultimately comes from the fact that you used a finite number of unions to cons |