[Prev][Next][Index][Thread]

confluence, conservativity and interpolation for typed lambda calculi

Date: Mon, 29 Jun 92 10:42:18 -0700

I am interested in confluence, conservativity and interpolation for
simply-typed (and other) lambda calculi, primarily those obtained by
adding one or more of the types

  empty, unit (terminal object), + and x (product)

to pure typed lambda calculus with function types. I would be happy to
collect results (published or unpublished) and summarize to this list. To
avoid too much duplication, I'll summarize what I am currently aware of.
It is clear that all systems are strongly normalizing (by interpretation
in System F, for example, or direct logical relation argument).

Confluence:

   With -> and (optionally) x, confluence is easily established and
well-known.  I am not sure about + off hand, but I assume that the same
methods will do here.  Confluence fails with unit, with ways to work
around this described in Lambek and Scott and in a recent ICALP paper by
Curien and DiCosmo. It seems likely that confluence with an empty type
(initial object) would fail for the same reason.  Has anyone studied this
at all?

Conservativity:

    Confluence provides a simple proof of conservativity for deductions
>from empty hypotheses. For example, confluence for -> and x implies that
an equation using only -> types is provable in this calculus iff it is
provable in the lambda calculus with only -> types.

    Question: what about the other cases? Either syntactic or semantic
proofs would be of interest. As far as semantic proofs go, failure of
completeness for Henkin models is relevant; semantic proofs will have to
use categorical models, perhaps Kripke models (there is some discussion of
this in my Kripke models paper with Moggi).

    The general form of conservativity (for logics without a deduction
theorem) is that if ${\cal L}_1$, contains ${\cal L}_2$, ${\cal F}$ is a
set of formulas in the language of ${\cal L}_2$ and $F$ is a single such
formula, then ${\cal L}_1$ is \idef{conservative over} ${\cal L}_2$ if
${\cal F} \ts F$ in the proof system of ${\cal L}_2$ iff ${\cal F} \ts F$
in the proof system of ${\cal L}_1$.  Jacopini's correspondence between
reduction and proofs from equational hypotheses is relevant here, but I
have not investigated how far this will go.

Interpolation:

    This generally fails for equational logics, but can be restored using
existentially quantified function symbols. Does interpolation hold in any
interesting cases here?


Thanks, John Mitchell