[TYPES] correctness of closure conversion for untyped lambda calculus wrt. denotational semantics

[Jeremy Siek]

Hi Gabriel,

Yes, one needs to relate the source and target denotations, and the
relation that Adam uses
is quite simple and natural:

n1 ≃_N n2    :=     n1 = n1
f1 ≃_{A \to N} f2   :=   forall x1 : P[A], forall x2 : C[A], x1 ≃_A x2
implies f1 x1 ≃_N f2 x2

(PLDI 2007, section 9.1, page 63)

I'm not seeing the definition that you listed... is that from another paper
or the mechanization?

Cheers,
Jeremy



On Tue, Oct 2, 2018 at 6:35 AM Gabriel Scherer <gabriel.scherer at gmail.com>
wrote:

> I think that the failure of full-abstraction limits the amount of
> "denotational semantics" you can use in a proof, in the following sense:
> natural/good denotational semantics tend to be fully abstract themselves,
> in the sense that observationally distinguishable terms have distinct
> semantics. For such a denotational semantics [[.]] on the target language,
> you cannot hope to prove a natural correctness result of the form
>
>    [[ closure-convert(t] ]] = from-lc([[ t ]])
>
> where from-lc embeds the denotational semantic of the source term into the
> semantic space of the target calculus.
>
> I went back to look at Adam's article on STLC. His correctness statement
> is weaker, it relies on a heterogeneous logical relation between the source
> and target denotational semantics, with a definition of the form
>
>     [[ lam x. t ]] ~ closure-app-env[[ (env, lam ys x. u) ]] : A -> B
>     := forall (v ~ v' \in [[A]]), [[ lam x. t]] v ~ closure-app-env[[
> (env, lam x. u) ]] v'
>
> where closure-app-env computes the set-theoretic semantics of
> partially-applying the closure environment.
>
> This does not imply full-abstraction, as the denotational semantics [[
> (env, lam ys x. u) ]] in the target may contain much more behaviors than
> closure-app-env[[ (env, lam ys x. u) ]] does.
>
> On Tue, Oct 2, 2018 at 2:42 AM Jeremy Siek <jeremy.siek at gmail.com> wrote:
>
>> Hi Gabriel, William,
>>
>> Yes indeed, it was just whole program correctness that I had in mind, and
>> not fully abstract compilation.
>>
>> -Jeremy
>>
>> > On Oct 1, 2018, at 5:28 PM, William J. Bowman <wjb at williamjbowman.com>
>> wrote:
>> >
>> > Gabriel,
>> >
>> > It sounds like you're describing a failure of full abstraction.
>> > I think the compiler could still satsify "whole-program correctness",
>> i.e., the
>> > translated (whole) program denotes the same value as the original, even
>> without
>> > primitive closures.
>> >
>> > --
>> > William J. Bowman
>> >
>> >> On Mon, Oct 01, 2018 at 11:26:31PM +0200, Gabriel Scherer wrote:
>> >> [ The Types Forum,
>> http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>> >>
>> >> Dear Jeremy,
>> >>
>> >> In what sense would closure conversion be correct for the untyped
>> >> lambda-calculus? Writing in an untyped language allows me to use
>> pair/tuple
>> >> operations to access the closure environment, which was not previously
>> >> possible on the non-closure-converted calculus. If your untyped target
>> >> language (I think it should be made precise) contains a primitive
>> >> representation of closures (not just pairs), you can prevent
>> environment
>> >> extraction, but then that corresponds to your third bullet of a target
>> that
>> >> "supports (explicit) closure creation".
>> >>
>> >> Best
>> >>
>> >>> On Mon, Oct 1, 2018 at 11:11 PM Jeremy Siek <jeremy.siek at gmail.com>
>> wrote:
>> >>>
>> >>> [ The Types Forum,
>> http://lists.seas.upenn.edu/mailman/listinfo/types-list
>> >>> ]
>> >>>
>> >>> I’m interested in finding literature on proofs of correctness of
>> closure
>> >>> conversion
>> >>> applied to the untyped lambda calculus with respect to a denotational
>> >>> semantics.
>> >>> (Bonus for mechanized proofs.)
>> >>>
>> >>> I’ve found papers that are a near miss for what I’m looking for, such
>> as:
>> >>> * closure conversion proofs for the STLC (Chlipala PLDI 2007)
>> >>> * closure conversion proofs based on operational semantics
>> >>>   (Minamide, Morrisett, and Harper POPL 1996, and many more)
>> >>> * correctness proofs using denotational semantics for compilers that
>> >>>   don’t do closure conversion, but instead compile to a machine that
>> >>>   supports closure creation (the VLISP project and many more).
>> >>>
>> >>> Thanks in advance for pointers!
>> >>>
>> >>> Best regards,
>> >>> Jeremy
>> >>>
>> >>>
>>
>