[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
On 4 February 2017 at 13:32, Gabriel Scherer <[email protected]> wrote: > 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. Gabriel, thanks for the answer and fair point! Another approach is a suitable form of hereditary substitution—I recently learned from Mietek Bak & others it can do the job (amazingly to me), where match expressions are pushed out. I don't master the relation with the techniques you mentioned, but I do understand the appropriate syntax of normal forms. A definition of the appropriate syntax is here, for those familiar with Agda: https://github.com/mietek/hilbert-gentzen/blob/master/IPC/Syntax/GentzenSpinalNormalForm.agda (the rest of the repo also contains the normalization procedure). * *Another version is at https://github.com/gallais/potpourri/blob/master/agda/papers/hs99/STLCSum.agda, with a pointer to Short Proofs of Normalization by Joachimski & Matthes (1999). > On Sat, Feb 4, 2017 at 3:17 AM, Paolo Giarrusso <[email protected]> wrote: >> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] >> >> On Thursday, 2 February 2017, Paul B Levy <[email protected]> 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/>* -- Paolo G. Giarrusso - Ph.D. Student, Tübingen University http://ps.informatik.uni-tuebingen.de/team/giarrusso/
