chyp 0.5.2

An interactive theorem prover for string diagrams

Chyp (pronounced "chip") is an interactive theorem prover for symmetric monoidal categories (SMCs), a.k.a. process theories. Symmetric monoidal categories are a very general way to reason about processes that can be composed in sequence or in parallel. String diagrams are a convenient notation for maps in an SMC, where processes are represented as boxes connected to each other by wires.

Chyp is short for Cospans of HYPergraphs, which refers to how string diagrams are represented and plugged together formally in the tool. By switching from terms to this combinatoric structure, we obtain a convenient rewrite theory for string diagrams that automatically handles the extra "bureaucracy" that comes from working with sequential and parallel composition together. There is a lot of theory behind this, which has been developed over a series of papers:

• String Diagram Rewrite Theory I: Rewriting with Frobenius Structure
• String Diagram Rewrite Theory II: Rewriting with Symmetric Monoidal Structure
• String diagram rewrite theory III: Confluence with and without Frobenius

Currently, Chyp implements the theory described in part II, using monogamous acyclic hypergraphs to represent morphisms in a symmetric monoidal category. Fancier types of rewriting (e.g. rewriting modulo Frobenius structure) is planned for the future.

Installation

The latest release of Chyp can be installed via pip and run from the command line as follows:

pip install chyp
chyp

This will automatically install dependencies: PySide6 (Qt6 GUI bindings), cvxpy (a convex solver used for diagram layout), and lark (parser library).

To run the latest git version, execute the following commands:

git clone https://github.com/akissinger/chyp.git
cd chyp
pip install .
python3 -m chyp

Using Chyp

The main way to interact with Chyp is by writing *.chyp prover files. These are source files written in a simple declarative language that lets you:

1. define generators,
2. build terms by composing generators,
3. define rewrite rules (i.e. axioms), and
4. prove new rules by rewriting.

You can find some examples of *.chyp files in the examples folder.

Defining generators and terms

Generators are defined via the gen statement, which takes a name, a number of input wires, and a number of output wires. For example, we can define three new generators f, g, and h with various arities as follows:

gen f : 2 -> 1
gen g : 1 -> 2
gen h : 1 -> 1

These can be given a colors by providing one or two hex codes after the definition, defining the background and forground color, respectively:

gen f : 2 -> 1 "00ff00"            # green background, default (black) foreground
gen g : 1 -> 2 "000000" "ffffff"   # black background, white foreground
gen h : 1 -> 1 "0000ff" "0000ff"   # blue background, blue foreground (i.e. hidden text)

Generators can be combined via parallel composition * and sequential composition ;. We can build composed maps from simpler ones using a let statement:

let a = (g * h) ; (h * f)

Parallel composition takes precendence over sequential composition, so the parentheses can be dropped in the above command, which can equivalently be written:

let a = g * h ; h * f

Any terms can be combined in parallel, but for sequential composition S ; T the number of outputs of S must match the number of inputs of T. There are also special generators id : 1 -> 1 and sw : 2 -> 2 corresponding to the identity and swap maps respectively. This enables us to wire boxes up in more complicated ways, like this:

let b = g * g ; id * sw * id ; f * f

There is also a special generator id0 : 0 -> 0, corresponding to the empty diagram, i.e. the "identity" process on zero wires.

Note that, as you type in the bottom half of the screen, Chyp will automatically update the proof state and the graph view in the top half. This gives instant feedback, which is handy when building complicated terms. As soon as Chyp is able to parse your code, it will highlight to current statement and show the associated diagram(s) on top. To manually check your code, press CTRL+R. This is mainly useful for getting useful errors printed in the terminal if something is wrong.

While combining id and sw suffices for building any permutation of wires, this is not very convenient for more complicated permutations. Hence, there is a more powerful version of sw which takes an arbitrary permutation. sw[x0, x1, ..., xk] defines the map on k+1 wires that sends input xi to output i (counting from 0). sw is actually shorthand for sw[1, 0]. Using this notation, we could equivalently write b from above as:

let b = g * g ; sw[0, 2, 1, 3] ; f * f

Note these indices are local to the swap map, so splitting or combining swap maps will change some indices in general. For example:

sw[1, 2, 0] * sw[1, 0] = sw[1, 2, 0, 4, 3]

The def statement is a close cousin to the let statement, but its behavior is slightly different. If we change let to def in the example above, we get:

def a = g * h ; h * f

Before, when we used a in another term, it would immediately be expanded to the RHS, but now if we use a, e.g. in:

let x = a ; a

we'll just see two a-labelled boxes. This is because, behind the scenes def introduces a new generator called a and a new rule, called a_def, that can be used to explicitly fold/unfold a in a proof.

To see how this works, we'll first need to introduce rules and rewriting.

Rules and rewriting

An algebraic theory can be presented by introducing some generators as well as some rewrite rules. Rules are defined via the rule statement, which gives the rule a name, then takes as input a pair of terms with the same number of inputs and outputs. For example, we could introduce a pair of rules relating the f and g generators as follows:

rule assoc : f * id ; f = id * f ; f
rule bialg : f ; g = g * g ; id * sw * id ; f * f

Now for the good part! The rewrite statement represents a transitive chain of rule applications. It consists of the keyword rewrite followed by a name to use for the resulting theorem, then a sequence of equalities, each giving a justifying rule. For example:

rewrite ba1 :
  f * id ; f ; g ; g * id
  = id * f ; f ; g ; g * id by assoc
  = g * f ; id * id * g ; id * sw * id ; f * f ; g * id by bialg

Now, when we place the cursor over any step of this rule, it is highlighted in green, and it shows where that rule is applied. The green highlighting is indicating that Chyp has successfully checked this step. Namely, it has matched the LHS of the given rule on the previous term, rewritten the LHS to the RHS, and checked the result is the same as the term given. If we make a mistake in the example above (e.g. try to replace assoc with bialg or sw with id * id), that line will turn red. This means Chyp was not able to find a matching for the rule given which implies the given equality.

By default, Chyp tries to apply rules from left to right. We can apply a rule in the other direction by prefixing the rule name with -. For example, the proof above can be done backwards as follows:

rewrite ba1_backwards :
  g * f ; id * id * g ; id * sw * id ; f * f ; g * id
  = id * f ; f ; g ; g * id by -bialg
  = f * id ; f ; g ; g * id by -assoc

The golden rule of Chyp is that only connectivity matters. So, if two terms give the same diagram, like a * b ; c * d and (a ; c) * (b ; d), Chyp treats them as identical. Since under the hood, Chyp does everything with graph rewriting and not term rewriting, the prover handles all of this extra book-keeping for you.

Sometimes it can be helpful for readability to do a trivial proof step that does nothing but write the same string diagram differently. We can do this just by dropping the by clause in a proof step:

rewrite foo :
  a * b ; c * d
  = (a ; c) * (b ; d)

The def statement introduced in the previous section is just syntactic sugar for a gen followed by a rule. That is:

def a = g * h ; h * f

is equivalent to:

gen a : 2 -> 2
rule a_def : a = g * h ; h * f

Note that Chyp automatically figures out the arity and coarity for the new generator, since it has to match that of the given RHS.

Automatically rewriting terms

Usually it is not very convenient to manually type in the results of rewriting a term. Chyp's solution for this is to introduce "holes", which you can then ask the rewriter to fill. For example, try typing this:

rewrite ba1 :
  f * id ; f ; g ; g * id
  = ? by assoc

Place your cursor on the last line, which should be red. Then press CTRL+N and Chyp will try to find the next matching of the assoc rule, apply it, and replace the hole ? with the result. Since this is now a correct application of the rule, the line will turn green.

Two hotkeys are provided which make adding new rewrite steps easier. CTRL+Enter will insert a new line below the current one containing the code = ? by and place the cursor at the end of the line, ready to take a rule name.

CTRL+SHIFT+Enter will insert a new line = ? by NAME where NAME is the name of the rule used on the current step, then automatically try to fill the hole. This is handy for repeatedly applying the same rule. For example, try typing this:

rewrite ba2 :
  id * f ; f ; g ; id * g
  = ? by bialg

Then press CTRL+N, followed by CTRL+SHIFT+Enter 3 times, and Chyp will compute the normal form with respect to the bialg rule:

rewrite ba2 :
  id * f ; f ; g ; id * g
  = g * f ; id * id * g ; id * sw * id ; f * f ; id * g by bialg
  = g * g * g ; id * id * id * sw * id ; id * id * f * f ; id * sw * id ; f * f ; id * g by bialg
  = g * g * g ; id * id * id * sw * id ; id * g * f * f ; sw * sw * id ; id * f * id * g ; sw * sw * id ; id * f * f by bialg
  = g * g * g ; id * id * id * sw * id ; id * g * f * g * g ; sw * sw * id * sw * id ; id * f * id * f * f ; sw * sw * id ; id * f * f by bialg

How to we know it's a normal form? Pressing CTRL+SHIFT+Enter one more time will result in a red line that reads = ? by bialg, which means Chyp wasn't able to find any more matchings of the bialg rule.

Tactics

Tactics are the bread and butter of interactive theorem provers. These are routines that can be called to try to solve a given goal. In Chyp, a goal corresponds to a single proof step LHS = RHS. Chyp has three built in tactics: refl, rule, and simp. If you've been following along, you've actually been using the first two already.

refl, which stands for "reflexivity of =", simply tries to prove LHS and RHS represent the same diagram, i.e. they are isomorphic cospans of hypergraphs. When you write a rewrite step without providing a rule, it is actually shorthand for applying the refl tactic. For example:

rewrite foo :
  a * b ; c * d
  = (a ; c) * (b ; d)

is actually shorthand for:

rewrite foo :
  a * b ; c * d
  = (a ; c) * (b ; d) by refl()

Note the parentheses tell Chyp that this is a tactic and not a rule name. They are empty because refl takes zero arguments.

The rule tactic applies the given rewrite rule to the LHS in every possible way until it produces RHS (or fails). Most of the rewrites we have done so far have used the rule tactic, which can be applied either explicitly or implicitly just by giving a rule name. Namely, for a rule R, writing:

rewrite foo : lhs = rhs by R

is actually shorthand for:

rewrite foo : lhs = rhs by rule(R)

Finally, the simp tactic applies a list of given rules as much as possible to both the LHS and RHS then compares the resulting diagrams. It could be the case that the given set of rules is non-terminating (i.e. they can be applied forever without reaching a normal form), in which case simp gives up after 256 rule applications.

This can be very useful if the set of rules provided actually yields unique normal forms, or in rewriting lingo the rules are confluent and terminating. For example, the monoid laws:

gen u : 0 -> 1
gen m : 2 -> 1
rule unitL : u * id ; m = id
rule unitR : id * u ; m = id
rule assoc : m * id ; m = id * m ; m

always yield unique normal forms. So, we can prove any true equation involving a monoid in a single step using simp, e.g.

rewrite random_monoid_eq :
  id * u * u * id ; m * m ; m
  = id * u * id ; id * m ; m by simp(unitL, unitR, assoc)

However, the beauty of interactive theorem provers is that sets of rules don't actually have to be that nice to benefit from automated tactics like simp, as long as they get a bit of help from a human when they get stuck.

One more thing worth mentioning is the simplifier automatically unfolds definitions, i.e. any rule ending in _def, both to the term being simplified and in the LHS of all of the rules given. So something like this will also work:

def m2 = id * sw * id ; m * m
rewrite another_monoid_eq :
  u * u * u * u ; m2
  = u * u by simp(unitL)

If you don't want this behaviour, you can pass the +nodefs flag as an argument to simp:

def m2 = id * sw * id ; m * m

rewrite another_monoid_eq1 :
  u * u * u * u ; m2
  = u * u by simp(+nodefs, unitL) # fails

rewrite another_monoid_eq2 :
  u * u * u * u ; m2
  = u * u by simp(+nodefs, m2_def, unitL) # succeeds again

These three tactics are all implemented in the chyp.tactic module. Tactic implements refl, and the other tactics are implemented as subclasses of Tactic that should override the check method, which tries to close the current goal, and the make_rhs method, which returns an iterator over possible terms to fill in a hole ?. Thanks to the API exposed by Tactic, the two tactics RuleTac and SimpTac are very simple, and it shouldn't be too hard to implement more.

In theory, if tactics only interact with the current goal via the public methods exposed by Tactic, it shouldn't be possible to prove anything that is not true. While this doesn't provide strong guarantees of soundness, like in the case of LCF-style theorem provers, it does attempt to provide some degree of assurance that (possibly very complex) tactics won't prove untrue statements.

Modules and importing

As structures and proofs get more complicated, we may want to split them into multiple files. Every chyp file defines a module, which can be imported in other chyp files. Suppose for example we define the following file monoid.chyp:

gen m : 2 -> 1
gen u : 0 -> 1
rule assoc : m * id ; m = id * m ; m
rule unitL : u * id ; m = id
rule unitR : id * u ; m = id

If we want to define commutative monoids, we could start a new file cmonoid.chyp in the same directory and write:

import monoid
rule comm : sw ; m = m

By default, this loads all of the generators and rules from the first file into the second one. We may not want this, if there is some possibility that the symbols in one file will clash with the symbols in another. We can give a module its own namespace by adding as ... to the import statement:

import monoid as M   # m is now M.m, u is M.u, assoc is M.assoc, etc.

This is especially important if we want to have multiple copies of the same structure. For example, we could start defining commutative semirings in a third file, csemiring.chyp:

import cmonoid as M1
import cmonoid as M2

gen cp : 1 -> 2
rule dist :
  M1.m * id ; M2.m = 
  = id * M1.m ; M2.m = cp * id * id ; id * sw * id ; M2.m * M2.m ; M1.m

You can also alias generators in imported modules as follows:

gen m1 : 2 -> 1
gen u1 : 0 -> 1
gen m2 : 2 -> 1
gen u2 : 0 -> 1
import cmonoid as M1(m = m1, u = u1)
import cmonoid as M2(m = m2, u = u2)

gen cp : 1 -> 2
rule dist :
  m1 * id ; m2 = 
  = id * m1 ; m2 = cp * id * id ; id * sw * id ; m2 * m2 ; m1

Even though we now have short aliases for generators, the rules still live in their respective namespaces. For example, M1.assoc can be used to rewrite m1 * id ; m1 to id * m1 ; m1 and M2.assoc will rewrite m2 * id ; m2 to id * m2 ; m2.

This is especially convenient if modules share generators in non-trivial ways. For example, a pair of Frobenius algebras interacting as a bialgebra could be defined this way, assuming frobenius.chyp and bialg.chyp have already been defined:

gen m1 : 2 -> 1
gen u1 : 0 -> 1
gen n1 : 1 -> 2
gen v1 : 1 -> 0

gen m2 : 2 -> 1
gen u2 : 0 -> 1
gen n2 : 1 -> 2
gen v2 : 1 -> 0

import frobenius as F1(m = m1, u = u1, n = n1, v = v1)
import frobenius as F2(m = m2, u = u2, n = n2, v = v2)
import bialg as B1(m = m1, u = u1, n = n2, v = v2)
import bialg as B2(m = m2, u = u2, n = n1, v = v1)

We can even set the generators in an imported module equal to arbitrary terms, as long as the types match.

To understand how this works, it is useful to know that this is just some syntactic sugar that takes advantage of the behaviour of the gen statement. Normally, the gen statement will add a new generator to the current namespace. However, if a term with that name already exists, it will simply check the already existing term has the right arity and coarity. This allows us to alias generators in a module using let statements before it is imported. So, in fact, the line:

import frobenius as F1(m = m1, u = u1, n = n1, v = v1)

is exactly equivalent to:

let F1.m = m1
let F1.u = u1
let F1.n = n1
let F1.v = v1
import frobenius as F1

Whenever an m is encountered in frobenius.chyp (which will be interpreted as F1.m), it will automatically get replaced by m1 thanks to the let statement.

If we alias generators to some more complicated terms, these just end up the RHS of the let statements. For example, we could get the "almost" Frobenius algebra laws of the ZW calculus with a statement like this:

gen m : 2 -> 1
gen u : 0 -> 1
gen n : 1 -> 2
gen v : 1 -> 0
gen d : 1 -> 1

import frobenius as W(m = d * d ; m, u = u, n = d ; n, v = d ; v)

where the last line is equivalent to:

let W.m = d * d ; m
let W.u = u
let W.n = d ; n
let W.v = d ; v
import frobenius as W

Finding modules

The import statement always looks for *.chyp files in the same directory of the current file. Chyp doesn't have a notion of "search paths" for modules, but this might be added in the future.

Files can be imported from subdirectories by adding dots:

import algebra.frobenius  # imports algebra/frobenius.chyp

You can go to a file being imported by placing the cursor on the import statement and pressing CTRL+G.