[TYPES] semantic coherence for simply typed lambda-calculus

[Paolo Giarrusso]

On 4 February 2017 at 13:32, Gabriel Scherer <gabriel.scherer at gmail.com> 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 <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/>*



-- 
Paolo G. Giarrusso - Ph.D. Student, Tübingen University
http://ps.informatik.uni-tuebingen.de/team/giarrusso/