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.
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).
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.
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).
This is a conference extended abstract of the following journal paper.
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.
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.
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.
This is a conference extended abstract of the following journal paper.
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.
This is a conference extended abstract of the following journal paper.
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.
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.
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.
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
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.
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.
Useful Pointers
ENS
LIENS
Lambda Calcul Typé
Roberto Di Cosmo
LIENS
École Normale Supérieure
45, rue d'Ulm
75005 PARIS
France
E-Mail:roberto@dicosmo.org