Speaker:

  dr Paolo Torrini, University of Leicester

  Time: 

  June 3, 2010, 14:00 in ATT SB2.07
 
  Title:

  Encoding graph transformation in intuitionistic linear logic

  Abstract:

  Graph transformation (GT) is a modelling technique based on the
  representation of states as graphs (or hyper-graphs) and state
  transitions as application of transformation rules.  There are
  several existing algebraic formalisations of graph transformation
  approaches based on categories, where rule matching and
  transformation are expressed in terms of glueing diagrams. Notably,
  in the DPO approach, a rule is represented as a span of total
  morphisms in the category of graphs, resulting in application as
  double pushout diagram.

  From the point of view of algebraic specification, GT can be
  regarded as an alternative to logic-based methods. However, theorem
  proving is needed for verification, and logic for mechanised theorem
  proving.  We have been trying to give a more concrete formalisation
  of DPO-GT using intuitionistic linear logic (ILL), hoping to make a
  prospected theorem-proving implementation more affordable than by
  using straightforward inductive definitions in HOL.  Unlike many
  state-oriented logics, linear logic is process oriented --- i.e. it
  is less about specifying states than transitions. There has been
  plenty of work on specifying processes with linear logic, though
  mostly directed to process calculi rather than GT.

  ILL allows for an elegant, straightforward encoding of GT-DPO at the
  most basic level, if hyperedges are represented as predicates and
  nodes as variables, in the graphs as well as in the rule patterns.
  A stumbling block comes with the fact that the matching of rule
  patterns to graphs may be required to be an injective morphism.
  Additionally, rule patterns if not graphs may typically include
  isolated nodes. Surjective morphisms can be naturally dealt with in
  terms of variable instantiation --- it suffices to assume that
  pattern variables are universally quantified.  Injective morphisms
  however require a treatment of variables as names. Notice that in
  this approach we do not have a notion of channel, therefore it does
  not seem natural to have names as a separate domain. Moreover, names
  here refer to nodes --- therefore to resources, that may be
  intuitively understood as locations.

  We have tried to deal with this issue by extending ILL with a linear
  existential quantifier (LinEx), and by giving an operational
  characterisation of name introduction that may be intuitively
  understood as recasting non-linear variables into linear ones,
  taking advantage of the underlying logic. LinEx has some of the
  features of well-known freshness quantifiers from the literature ---
  Gabbay and Pitt's New and Miller's Nabla. However, apart from the
  difference in the underlying logic and semantics, it does not
  exhibit anything like self-duality. It is generally weaker than New,
  and in particular 'LinEx x.p' is not equivalent to 'p', whereas
  'LinEx x y.A(x,y)' is equivalent to 'LinEx y x.  A(x,y)' (unlike
  Nabla). A preliminary formalisation is available at
  http://arxiv.org/abs/1003.5512