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

[Gabriel Scherer]

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