We redevelop and extend Dams's results on over- and under-approximation
with higher-order Galois connections:
(1) We show how Galois connections are generated from U-GLB-L-LUB-closed
binary relations, and we apply them to
lower and upper powerset constructions, which are
weaker forms of powerdomains
appropriate for abstraction studies.
(2) We use the powerset types within
a family of logical relations, show when the logical relations
preserve U-GLB-L-LUB-closure,
and show that simulation
is a logical relation. We use the logical relations to rebuild Dams's
most-precise simulations, revealing
the inner structure of under- and over-approximation.
(3) We extract validation and refutation logics from the logical relations,
state their resemblance to Hennessey-Milner logic
and description logic,
and obtain easy proofs of soundness and best precision.
