index.html

---
layout: default
title: Home
---

<div class="jumbotron">
  <h1>Quantomatic</h1>
  <p>Quantomatic is a
    <i>diagrammatic proof assistant</i>, meaning it provides machine-support for reasoning with
    <i>diagrammatic languages</i> (check out some of our
    <a href="papers.html">papers</a>). It allows users to draw diagrams and build up proofs using diagrammatic rewrite
    rules. It's easier to show you what that means than to tell you, so download it and try it out!</p>
  <p style="line-height: 2.5em">
    <a href="https://github.com/Quantomatic/quantomatic/releases/download/v0.7/Quantomatic-v0.7.jar" class="btn btn-primary btn-lg" role="button">
      <span class="glyphicon glyphicon-download-alt"></span>Download JAR (all platforms)</a>
    <a href="https://github.com/Quantomatic/quantomatic" class="btn btn-lg btn-success" role="button">GitHub Project &raquo;</a>
  </p>
</div>

<h1>Download</h1>

<p>
  You can choose between:
  <ul>
    <li>the latest stable release (recommended): <a href="https://github.com/Quantomatic/quantomatic/releases/download/v0.7/Quantomatic-v0.7.jar">From GitHub</a></li>
    <li>or you can
    <a href="https://github.com/Quantomatic/quantomatic">access the source code directly</a>.</li>
  </ul>
</p>

<p>
  Quantomatic requires java to run, which can be downloaded
  <a href="https://java.com/en/download/">here</a>, or found in your package manager.
</p>

<h2>Building from source</h2>

<p>
  If you wish to download the source code directly, you will need:
  <ul>
    <li>a recent JDK (at least version 7)</li>
    <li>
      <a href="http://git-scm.com/">git</a>
    </li>
    <li>
      <a href="http://www.scala-sbt.org/">sbt</a>
    </li>
  </ul>
  You will then need to clone Quantomatic and build/run the frontend using sbt:</p>

<pre>
git clone git://github.com/Quantomatic/quantomatic.git -b integration
cd ./scala
sbt run
</pre>

<p>Note this assumes you want the latest development version. To get source for the latest stable version, remove <code>-b integration</code> from the <code>git clone</code> command above. You will see a number of options once <code>sbt run</code> is complete. Choose QuantoDerive to run the main GUI.
</p>

<h1>Sample projects</h1>

<p>The <em>Using Quantomatic</em> section below gives instructions for getting it up and running with a sample project.
  This section provides additional sample projects to get you started.
The sample projects are now all hosted in the same repository on
<a href="https://github.com/Quantomatic/sample-projects">GitHub</a>.</p>

<p>Not sure what these are?
  Try the <a href="./quantojs/zoology.html">Qubit Zoology</a> for a selection of languages and frameworks.</p>

  <h3>
    Stabilizer ZX-calculus project
  </h3>

  <p>
    This contains all of the Stabilizer ZX-calculus axioms and some useful theorems and simplification procedures. It also includes sample
      graphs and derivations.
    </p>
    
<p>
    <a href="https://github.com/Quantomatic/sample-projects/blob/master/zx-stabilizer.zip?raw=true" class="btn btn-default" role="button">
      <span class="glyphicon glyphicon-download-alt"></span> Download zip</a>

  </p>
  
  <h3>
    Clifford+T ZX-calculus project
  </h3>

  <p>
    This contains all of the Clifford+T ZX-calculus axioms.
  </p>
    <p>
      <a href="https://github.com/Quantomatic/sample-projects/blob/master/zx-cliffordt.zip?raw=true" class="btn btn-default" role="button">
        <span class="glyphicon glyphicon-download-alt"></span> Download zip</a>
    </p>
    

<h3>Bialgebra project</h3>

<p>This project contains the axioms for a (variable-arity) commutative bialgebra and a strongly-normalising simplification procedure.</p>

<p>
  <a href="https://github.com/Quantomatic/sample-projects/blob/master/bialgebra-project.zip?raw=true" class="btn btn-default" role="button">
    <span class="glyphicon glyphicon-download-alt"></span> Download zip</a>
</p>

<p>
    <a href="https://github.com/Quantomatic/sample-projects/" class="btn btn-default" role="button">
      View all the sample projects on Github
    </a>
</p>



<h1>Using Quantomatic</h1>

<p>To start experimenting with Quantomatic,
  <em>download the sample project below</em> and unzip it somewhere on your computer.

  <p>
    <a href="https://github.com/Quantomatic/sample-projects/blob/master/zx-stabilizer.zip?raw=true" class="btn btn-default" role="button">
      <span class="glyphicon glyphicon-download-alt"></span> Download sample project zip</a>
  </p>

  <p>Once you have downloaded the sample project, open it in Quantomatic with
    <code>File > Open Project...</code> by selecting (or navigating to) the
    <i>directory</i> in the file browser and clicking
    <code>Open</code>. At this point, you should be seeing something like this:</p>

  <img class="img-thumbnail center-block" src="images/screens/start.jpg" style="width:457px; height:301px" />
  <br />

  <p>
    You can change the font size etc. by going to the
    <code>Window</code> menu and choosing
    <code>Increase UI scaling</code> or
    <code>Decrease UI scaling</code> accordingly.
  </p>

  <h3>Graph editing</h3>

  <p>Expand the graphs folder on the left and double-click
    <code>sample.qgraph</code>. This will open the graph editor:</p>

  <img class="img-thumbnail center-block" src="images/screens/graph_open.jpg" style="width:457px; height:301px" />
  <br />

  <p>You can interact with this as you would expect: Drag nodes around, copy and paste, use the
    <kbd>=</kbd> and
    <kbd>-</kbd> keys to zoom in and out, etc.. Double-click nodes (or edges) to edit data. One handy trick is to let Quantomatic
    do some automatic layout for you. Notice how there are a bunch of nodes clustered up in a particularly unhelpful way
    in the above graph? Try selecting them and holding down the
    <kbd>R</kbd> key to
    <em>relax</em> the node positions:</p>

  <img class="img-thumbnail center-block" src="images/screens/graph_relax.jpg" style="width:457px; height:301px" />
  <br />

  <p>That's better! Next, have a look at the tools we have available:</p>

  <img class="img-thumbnail center-block" src="images/screens/tools.jpg" />
  <br />

  <p>From left-to-right, these are:
    <code>Select</code>,
    <code>Add Vertex</code>,
    <code>Add Boundary</code>,
    <code>Add Edge</code>, and
    <code>Edit !-Boxes</code>. We have already been using the
    <code>Select</code> tool, so click on the
    <code>Add Vertex</code> tool. Notice now the vertex types at the bottom of the screen is now enabled. Pick a vertex type:</p>

  <img class="img-thumbnail center-block" src="images/screens/vertex_type.jpg" />
  <br />

  <p>Since the sample project is set up for the ZX-calculus, the available types are well...
    <code>Z</code> and
    <code>X</code>. We'll ignore the
    <code>&lt;wire&gt;</code> type for now. Once a type is selected, clicking on the screen will add vertices of that type.</p>

  <p>Similar to the vertex tool is the boundary tool. These create dummy vertices which serve as free edges, or boundaries to
    a graph. These are important for creating rules. Note that these don't become proper inputs/outputs until we connect
    some edges to them. To do that, try out the edge tool:</p>

  <img class="img-thumbnail center-block" src="images/screens/edge.jpg" />
  <br />

  <p>Edges are created by clicking and dragging from one vertex to another. They can either be directed or undirected, which
    is set by the checkbox in the lower-right corner. Some theories can have multiple types of edges, which you can pick
    from the
    <code>Edge Type</code> drop-down, but the ZX-calculus only allows one edge type, so no need to mess with it.</p>

  <p>The tool that needs the most explanation is the
    <code>Edit !-Box</code> tool. !-boxes (or &quot;bang-boxes&quot;) allow you to mark sub-graphs that can be repeated any number of times. With
    the !-box tool selected, click and drag around some vertices to create a new !-box:</p>

  <img class="img-thumbnail center-block" src="images/screens/bbox.jpg" />
  <br />

  <p>To add are remove nodes from a !-box, click and drag from upper-left corner of the !-box to the thing you want to add/remove.
    This also works for
    <em>other</em> !-boxes. To nest one !-box inside another, click and drag from the parent's corner to the child's:</p>

  <div class="center-block" style="width: 680px">
    <img class="img-thumbnail" src="images/screens/nest1.jpg" style="height:275px; width:320px" />
    <span class="glyphicon glyphicon-arrow-right"></span>
    <img class="img-thumbnail" src="images/screens/nest2.jpg" style="height:275px; width:320px" />
  </div>
  <br />

  <p>Just like with nodes, repeating the process will remove the child !-box from the parent. QuantoDerive tries its best to
    only draw !-boxes around nodes that are actually
    <em>inside</em> that !-box, but sometimes things can go wrong. For example, if a vertex ends up between two vertices that
    are both in a !-box
    <code>bx0</code>, it might appear to be in
    <code>bx0</code> as well. This can get confusing, so QuantoDerive tries to help you out:</p>

  <img class="img-thumbnail center-block" src="images/screens/not_in_bbox.jpg" />
  <br />

  <p>The node
    <code>v3</code> above is not actually in
    <code>bx0</code>, so QuantoDerive is giving you a (not-so-subtle) hint to move it somewhere else.</p>

  <h3>Rule editing</h3>

  <p>Rule editing is similar, except now we work with two graphs side-by-side:</p>

  <img class="img-thumbnail center-block" src="images/screens/rule.jpg" style="width:457px; height:301px" />
  <br />

  <p>Here the blue outline shows which graph has the keyboard focus, e.g. for copy-and-paste and
    <kbd>R</kbd> (relaxing). To make a valid rule, the LHS and RHS should have identical boundaries and !-boxes. Not only should
    the numbers match, but also the labels. For example, in the rule above, both sides have two boundary vertices, labelled
    <code>b0</code> and
    <code>b1</code>.</p>

  <p>Rules are created by selecting
    <code>File > New Axiom</code>. Soon, you will also be able to create rules from derivations, i.e. theorems.</p>

  <h3>Starting a derivation</h3>

  <p>To start a new derivation, open a graph that will serve as a starting point, and select
    <code>Derive > Start derivation</code>.</p>

  <img class="img-thumbnail center-block" src="images/screens/start_derivation.jpg" />
  <br />

  <p>This opens up the derivation editor. Nothing is happening yet because no rules have been added. Click the
    <code>+</code> button in the
    <code>Rewrite</code> pane to add some rules.</p>

  <img class="img-thumbnail center-block" src="images/screens/add_rules.jpg" />
  <br />

  <p>I usually add all of them because...why not? You can also search through your rules using the "Filter" bar at the top.
    As soon as you add some rules, QuantoDerive will start eagerly searching for matchings:
  </p>

  <img class="img-thumbnail center-block" src="images/screens/rewrite_panel.jpg" />
  <br />

  <p>The more cores your computer has, the more fun this part is! Currently, QuantoDerive will find up to 50 matchings for each
    rule, which you can browse through using the left and right arrow buttons. Also note that selecting subgraphs on the
    left will refine the search. One you find the rewrite you want, click
    <code>Apply</code>. This will create a proof step, which you can view at any time by clicking on it in the history view:</p>

  <img class="img-thumbnail center-block" src="images/screens/history.jpg" style="width:457px; height:301px" />
  <br />

  <p>The piece of graph that was removed is highlighted on the LHS, while the new piece of graph that was added is shown on
    the RHS. Rewriting always takes place at the end of a chain of rewrite steps, which is called a
    <em>proof head</em>. The derivation editor is designed so that you can try rules out, and if they don't work, you can back
    up and try other things without ever losing your work. This means that histories can branch and have multiple heads.
    To create a new head, click a rewrite step somewhere in the path, and click the
    <code>New Proof Head</code> button in the toolbar:</p>

  <div class="center-block" style="width: 540px">
    <img class="img-thumbnail" src="images/screens/new_head_button.jpg" style="height:182px; width:263px" />
    <span class="glyphicon glyphicon-arrow-right"></span>
    <img class="img-thumbnail" src="images/screens/new_head.jpg" style="height:182px; width:249px" />
  </div>
  <br />

  <h3>Using the simplifier</h3>

  <p>When you are tired of applying rewrites one at a time, click on a proof head, and switch over the the simplify panel. Notice
    there isn't a whole lot to see. That's because we haven't loaded any
    <em>simp</em>lification
    <em>proc</em>edures, aka
    <em>simprocs</em> yet. These are little pieces of code that define a simplification strategy. On the left, open the
    <code>simprocs</code> folder and double-click
    <code>basic-simp.py</code>:</p>

  <img class="img-thumbnail center-block" src="images/screens/simproc.jpg" style="width:457px; height:301px" />
  <br />

  <p>This one's as basic as they come. It loads a some rules from the project into a list called
    <code>simps</code>, then it will try to apply rules from
    <code>simps</code> until either it runs out of rules to apply, or you stop it. That's what
    <code>REDUCE(simps)</code> does. Click the
    <img src="images/gui/start.png" /> button in the toolbar to execute this code, which will
    <em>register</em> the procedure
    <code>basic-simp</code> with QuantoDerive. Now, go back to your derivation and click the refresh button:</p>

  <img class="img-thumbnail center-block" src="images/screens/refresh.jpg" />
  <br />

  <p>There it is, ready to go. Select
    <code>basic-simp</code> and click play:</p>

  <img class="img-thumbnail center-block" src="images/screens/basic_simp.jpg" style="width:457px; height:301px" />
  <br />

  <p>Well, that didn't get us very far. It is basic, after all. Go back to
    <code>simprocs</code> and open
    <code>rotate-simp.py</code> and execute it. Now, back in our derivation, click the refresh button again and run
    <code>rotate-simp</code>.</p>

  <img class="img-thumbnail center-block" src="images/screens/rotate_simp.jpg" style="width:457px; height:301px" />
  <br />

  <p>That's better! Of course, your results may vary depending on what nodes you added earlier.</p>

  <p>So, that's pretty much all there is to it. Play around with creating some new rules or even a new project.</p>

  <!-- There is a button on the Quantomatic GUI that links to the Simproc API.
  If you move this information, please update where the button links to.
  It's the SimprocAPIAction in gui.QuantoDerive  -->
  <div id="SimprocAPI" class="anchor"></div>
  <h3>The simproc API</h3>

  <p>Simplification procedures are implemented in Python, via a built-in interpreter in Quantomatic based in <a href="http://jython.org">jython</a>. The following is a (non-exhaustive) list of python bindings provided by Quantomatic, via the <code>quanto.util.Scripting</code> object. The API is a work-in-progress, and subject to change and/or expansion as more features from the simplifier are exposed. If you wish to get the most up-to-date look at what bindings are available, have a look at <a href="https://github.com/Quantomatic/quantomatic/blob/integration/scala/src/main/scala/quanto/util/Scripting.scala">the soure code</a>.</p>

  <p>Generally, a simproc file will construct an object extending the class <code>quanto.rewrite.Simproc</code>, then register it with a name. When this simproc is called from the GUI, it will call the method <code>simp()</code>, which takes a graph as its input and returns a lazy list of rewrite steps. These steps consist of a new graph, as well as the matched rule which produced it. First some basic functions:</p>

  <pre>
    load_rule(path)
      load a rule located in 'path'. Note this path is relative to the
      project root, and the .qrule extension should be omitted.

    load_rules(paths)
      same, but takes a list of paths and returns a list of rules. In
      other words, it is shorthand for 'map(load_rule, paths)'.

    register_simproc(name, simproc)
      takes a simproc object and registered with the given name. This
      makes it available in the GUI simplifier.

    load_graph(path)
      load a graph located in 'path'. Again this path is relative to the
      project root, and the .qgraph extension should be omitted. This is
      rarely used in simprocs, but useful for testing or batch processing.

    save_graph(graph, path)
      save a graph to the given 'path'. Paths follow the same rules as
      above.
  </pre>


  <p>The easiest way to construct a simproc object is to chain together some of the simpler, built-in simprocs into more complicated ones. Here's a list of the current built-in simprocs:</p>

  <pre>
    EMPTY
      a trivial simproc which does nothing

    REWRITE(rules)
      takes a rule or list of rules and applies the first rule that
      matches.

    REWRITE_METRIC(rules, f)
      takes a rule or list of rules and a function f from graphs to
      integers. It will apply the first rule that matches *and*
      (strictly) reduces the value of f.

    REWRITE_WEAK_METRIC(rules, f)
      same as above, except the rewrite only needs to be non-increasing
      on f.

    REWRITE_TARGETED(rule, v, f)
      takes a rule, the name of a vertex 'v' within the rule (as a string),
      and a targeting function 'f' from graphs to a vertex name. It will
      apply the rule on a graph 'g' by first attempting to match 'v' on
      'f(g)', then matching the rest.
  </pre>

  <p>Simprocs are combined via two combinators:</p>

  <pre>
    s >> t
      apply simproc 's' until it produces no new rewrites, then apply 't'

    REPEAT(s)
      apply simproc 's' until it yields no new rewrites, then repeat until
      applying 's' yields no rewrites at all.
  </pre>

  <p>It is so comment to wrap <code>REWRITE_XXXX</code> in <code>REPEAT</code> that certain shorthands have been introduced:</p>

  <pre>
    REDUCE(rules) := REPEAT(REWRITE(rules))

    REDUCE_METRIC(rules, f) := REPEAT(REWRITE_METRIC(rules, f))

    REDUCE_WEAK_METRIC(rules, f) := REPEAT(REWRITE_METRIC(rules, f))

    REDUCE_TARGETED(rule, v, f) := REPEAT(REWRITE_TARGETED(rule, v, f))
  </pre>

  <p>That's basically it. Since the interpreter is <code>jython</code> under the hood, simprocs can access all of the data associated with graphs, vertices, etc. Here are a few methods of Quantomatic's <code>Graph</code> type which are handy for writing metrics or targeting functions:</p>

  <pre>
    graph.typeOf(v)
      returns a string containing the type of the vertex, e.g. 'Z' or 'X'

    graph.isBoundary(v)
      returns true if the given vertex is a boundary

    graph.isAdjacentToType(v, str)
      returns true if the vertex is adjacent to a vertex of the given type

    graph.isAdjacentToBoundary(v)
      returns true if the given vertex is touching the boundary.
  </pre>

  <p>A couple of the built-in methods also have wrapper functions that enable more compact and 'pythonic' code to be written:</p>

  <pre>
    verts(graph)
      return a list of vertices in the graph, in a python-iterable format.

    vertex_angle_is(graph, v, str)
      returns true if the angle of v is equal to the given string value.
  </pre>


  <p>You can see most of these functions in action in the simproc <code>rotate-simp.py</code>:

  {% highlight python %}
    simps0 = load_rules([
      "axioms/red_copy", "axioms/green_copy",
      "axioms/red_sp", "axioms/green_sp",
      "axioms/hopf",
      "axioms/red_scalar", "axioms/green_scalar",
      "axioms/red_loop", "axioms/green_loop"])

    simps = simps0 + load_rules(["axioms/green_id", "axioms/red_id"])

    green_id_inv = load_rule("axioms/green_id").inverse()
    red_id_inv = load_rule("axioms/red_id").inverse()
    rotate = load_rule("theorems/rotate_targeted")

    def num_boundary_X(g):
      return len([v for v in verts(g)
        if g.isBoundary(v) and g.isAdjacentToType(v, 'X')])

    def next_rotation_Z(g):
      vs = [(g.arity(v),v) for v in verts(g)
        if g.typeOf(v) == 'Z' and
           vertex_angle_is(g, v, '0') and
           not g.isAdjacentToBoundary(v)]
      if (len(vs) == 0): return None
      else: return min(vs)[1]


    simproc = (
      REDUCE(simps) >>
      REDUCE_METRIC(green_id_inv, num_boundary_X) >>
      REPEAT(
        REDUCE_TARGETED(rotate, "v10", next_rotation_Z) >>
        REDUCE(simps0)
      ) >>
      REDUCE(simps)
    )

    register_simproc("rotate-simp", simproc)
  {% endhighlight %}

  <!-- <h1>News</h1>
<ul class="posts">
  {% for post in site.posts %}
    <li><span>{{ post.date | date_to_string }}</span> &raquo; <a href="{{ post.url }}">{{ post.title }}</a></li>
  {% endfor %}
</ul> -->