|
top_refinement_relations: THEORY
%------------------------------------------------------------------------------
%
% Theories, proofs and test:
% Relation between domain partitioned with equivalence relation,
% codomain partitioned with equivalence relation and two functions:
% f [domain -> codomain] and g [codomain -> domain]
%
% Author: Dragan Stosic
%
% In this work I have presented an approach ( aka abstract-algorithm
% formal description ) how to obtain the transformation-relation based
% on equivalence relations on domain and codomain and two functions: one
% from domain to codomain and another from codomain to domain. I named
% this relation "refinement relation" from the following reason:
% Short description:
% Lets have two equivalence relations: le_T (on domain) and le_U (on
% codomain) and two functions f [ domain - codomain ] and g[ codomain -
% domain ]. If we pick an element t1 from the domain such that le_T(
% t1, g(u1)) then f(t1) belongs to le_U(u2,f(t1)). According to the
% properties of the equivalence relation instead of using f(t1) element
% of the function f-image in some other calculus , we can substitute
% that element with any other which belongs to the Equivalence Class
% derived from the f(t1) element. In other words, we can refine f(t1)
% with the class representative of the Equivalence Class(f(t1)). We can
% state : f(t1) refined with rep( EquivClass(f(t1)) ->
% RR{(,)(,)...(t1,f(t1)),(t1,rep( EquivClass(f(t1))), (,)...}.
% In other words: t1 can be either paired with the f(t1) or any element
% that satisfied rep( EquivClass(f(t1))).
% The same concept holds in the opposite direction: from codomain to
% domain.
% Note that : My intention is not to dive deep in the rewriting theory
% and to explore equivalence relation as reduction. This work is not
% related to the rewriting equivalence theory; this is refinement
% between elements of collection within the equivalence class induced by
% equivalence relation.
% I have developed two different ways how to formalise the "refinement"
% relation. First approach is based on extended equivalence relation
% while second approach is based on extended equivalence relation
% induced by the inverse image of the equivalences relations
% respectivelly ( f induces inverse image of le_U and g induces inverse
% imagde of le_T ). Also I have established connection between those two
% definitions of the refinement relations.
% Finally, I have tested my conclusions through several simplest
% examples theories.
%------------------------------------------------------------------------------
BEGIN
IMPORTING relation_extension,
relation_extension_props,
relation_inverse_image,
relation_inverse_extension,
rr_rel,
simplest_examples
END top_refinement_relations
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
