Catálogo de publicaciones - libros

Since Val Tannen’s pioneering work on the combination of simply-typed λ -calculus and first-order rewriting [11], many authors have contributed to this subject by extending it to richer typed λ -calculi and rewriting paradigms, culminating in the Calculus of Algebraic Constructions. These works provide theoretical foundations for type-theoretic proof assistants where functions and predicates are defined by oriented higher-order equations. This kind of definitions subsumes usual inductive definitions, is easier to write and provides more automation. On the other hand, checking that such user-defined rewrite rules, when combined with β -reduction, are strongly normalizing and confluent, and preserve the decidability of type-checking, is more difficult. Most termination criteria rely on the term structure. In a previous work, we extended to dependent types and higher-order rewriting, the notion of “sized types” studied by several authors in the simpler framework of ML-like languages, and proved that it preserves strong normalization. The main contribution of the present paper is twofold. First, we prove that, in the Calculus of Algebraic Constructions with size annotations, the problems of type inference and type-checking are decidable, provided that the sets of constraints generated by size annotations are satisfiable and admit most general solutions. Second, we prove the latter properties for a size algebra rich enough for capturing usual induction-based definitions and much more.

In proof systems like Coq [16], proof-checking involves comparing types modulo β -conversion, which is potentially a time-consuming task. Significant speed-ups are achieved by compiling proof terms, see [9]. Since compilation erases some type information, we have to show that convertibility is preserved by type erasure. This article shows the equivalence of the Calculus of Inductive Constructions (formalism of Coq) and its domain-free version where parameters of inductive types are also erased. It generalizes and strengthens significantly a similar result by Barthe and Sørensen [5] on the class of functional Domain-free Pure Type Systems.

We consider the setting of L-nets, recently introduced by Faggian and Maurel as a game model of concurrent interaction and based on Girard’s Ludics. We show how L-nets satisfying an additional condition, which we call logical L-nets, can be sequentialized into traditional tree-like strategies, and vice-versa.

Recent work establishes a direct link between the complexity of a linear logic proof in terms of the exchange rule and the topological complexity of its corresponding proof net, expressed as the minimal rank of the surfaces on which the proof net can be drawn without crossing edges. That surface is essentially computed by sequentialising the proof net into a sequent calculus which is derived from that of linear logic by attaching an appropriate structure to the sequents. We show here that this topological calculus can be given a better-behaved logical status, when viewed in the variety-presentation framework introduced by the first author. This change of viewpoint gives rise to permutative logic, which enjoys cut elimination and focussing properties and comes equipped with new modalities for the management of the exchange rule. Moreover, both cyclic and linear logic are shown to be embedded into permutative logic. It provides the natural logical framework in which to study and constrain the topological complexity of proofs, and hence the use of the exchange rule.

Focusing is traditionally seen as a means of reducing inessential non-determinism in backward-reasoning strategies such as uniform proof-search or tableaux systems. In this paper we construct a form of focused derivations for propositional linear logic that is appropriate for forward reasoning in the inverse method. We show that the focused inverse method conservatively generalizes the classical hyperresolution strategy for Horn-theories, and demonstrate through a practical implementation that the focused inverse method is considerably faster than the non-focused version.

Girard’s Geometry of Interaction (GoI) develops a mathematical framework for modelling the dynamics of cut-elimination. We introduce a typed version of GoI, called Multiobject GoI (MGoI) for multiplicative linear logic without units in categories which include previous (untyped) GoI models, as well as models not possible in the original untyped version. The development of MGoI depends on a new theory of partial traces and trace classes, as well as an abstract notion of orthogonality (related to work of Hyland and Schalk) We develop Girard’s original theory of types, data and algorithms in our setting, and show his execution formula to be an invariant of Cut Elimination. We prove Soundness and Completeness Theorems for the MGoI interpretation in partially traced categories with an orthogonality.

The constraint satisfaction problem (CSP) and quantified constraint satisfaction problem (QCSP) are common frameworks for the modelling of computational problems. Although they are intractable in general, a rich line of research has identified restricted cases of these problems that are tractable in polynomial time. Remarkably, many tractable cases of the CSP that have been identified are solvable by a single algorithm, which we call here the consistency algorithm. In this paper, we give a natural extension of the consistency algorithm to the QCSP setting, by making use of connections between the consistency algorithm and certain two-person pebble games. Surprisingly, we demonstrate a variety of tractability results using the algorithm, revealing unified structure among apparently different cases of the QCSP.

We describe a simple algebraic semi-decision procedure for detecting unsatisfiability of a (quantifier-free) conjunction of nonlinear equalities and inequalities. The procedure consists of Gröbner basis computation plus extension rules that introduce new definitions, and hence it can be described as a critical-pair completion-based logical procedure. This procedure is shown to be sound and refutationally complete. When projected onto the linear case, our procedure reduces to the Simplex method for solving linear constraints. If only finitely many new definitions are introduced, then the procedure is also terminating. Such terminating, but potentially incomplete, procedures are used in “incompleteness-tolerant” applications.

We investigate properties of the coprimality relation within the family of finite models being initial segments of the standard model for coprimality, denoted by $\mathrm{FM}((\omega,\bot))$ . Within $\mathrm{FM}((\omega,\bot))$ we construct an interpretation of addition and multiplication on indices of prime numbers. Consequently, the first order theory of $\mathrm{FM}((\omega,\bot))$ is Π $^{\rm 0}_{\rm 1}$ –complete (in contrast to the decidability of the theory of multiplication in the standard model). This result strengthens an analogous theorem of Marcin Mostowski and Anna Wasilewska, 2004, for the divisibility relation. As a byproduct we obtain definitions of addition and multiplication on indices of primes in the model $(\omega,\bot,\leq_{P_2})$ , where P _2 is the set of primes and products of two different primes and ≤_ X is the ordering relation restricted to the set X . This can be compared to the decidability of the first order theory of $(\omega,\bot,\leq_P)$ , for P being the set of primes (Maurin, 1997) and to the interpretation of addition and multiplication in $(\omega,\bot,\leq_{P^2})$ , for P ^2 being the set of primes and squares of primes, given by Bès and Richard, 1998.

This work deals with the expressive power of logics on finite structures with access to an additional “arbitrary” linear order. The queries that can be expressed this way are the order-invariant queries for the logic. For the standard logics used in computer science, such as first-order logic, it is known that access to an arbitrary linear order increases the expressiveness of the logic. However, when we look at the separating examples, we find that they have satisfying models whose Gaifman Graph is complex – unbounded in valence and in treewidth. We thus explore the expressiveness of order-invariant queries over graph-theoretically well-behaved structures. We prove that first-order order-invariant queries over strings and trees have no additional expressiveness over first-order logic in the original signature. We also prove new upper bounds on order-invariant queries over bounded treewidth and bounded valence graphs. Our results make use of a new technique of independent interest: the application of algebraic characterizations of definability to show collapse results.