Catálogo de publicaciones - libros

Soft Linear Logic (SLL) is a subsystem of second-order linear logic with restricted rules for exponentials, which is correct and complete for PTIME. We design a type assignment system for the -calculus (STA), which assigns to -terms as types (a proper subset of) SLL formulas, in such a way that typable terms inherit the good complexity properties of the logical system. Namely STA enjoys subject reduction and normalization, and it is correct and complete for PTIME and FPTIME.

A longstanding open problem is whether there exists a non-syntactical model of the untyped -calculus whose theory is exactly the least -theory . In this paper we investigate the more general question of whether the equational/order theory of a model of the untyped -calculus can be recursively enumerable (r.e. for brevity). We introduce a notion of of -calculus, which covers in particular all the models individually introduced in the literature. We prove that the order theory of an effective model is never r.e.; from this it follows that its equational theory cannot be , . We then show that no effective model living in the stable or strongly stable semantics has an r.e. equational theory. Concerning Scott’s semantics, we investigate the class of graph models and prove that no order theory of a graph model can be r.e., and that there exists an effective graph model whose equational/order theory is the minimum one. Finally, we show that the class of graph models enjoys a kind of downwards Löwenheim-Skolem theorem.

Normal form bisimulation is a powerful theory of program equivalence, originally developed to characterize Lévy-Longo tree equivalence and Boehm tree equivalence. It has been adapted to a range of untyped, higher-order calculi, but types have presented a difficulty. In this paper, we present an account of normal form bisimulation for types, including recursive types. We develop our theory for a continuation-passing style calculus, Jump-With-Argument (JWA), where normal form bisimilarity takes a very simple form. We give a novel congruence proof, based on insights from game semantics. A notable feature is the seamless treatment of eta-expansion. We demonstrate the normal form bisimulation proof principle by using it to establish a syntactic minimal invariance result and the uniqueness of the fixed point operator at each type.

Models of the untyped -calculus may be defined either as applicative structures satisfying a bunch of first-order axioms (-models), or as reflexive objects in cartesian closed categories (categorical models). In this paper we show that any categorical model of -calculus can be presented as a -model, even when the underlying category does not have enough points. We provide an example of an extensional model of -calculus in a category of sets and relations which has not enough points. Finally, we present some of its algebraic properties which make it suitable for dealing with non-deterministic extensions of -calculus.

We show how to extract classical programs expressed in Krivine -calculus from proof-terms built in a proof-irrelevant and classical version of the calculus of constructions with universes. For that, we extend Krivine’s realisability model of classical second-order arithmetic to the calculus of constructions with universes using a structure of -set which is reminiscent of -sets, and show that our realisability model validates Peirce’s law and proof-irrelevance. Finally, we extend the extraction scheme to a primitive data-type of natural numbers in a way which preserves the whole compatibility with the classical realisability interpretation of second-order arithmetic.

It is commonly agreed that the success of future proof assistants will rely on their ability to incorporate computations within deduction in order to mimic the mathematician when replacing the proof of a proposition P by the proof of an equivalent proposition P’ obtained from P thanks to possibly complex calculations.

In this paper, we investigate a new version of the calculus of inductive constructions which incorporates arbitrary decision procedures into deduction via the conversion rule of the calculus. The novelty of the problem in the context of the calculus of inductive constructions lies in the fact that the computation mechanism varies along proof-checking: goals are sent to the decision procedure together with the set of user hypotheses available from the current context. Our main result shows that this extension of the calculus of constructions does not compromise its main properties: confluence, subject reduction, strong normalization and consistency are all preserved.

It is well-known that every first-order property on words is expressible using at most three variables. The subclass of properties expressible with only two variables is also quite interesting and wellstudied. We prove precise structure theorems that characterize the exact expressive power of first-order logic with two variables on words. Our results apply to FO2[<] and [<; Suc], the latter of which includes the binary successor relation in addition to the linear ordering on string positions.

For both languages, our structuretheorems showexactly whatis expressible using a given quantifier depth, n, and using m blocks of alternating quantifiers, for any m ≤ n. Using these characterizations, we prove, among other results, that there is a strict hierarchy of alternating quantifiers for both languages. The question whether there was such a hierarchy had been completely open. As another consequence of our structural results, we show that satisfiability for FO2[<], which is NEXP-complete in general, becomes NP-complete once we only consider alphabets of a bounded size.

We study the complexity of satisfiability for DLP, an expressive logic introduced by Demri that allows to reason about dynamic policies. DLP extends the logic DLP of Pucella and Weissman, which in turn extends van der Meyden’s Dynamic Logic of Permission (DLP). DLP generously enhances DLP and DLP by allowing to update the policy set by adding or removing policy transitions, which are defined as a direct product of two sets, each specified by a formula of the logic itself. It is proven that satisfiability for DLP is complete for deterministic exponential time. Our results close the complexity gap of satisfiability for DLP from 2EXP, and for DLP from NEXP, to EXP respectively, matching the EXP lower bound both inherit from Propositional Dynamic Logic (PDL). To prove the EXP upper bound for DLP, we first proceed by accurately identifying a suitable generalization of PDL, which allows to use compressed programs and then find a satisfiability preserving translation from DLP to this extension of PDL. To finally show the EXP upper bound for DLP, we prove that satisfiability of our extension of PDL lies in EXP!.

Existing definitions of the relativizations of , and do not preserve the inclusions  ⊆ ,  ⊆ . We start by giving the first definitions that preserve them. Here for and we define their relativizations using Wilson’s stack oracle model, but limit the height of the stack to a constant (instead of log()). We show that the collapse of any two classes in {(), , , , } implies the collapse of their relativizations. Next we develop theories that characterize the relativizations of subclasses of by modifying theories previously defined by the second two authors. A function is provably total in a theory iff it is in the corresponding relativized class. Finally we exhibit an oracle that makes () a proper hierarchy. This strengthens and clarifies the separations of the relativized theories in [Takeuti, 1995]. The idea is that a circuit whose nested depth of oracle gates is bounded by cannot compute correctly the ( + 1) compositions of every oracle function.

Recently a mapping , the so-called miniaturization mapping, has been introduced and it has been shown that faithfully translates subexponential parameterized complexity into (unbounded) parameterized complexity  [2]. We determine the preimages under of various (classes of) problems and show that they coincide with natural reparameterizations which take into account the amount of nondeterminism needed to solve them.