{
  "id": "1403.3772",
  "version": "v2",
  "published": "2014-03-15T08:57:26.000Z",
  "updated": "2016-10-08T13:07:26.000Z",
  "title": "Study of Behaviours via Visitable Paths",
  "authors": [
    "Christophe Fouqueré",
    "Myriam Quatrini"
  ],
  "categories": [
    "cs.LO"
  ],
  "abstract": "Around 2000, J.-Y. Girard developed a logical theory, called Ludics. This theory was a step in his program of Geometry of Interaction, the aim of which being to account for the dynamics of logical proofs. In Ludics, objects called designs keep only what is relevant for the cut elimination process, hence the dynamics of a proof: a design is an abstraction of a formal proof. The notion of behaviour is the counterpart in Ludics of the logical notions of formula or type. Formally a behaviour is a closed set of designs. Our aim is to explore the constructions of behaviours and to analyse their properties. In this paper a design is viewed as a set of coherent paths. We recall or give variants of properties concerning visitable paths, where a visitable path is a path in a design of a set of designs that may be traversed by interaction with a design of the orthogonal of the set. We are then able to answer the following question: which properties should satisfy a set of paths for being exactly the set of visitable paths of a behaviour? Such a set and its dual should be prefix-closed, daimon-closed and satisfy two saturation properties. This allows us to have a means for defining the whole set of visitable paths of a given set of designs without closing it explicitly, that is without computing the orthogonal of this set of designs. We finally apply all these results for making explicit the structure of a behaviour generated by constants and multiplicative/additive connectives. We end by proposing an oriented tensor for which we give basic properties.",
  "revisions": [
    {
      "version": "v1",
      "updated": "2014-03-15T08:57:26.000Z",
      "title": "Ludics Characterization of Multiplicative-Additive Linear Behaviours",
      "abstract": "Ludics is a logical theory that J.-Y. Girard developed around $2000$. At first glance, it may be considered as a Brouwer-Heyting-Kolmogorov interpretation of Logic as a formula is denoted by the set of its proofs. More primitively, Ludics is a theory of interaction that models (a variant of) second-order multiplicative-additive Linear Logic. A formula is denoted by a set of objects called a behaviour, a proof by an object that satisfies some criteria. Our aim is to analyze the structure of behaviours in order to better understand and refine the usual notion of formulas or types. More precisely, we study properties that guarantee a behaviour to be recursively decomposable by means of multiplicative-additive linear connectives and linear constants.",
      "comment": null,
      "journal": null,
      "doi": null
    },
    {
      "version": "v2",
      "updated": "2016-10-08T13:07:26.000Z"
    }
  ],
  "analyses": {
    "subjects": [
      "F.4.1"
    ],
    "keywords": [
      "multiplicative-additive linear behaviours",
      "ludics characterization",
      "second-order multiplicative-additive linear logic",
      "multiplicative-additive linear connectives",
      "first glance"
    ],
    "note": {
      "typesetting": "TeX",
      "pages": 0,
      "language": "en",
      "license": "arXiv",
      "status": "editable",
      "adsabs": "2014arXiv1403.3772F"
    }
  }
}