Re: [TYPES] semantic coherence for simply typed lambda-calculus

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Hello Paul,

I ran into the problem you describe when writing up my thesis, see

   http://www.cse.chalmers.se/~abela/diss.pdf

The interesting part starts on page 34 in paragraph

   The remainder of this section is devoted to the proof that two
well-kindedness derivations for the same constructors do not
yield different semantics. More precisely, assume two derivations
D :: ∆ ⊢ F : κ and D' :: ∆' ⊢ F : κ and two valuations θ ∈ [[∆]]
and θ' ∈ [[∆']]. If θ(X)= θ'(X) for all X ∈ FV(F), then
[[D]]θ =[[D']]θ'. This result is not completely trivial,
i. e., cannot be proven directly by induction on the derivations,
since in derivations for non-β-normal F, some kinds in the
middle of derivations can be canceled out. For example, consider
F =(λX.Y)G. Some kind κ for X (and G) is mentioned in the
middle of a well-kindness derivation of F, but it can differ
from derivation to derivation. Still, the semantics of F in
environment θ should be just θ(Y), independent of kind κ.


The solution is the same.  Start with normal forms and then show that 
the denotation is preserved by beta-expansion.

The idea for this proof was from my supervisor Martin Hofmann.

Best,
Andreas

On 04.02.2017 15:29, Paolo Giarrusso wrote:
> [ 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/>*
>
>
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

[email protected]
http://www.cse.chalmers.se/~abela/