[Prev][Next][Index][Thread]
Coherence of Subsumption
Date: 26 Jul 1989 1639-PDT (Wednesday)
Here is the abstract and introduction of a paper by Pierre-Louis Curien
(LIENS, curien@frulm63.bitnet) and Giorgio Ghelli (Pisa,
ghelli@di.unipi.it), which will appear as a technical report in both
author's places. If you are interested to see the full paper, address
requests to either author. Notice that PL Curien, who was visiting DEC SRC
since January 1989 will be back in Paris from the beginning of august.
Coherence of Subsumption
Abstract
Subsumption used in subtyping breaks the term-as-proofs paradigm.
Semantics most naturally are associated with proofs. Thus a problem of
coherence arises: different typing proofs of the same term must have
related meanings. We propose a proof-theoretical, rewriting approach to
this problem. We focus on a second order lambda calculus with bounded
quantification, which is rich enough to make the problem interesting. We
define a normalizing rewrite system on the proofs, in which different
proofs of the same typing judgement are transformed in a unique normal
proof, and in which normal proofs of judgements assigning different types
to the same term are strongly related. This rewriting system is not
defined on the proofs themselves but on the terms of an auxiliary type
system, in which the terms are enriched to carry a complete information
about their typing proof . This technique gives also a simple proof of the
existence of a minimum type for each term. From an analysis of the proofs
in normal form we obtain a deterministic type-checking algorithm, which is
sound and complete by construction.
Introduction
In many typed calculi only well-typed terms can be assigned a reasonable
semantics. Thus often the semantics of a term is defined not by induction
on its structure, but by induction on the structure of a typing proof.
Since in such type systems type rules are often non deterministic, a
single term can be proved well-typed in many different ways. In this
context some problems arise:
Semantic coherence: the problem of proving that different semantic
interpretations of the same term, corresponding to different typing
proofs, are equal or at least equivalent is some sense.
Most general typing: the problem of proving that a most general type, in
some sense, can be assigned to each well typed term. In a system with
structural subtyping, most general means minimum with respect to the
subtyping relation.
Soundness and completeness of type-checking: the problem of finding a
deterministic type checking algorithm which is sound and complete with
respect to the typing rules. Determinism, soundness and completeness
ensure that the algorithm is a semi-decision procedure.
Observe that these three problems seem, or at least have been often
considered unrelated. We approach them in a unified way, and exploit the
approach in the context of the language F<=, a second order
lambda-calculus with bounded quantification. It is the core of the
language Quest of L. Cardelli [Cardelli 89], and mostly identical to the
language Fun of [Cardelli, Wegner 88] (Fun has records and has a more
restrictive for all introduction rule). We refer to these papers for
motivation about structural subtyping discipline. Here is a brief outline
of the already existing solutions to these problems we are aware of:
Semantic coherence for Fun has been solved in [Bruce, Longo 88] : K. Bruce
and G. Longo define an auxiliary language Minimal Bounded Fun, and
interpret Fun via this language. They quote that the problem of the
existence of a minimum type has been solved by R. Amadio, and use this
result.
In [Breazu, Coquand, Gunter, Scedrov 89] coherence is carefully proved for
a special syntactic interpretation of subtyping in F.
A deterministic algorithm to type-check Fun was since long known by
Cardelli [personal communication]. A lemma proving that this algorithm is
sound and complete if it always terminates was known by V. Breazu
[personal communication].
In this paper we solve all the three problems together. We give sufficient
conditions which ensure at the same time coherence and minimal typing, and
which are independent from any specific model. Our result of soundness and
completeness is independent from termination. In a companion paper [Ghelli
89] one of the authors shows the termination of the algorithm, thus
turning the semi-decision procedure into a decision procedure: this solves
the long standing problem of the decidability of type-checking of Fun.
We define a normalizing rewriting system on the typing proofs, which
reduces all the proofs of a given typing judgement to a single canonical
proof. This property is the key to solve the semantic coherence problem,
as it ensures that the satisfaction of the equations underlying this
rewriting system guarantees that different proofs of the same judgement
receive the same meaning. The rewrite system is not defined directly on
proofs but on the terms of a more explicit system, which is defined by
enriching the terms of the original system to keep a complete trace of
typing proofs.This device allows an elegant management of proof
simplification and sheds some light on the relation between type systems
in which the subtype relation allows to give more than one type to each
term, and systems in which the subtype relation induces a coercion
function from a subtype to a supertype. An explicit system of this kind
was already present in [Bruce, Longo 88] (full version), but was not
pushed there to the point where an explicit term completely codifies a
proof (we shall be more specific below).
Here is a brief outline of the organization of the paper. In section 2 the
type system of F<= is defined together with our enriched type system. In
section 3 we abstractly state conditions on a proof reduction system which
are sufficient to allow the proof of coherence and type minimality
properties. In section 4 the proof rewriting system is defined and some of
its properties are studied. In section 5 the desired properties are
proved. In section 6 we derive a type-checking algorithm from the analysis
of canonical proofs. In section 7 we show how the known models fit in our
framework, i.e. validate the equations underlying the rewriting system
defined in section 4. In section 8 some conclusions and directions for
future work are drawn.