[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Dear Paul,
Since there was (several replies but) no answer to your question (asking
for a reference), this may be of interest to the list.
Our coherence theorem for Call-by-Push-Value from the paper in
collaboration with M. Fiore and P.-L. Curien [1] extends to Curry's
style with the help of a concise strong normalisation proof adapted from
[2,3]. In this setting strong normalisation is essentially the
completeness of focusing, so enough to reach the useful normal forms.
This is written in the following short note:
<http://guillaume.munch.name/files/curry.pdf> (section 6.5). It holds
for any CBPV model (for any sensible interpretation including
call-by-name and call-by-value) though you only asked for the case of
BiCCCs (where the various sensible interpretations coincide).
In Curry's style, it turns out, one has to be clear about how
conversions are defined, since the notion of type-preserving conversion
between terms does not coincide with that of conversion between
derivations. For instance if x does not appear in M then (λx.M) * →
(λx.M) N preserves the typing whatever the type of N, but this does not
correspond to a conversion between derivations if the type of x must
change. A similar example involves the empty type instead of the unit
type. But, using strong normalisation again one can prove that their
equivalence closures are the same.
This note substantiates Gabriel's and Paolo's good insights.
Best regards,
Guillaume
[1] P.-L. Curien, M. Fiore, and G. MM, “A Theory of Effects and
Resources: Adjunction Models and Polarised Calculi”, in Proc. POPL, 2016.
[2] G. MM, “Focalisation and Classical Realisability”, in Proc. CSL, 2009.
[3] G. MM, “λ-calcul, machines et orthogonalité”, manuscript, June 2012.
Le 02/02/2017 à 20:11, Paul B Levy a écrit :
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Dear all,
Take simply typed lambda-calculus with ->, x, +, 0, 1 types.
Specifically the Curry-style formulation with no type annotations
whatsoever, neither on lambda nor on inl nor on anything else.
Here are the two "coherence" statements I'm interested in.
(1) Any two derivations of Gamma |- M : A have the same denotation.
(2) More generally, for any bicartesian closed category C, any two
derivations of Gamma |- M : A have the same denotation in C.
I can see roughly how to prove these, but before working it out would
like to ask: do these results appear in the literature? My impression
is that people have studied semantic coherence for fancy languages (e.g.
with subtypes and dependent types), so surely the above statements, or
at least (1), are a simple case of some result in the literature.
Best regards,
Paul
--
Guillaume Munch-Maccagnoni
Researcher at Inria Bretagne Atlantique
Team Gallinette
