[ 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/
