{
"cells": [
{
"cell_type": "code",
"execution_count": 1,
"metadata": {},
"outputs": [],
"source": [
"import sys\n",
"sys.path.append('..')\n",
"import pypn as pn\n",
"from pypn.variables import *"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# PyPN\n",
"\n",
"PyPN (pronounced like the famous hobbit) is a python library and linear logic theorem prover based on proof nets.\n",
"\n",
"Currently, it's mainly intended to support reasoning in multiplicative linear logic (MLL) plus the n-ary MIX rule, which was the main thing I was interested in when I first wrote it. In \"one-sided\" form, MLL is very simple:\n",
"$$\n",
"\\frac{\\vdash \\Gamma, A \\quad \\vdash \\Delta, B}{\\vdash \\Gamma,\\Delta, A \\otimes B}\n",
"\\qquad\\qquad\n",
"\\frac{\\vdash \\Gamma, A, B}{\\vdash \\Gamma, A ⅋ B}\n",
"$$\n",
"\n",
"$$\n",
"\\frac{}{\\vdash 1}\n",
"\\qquad\\qquad\n",
"\\frac{\\vdash \\Gamma}{\\vdash \\Gamma,\\bot}\n",
"\\qquad\\qquad\n",
"\\frac{}{\\vdash A^{\\perp}, A}\n",
"$$\n",
"\n",
"Adding the n-ary MIX rule is equivalent to requiring the two units to coincide, i.e. $I := 1 \\equiv \\bot$. In particular, it implies the binary MIX rule, which looks like \"mixing\" together the contents of two sequents, whence the name.\n",
""
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Okay, down to business. The first thing to note is we imported all of the symbols in `pypn.variables`. This dumps a lot of variables and atoms into our namespace to play with. Variables are named `{A0,...,Z0,A1,...,Z1,A2,...,Z2}`, i.e. every capital letter, followed by a 0, 1, or 2. If you need more, use the `Var` constructor:"
]
},
{
"cell_type": "code",
"execution_count": 2,
"metadata": {},
"outputs": [],
"source": [
"Sandwich = Var('Sandwich')"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Variables can be combined to make expressions via MLL connectives, which are implemented as overloaded operators.\n",
"\n",
"$I \\leadsto$ `pn.I`\n",
"\n",
"$X_0 \\otimes Y_0 \\leadsto$ `X0 * Y0`\n",
"\n",
"$X_0 ⅋ Y_0 \\leadsto$ `X0 + Y0`\n",
"\n",
"$X_0^{\\perp} \\leadsto$ `~X0`\n",
"\n",
"$X_0 ⊸ Y_0 := X_0^{\\perp} ⅋ Y_0 \\leadsto$ `X0 >> Y0`\n",
"\n",
"These will all return an object of type `Expr`, which also implements these operations. In fact, `Var` is a subclass of `Expr`."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Complex expressions are normalised by pushing negation inside:"
]
},
{
"cell_type": "code",
"execution_count": 3,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Expr((X0 * ~Y0) + (X1 * ~Y1))"
]
},
"execution_count": 3,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"~((X0 >> Y0) * (X1 >> Y1))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Operator precedence comes from Python, which sometimes does the Right Thing:"
]
},
{
"cell_type": "code",
"execution_count": 4,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 4,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"X0 * Y0 >> X1 * Y1 == (X0 * Y0) >> (X1 * Y1)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"...and other times not. Notably, `>>` associates to the left, rather the the right, as we would expect for implication:"
]
},
{
"cell_type": "code",
"execution_count": 5,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 5,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"X0 >> X1 >> X2 == (X0 >> X1) >> X2"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Atoms behave in almost exactly the same way as variables, except they are named by lower-case letters and they know they are \"positive\". Expressions can be positive, negative, or neither depending on where negations appear: tensors and pars of positive elements are positive, negations of positive elements are negative, and anything else is neither.\n",
"\n",
"This won't play a role for MLL+MIX, but can be important for some extensions to the logic."
]
},
{
"cell_type": "code",
"execution_count": 6,
"metadata": {
"scrolled": true
},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
" a0: positive\n",
" a0 * b0: positive\n",
" a0 + b0: positive\n",
" ~a0: negative\n",
" ~a0 * ~b0: negative\n",
" ~a0 + ~b0: negative\n",
" ~a0 * b0: neither\n",
" ~a0 + b0: neither\n",
" A0: neither\n",
" B0: neither\n",
" C0: neither\n"
]
}
],
"source": [
"exprs = [a0, a0 * b0, a0 + b0, ~a0, ~a0 * ~b0, ~a0 + ~b0, ~a0 * b0, ~a0 + b0, A0, B0, C0]\n",
"for e in exprs:\n",
" print(str(e).rjust(10), end=': ')\n",
" if e.positive(): print(\"positive\")\n",
" elif e.negative(): print(\"negative\")\n",
" else: print(\"neither\")"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Now, we are ready to prove some stuff. The simplest way to prove one formula entails another is to pass it to `pn.prove`. If successful, it will return a proof net, which can you draw with `pn.draw`."
]
},
{
"cell_type": "code",
"execution_count": 7,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"\n",
" \n",
" \n",
" "
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"p = pn.prove((X0 >> Y0) * (X1 >> Y1), X0 >> ((Y0 >> X1) >> Y1))\n",
"pn.draw(p)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"If it `pn.prove` fails, it will return `None`. For convenience, `pn.draw(None)` will simply print a helpful message:"
]
},
{
"cell_type": "code",
"execution_count": 8,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"FAIL\n"
]
}
],
"source": [
"p = pn.prove(X0 + X1, X0 * X1)\n",
"pn.draw(p)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"But what does it do? It starts by calling `pn.proofnet.decompose` on the hypothesis and `pn.proofnet.compose` on the conclusion, which give a pair of trees:"
]
},
{
"cell_type": "code",
"execution_count": 9,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"\n",
" \n",
" \n",
" "
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"g = pn.Graph()\n",
"nodes, row = pn.proofnet.decompose((X0 >> Y0) * (X1 >> Y1), g)\n",
"pn.proofnet.compose(X0 >> ((Y0 >> X1) >> Y1), g, row+1)\n",
"\n",
"pn.draw(g)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"It then plugs pairs of inputs and outputs and checks that the proofnet is still valid via the function `checker`. Once all the nodes but the hypothesis and conclusion are plugged, a proof is accepted if it passes the `checker`. If it fails the checker, it keeps trying all type-respecting pluggings until a valid one is found or all possibilities are exhausted. This (super simple) strategy is exponential, even with a poly-time `checker` function, but this only really becomes a problem if you have lots of repeated variables in a formula.\n",
"\n",
"`checker` is the most important part of this process, and it is passed in as an argument to `pn.prove`. This can be any function that takes a `pn.Graph` and returns a boolean, so its possible to prove unsound stuff if you change the checker:"
]
},
{
"cell_type": "code",
"execution_count": 10,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"\n",
" \n",
" \n",
" "
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"p = pn.prove(X0 + X1, X0 * X1, checker=lambda x: True)\n",
"pn.draw(p)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"If no `checker` is provided, the default is `pn.proofnet.cut_checker`, which repeatedly removes root notes, subject to condition that \"par-like\" nodes disconnect the graph. Other possibilities are:\n",
"\n",
" * `pn.proofnet.switching_checker`, which implements the Danos-Regnier \"switching\" conditions\n",
" * `pn.proofnet.hocc_cut_checker`, which implements a looser condition than `cut_checker` which is sound for higher-order causal categories (see https://arxiv.org/abs/1701.04732), but not plain MLL+MIX\n",
"\n",
"In particular, in HOCC-logic, tensor and par coincide for purely positive (and hence purely negative) formulae."
]
},
{
"cell_type": "code",
"execution_count": 11,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"\n",
" \n",
" \n",
" "
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"p = pn.prove(a0+b0, a0*b0, checker=pn.proofnet.hocc_cut_checker)\n",
"pn.draw(p)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Note this only holds for atoms `{a0, b0}`, which are assumed to be positive, as mentioned earlier. Variables `{A0,B0}` (which stand for arbitrary formulae) will still not satisfy this entailment:"
]
},
{
"cell_type": "code",
"execution_count": 12,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"FAIL\n"
]
}
],
"source": [
"p = pn.prove(A0+B0, A0*B0, checker=pn.proofnet.hocc_cut_checker)\n",
"pn.draw(p)"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
}
],
"metadata": {
"kernelspec": {
"display_name": "Python 3",
"language": "python",
"name": "python3"
},
"language_info": {
"codemirror_mode": {
"name": "ipython",
"version": 3
},
"file_extension": ".py",
"mimetype": "text/x-python",
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.7.5"
}
},
"nbformat": 4,
"nbformat_minor": 2
}