[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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.sche...@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.s...@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 <w...@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.s...@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 >> >>> >> >>> >> >