PLDI16-reviews.txt

===========================================================================
                           PLDI '16 Review #254A
---------------------------------------------------------------------------
Paper #254: Constructive Galois Connections: Taming the Galois Connection
            Framework for Mechanized Metatheory
---------------------------------------------------------------------------

                 Reviewer expertise: Z. Some familiarity
                      Overall merit: C. Weak paper, though I will not fight
                                        strongly against it

                         ===== Paper summary =====

This paper presents a new framework for abstract interpretation based on "constructive Galois connections", which uses monadic functions for abstraction and concretization to isolate non-constructive specifications from algorithms. This supports integration of the framework into a constructive mechanization framework without sacrificing any of the generality afforded by classical abstract interpretation. The authors demonstrate this theory by mechanizing two published abstract interpretation proofs. The first is a verified abstract interpreter which uses Cousot's preferred "calculational" style, and the second is a hybrid static/dynamic semantics for gradually-typed languages. The paper concludes with a discussion that relates constructive Galois connections to classical ones, via "Kleisi Galois connections".

                      ===== Comments for author =====

Strengths:

- This work gives fresh results for a long-running sequence of prior questions and results.

- The technical insights and developments seem interesting and relevant to the theory in this area.

- The paper is very polished, organized, and thoughtfully-written.

Weaknesses:

- The paper does not attempt to motivate its contributions on problems that are of clear practical importance.

- The case studies are given "as-is", and it is not clear exactly what benefit the approach brings to them.

Discussion:

This is a well-written paper containing a number of theoretical insights and results that seem to address some long-standing questions from the abstract interpretation literature. The introduction does a fine job setting the historical context and explaining what the paper sets out to accomplish, as well as the basics of the approach. The work also seems solid and meticulous. However, as written it is unclear how these contributions extend beyond theoretical significance, and thus that this work will have substantial impact on, or win the attention of, much of the PLDI community.

The core of the problem with the paper as it is currently written lies in the case studies. These need to demonstrate the value of the contributions in addressing a real problem---i.e., one which is likely to resonate with the intended audience---significantly better than prior work. Both case studies seem to have potential; verified static analysis and gradual type systems are interesting topics with good practical significance. However, both of the case studies given are based heavily on prior work, and the paper does not effectively demonstrate that constructivity translates into useful results that move the state-of-the-art forward with respect to either application. Re-working the case studies to highlight these points would make the paper stronger from a practical perspective.

===========================================================================
                           PLDI '16 Review #254B
---------------------------------------------------------------------------
Paper #254: Constructive Galois Connections: Taming the Galois Connection
            Framework for Mechanized Metatheory
---------------------------------------------------------------------------

                 Reviewer expertise: Y. Knowledgeable
                      Overall merit: C. Weak paper, though I will not fight
                                        strongly against it

                         ===== Paper summary =====

The paper describes a simple way to prove soundness of static analyzers using
type theory and Galois connections.

To explain the problem the paper uses the following example. When
abstracting integers wrt. the sign, the abstraction function
\alpha Pow Z -> Z# maps a set of integers I into the sign as follows:
\alpha (I) = \bigsum_{i \in I} \sign (i)
where
\sign (i) = {NEG, if i < 0 | ZERO, if i = 0 | POS, if i > 0}
Here Z# contains the signs closed up under the obvious join,
and \bigsum iterates this join function.

The problem is that \bigsum in \alpha iterates over a potentially
infinite set, and hence \alpha isn't computable. One can't directly
define \alpha as above in a proof assistant based on constructive
logic.

There are tricks one can do to work around the problem. E.g., one
can define \alpha as a functional relation, rather than a function. But
these are considered unpleasant.
Instead, the authors propose dropping \alpha, and re-basing the
theory around the helper function \sign. Or, more precisely, basing the
theory on the general notion of "extraction functions" [23], of
which \sign is an example.

This leads to pleasantly effective proofs in at least two case
studies: the first is based on Cousot's example with the WHILE
language, and the second is about gradual types. To increase
credibility, the proofs of the case studies are formalized in Agda,
together with the requisite simple meta theory.

                      ===== Comments for author =====

Pros:
  1. Nice and simple idea
  2. Useful in many abstract domains since extraction is common, e.g., for pointer and shape analysis
Cons:
  1. The significance of the results for proving the correctness of
  complex abstract interpreters is not clear

In principle, the paper is a nice read, laying out its claim in
detail, and making seemingly deep connections with the theory of
monads via Kleisli categories (which, however, seems inessential for
understanding the broader idea).


But, when all is said and done, I couldn't escape the feeling that
this is a rather simple move, which ought to be very well-known and
unsurprising in the literature on Abstract Interpretation.


The connection to dependently typed programming perhaps increases
the curiosity factor of the paper, but does not seem important to
the general idea, beyond the initial motivation.


The idea that extraction functions drastically simplify the theory
of abstract interpretation is of course well known in the AI
community. Also, it cannot be used to justify abstractions of
non-powerset concrete domains. I suppose one could argue that most
concrete domains are powerset domains but perhaps you need to
justify other operations in AI such as semantic reductions.


There is Theorem 4 on page 10 of the paper, which relates
constructive Galois connections to Kleisli ones. But, the relation
requires the axiom of choice, and the later is not a theorem in all,
or even most, constructive logics. In Coq, for example, choice has
to be added as an axiom, which would put us back to square one
(i.e., we're adding axioms to the system, which, albeit not excluded
middle, will still conflict with extraction).

===========================================================================
                           PLDI '16 Review #254C
---------------------------------------------------------------------------
Paper #254: Constructive Galois Connections: Taming the Galois Connection
            Framework for Mechanized Metatheory
---------------------------------------------------------------------------

                 Reviewer expertise: Z. Some familiarity
                      Overall merit: C. Weak paper, though I will not fight
                                        strongly against it

                         ===== Paper summary =====

This paper proposes a modified mathematical approach for formalizing
abstract interpretation which differs from the traditional use of a
Galois connection in a way that is argued to allow for flexible
reasoning within constructive logic, in particular machine-checked
proof systems that also support extraction of certified programs. The
paper begins by presenting a standard example of integer sign analysis
for a while language, and observes four possible formulations of the
soundness condition, using differing combinations of abstraction and
concretization operators. But this abstraction operator is difficult
to represent constructively. The paper then presents two replacement
Galois connection definitions, both of which are introduced using the
powerset monad, and the second of which, the "constructive Galois
connection" simplifies the abstraction function to operate on values
instead of sets. The paper uses this new style of definition to redo
the while language example, showing that it allows for a style of
computational derivation of the interpreter which is well-regarded in
informal proofs but has not previously been formalized. In a second
case study the paper applies this new approach to a recent abstract
interpretation approach to gradual types, arguing that it leads to
simpler proofs. Finally the paper proves some general relationships
between the two new kinds of Galois connection and the original
one. The paper's approach is developed as a proof library in Agda.

                      ===== Comments for author =====

Key strengths and weaknesses:

+ Approach improves the match between calculational development and
constructive logic

+ In the paper's examples, results are obtained more elegantly

- Intuition behind the approach is not well conveyed

- Program extraction, important to motivation, is not demonstrated

Abstract interpretation has always been a mathematically-oriented
approach to static analysis, so it is natural to use it in conjunction
with machine-checked proof assistants. As the paper describes, there
have been several recent successes in this direction, but they are
less than completely satisfying from the standpoint of mathematical
elegance, because the desire to use proof assistants based on
constructive logic, which allow for a close mapping between proof
development and executable code, is incompatible with some of the
reasoning using functions over arbitrary sets that is used in
non-machine-checked abstract interpretation proofs. At least in the
excerpted parts of examples shown in the paper, the paper's new
"constructive Galois connection" definitions seems successful in
bridging this gap: it allows formalization in Agda, and the proofs
have a similar structure to classic ones.

As far as I can see, though, this is only a contribution to the proof
theory of abstract interpretation, and it's not clear how much use it
would see beyond constructive logic environments like some proof
assistants. The paper proves that its new formalism has only a subset
of the expressiveness of the traditional one, though by calling what
is left "noncomputational" it seems to be implicitly arguing that the
new formalism captures all that is important for abstract
interpretations that are implemented. The paper's case study
formalizing [15] argues that an \eta-based presentation is simpler
than the previous \alpha-based one, though this feels like a somewhat
subjective judgment to trust the present paper's authors on. The paper
argues that the \eta approach reduces the need for set-theoretic
reasoning, but such reasoning does not seem difficult informally, so
one's feelings on this point might depend on how much one's intuition
about elegance is shaped by a constructive approach.

Though the paper's approach seems to work as a matter of formalism, I
didn't find that the paper did a good job in conveying the intuitions
that the author(s) apparently had about why the approach makes
sense. The paper describes its approach as in some sense adding the
powerset monad to the Galois connection definition, perhaps with the
intuition that the monad captures and isolates what the paper calls
"specification effects" analogous to how a monad in a purely
functional programming language can capture I/O effects. Though I see
that the powerset operations obey the monad algebraic properties, I
wasn't able to follow the connection to noncomputability or
"specification-nees". If anything it seemed from the later examples
and proofs that the paper's approach really consists in taking away
powersets rather than adding them. Contrary to the parallel shown in
Figure 3, the example of the while language and the proofs of Section
6 show that a constructive Galois connection between posets A and B is
related to a classic Galois connection between P(A) and P(B), not one
between A and B. It makes more sense to me that removing powersets
instead of adding them would be the thing that makes an abstract
interpretation more computable, especially given the paper's
motivation in Section 2.3, but this feels like it is changing the
nature of the abstract interpretation.

Though the paper describes the benefits of its approach for soundness
proofs, I'm left wondering how well the approach works for precision
proofs, which are often also desirable. For instance in the while
language case, how would one use a formalism without \alpha to prove
that the most precise abstraction of plus has POS + POSZ = POS, rather
than POSZ or top? This feels like it is more inherently a set-based
property of the abstraction to me. This seems to me like a classic
part of building an abstract interpreter, and it's not clear whether
it is included in what the paper formalizes in Agda. (The paper
mentions that this proof is "available as supplemental material to
this paper", but I did not see it available in the reviewing
interface, perhaps because it has not been anonymized?)

Given that a key part of the paper's motivation is constructive logic
allowing implementations to be extracted, it would have better
completed the story to see a discussion of how one gets a running
abstract interpreter from the paper's formal development. I don't know
that Agda supports extraction in the style of Coq, but is the abstract
interpreter than the paper proves sound also practically executable as
an Agda program?

Some smaller comments:

"To abstract integers, the goal is to design a set with finite
elements": the set of integers already have the property that each
element is a finite object, at least in some sense. It seems more
likely the paper means "a set with only finitely many elements",
i.e. "a finite set". However the usual presentation of abstract
interpretation does not depend on the abstract domain being finite:
for instance consider constant propagation or intervals over integers.

"the least upper bound, which selects the smallest element that is
larger than both operands": I presume the paper means the usual
definition which is usually described with "larger than or equal to".
If the author(s) prefer to use "larger" for \subseteq, I think it
would be best to remark on this usage, or at least give an example
that requires this reading.

"Although [the best specification] inhabits Z^# \times Z^# \to Z^#, it
is not implementable as an algorithm": perhaps the paper should say
"not in general implementable as an algorithm"? In this particular
example, the best specification for any particular arithmetic operator
is in fact a finite map, so trivially implementable.

Since issues of constructability are key to the paper's motivation, I
would have liked to see a somewhat more detailed discussion on the
point in 2.3. Are there alternative models of sets, other than as
predicates, that would not have the same constructive logic problems?
How does using a classical axiom in a soundness proof make it
impossible to have an extractable constructive implementation?

"they are the natural by-product >of< the more general framework"

"P(A) is modelled as the antitonic A \searrow prop in constructive
logic": for what ordering on propositions in this mapping antitone?

"This definition is identical to that for Kleisli, except \alpha^k has
been replace>d< with pure(\eta)."

"\eta^z \in Z \nearrow Z^#" (Figure 4): what ordering on Z is being
used here? Not the standard one, I believe. (E.g. since POS is not
greater than ZER in the ordering on Z^#.)

"it is the identify function embedding into a larger set": either it
is the identity function, or it is a function that identifies one set
with a subset of another.