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
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.
