[TYPES] semantic coherence for simply typed lambda-calculus

[Guillaume Munch-Maccagnoni]

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