Abstracts
Here are the abstracts of most of the works you can find referenced in my publications page, where you will find the pointers to the online available documents.
Provable isomorphisms of types: from Lambda Calculus to Information Retrieval and Language Design.
This book (see here for a more detailed overview) is devoted to the study of the notion of type-isomorphisms in functional languages, both from a theoretical and a practical point of view.
Based on my PhD dissertation, it has been extensively revised, updated and provided with a completely new introduction to the topic, that makes it accessible to a wide spectrum of readers. It tries hard to provide a complete reference and discussion of all research done in this area, from the definition of confluent rewriting systems for typed lambda calculi equipped with various extensionality rules, to the characterization of isomorphisms of types in different typed calculi, to the applications to extensions of ML-style type-inference algorithms and the design of library search tools based on types (you can test a sample implementation right now: english or french).
Provable isomorphisms of types
A constructive characterization is given of the isomorphisms which must hold in all models of the typed lambda calculus with surjective pairing. By the close relation between closed Cartesian categories and models of these calculi, we also produce a characterization of those isomorphisms which hold in all CCC's. By the correspondence between these calculi and proofs in intuitionistic positive propositional logic, we thus provide a characterization of equivalent formulae of this logic, where the definition of equivalence of terms depends on having ``invertible'' proofs between the two terms. Rittri (1989), on types as search keys in program libraries, provides an interesting example of use of these characterizations.
Constuctively Equivalent Propositions and Isomorphisms of Objects (or Terms as Natural Transformations)
In these notes, we sketch a recent application of the typed and type-free l-calculus to Proof Theory and Category Theory. The proof is fairly incomplete and we refer the reader interested in the lengthy technical details to Bruce & DiCosmo & Longo [1990]. Our main purpose here is to hint a logical framework for the result therein, in a rather preliminary and problematic form.
The questions we raise here are the following: when two propositions can be considered as truly equivalent? Or, when is it that types may be viewed at as isomorphic under all circumstances?
In proof-theoretic terms this may be understood as in definition 0.1 below, on the grounds of the ``types-as-propositions'' analogy between the typed l-calculus and intuitionistic propositional logic (bf IPL).
Type isomorphisms in a type assignment framework
This is a conference extended abstract of the following journal paper.
Deciding Type isomorphisms in a type assignment framework
We exhibit confluent and effectively weakly normalizing (thus decidable) rewriting systems for the full equational theory underlying cartesian closed categories, and for polymorphic extensions of it. The l -calculus extended with surjective pairing has been well-studied in the last two decades. It is not confluent in the untyped case, and confluent in the typed case. But to the best of our knowledge the present work is the first treatment of the lambda calculus extended with surjective pairing and terminal object via a confluent rewriting system, and is the first solution to the decidability problem of the full equational theory of Cartesian Closed Categories extended with polymorphic types. Our approach yields conservativity results as well. In separate papers we apply our results to the study of provable type isomorphisms, and to the decidability of equality in a typed l -calculus with subtyping.
Second order Isomorphic Types. A proof theoretic study on second order lambda-calculus with surjective pairing and terminal object
We investigate invertible terms and isomorphic types in the second order lambda calculus extended with surjective pairs and terminal (or Unit) type. These two topics are closely related: on one side, the study of invertibility is a necessary tool for the characterization of isomorphic types; on the other hand, we need the notion of isomorphic types to study the typed invertible terms. The result of our investigation is twofold: we give a constructive characterization of the invertible terms, extending previous work by Dezani and Bruce-Longo citeDezani,BruceLongo85, and a decidable equational theory of the isomorphisms of types which hold in all models of the calculus, which is a conservative extension to the second order case of the results previously achieved for the case of first order typed calculi. Via the Curry-Howard correspondence, this work also provides a decision procedure for strong equivalence of formulae in second order intuitionistic positive propositional logic, that is suitable to search equivalent proofs in automated deduction systems.
Keywords: Type Isomorphisms, Invertibility, System F, Polymorphism, Surjective Pairing, Terminal Object, Equational Theories, l -Calculus, Proof Search.
Type isomorphisms of modules
We study a formal notion of type isomorphism for module signatures, which naturally extends the notion of isomorphism for types in functional languages. Isomorphisms between module types surprisingly have nontrivial interactions with the theory of isomorphisms of the base language to which the module system is added. We investigate the power of this notion in equating module signatures, and we study its decidability. This work does not impose any limitative assumption on the module system as we handle type declarations in signatures, type sharing and higher order modules.
A confluent reduction system for the lambda-calculus with surjective pairing and terminal object
This is a conference extended abstract of the following journal paper.
A confluent reduction system for the lambda-calculus with surjective pairing and terminal object
We exhibit confluent and effectively weakly normalizing (thus decidable) rewriting systems for the full equational theory underlying cartesian closed categories, and for polymorphic extensions of it. The l -calculus extended with surjective pairing has been well-studied in the last two decades. It is not confluent in the untyped case, and confluent in the typed case. But to the best of our knowledge the present work is the first treatment of the lambda calculus extended with surjective pairing and terminal object via a confluent rewriting system, and is the first solution to the decidability problem of the full equational theory of Cartesian Closed Categories extended with it polymorphic types. Our approach yields conservativity results as well. In separate papers we apply our results to the study of provable type isomorphisms, and to the decidability of equality in a typed l -calculus with subtyping.
A confluent reduction for the extensional typed lambda-calculus with pairs, sums, recursion and terminal object
This is a conference extended abstract of the following journal paper.
Simulating Expansions without Expansions
We add extensional equalities for the functional and product types to the typed l -calculus with not only products and terminal object, but also sums condinitialand initial object and bounded recursion (a version of recursion that does not allow recursive calls of infinite length). We provide a confluent and strongly normalizing (thus decidable) rewriting system for the calculus, that stays confluent when allowing unbounded recursion. For that, we turn the extensional equalities into expansion rules, and not into contractions as is done traditionally. We first prove the calculus to be weakly confluent, which is a more complex and interesting task than for the usual l -calculus. Then we provide an effective mechanism to simulate expansions without expansion rules, so that the strong normalization of the calculus can be derived from that of the underlying, traditional, non extensional system. These results give us the confluence of the full calculus, but we also show how to deduce confluence directly form our simulation technique, without the weak confluence property.
Combining first order algebraic rewriting systems, recursion and extensional lambda calculi
It is well known that confluence and strong normalization are preserved when combining left-linear algebraic rewriting systems with the simply typed lambda calculus. It is equally well known that confluence fails when adding either the usual extensional rule for eta, or recursion together with the usual contraction rule for surjective pairing.
We show that confluence and normalization are modular properties for the combination of left-linear algebraic rewriting systems with typed lambda calculi enriched with expansive extensional rules for eta and surjective pairing. For that, we use a translation technique allowing to simulate expansions without expansion rules. We also show that confluence is maintained in a modular way when adding fixpoints. This result is also obtained by a simple translation technique allowing to simulate bounded recursion with beta reduction.
Expanding Extensional Polymorphism
We prove the confluence and strong normalization properties for second order lambda calculus equipped with an expansive version of eta-reduction. Our proof technique, based on a simple abstract lemma and a labelled l-calculus, can also be successfully used to simplify the proofs of confluence and normalization for first order calculi, and can be applied to various extensions of the calculus presented here.
An extensional operational and axiomatic semantics for type-inference with recursion and algebraic data types
In this paper, we provide an operational semantics of core-ML with recursion and algebraic data types which agrees precisely with the usual axiomatic semantics in the presence of extensionality axioms/. This result has been missed for a long time due to the traditional use of contractive reduction rules for familiar extensional equalities like eta and Surjective Pairing: these rules do not interact nicely with the implicit polimorphic typing discipline that is the base of many strongly typed functional programming languages, as even such a fundamental property as Subject Reduction does not hold in their presence.
We use here the more satisfactory approach to extensionality that uses expansion rules, and then we can give a simple translation of (extensional) Core-ML into (extensional) System F that preserves types and allows a proper simulation of the reductions of Core-ML. This provides an operational notion of reduction for Core-ML that takes into account the extensional equalities on the arrow and the product types.
But this is not all: we also show how we can add, using some simple but powerful lemmas from the theory of rewriting, algebraic data types and recursion preserving confluence (hence determinacy) of the system under very liberal conditions.
To the author's best knowledge, this is the first satisfactory treatment of a polymorphic type inference systems in the presence of extensionality.
Keywords: type-inference, language design, rewriting, ML, semantics, algebraic data types
Rewriting with polymorphic extensional lambda-calculus
We provide a confluent and strongly normalizing rewriting system, based on expansion rules, for the extensional/ second order typed lambda calculus with product and unit types: this system siunitis the second order extension of the lambda calculus associated to the Cartesian Closed Categories, and corresponds to the Intuitionistic Positive Calculus with implication, conjunction, quantification over proposition and the constant True. This result is an important step towards a new theory of reduction based on expansion rules, and gives a natural interpretation to the notion of second order eta-long normal forms used in higher order resolution and unification, that are here just the normal forms of our reduction system.
On the Power of Simple Diagrams
In this paper we focus on a set of abstract lemmas that are easy to apply and turn out to be quite valuable in order to establish confluence and/or normalization modularly, especially when adding rewriting rules for extensional equalities to various calculi. We show the usefulness of the lemmas by applying them to various systems, ranging from simply typed lambda calculus to higher order lambda calculi, for which we can establish systematically confluence and/or normalization (or decidability of equality) in a simple way. Many result are new, but we also discuss systems for which our technique allows to provide a much simpler proof than what can be found in the literature.