[TYPES] semantic coherence for simply typed lambda-calculus

[Gabriel Scherer]

Paolo, I had the exact same argument in mind, but I think that
beta-normal forms don't cut it when you have types of both
polarities. Consider for example the β-normal form

  (match x with
    | inj₁ () -> λy.t
    | inj₂ () -> λy.t
  ) (u)

This does not satisfy the subformula property, as the principal type
of the "blocked" redex ((λy.t) u) is arbitrary.

You need your notion of reduction to have enough commuting conversions
to recover the subformula property. A sequent-calculus presentation
gives this for free (there are ugly-but-simple sequent terms for this
calculus in my thesis manuscript, Section 4.1.4,
http://www.ccs.neu.edu/home/gasche/phd_thesis/scherer-thesis.pdf;
a proper abstract machine calculus would be more elegant), or looking
at cut-free focused term also does the job – completeness of focusing
then embeds the suitable normalization procedure.

On Sat, Feb 4, 2017 at 3:17 AM, Paolo Giarrusso <p.giarrusso at gmail.com> wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> On Thursday, 2 February 2017, Paul B Levy <P.B.Levy at cs.bham.ac.uk> wrote:
>
>> [ 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.
>>
>
> To double-check: Gamma, M and A are all fixed, right?
>
> It seems one can remove the ambiguity in typing by normalizing M first and
> then relying on the subformula property. Here's a potential proof
> sketch—I'd love to know if this approach makes sense. (And I'm not even
> sure if all the steps I'm relying on have actually been proven).
>
> Use untyped normalization on M to obtain M'. Since M is typable,
> normalization terminates—even untyped normalization (right?), since types
> don't affect evaluation.
> By preservation, M' should have the same type (even though it's untyped
> evaluation, right?). By the subformula property of normalization, all types
> in the derivation of M' are "subformulas" of A so there is no ambiguity in
> its derivation of Gamma |- M' : A.* Let's call that derivation D.
>
> Since normalization preserves the denotation, if we have two derivations D1
> and D2 of Gamma |- M : A, we have that
> [[ D1 ]] = [[ D ]] = [[ D2 ]]
> hence we have (1) (and I expect (2) as well).
>
> * I think this is not so trivial; however, this step is confirmed by the
> theory of bidirectional typechecking. Quoting Dunfield and Krishnaswami
> (2013):
>
>> As shown by Watkins et al. (2004), bidirectional typechecking can be
> understood in terms of the normalization of intuitionistic type theory, in
> which normal forms correspond to the checking mode of bidirectional
> typechecking, and neutral (or atomic) terms correspond to the synthesis
> mode. This enables a proof of the elegant property that type annotations
> are only necessary at reducible expressions, and that normal forms need no
> annotations at all.
>
> Dunfield and Krishnaswami (2013). Complete and Easy Bidirectional
> Typechecking for Higher-Rank Polymorphism, ICFP 2013, ACM.
>
>
> --
> Paolo G. Giarrusso - Ph.D. Student, Tübingen University
> *http://ps.informatik.uni-tuebingen.de/team/giarrusso/
> <http://ps.informatik.uni-tuebingen.de/team/giarrusso/>*