Corrigendum for
---
M. J. Frade, A. Saabas, T. Uustalu. Bidirectional data-flow analyses,
type-systematically.
In Proc. of PEPM 2009, pp. 141-149. ACM Press, 2009.
doi:10.1145/1480945.1480965
---
p 145, col 1, Thm 1: The Galois connection described here is actually
not coreflective.
Accordingly, these corrections are needed to rectify the statements:
in (5): replace "form a coreflective Galois connection" with
"form a Galois connection";
delete "Moreover, or any joins-closed relation R,
f2R(R2f^{\from}(R), R2f^{\to}(R)) \subseteq R";
in (6): replace "we have R = f2R(R2f^{\from}(R), R2f^{\to}(R))" with
"we have R \subseteq f2R(R2f^{\from}(R), R2f^{\to}(R))".
Yasuaki Morita spotted this error.
A coreflection is obtained by confining to those joins-closed
relations R that satisfy the following "butterfly" property:
for all d0,d,d1,d0',d',d1' \in D,
if d0 \leq d \leq d1 and d0' \leq d' \leq d1'
and (d0,d1') \in R and (d1,d0') \in R,
then (d,d') \in R
(*)
These make the image of right adjoint f2R.
A reflection is obtained by confining to those pairs of monotone
functions f^{\from}, f^{\to} that satisfy the inequations
for all d' \in D,
f^{\from}(d') \leq f^{\from}(d' \meet f^{\to}(f^{\from}(d')))
for all d \in D,
f^{\to}(d) \leq f^{\to} (d \meet f^{\from}(f^{\to}(d)))
(**)
These make the image of the left adjoint
\langle R2f^{\from}, R2f^{\to} \rangle.
These narrower posets of joins-closed relations and pairs of monotone
functions (satisfying (*) and (**) respectively) are isomorphic.
We are currently (in Apr. 2024) writing a paper where we explain this
and a lot more.
p 148, fig 8, col 2:
The clause for [dup]^{\to}(e::es) contains a typo.
Read es for *.