Pointfree factorization of operation refinement

• Autor(es): Oliveira, José Nuno Fonseca ; Rodrigues, César J.
• Data: 2006
• Identificador Persistente: http://hdl.handle.net/1822/6563
• Origem: RepositóriUM - Universidade do Minho
• Assunto(s): Theoretical foundations; Refinement; Calculation; Reusable theories
• Tipo de Documento: Documento de conferência
• Idioma: Inglês

Descrição

The standard operation refinement ordering is a kind of “meet of op- posites”: 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 mathe- matically 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 ex- ploit factor instantiation across different subclasses of (relational) operation. The prospect of generalizing the factorization to coalgebraic refinement is discussed