Gallier, Jean H
Email Address
ORCID
Disciplines
relationships.isProjectOf
relationships.isOrgUnitOf
Position
Introduction
Research Interests
Collection
38 results
Search Results
Now showing 1 - 10 of 38
Publication Proving Properties of Typed Lambda-Terms Using Realizability, Covers, and Sheaves (Preliminary Version)(1993-11-10) Gallier, Jean HWe present a general method for proving properties of typed λ-terms. This method is obtained by introducing a semantic notion of realizability which uses the notion of a cover algebra (as in abstract sheaf theory). For this, we introduce a new class of semantic structures equipped with preorders, called pre-applicative structures. These structures need not be extensional. In this framework, a general realizability theorem can be shown. Kleene's recursive realizability and a variant of Kreisel's modified realizability both fit into this framework. Applying this theorem to the special case of the term model, yields a general theorem for proving properties of typed λ-terms, in particular, strong normalization and confluence. This approach clarifies the reducibility method by showing that the closure conditions on candidates of reducibility can be viewed as sheaf conditions. The above approach is applied to the simply-typed λ-calculus (with types →, x, +, and ⊥), and to the second-order (polymorphic λ-calculus (with types → and ∀2), for which it yields a new theorem.Publication What's So Special About Kruskal's Theorem and the Ordinal To? A Survey of Some Results in Proof Theory(1993-09-30) Gallier, Jean HThis paper consists primarily of a survey of results of Harvey Friedman about some proof theoretic aspects of various forms of Krusal's tree theorem, and in particular the connection with the ordinal Ƭo. We also include a fairly extensive treatment of normal functions on the countable ordinals, and we give a glimpse of Veblen Hierarchies, some subsystems of second-order logic, slow-growing and fast-growing hierarchies including Girard's result, and Goodstein sequences. The central theme of this paper is a powerful theorem due to Kruskal, the "tree theorem", as well as a "finite miniaturization" of Kruskal's theorem due to Harvey Friedman. These versions of Kruskal's theorem are remarkable from a proof-theoretic point of view because they are not provable in relatively strong logical systems. They are examples of so-called "natural independence phenomena", which are considered by more logicians as more natural than the mathematical incompleteness results first discovered by Gödel. Kruskal's tree theorem also plays a fundamental role in computer science, because it is one of the main tools for showing that certain orderings on trees are well founded. These orderings play a crucial role in proving the termination of systems of rewrite rules and the correctness of Knuth-Bandix completion procedures. There is also a close connection between a certain infinite countable ordinal called Ƭoand Kruskal's theorem. Previous definitions of the function involved in this connection are known to be incorrect, in that, the function is not monotonic. We offer a repaired definition of this function, and explore briefly the consequences of its existence.Publication Constructive Logics Part I: A Tutorial on Proof Systems and Typed Lambda-Calculi(1991-10-01) Gallier, Jean HThe purpose of this paper is to give an exposition of material dealing with constructive logic, typed λ-calculi, and linear logic. The emergence in the past ten years of a coherent field of research often named "logic and computation" has had two major (and related) effects: firstly, it has rocked vigorously the world of mathematical logic; secondly, it has created a new computer science discipline, which spans from what is traditionally called theory of computation, to programming language design. Remarkably, this new body of work relies heavily on some "old" concepts found in mathematical logic, like natural deduction, sequent calculus, and λ-calculus (but often viewed in a different light), and also on some newer concepts. Thus, it may be quite a challenge to become initiated to this new body of work (but the situation is improving, there are now some excellent texts on this subject matter). This paper attempts to provide a coherent and hopefully "gentle" initiation to this new body of work. We have attempted to cover the basic material on natural deduction, sequent calculus, and typed λ-calculus, but also to provide an introduction to Girard's linear logic, one of the most exciting developments in logic these past five years. The first part of these notes gives an exposition of background material (with the exception of the Girard-translation of classical logic into intuitionistic logic, which is new). The second part is devoted to linear logic and proof nets.Publication Complete Sets of Transformations for General E-Unification(1989-02-01) Gallier, Jean H; Snyder, WayneThis paper is concerned with E-unification in arbitrary equational theories. We extend the method of transformations on systems of terms, developed by Martelli-Montanari for standard unification, to E-unification by giving two sets of transformations, BT and T, which are proved to be sound and complete in the sense that a complete set of E-unifiers for any equational theory E can be enumerated by either of these sets. The set T is an improvement of BT, in that many E-unifiers produced by BT will be weeded out by T. In addition, we show that a generalization of surreduction (also called narrowing) combined with the computation of critical pairs is complete. A new representation of equational proofs as certain kinds of trees is used to prove the completeness of the set BT in a rather direct fashion that parallels the completeness of the transformations in the case of (standard) unification. The completeness of T and the generalization of surreduction is proved by a method inspired by the concept of unfailing completion, using an abstract (and simpler) notion of the completion of a set of equations.Publication Notes on RSA(2010-05-01) Gallier, Jean HPublication On Girard's "Candidats de Reductibilité"(1989-11-01) Gallier, Jean HWe attempt to elucidate the conditions required on Girard's candidates of reducibility (in French, "candidats de reductibilité ") in order to establish certain properties of various typed lambda calculi, such as strong normalization and Church-Rosser property. We present two generalizations of the candidates of reducibility, an untyped version in the line of Tait and Mitchell, and a typed version which is an adaptation of Girard's original method. As an application of this general result, we give two proofs of strong normalization for the second-order polymorphic lambda calculus under βη-reduction (and thus under β-reduction). We present two sets of conditions for the typed version of the candidates. The first set consists of conditions similar to those used by Stenlund (basically the typed version of Tait's conditions), and the second set consists of Girard's original conditions. We also compare these conditions, and prove that Girard's conditions are stronger than Tait's conditions. We give a new proof of the Church-Rosser theorem for both β-reduction and βη-reduction, using the modified version of Girard's method. We also compare various proofs that have appeared in the literature (see section 11). We conclude by sketching the extension of the above results to Girard's higher-order polymorphic calculus Fω, and in appendix 1, to Fω with product types.Publication A Proof of Strong Normalization for the Theory of Constructions Using a Kripke-Like Interpretation(1990-07-01) Coquand, Thierry; Gallier, Jean HWe give a proof that all terms that type-check in the theory of contructions are strongly normalizing (under ß-reduction). The main novelty of this proof is that it uses a "Kripke-like" interpretation of the types and kinds, and that it does not use infinite contexts. We explore some consequences of strong normalization, consistency and decidability of typechecking. We also show that our proof yields another proof of strong normalization for LF (under ß-reduction), using the reducibility method.Publication Kripke Models and the (In)equational Logic of the Second-Order Lambda-Calculus(1995-09-01) Gallier, Jean HWe define a new class of Kripke structures for the second-order λ-calculus, and investigate the soundness and completeness of some proof systems for proving inequalities (rewrite rules) as well as equations. The Kripke structures under consideration are equipped with preorders that correspond to an abstract form of reduction, and they are not necessarily extensional. A novelty of our approach is that we define these structures directly as functors A:W → Preor equipped with certain natural transformations corresponding to application and abstraction (where W is a preorder, the set of worlds, and Preor is the category of preorders). We make use of an explicit construction of the exponential of functors in the Cartesian-closed category PreorW, and we also define a kind of exponential ∏ Φ (As) sЄТ to take care of type abstraction. However, we strive for simplicity, and we only use very elementary categorical concepts. Consequently, we believe that the models described in this paper are more palatable than abstract categorical models which require much more sophisticated machinery,(and are not models of rewrite rules anyway). We obtain soundness and completeness theorems that generalize some results of Mitchell and Moggi to the second-order λ-calculus, and to sets of inequalities (rewrite rules).Publication Structure From Motion With Directional Correspondence for Visual Odometry(2011-01-01) Naroditsky, Oleg; Zhou, Xun S.; Gallier, Jean H; Roumeliotis, Stergios I.; Daniilidis, KostasThis report presents two efficient solutions to the two-view, relative pose problem from three image point correspondences and one common reference direction. This three-plus-one problem can be used either as a substitute for the classic five-point algorithm using a vanishing point for the reference direction, or to make use of an inertial measurement unit commonly available on robots and mobile devices, where the gravity vector becomes the reference direction. We provide a simple closed-form solution and a solution based on techniques from algebraic geometry and investigate numerical and computational advantages of each approach. In a set of real experiments, we demonstrate the power of our approach by comparing it to the five-point method in a hypothesize-and-test visual odometry setting.Publication Logarithms and Square Roots of Real Matrices(2008-05-02) Gallier, Jean HThe need for computing logarithms or square roots of real matrices arises in a number of applied problems. A significant class of problems comes from medical imaging. One of these problems is to interpolate and to perform statistics on data represented by certain kinds of matrices (such as symmetric positive definite matrices in DTI). Another important and difficult problem is the registration of medical images. For both of these problems, the ability to compute logarithms of real matrices turns out to be crucial. However, not all real matrices have a real logarithm and thus, it is important to have sufficient conditions for the existence (and possibly the uniqueness) of a real logarithm for a real matrix. Such conditions (involving the eigenvalues of a matrix) are known, both for the logarithm and the square root. As far as I know, with the exception of Higham's recent book [18], proofs of the results involving these conditions are scattered in the literature and it is not easy to locate them. Moreover, Higham's excellent book assumes a certain level of background in linear algebra that readers interested in applications to medical imaging may not possess so we feel that a more elementary presentation might be a valuable supplement to Higham [18]. In this paper, I present a unified exposition of these results, including a proof of the existence of the Real Jordan Form, and give more direct proofs of some of these results using the Real Jordan Form.