| products/sources/formale sprachen/Isabelle/HOL/SPARK/Tools/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: xts701.cob Sprache: PVSOriginal von: PVS© |
|
||||||
|
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.19 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
