The standard operation refinement ordering is a kind of "meet of opposites": non-determinism reduction suggests "smaller" behaviour while increase of definition suggests "larger" behaviour. Groves' factorization of this ordering into two simpler relations, one per refinement concern, makes it more mathematically tractable but is far from fully exploited in the literature. We present a pointfree theory for this factorization which is more agile and calculational than the standard set-theoretic approach. In particular, we show that factorization leads to a simple proof of structural refinement for arbitrary parametric types and exploit factor instantiation across different subclasses of (relational) operation. The prospect of generalizing the factorization to coalgebraic refinement is discussed. © Springer-Verlag Berlin Heidelberg 2006.
CITATION STYLE
Oliveira, J. N., & Rodrigues, C. J. (2006). Pointfree factorization of operation refinement. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4085 LNCS, pp. 236–251). Springer Verlag. https://doi.org/10.1007/11813040_17
Mendeley helps you to discover research relevant for your work.