Catálogo de publicaciones - libros

Navigation is at the core of most XML processing tasks. The W3C endorsed navigation language XPath is part of XPointer (for creating links between elements in (different) XML documents), XSLT (for transforming XML documents) and XQuery (for, indeed, querying XML documents). Navigation in an XML document tree is the task of moving from a given node to another node by following a path specified by a certain formula. Hence formulas in navigation languages denote paths, or stated otherwise binary relations between nodes. Binary relations can be expressed in XPath or with first or second order formulas in two free variables. The problem with all of these formalisms is that they are not compositional in the sense that each subexpression also specifies a binary relation. This makes a mathematical study of these languages complicated because one has to deal with objects of different sorts. Fortunately there exists an algebraic formalism which is created solely to study binary relations. This formalism goes back to logic pioneers as de Morgan, Peirce and Schröder and has been formalized by Tarski as relation algebras [7]. (Cf., [5] for a monograph on this topic, and [8] for a database oriented introduction). A relation algebra is a boolean algebra with three additional operations. In its natural representation each element in the domain of the algebra denotes a binary relation. The three extra operations are a constant denoting the identity relation, a unary conversion operation, and a binary operation denoting the composition of two relations. The elements in the algebra denote first order definable relations. Later Tarski and Ng added the Kleene star as an additional operator, denoting the transitive reflexive closure of a relation [6]. We will show that the formalism of relation algebras is very well suited for defining navigation paths in XML documents. One of its attractive features is that it does not contain variables, a feature shared by XPath 1.0 and the regular path expressions of [1]. The connection between relation algebras and XPath was first made in [4]. The aim of this talk is to show that relation algebras (possibly expanded with the Kleene star) can serve as a unifying framework in which many of the proposed navigation languages can be embedded. Examples of these embeddings are 1 Every Core XPath definable path is definable using composition, union and the counterdomain operator ~ with semantics ~ R  = {( x , x )| not  ∃  y : xRy }. 2 Every first order definable path is definable by a relation algebraic expression. 3 Every first order definable path is definable by a positive relation algebraic expression which may use the Kleene star. 4 The paths definable by tree walk automata and certain tree walk automata with pebbles can be characterized by natural fragments of relation algebras with the Kleene star. All these results hold restricted to the class of finite unranked sibling ordered trees. The main open problem is the expressive power of relation algebras expanded with the Kleene star, interpreted on this class of models. Is this formalism equally expressive as binary first order logic with transitive closure of binary formulas? Whether the latter is equivalent to binary monadic second order logic is also open [2,3]. So in particular we do not know whether each regular tree language can be defined in relation algebras with the Kleene star.

We discuss the verification of timed systems within predicate logics with explicit time and arithmetical operations. The main problem is to find efficient algorithms to treat practical problems. One way is to find practically decidable classes that englobe this or that class of practical problems. This is our main goal, where we concentrate on one approach that permits to arrive at a kind of small model property. We will also touch the question of extension of these results to probabilistic systems that will be presented in more detail elsewhere.

This note describes a formal rule for analogical reasoning in the legal context. The rule derives first order sentences from partial decision descriptions. The construction follows the principle, that the acceptance of an incomplete argument induces the acceptance of the logically weakest assumptions, which complete it.

We prove a strong normalization theorem for abstract term rewriting systems based on domain-theoretic models. The theorem applies to extensions of Gödel’s system T by various forms of recursion related to bar recursion for which strong normalization was hitherto unknown.

We describe a polymorphic extension of the substructural lambda calculus αλ associated with the logic of bunched implications. This extension is particularly novel in that both variables and type variables are treated substructurally, being maintained through a system of zoned, bunched contexts. Polymorphic universal quantifiers are introduced in both additive and multiplicative forms, and then metatheoretic properties, including subject-reduction and normalization, are established. A sound interpretation in a class of indexed category models is defined and the construction of a generic model is outlined, yielding completeness. A concrete realization of the categorical models is given using pairs of partial equivalence relations on the natural numbers. Polymorphic existential quantifiers are presented, together with some metatheory. Finally, potential applications to closures and memory-management are discussed.

In previous work we presented a foundational calculus for spatially distributed computing based on intuitionistic modal logic. With the modalities □ and $\Diamond$ we were able to capture two key invariants: the mobility of portable code and the locality of fixed resources. This work investigates issues in distributed control flow through a similar propositions-as-types interpretation of classical modal logic. The resulting programming language is enhanced with the notion of a network-wide continuation, through which we can give computational interpretation of classical theorems (such as $\Box A \equiv \lnot \Diamond \lnot A$ ). Such continuations are also useful primitives for building higher-level constructs of distributed computing. The resulting system is elegant, logically faithful, and computationally reasonable.

By Rutten’s dualization of the Birkhoff Variety Theorem, a collection of coalgebras is a covariety (i.e., is closed under coproducts, subcoalgebras, and quotients) iff it can be presented by a subset of a cofree coalgebra. We introduce inference rules for these subsets, and prove that they are sound and complete. For example, given a polynomial endofunctor of a signature Σ, the cofree coalgebra consists of colored Σ-trees, and we prove that a set  T of colored trees is a logical consequence of a set  S iff T  contains every tree such that all recolorings of all its subtrees lie in  S . Finally, we characterize covarieties whose presentation needs only n  colors.

A semantic formulation of Lindley and Stark’s ⊤ ⊤-lifting is given. We first illustrate our semantic formulation of the ⊤ ⊤-lifting in Set with several examples, and apply it to the logical predicates for Moggi’s computational metalanguage. We then abstract the semantic ⊤ ⊤-lifting as the lifting of strong monads across bifibrations with lifted symmetric monoidal closed structures.

We are interested in the question whether the models induced by the infinitary lambda calculus are orderable, that is whether they have a partial order with a least element making the context operators monotone. The first natural candidate is the prefix relation: a prefix of a term is obtained by replacing some subterms by $\bot$ . We prove that six models induced by the infinitary lambda calculus (which includes Böhm and Lévy-Longo trees) are orderable by the prefix relation. The following two orders we consider are the compositions of the prefix relation with either transfinite η -reduction or transfinite η -expansion. We prove that these orders make the context operators of the η -Böhm trees and the ∞ η -Böhm trees monotone. The model of Berarducci trees is not monotone with respect to the prefix relation. However, somewhat unexpectedly, we found that the Berarducci trees are orderable by a new order related to the prefix relation in which subterms are not replaced by $\bot$ but by a lambda term O called the ogre which devours all its inputs. The proof of this uses simulation and coinduction. Finally, we show that there are 2^ c unorderable models induced by the infinitary lambda calculus where c is the cardinality of the continuum.

We provide a game-theoretic characterisation of higher-order matching. The idea is suggested by model checking games. We then show that some known decidable instances of matching can be uniformly proved decidable via the game-theoretic characterisation.