A formal account of nets

From LLWiki
(Difference between revisions)
Jump to: navigation, search
(a draft definition of boxes)
(The short story)
 
Line 11: Line 11:
 
* the top/down or passive/active orientation of cells is related with the distinction between premisses and conclusions of rules, (and in that sense, a cut is not a logical rule, but the focus of interaction between two rules);
 
* the top/down or passive/active orientation of cells is related with the distinction between premisses and conclusions of rules, (and in that sense, a cut is not a logical rule, but the focus of interaction between two rules);
 
* cuts are thus wires rather than cells/links: this fits with the intuition of GoI, but not with the most common presentations of proof nets;
 
* cuts are thus wires rather than cells/links: this fits with the intuition of GoI, but not with the most common presentations of proof nets;
* because the notion of subnet is not trivial in multiport interaction nets, and to avoid the use of geometric conditions (boxes must not overlap but can be nested), we introduce boxes as particular cells);
+
* because the notion of subnet is not trivial in multiport interaction nets, and to avoid the use of geometric conditions (boxes must not overlap but can be nested), we introduce boxes as particular cells;
 
* when representing proof nets, we introduce axioms explicitly as cells, so that axiom-cuts do not vanish.
 
* when representing proof nets, we introduce axioms explicitly as cells, so that axiom-cuts do not vanish.
  +
 
== Nets ==
 
== Nets ==
   

Latest revision as of 15:43, 25 June 2013

The aim of this page is to provide a common framework for describing linear logic proof nets, interaction nets, multiport interaction nets, and the likes, while factoring out most of the tedious, uninteresting details (clearly not the fanciest page of LLWiki).

Contents

[edit] Preliminaries

[edit] The short story

  • the general flavor is that of multiport interaction nets;
  • the top/down or passive/active orientation of cells is related with the distinction between premisses and conclusions of rules, (and in that sense, a cut is not a logical rule, but the focus of interaction between two rules);
  • cuts are thus wires rather than cells/links: this fits with the intuition of GoI, but not with the most common presentations of proof nets;
  • because the notion of subnet is not trivial in multiport interaction nets, and to avoid the use of geometric conditions (boxes must not overlap but can be nested), we introduce boxes as particular cells;
  • when representing proof nets, we introduce axioms explicitly as cells, so that axiom-cuts do not vanish.

[edit] Nets

[edit] Wires

A wiring is the data of a finite set P of ports and of a partition W of P by pairs (the wires): if \{p,q\}\in{W}, we write W(p) = q and W(q) = p. Hence a wiring is equivalently given by an involutive permutation W of finite domain P, without fixpoints (forall p, {W}(p)\not=p): the wires are then the orbits. Another equivalent presentation is to consider W as a (simple, loopless, undirected) graph, with vertices in P, all of degree 1.

We say two wirings are disjoint when their sets of ports are. A connection between two disjoint wirings W and W' is a partial injection (I,I',f):P\pinj P': I\subseteq P, I'\subseteq P' and f is a bijection I\cong I'. We then write W\bowtie_f{{W}'} for the wiring obtained by identifying the ports pairwise mapped by f, and then ``straightening`` the paths thus obtained to recover wires: notice this might also introduce loops and we write \Inner{W}{W'}_f for the number of loops thus appeared.

We describe these operations a bit more formally. Write P = P_0\uplus I and P' = P_0'\uplus I'. Then consider the graph W\dblcolon_f{{W}'} with vertices in P\cup P', and such that there is an edge between p and q iff q = W(p) or q = W'(p) or q = f(p) or p = f(q): in other words, W\dblcolon_f{{W}'}=W\cup W'\cup f\cup f^{-1}. Vertices in P_0\cup P'_0 are of degree 1, and the others are of degree 2. Hence maximal paths in W\dblcolon_f{{W}'} are of two kinds:

  • straight paths, with both ends in P_0\cup P_0';
  • cycles, with vertices all in I\cup I'.

Then the wires in W\bowtie_f{{W}'} are the pairs {p,p'} such that p and p' are the ends of a path in W\dblcolon_f{{W}'}. And \Inner{W}{W'}_{f} is the number of cycles in W\dblcolon_f{{W}'}, or more precisely the number of support sets of cycles (i.e. we forget about the starting vertice of cycles).

Lemma

Consider three wirings (P,W), (P',W') and (P'',W''), and two connections (I,I',f):P\pinj P' and (J',J'',g):P'\pinj P'' such that I'\cap J'=\emptyset. Then

 (W\bowtie_f W')\bowtie_g W''=
  W\bowtie_f(W'\bowtie_g W'')

and

 \Inner{W}{W'}_{f}+\Inner{(W\bowtie_f{{W}'})}{{W}''}_g=
    \Inner{W}{(W'\bowtie_g W'')}_f+\Inner{{W}'}{{W}''}_g.

Proof.  The first equation holds because open maximal paths in W\dblcolon_f{W'\bowtie_g}{{W}''} correspond with those in W\dblcolon_f{(W'\dblcolon_g{{W}''})}, hence in (W\dblcolon_f W')\dblcolon_g W'', hence in {W\bowtie_f{{W}'}}\dblcolon_g{{W}''}. The second equation holds because both sides are two possible writings for the number of loops in {(W\dblcolon_f{{W}'})}\dblcolon_g{{W}''}

[edit] Nets

A signature is the data of a set Σ of symbols, together with arity functions \alpha:\Sigma\to\mathbf{N}\setminus\{0\} (number of active ports, or conclusions) and \pi:\Sigma\to\mathbf N (number of passive ports, or hypotheses). In the remaining, we assume such a signature is given.

A cell c with ports in P is the data of a symbol \sigma\in\Sigma and of two disjoint lists of pairwise distinct ports: \alpha(c)\in P^{\alpha(\sigma)} is the list of active ports and \pi(c)\in P^{\pi(\sigma)} is the list of passive ports.

A net is the data of a wiring (P,W), of a set C of disjoint cells on P, and of a number L\in\mathbf N (the number of loops). It follows from the definitions that each port p\in P appears in exactly one wire and in at most one cell: we say p is free if it is not part of a cell, and p is internal otherwise. Moreover, we say p is dangling if p is free and W(p) is internal. We write fp(R) for the set of free ports of a net R.

Generally, the “names” of internal ports of a net are not relevant, but free ports matter most often: internal ports are the analogue of bound variables in λ-terms. More formally, an isomorphism from net R to net R' is the data of a bijection of ports \phi:P\cong P' and a bijection of cells \psi:C\cong C' such that:

  • for all p\in P, W'(φ(p)) = φ(W(p));
  • for all c\in C:
    • σψ(c) = σc,
    • for all i\in\{0,\dotsc,\alpha(\sigma_c)-1\}, α(ψ(c))i = φ(α(c)i),
    • for all j\in\{0,\dotsc,\pi(\sigma_c)-1\}, π(ψ(c))j = φ(π(c)j);
  • L = L'.

Observe that under these conditions ψ is uniquely induced by φ. We say that the isomorphism φ is nominal if moreover p\in\textrm{fp}(R) implies p = φ(p).

[edit] Subnets

We say two nets are disjoint when their sets of ports are. Let R and R' be disjoint nets, and (I,I',f) be a connection between W and W', such that I\subseteq \textrm{fp}(R) and I'\subseteq \textrm{fp}(R'). We then write R\bowtie_f{R'} for the net with wiring W\bowtie_f{W'}, cells C\cup C' and loops \Inner{R}{R'}_f=L+L'+\Inner{W}{W'}_f. We say this connection is orthogonal if \Inner{W}{W'}_f=0, and it is modular if the ports in I\cup I' are all dangling: a modular connection is always orthogonal.

We say R0 is a subnet of R, if there exists a net R' and a connection (I,I',f) between R0 and R' such that R=R_0\bowtie_f{R'}.

Lemma

Let R0, R1 and R' be nets such that R0 and R1 are disjoint from R, (I,I',f) be a connection \textrm{fp}(R_0)\pinj \textrm{fp}(R') and φ an isomorphism R_0\cong R_1 such that φ(p) = φ(p') for all p\in\textrm{fp}(R_0)\setminus I. Then R_0\bowtie_f{R'} is nominally isomorphic to R_1\bowtie_{f\circ\phi^{-1}}{R'}.

[edit] Rewriting

A net rewriting rule is a pair (r0,r1) of nets such that fp(r0) = fp(r1). Then an instance of this rule is a pair (R0,R1) such that there exist:

  • nets R'0 and R'1 isomorphic to r0 and r1 respectively, namely R'i = φi(ri), so that moreover φ0(p) = φ1(p) for all p\in\textrm{fp}(r_0) (in particular, fp(R'0) = fp(R'1));
  • a net R'', disjoint from R'0 and R'1;
  • a connection (\textrm{fp}(R'_0),J,f):\textrm{fp}(R'_0)\pinj \textrm{fp}(R'');

such that each Ri is nominally isomorphic to R'_i\bowtie_f{R''}.

[edit] Typing

A typing system on signature Σ is the data of a set Θ of types, an involutive negation \cdot\orth:\Theta\to\Theta, together with a typing discipline for each symbol, i.e. a relation \Theta(\sigma)\subseteq\Theta^{\alpha(\sigma)}\times\Theta^{\pi(\sigma)}. We then write A_1,\cdots,A_{\pi(\sigma)}\vdash_\sigma
B_1,\cdots,B_{\alpha(\sigma)} for (\vec A,\vec B)\in\Theta(\sigma).

Then a typing for net R = (P,W,C) is a function \tau:P\to \Theta such that:

  • for all p\in P, \tau(W(p))=\tau(p)\orth;
  • for all c\in C of symbol σ, \tau(\pi(c))\vdash\tau(\alpha(c))\orth;

where, in the last formula, we implicitly generalized τ to lists of ports and \cdot\orth to lists of formulas, in the obvious, componentwise fashion. The interface of the typed net (R,τ) is then the restriction of τ to fp(R).

The idea, is that a wire {p,q} bears the type τ(q) (resp. τ(p)) in the direction (p,q) (resp. (q,p)), so that a rule \vec A\vdash_\sigma \vec B reads as an inference from passive inputs (hypotheses) to active outputs (conclusions).

Observe that if (R,τ) is a typed net, and \phi:R\cong R' is an isomorphism, then R' is typed and its interface is \tau\circ\phi^{-1}: in particular, if φ is nominal, R' and R have the same interface.

Now let (R,τ) and (R',τ') be typed nets and (I,I',f) a connection so that \tau'\circ f and \tau\orth=\cdot\orth\circ\tau coincide on I. Then this induces a typing of R\bowtie_f{R'} preserving the interface on the remaining free ports.

[edit] Boxes

A signature with boxes is the data of a signature Σ, together with a box arity β(σ) for all symbol \sigma\in\Sigma.

Then a net on signature with boxes (Σ,β) is the same as a net R on Σ plus, for each cell c of R, the data β(c) of a β(σc)-tuple of nets (with boxes) with free ports the internal ports of c.

Personal tools