Since the World Wide Web Consortium (W3C) has recommended XQuery as the standard XML query language, the interest in using existing relational technology to query the XML data has dramatically increased. The most significant challenge of the relational approach is how to fully support XQuery semantics in XQuery-to-SQL translation. To eliminate the implicit semantics of XQuery, an XQuery fragment must be defined with simple syntax and explicit semantics. XQ is proposed as an XQuery fragment to express XML queries. <br /><br /> In this thesis, XQ is intensively investigated. It is encoded by <em>System F</em>, a second-order lambda calculus with a considerable expressive power and a strong normalization property. Since XML data is defined as inductive data types, XML tree and XML forest, in <em>System F</em>, all basic XML operators in XQ have been successfully encoded. Also, the semantics of XQ are represented in <em>System F</em> where XQ's semantics environment is encoded by an <em>Environment</em> data type with the corresponding operators. The successful encoding of XQ by <em>System F</em> ensures the termination of XQ query evaluation. <br /><br /> Moreover, an extension of XQ by a new tree operator Xtree and a vertical Vfor clause is proposed in this thesis to express some <em>undefinable</em> XQ queries. It is demonstrated that this extension still allows XQ to retain its XQ-to-SQL translation property that ensures the polynomial evaluation time complexity, and its <em>System F</em> encodable property that ensures the termination of query evaluation.

Since the World Wide Web Consortium (W3C) has recommended XQuery as the standard XML query language, the interest in using existing relational technology to query the XML data has dramatically increased. The most significant challenge of the relational approach is how to fully support XQuery semantics in XQuery-to-SQL translation. To eliminate the implicit semantics of XQuery, an XQuery fragment must be defined with simple syntax and explicit semantics. XQ is proposed as an XQuery fragment to express XML queries. <br /><br /> In this thesis, XQ is intensively investigated. It is encoded by <em>System F</em>, a second-order lambda calculus with a considerable expressive power and a strong normalization property. Since XML data is defined as inductive data types, XML tree and XML forest, in <em>System F</em>, all basic XML operators in XQ have been successfully encoded. Also, the semantics of XQ are represented in <em>System F</em> where XQ's semantics environment is encoded by an <em>Environment</em> data type with the corresponding operators. The successful encoding of XQ by <em>System F</em> ensures the termination of XQ query evaluation. <br /><br /> Moreover, an extension of XQ by a new tree operator Xtree and a vertical Vfor clause is proposed in this thesis to express some <em>undefinable</em> XQ queries. It is demonstrated that this extension still allows XQ to retain its XQ-to-SQL translation property that ensures the polynomial evaluation time complexity, and its <em>System F</em> encodable property that ensures the termination of query evaluation.

Zugl.: Braunschweig, Techn. Univ., Diss., 2009

This thesis develops a semiunification-based type inference procedure for the rank 2 fragment of System F, with an emphasis on practical considerations for the adoption of such a procedure into existing programming languages. Current semiunification-based rank 2 inference procedures (notably that of Kfoury and Wells) are limited in several ways, which hinder their use in real-world settings. First of all, the translation from an instance of the type inference problem to an instance of the semiunification problem (SUP) is indirect; in particular, because of a series of source-level transformations that take place before translation, the translation is not syntax-directed. As a result, type errors discovered during the semiunification process cannot be cleanly translated back to specific subexpressions of the source program that caused the error. Also, because the rank 2 fragment of System F lacks a principal types property, an inference procedure cannot output a single type that encompasses all of a given term's derivable types. The procedure must therefore either rely on user assistance to produce the right type, or simply choose arbitrarily one of the given term's possible types. The algorithm of Kfoury and Wells in particular makes degenerate type assumptions in the absence of user assistance, and consequently produces types that are of no practical use. We build up our system in stages; we begin by improving the SUP translation. Whereas termination for the Kfoury-Wells rank 2 inference procedure is assured by translating terms into instances of the acyclic semiunification problem (a decidable subset of SUP, which is undecidable in general), we formulate and target the R-acyclic semiunification problem---a larger decidable subset of SUP that facilitates a more concise translation from source terms. We next eliminate the source-level transformation of terms, in order to formulate a truly syntax-directed translation from a source term to a set of SUP-like constraints. In doing so, we find that even the full SUP itself is not sufficiently equipped to support such a translation. We formulate USUP, a superset of SUP that incorporates a new class of identifier we call an unknown. We formulate decidable subsets of USUP, and then formulate a truly syntax-directed translation from source terms into USUP, with guaranteed termination. Finally, to address the principal types problem, we introduce a notation for types in which we allow a particular class of variable to stand for type constructors, rather than ordinary types (an idea based on the so-called third-order lambda-calculus). We show that, with third-order types we can not only output large sets of useful types for a given term, without programmer assistance, but the types we output also generalize over more System F types than any type within System F itself can do, and still be a valid type for the source term. Thus, our system increases opportunities for separate compilation and code reuse beyond any existing system of which we are aware. Our system is sound, though incomplete in certain well-characterized ways, despite which our system performs exactly as one would hope on a variety of examples, which we illustrate in this thesis.

This thesis develops a semiunification-based type inference procedure for the rank 2 fragment of System F, with an emphasis on practical considerations for the adoption of such a procedure into existing programming languages. Current semiunification-based rank 2 inference procedures (notably that of Kfoury and Wells) are limited in several ways, which hinder their use in real-world settings. First of all, the translation from an instance of the type inference problem to an instance of the semiunification problem (SUP) is indirect; in particular, because of a series of source-level transformations that take place before translation, the translation is not syntax-directed. As a result, type errors discovered during the semiunification process cannot be cleanly translated back to specific subexpressions of the source program that caused the error. Also, because the rank 2 fragment of System F lacks a principal types property, an inference procedure cannot output a single type that encompasses all of a given term's derivable types. The procedure must therefore either rely on user assistance to produce the right type, or simply choose arbitrarily one of the given term's possible types. The algorithm of Kfoury and Wells in particular makes degenerate type assumptions in the absence of user assistance, and consequently produces types that are of no practical use. We build up our system in stages; we begin by improving the SUP translation. Whereas termination for the Kfoury-Wells rank 2 inference procedure is assured by translating terms into instances of the acyclic semiunification problem (a decidable subset of SUP, which is undecidable in general), we formulate and target the R-acyclic semiunification problem---a larger decidable subset of SUP that facilitates a more concise translation from source terms. We next eliminate the source-level transformation of terms, in order to formulate a truly syntax-directed translation from a source term to a set of SUP-like constraints. In doing so, we find that even the full SUP itself is not sufficiently equipped to support such a translation. We formulate USUP, a superset of SUP that incorporates a new class of identifier we call an unknown. We formulate decidable subsets of USUP, and then formulate a truly syntax-directed translation from source terms into USUP, with guaranteed termination. Finally, to address the principal types problem, we introduce a notation for types in which we allow a particular class of variable to stand for type constructors, rather than ordinary types (an idea based on the so-called third-order lambda-calculus). We show that, with third-order types we can not only output large sets of useful types for a given term, without programmer assistance, but the types we output also generalize over more System F types than any type within System F itself can do, and still be a valid type for the source term. Thus, our system increases opportunities for separate compilation and code reuse beyond any existing system of which we are aware. Our system is sound, though incomplete in certain well-characterized ways, despite which our system performs exactly as one would hope on a variety of examples, which we illustrate in this thesis.

Dans cette thèse on s'intéresse aux formes de "circularité" qui apparaissent dans la théorie de la preuve de la logique du second ordre et de son contrepartie constructive, le Système F.Ces "circularités", ou "cercles vicieux" (Poincaré 1900), sont analysées sur la base d'une distinction entre deux points de vue distincts et irréductible (à cause des théorèmes d'incomplétude): le premier ("le pourquoi", Girard 1989) concerne la cohérence et l'Hauptsatz et demande des méthodes infinitaires (i.e. non élémentaires) de preuve. Le deuxième ("le comment", Girard 1989) concerne le contenu computationnel et combinatoire des preuves, donné par la correspondance entre preuves et programmes, et ne demande que de méthodes élémentaires de preuve.Dans la première partie de la thèse, dévouée au "pourquoi", les arguments philosophiques traditionnels sur les "cercles vicieux" sont confrontés avec la perspective qui émerge de la démonstration de l' Hauptsatz pour la logique de second ordre (obtenue par Girard avec la technique des candidats de réductibilité).Dans la deuxième partie de la thèse, dévouée au "comment", deux approches combinatoires aux cercles vicieux sont proposés: la première se basant sur la théorie du polymorphisme paramétrique, la deuxième sur l'analyse géométrique du typage qui vient de la théorie de l'unification. / In this dissertation several issues concerning the proof-theory of second order logic and its constructive counterpart (System F, Girard 1971) are addressed. The leitmotiv of the investigations here presented is the apparent "circularity'' or "impredicativity'' of second order proofs. This circularity is reflected in System F by the possibility to type functions applied to themselves, in contrast with Russell's idea that typing should rather forbid such ``vicious circles'' (Poincare 1906). A fundamental methodological distinction between two irreducible (because of incompleteness) approaches in proof theory constitutes the background of this work: on the one hand, "why-proof theory'' ("le pourquoi'', Girard 1989) addresses coherence and the Hauptsatz and requires non-elementary ("infinitary'') techniques; on the other hand, "how-proof theory'' ("le comment'', Girard 1989) addresses the combinatorial and computational content of proofs, given by the correspondence between proofs and programs, and is developed on the basis of elementary ("finitary'') techniques. }In the first part of the thesis, dedicated to "why-proof theory'', the traditional philosophical arguments on "vicious circles'' are confronted with the perspective arising from the proof of the Hauptsatz for second order logic (first obtained in Girard 1971 with the technique of reducibility candidates).In the second part of the thesis, dedicated to "how-proof theory'', two combinatorial approaches to "vicious circles'' are presented, with some technical results: the first one based on the theory of parametric polymorphism, the second one on the geometrical analysis of typing coming from unification theory.