Workshop on Chu Spaces: Theory and Applications |

25th June 2000. |

Organised by Valeria de Paiva and Vaughan Pratt |

Chu Spaces and Realizability

We describe a form of realizability for Classical Linear Logic, related both to double gluing and to Chu spaces. Roughly, the Linear realizability categories relate to Chu spaces as the usual category of modest sets relates to the classical category of sets. However, the construction is significantly *different* to that which arises by simply applying the Chu construction to the category of modest sets. Examples of the construction include process realizability, concurrent games and geometry of interaction.

Chu Spaces through History

Continuity and Convergence in the Basic Picture

Joint work with Giovanni Sambin

When the classical definition of topological space is analyzed at the light of a constructive and predicative foundation like Martin Loef's type theory it naturally leads to the notion of basic pair. A basic pair is formed by two sets, the set X of concrete points and the set S of observables linked by a bynary relation called forcing. Any relation between two sets is sufficient to introduce the topological notions of open and closed subsets, both in the concrete (pointwise) and in the formal (pointfree) sense. A new discovery is that when closed subsets are defined primitively, instead of as complements of open subsets, a deeper logical structure emerges. While open subsets are defined by a combination of existential-universal quantifiers, closed subsets are characterized by the inverse combination universal-existential ones. The two notions are linked one to another by a logical duality which witnesses how logic and mathematics are deeply connected.

The theory of basic pairs, that is the most basic notion of (nondistributive) topological space, was developed by Sambin by relying on some ideas and inspiring principles: preservation of symmetry, simple definitions and structures, deep connection between logic and mathematics, and all of this adopting an intuitionistic and predicative foundation, for instance Martin-Loef's type theory.

Such principles are here applied to study the notions of continuity, convergence and to introduce the notion of morphisms between basic pairs. We will see how continuity is characterized in a fully structural way by commutative squares once it is deprived of notions like functions and it is made symmetric. We will also see that continuity and convergence are independent notions. Finally, we will see that once topological spaces are presented formally, continuity and convergence actually characterize ``usual'' continuous functions.

Perfect graphs and their total completions

A graph is perfect if the chromatic number of each its induced subgraph H equals the clique number of H. Our aim of this talk is to establish the relation between totality and perfectness. We present total completions of perfect graphs as certain Chu spaces over 2 , and study the coloring problems and the extremal problems for those graphs.

Full completeness of the multiplicative linear logic of Chu spaces

We show that the cut-free proofs of theorems of multiplicative linear logic are in natural bijection with the binary logical transformations of the corresponding operations on the category of Chu spaces on a two-letter alphabet. Joint work with Harish Devarajan, Gordon Plotkin, and Vaughan Pratt.

A 2-dimensional view of the Chu construction

The cyclic Chu-construction for closed bicategories, generalizing the original Chu-construction for symmetric monoidal closed categories, turns out to have a non-cyclic counterpart. Both constructions are based on the so-called Chu-cell and can be generalized to chains of composable 1-cells. This leads to two hierarchies of closed bicategories for any closed bicategory B. Chu-cells in rel correspond to bipartite state transition systems. Even though the Chu-construction fails here due to the lack of pullbacks, basic game-theoretic constructions can be performed on cyclic Chu-cells.

Towards semantics of self-adaptive software

When people perform computations, they routinely monitor their results, and try to adapt and improve their algorithms when a need arises. The idea of self-adaptive software is to implement this common facility of human mind within the framework of the standard logical methods of software engineering. The ubiquitous practice of testing, debugging and improving programs at the design time should be automated, and established as a continuing run time routine.

Technically, the task thus requires combining functionalities of automated software development tools and of runtime environments. Such combinations lead not just to challenging engineering problems, but also to novel theoretical questions. Formal methods are needed, and the standard techniques do not suffice.

As a first contribution in this direction, we present a basic mathematical framework suitable for describing self-adaptive software at a high level of semantical abstraction. A static view leads to a structure akin to the Chu construction. A dynamic view leads to a generalized version of this construction, with a time extension.

Importance of Chu Spaces in Philosophy and Computation

In their role as an alternative to the relational structures traditionally modeling first order logic, Chu spaces shift the emphasis from the camaraderie implicit in relationships to the competition implicit in opposition or duality. In this respect they join Hamiltonian mechanics in supplying respectively mathematical and physical frameworks supporting Cartesian dualism, a briefly popular 17th century world view strongly deserving of revival in the 21st century in the light of modern science and mathematics.

The essence of the points and states (dual points) of Chu spaces may be found in the subjects and predicates of linguistics, the individuals and predicates of logic, the positions and momenta of physics, the inbound and outbound arrows at categorical objects, and, most importantly for this talk, the events and states of computational process algebra.

I will focus on John Allen's theory of time and action, which has enjoyed some popularity in AI, and give a Chu-theoretic account of the hidden geometry in his interval algebra. Orthocurrence as the Chu tensor product left adjoint to Chu's internal hom accounts efficiently for both nonrelativistic and relativistic interval configurations or states, automatically producing not only Allen's 13 nonrelativistic states but also the relativistic state counts of 29 and 82 found by Rodriguez and Anger. It further organizes them as three attractively structured higher-dimensional automata manifesting concurrency, and in the relativistic case choice as well.

A Parigot-style Term Calculus for Full Intuitionistic Linear Logic

This note describes a natural deduction formulation for Full Intuitionistic Linear Logic (FILL), a variant of Linear Logic, first described by Hyland and de Paiva. The system FILL has all the multiplicative connectives of Classical Linear Logic (CLL), but it is { not} involutive: (not not A) is not the same as A, as in CLL. FILL has arisen from its categorical model, the Dialectica construction, a cousin of the Chu Spaces construction.

Our natural deduction formulation of FILL is based on Pym and Ritter's extension of Parigot's lambda-mu natural deduction system for (propositional) classical logic. Their extension, called lambda-mu-nu, was used to provide a term calculus for a multiplicative version of disjunction in classical logic. We provide a term-calculus for FILL based on lambda-mu-nu, which we call FILL-mu and prove its basic proof-theoretical properties.

The motivation for using Parigot's system lambda-mu and the associated lambda-mu-nu extension is that, like classical logic, FILL, is better presented using multiple-conclusions. In fact, the system FILL does seem to require multiple-conclusions for the description of its basic connectives. Thus we use the lambda-mu-nu calculus as a way of bypassing a system of multiple-conclusions natural deduction. Surprising at it may seem, this paper is not a corollary of Bierman's " Towards a Classical Linear lambda-calculus", where a similar idea is explored for classical linear logic. Bierman can use Parigot's ideas almost directly, whereas we have to contend with the subtle intuitionistic characteristics of FILL. This means first that we have to discuss disjunction independently of other connectives. Secondly it means that we have to use more powerful decorating mechanisms to keep track of dependencies between formulae than either Bierman or Pym and Ritter need to.

Joint work with Valeria de Paiva

Dialectica and Chu Constructions: Cousins?

In this talk I will start by recalling two varieties of dialectica categories in the literature and comparing them to Chu's construction. Then I shall present a mild generalisation of the construction and point out some further work.

The Elusive Infon

The search for a unit of information content ("infon") on which to ground a variety of informational metaphors - communication as information exchange, cognition as information processing, etc. - leads to conflicting desiderata, especially concerning the following issues: (i) whether or not information content is structured like sentences of a language, (ii) whether the possession of content is absolute or relative, and (iii) whether a sign has one or many contents. Consideration of these issues lead Jon Barwise and me to develop a model of informational systems that (as it turns out) use Chu spaces. In this talk, I aim to explain the motivation for this model, and assess its merits as a solution to the search for the elusive infon.

Back to top of page

*Page maintained by paiva@parc.xerox.com
Last modified: 16 May 2000
*