Next: Podsumowanie Up: autoref_pol Previous: Tematyka badañ
Omówienie uzyskanych wyników
W rozdzia³ach 2 i 3 dowodzimy, ¿e mo¿liwy jest jednolity opis algebraicznych równowa¿no¶ci obserwacyjnych oraz równowa¿no¶ci bisymulacyjnych. Punktem startu naszych badañ by³a praca [1], w której zaobserwowano, ¿e równowa¿no¶ci obserwacyjne ró¿nych klas modeli algebraicznych mo¿na uj±æ wspólnie, o ile klasa modeli jest tzw. kategori± konkretn±, w której dodatkowo wykonalne s± algebraiczne konstrukcje podalgebry generowanej przez zbiór i algebry ilorazowej. Przyk³adami takich kategorii s± m.in. algebry standardowe, czê¶ciowe oraz regularne, wykorzystywane jako modele dla specyfikacji algebraicznych. W naszych badaniach opieramy siê ponadto na wynikach pracy [2], w której zaproponowano wspólny opis ró¿norodnych równowa¿no¶ci bisymulacyjnych za pomoc± morfizmów otwartych w kategorii. W podej¶ciu tym wyró¿nia siê podkategoriê obiektów obserwacyjnych, które okre¶laj± klasê morfizmów otwartych, reprezentuj±cych funkcyjne bisymulacje; para takich morfizmów reprezentuje abstrakcyjnie relacjê bisymulacjê.
W rozdziale 2 pokazujemy, ¿e formalizm morfizmów otwartych jest wystarczaj±co elastyczny i ogólny, aby zastosowaæ go do opisu równowa¿no¶ci obserwacyjnej algebr. Dok³adniej, wskazujemy podkategorie obiektów obserwacyjnych w kategoriach algebr standardowych, czê¶ciowych oraz regularnych. Rezultaty s± sformu³owane ogólnie, co pozwala na ich zastosowanie do innych klas modeli o podobnej strukturze, pod warunkiem, ¿e funktor zapominaj±cy daj±cy no¶niki rodzajów obserwowalnych ma lewy sprzê¿ony. Warunek ten nastêpnie os³abiamy, ¿±daj±c istnienia lewego multi-sprzê¿onego lub nawet tylko pre-sprzê¿onego (pojêcie wprowadzone w pracy). Reasumuj±c, obserwacyjna równowa¿no¶æ szerokiej klasy modeli algebraicznych zosta³a przedstawiona jako bisymulacyjna równowa¿no¶æ przy pomocy morfizmów otwartych wyznaczonych przez pewne podkategorie obiektów obserwacyjnych.
W przypadku wszystkich równowa¿no¶ci algebraicznych rozwa¿anych przez nas, otwarte morfizmy posiadaj± pewn± w³asno¶æ (nazywan± w pracy determinizmem), któr± interpretujemy jako brak obserwowalnego zachowania niedeterministycznego. Jest to bardzo ciekawe spostrze¿enie, odró¿niaj±ce modele systemów sekwencyjnych od inherentnie niedeterministycznych modeli systemów wspó³bie¿nych. W pracy zbadano pewne w³asno¶ci deterministycznych klas morfizmów otwartych. Pokazano m.in, ¿e równowa¿no¶æ jest niezmiennicza ze wzglêdu na pewne operacje domkniêcia podkategorii obiektów obserwacyjnych, co pozwala na istotne ograniczenie liczby obiektów tej podkategorii.
W rozdziale 3 stawiamy sobie nastêpuj±ce pytanie: kiedy równowa¿no¶æ bisymulacyjna okre¶lona przez morfizmy otwarte mo¿e byæ ujêta jako algebraiczna równowa¿no¶æ obserwacyjna w kategorii konkretnej (tzn., kiedy jest ona faktoryzowana przez pewn± rodzinê kongruencji czê¶ciowych)? Motywacj± do badania takiego zagadnienia jest m.in. fakt, i¿ silna równowa¿no¶æ bisymulacyjna systemów tranzycyjnych faktoryzowana jest przez najwiêksze bisymulacje. W pracy sformu³owany zosta³ warunek wystarczaj±cy dla faktoryzacji równowa¿no¶ci bisymulacyjnej zadanej przez otwarte morfizmy: faktoryzacja ta ma miejsce, gdy ka¿dy obiekt ma najwiêksz± otwart± kongruencjê (dana równowa¿no¶æ jest wtedy faktoryzowana w³a¶nie przez najwiêksze otwarte kongruencje). Ponadto udowodnione zosta³o, ¿e warunkiem koniecznym i wystarczaj±cym jest wymóg, aby maksymalne otwarte kongruencje w ka¿dym obiekcie dawa³y izomorficzne ilorazy.
Jako przyk³ady modeli, do których stosuj± siê uzyskane wyniki, rozpatrujemy pewn± podklasê struktur zdarzeñ oraz kategoriê presnopów, zaproponowanych ostatnio jako jednolity model systemów wspó³bie¿nych. Okazuje siê te¿, ¿e kategorie rozwa¿anych przez nas modeli algebraicznych równie¿ spe³niaj± wymagane warunki, a ich równowa¿no¶ci obserwacyjne stanowi± szczególny przypadek faktoryzacji równowa¿no¶ci okre¶lonej przy pomocy otwartych morfizmów.
Podsumowuj±c, w rozdzia³ach 2 i 3 wskazane zosta³y ogólne warunki wystarczaj±ce dla wzajemnej odpowiednio¶ci dwóch ró¿nych koncepcyjnie metod definiowania obserwacyjnej równowa¿no¶ci: poprzez faktoryzacjê oraz za pomoc± obiektów obserwacyjnych. Ponadto pokazano, ¿e uzyskane wyniki stosuj± siê do wielu powszechnie stosowanych modeli systemów.
W rozdziale 4 koncentrujemy siê na innym stosowanym ostatnio powszechnie podej¶ciu do definiowania ró¿norodnych równowa¿no¶ci bisymulacyjnych, opartym na pojêciu koalgebry. Obserwowalne zachowanie obiektu modelowane jest tu przez strukturê koalgebry, a rolê funkcyjnych relacji bisymulacji, analogiczn± do otwartych morfizmów, pe³ni± morfizmy koalgebr. Dotychczas nie by³y znane ¿adne porównania otwartych morfizmów i morfizmów koalgebr, a jedyne udane próby porównania podej¶cia algebraicznego z koalgebraicznym mo¿liwe by³y dopiero przy za³o¿eniach, dopuszczaj±cych w algebrze tylko operacje o jednym argumencie nieobserwowalnego rodzaju. G³ównym wynikiem rozdzia³u 4 jest wskazanie funktora z danej kategorii (w której wyró¿niono podkategoriê obiektów obserwacyjnych) w odpowiedni± kategoriê koalgebr, przeprowadzaj±cego na morfizmy koalgebr dok³adnie te morfizmy w kategorii, które s± otwarte. Rezultat ten pozwala wnioskowaæ, ¿e idee le¿±ce u podstaw otwartych morfizmów s± w istocie rzeczy koalgebraicznej natury, i ¿e to koalgebry stanowi± najbardziej fundamentalny sposób opisu obserwowalnego zachowania modelowango systemu. W przypadku kategorii presnopów, wspomniany funktor stanowi wierne i pe³ne w³o¿enie kategorii - w pracy charakteryzujemy podkategoriê koalgebr równowa¿n± kategorii presnopów.
Wzajemna odpowiednio¶æ pomiêdzy otwartymi morfizmami a morfizmami koalgebr nie rozszerza siê na odpowiednio¶æ miêdzy relacjami bisymulacji - w uproszczeniu, kategoria koalgebr posiada w ogólno¶ci wiêcej obiektów, a zatem potencjalnie wiêcej relacji bisymulacji. Dlatego potrzebne jest scharakteryzowanie podkategorii koalgebr odpowiadaj±cych konkretnym modelom. Takie chatrakteryzacje istniej± dla ró¿nym modeli systemów wspó³bie¿nych, m.in. dla systemów tranzycyjnych czy struktur zdarzeñ. W rozdziale 4 rozwa¿amy ponownie kategorie algebr standardowych i czê¶ciowych. Podajemy charakteryzacje odpowiadaj±cych im podkategorii koalgebr, poprzez podkategorie presnopów zachowuj±cych odpowiednio skoñczone produkty (algebry standardowe) i pewne skoñczone granice (algebry czê¶ciowe). Uzyskane wyniki stanowi± uogólnienie znanych twierdzeñ o reprezentacji algebr w kategoriach funktorów. Pozwalaj± one równie¿ na opis równowa¿no¶ci obserwacyjnej algebr w terminach bisymulacji koalgebraicznej.
Rozdzia³ 5 po¶wiêcony jest zagadnieniom znacznie bli¿szym zastosowañ. Proponujemy w nim metodologiê krokowej implementacji behawioralnej dla algebr regularnych. W uproszczeniu, algebry regularne rozszerzaj± algebry standardowe przez umo¿liwienie opisu potencjalnie nieskoñczonych struktur danych, np. strumieni, leniwych list, itp. W konsekwencji, przyjête metody implementacji, np. podej¶cie konstruktorowe, nie daj± siê bezpo¶rednio zastosowaæ. W pracy przedstawiamy adaptacjê behawioralnej implementacji konstruktorowej dla algebr regularnych. Zaproponowana zosta³a metoda systematycznego definiowania operacji w algebrze regularnej, nazywana w pracy -indukcj±. Podane zosta³o równie¿ satysfakcjonuj±ce rozwi±zanie pozwalaj±ce na ,,wspó³istnienie'' w algebrze regularnej rodzajów algebraicznych, tzn. posiadaj±cych tylko finitarne warto¶ci.
Wa¿nym zagadnieniem zwi±zanym z omawianymi metodami jest dowodzenie poprawno¶ci implementacji. W pracy podajemy warunek u³atwiaj±cy dowodzenie poprawno¶ci kroku implementacyjnego (nazywany w pracy: behavioural consistency). Wskazujemy ponadto, i¿ dla nieodró¿nialno¶ci obserwacyjnej w algebrze regularnej wystarczy rozpatrywaæ tylko finitarne konteksty (tzn. bez -termów), co jest kluczowe dla dowodzenia w³asno¶ci implementacji. Z drugiej strony pokazujemy, ¿e dowodz±c równowa¿no¶ci dwóch algebr nie mo¿na w ogólno¶ci ograniczyæ siê do kontekstów finitarnych. Natomiast gdy wszystkie rodzaje obserwowalne s± algebraiczne, finitarne konteksty wystarczaj± w dowodzie równowa¿no¶ci algebr regularnych. Poniewa¿ w praktycznych przyk³adach warunek powy¿szy jest na ogó³ spe³niony, uzyskane wyniki mog± stanowiæ punkt wyj¶cia dla efektywnych metod dowodzenia behawioralnych w³asno¶ci algebr regularnych.
Rozdzia³ 5 zawiera równie¿ seriê przyk³adowych specyfikacji i ich behawioralnych implementacji, ilustruj±cych zastosowania naszych rezultatów.
Next: Podsumowanie Up: autoref_pol Previous: Tematyka badañ Slawomir Lasota 2000-03-17