Różnice między wybraną wersją a wersją aktualną.
| Both sides previous revision Poprzednia wersja Nowa wersja | Poprzednia wersja | ||
|
pl:miw:miw08_xtt_rif [2008/05/28 12:44] miw |
pl:miw:miw08_xtt_rif [2019/06/27 15:50] (aktualna) |
||
|---|---|---|---|
| Linia 1: | Linia 1: | ||
| ====== Opis ====== | ====== Opis ====== | ||
| + | __**Projekt zakończony**__ | ||
| + | |||
| Mateusz Mazur, <m-a-t-i@o2.pl> | Mateusz Mazur, <m-a-t-i@o2.pl> | ||
| Linia 8: | Linia 10: | ||
| * Elementy przestarzałe zostały przeniesione [[pl:miw:miw08_xtt_rif:obsolate|tutaj]]. | * Elementy przestarzałe zostały przeniesione [[pl:miw:miw08_xtt_rif:obsolate|tutaj]]. | ||
| * :!:**[[pl:miw:miw08_xtt_rif:spotkania|Spotkania]]**. | * :!:**[[pl:miw:miw08_xtt_rif:spotkania|Spotkania]]**. | ||
| - | * [[http://saxon.sourceforge.net/|SAXON]] translator XSLT zaimplemantowany w JAVA oraz .NET (jest wersja Open Source, która nie zawiera paru dodatkowych funkcji) | + | * [[http://saxon.sourceforge.net/|SAXON]] translator XSLT zaimplementowany w JAVA oraz .NET (jest wersja Open Source, która nie zawiera paru dodatkowych funkcji) |
| * [[http://www.gingerall.org/sablotron.html|Sablotron]] | * [[http://www.gingerall.org/sablotron.html|Sablotron]] | ||
| * [[http://xml.apache.org/]] | * [[http://xml.apache.org/]] | ||
| * :!:**[[http://www.w3.org/2005/rules/wg/wiki/Arch/XML_Syntax_Issues_2]]** | * :!:**[[http://www.w3.org/2005/rules/wg/wiki/Arch/XML_Syntax_Issues_2]]** | ||
| + | |||
| ====== Sprawozdanie ====== | ====== Sprawozdanie ====== | ||
| Linia 17: | Linia 20: | ||
| //W oparciu o dokumentację z 15.04.2008// ({{:pl:miw:miw08_xtt_rif:rif_bld_fld_freez.zip|rif_bld_fld_freez.zip}}) | //W oparciu o dokumentację z 15.04.2008// ({{:pl:miw:miw08_xtt_rif:rif_bld_fld_freez.zip|rif_bld_fld_freez.zip}}) | ||
| ---- | ---- | ||
| + | * 08.05.18 - nowy szkic specyfikacji. Nowości: | ||
| + | * Dokument: [[http://www.w3.org/2005/rules/wg/draft/ED-rif-dtb-20080518/|RIF Data Types and Built-Ins]] | ||
| + | * Dokument: [[http://www.w3.org/2005/rules/wg/draft/ED-rif-ucr-20080518/|RIF Use Cases and Requirements]] | ||
| + | * Rozdział w RIF-BLD: [[http://www.w3.org/2005/rules/wg/draft/ED-rif-bld-20080518/diff-since-20080415#Interpretation_of_Documents|Interpretation of Documents]] | ||
| + | * BLD: zmiany w opisie termów | ||
| + | * BLD: zmiany w opisie dobrze sformułowanych formuł | ||
| + | * BLD: zmiany w gramatyce | ||
| ===== Wprowadzenie do RIF ===== | ===== Wprowadzenie do RIF ===== | ||
| Linia 89: | Linia 99: | ||
| - | Aby uprościć język, będziemy często używać identyfikatorów przstrzeni symboli, by odwoływać się do konkretnych przestrzeni (np. zostanie użyte "przestrzeń nazw ''xsd:string''" zamiast "przestrzeń nazw identyfikowana przez ''xsd:string''"). | + | Aby uprościć język, będziemy często używać identyfikatorów przestrzeni symboli, by odwoływać się do konkretnych przestrzeni (np. zostanie użyte "przestrzeń nazw ''xsd:string''" zamiast "przestrzeń nazw identyfikowana przez ''xsd:string''"). |
| By odwołać się do stałej w określonej przestrzeni nazw RIF, używamy następującej składni prezentacji: | By odwołać się do stałej w określonej przestrzeni nazw RIF, używamy następującej składni prezentacji: | ||
| Linia 125: | Linia 135: | ||
| //[[http://www.w3.org/2005/rules/wg/draft/rif-bld/#Well-formedness_of_Terms|Well-formedness of Terms]]//\\ | //[[http://www.w3.org/2005/rules/wg/draft/rif-bld/#Well-formedness_of_Terms|Well-formedness of Terms]]//\\ | ||
| - | Zbiór wyszystkich symboli, ''Const'', jest podzielony na: | + | Zbiór wszystkich symboli, ''Const'', jest podzielony na: |
| * Pozycjonowane symbole predykatów (ang. positional predicate symbols) | * Pozycjonowane symbole predykatów (ang. positional predicate symbols) | ||
| * Symbole predykatów z nazwanymi argumentami (ang. predicate symbols with named arguments) | * Symbole predykatów z nazwanymi argumentami (ang. predicate symbols with named arguments) | ||
| Linia 138: | Linia 148: | ||
| * Dla symboli z nazwanymi argumentami, arność jest zbiorem ''{s_1 ... s_k}'' nazw argumentów (''s_i'' należy do ''ArgNames''), które są dozwolone dla danego symbolu. | * Dla symboli z nazwanymi argumentami, arność jest zbiorem ''{s_1 ... s_k}'' nazw argumentów (''s_i'' należy do ''ArgNames''), które są dozwolone dla danego symbolu. | ||
| - | Arność symbolu (czy predykatu, funkcji, bądźor osobnika) nie jest określona w RIF-BLD kategorycznie. Przeciwnie, jest ona wnioskowana jak następuje: | + | Arność symbolu (czy predykatu, funkcji, bądź osobnika) nie jest określona w RIF-BLD kategorycznie. Przeciwnie, jest ona wnioskowana jak następuje: |
| - | * Każdy stały symbol w foirmule RIF-BLD (lub zbiorze formuł) może się pojawić conajwyżej w jednym z kontekstów: | + | * Każdy stały symbol w formule RIF-BLD (lub zbiorze formuł) może się pojawić co najwyżej w jednym z kontekstów: |
| * jako osobnik, | * jako osobnik, | ||
| * jako symbol funkcji o określonej arności | * jako symbol funkcji o określonej arności | ||
| - | * jako symbol predykatu o określonej atności. | + | * jako symbol predykatu o określonej arności. |
| * Arność symbolu i jego typ jest określany przez jego kontekst. | * Arność symbolu i jego typ jest określany przez jego kontekst. | ||
| * Jeśli symbol ze zbioru ''Const'' pojawi się więcej niż w jednym kontekście w zbiorze formuł, to zbiór nie jest poprawnie sformułowany w RIF-BLD. | * Jeśli symbol ze zbioru ''Const'' pojawi się więcej niż w jednym kontekście w zbiorze formuł, to zbiór nie jest poprawnie sformułowany w RIF-BLD. | ||
| Linia 165: | Linia 175: | ||
| * //Atomiczną (ang. atomic)//: Jeśli ''t'' jest dobrze sformułowaną formułą atomiczną, to jest również dobrze sformułowaną formułą. | * //Atomiczną (ang. atomic)//: Jeśli ''t'' jest dobrze sformułowaną formułą atomiczną, to jest również dobrze sformułowaną formułą. | ||
| * //Koniunktywna (ang. conjunction)//: Jeśli ''t_1, ..., t_n'', ''n >= 0'' są dobrze sformułowanymi formułami, to również formuła koniunktywna ''And(t_1 ... t_n)'' jest dobrze sformułowana. W specjalnym przypadku, ''And()'' jest dozwolone i traktowane jako tautologia (ang. tautology), t.j. formuła, która jest zawsze prawdziwa. | * //Koniunktywna (ang. conjunction)//: Jeśli ''t_1, ..., t_n'', ''n >= 0'' są dobrze sformułowanymi formułami, to również formuła koniunktywna ''And(t_1 ... t_n)'' jest dobrze sformułowana. W specjalnym przypadku, ''And()'' jest dozwolone i traktowane jako tautologia (ang. tautology), t.j. formuła, która jest zawsze prawdziwa. | ||
| - | * //Dysjunktywna (ang. disjunction)//: Jeśli ''t_1, ..., t_n'', ''n >= 0'' są dobrze sformułowanymi formułami, to również formuła dyjunktywna ''Or(t_1 ... t_n)'' jest dobrze sformułowana. Gdy ''n=0'', dostajemy ''Or()'' jako specjalny przypadek; Jest on traktowany jako it is treated as a zaprzeczenie, t.j. formuła która jest zawsze fałszywa. | + | * //Dysjunktywna (ang. disjunction)//: Jeśli ''t_1, ..., t_n'', ''n >= 0'' są dobrze sformułowanymi formułami, to również formuła dysjunktywna ''Or(t_1 ... t_n)'' jest dobrze sformułowana. Gdy ''n=0'', dostajemy ''Or()'' jako specjalny przypadek; Jest on traktowany jako it is treated as a zaprzeczenie, t.j. formuła która jest zawsze fałszywa. |
| * //Istnienia (ang. existentials)//: Jeśli ''t'' jest dobrze sformułowaną formułą oraz ''?V_1, ..., ?V_n'' są zmiennymi, wtedy ''Exists ?V_1 ... ?V_n(t)'' jest formułą istnienia. | * //Istnienia (ang. existentials)//: Jeśli ''t'' jest dobrze sformułowaną formułą oraz ''?V_1, ..., ?V_n'' są zmiennymi, wtedy ''Exists ?V_1 ... ?V_n(t)'' jest formułą istnienia. | ||
| Formuły zbudowane z użyciem powyższych definicji są nazywane warunkami RIF-BLD. Następujące formuły prowadzą do pojęcia reguły RIF-BLD: | Formuły zbudowane z użyciem powyższych definicji są nazywane warunkami RIF-BLD. Następujące formuły prowadzą do pojęcia reguły RIF-BLD: | ||
| * //Implikacja reguł (ang. rule implication)//: Jeśli ''t'' jest dobrze sformułowaną formułą atomiczną oraz ''p'' jest warunkiem RIF-BLD to ''t :- p'' jest dobrze sformułowaną formułą, nazywaną regułą wynikania (ang. rule implication), pod warunkiem, że ''t'' nie jest zdefiniowane zewnętrznie (t.j. nie ma postaci ''External(...)''). | * //Implikacja reguł (ang. rule implication)//: Jeśli ''t'' jest dobrze sformułowaną formułą atomiczną oraz ''p'' jest warunkiem RIF-BLD to ''t :- p'' jest dobrze sformułowaną formułą, nazywaną regułą wynikania (ang. rule implication), pod warunkiem, że ''t'' nie jest zdefiniowane zewnętrznie (t.j. nie ma postaci ''External(...)''). | ||
| - | * //Reguła kwantyfikująca (ang. quantified rule)//: Jeśli ''t'' jest regułą wynikania oraz ''?V_1, ..., ?V_n'' są zmiennymi, wtedy ''Forall ?V_1 ... ?V_n(t)'' jest dobrze sformułowaną formułą, nazywaną regułą kawntyfikującą. Wymaga się aby wszystkie wolne (t.j. nie kwantyfikujące) zmienne w ''t'' pojawiły się w prefiksie ''Forall ?V_1 ... ?V_n''. Reguły kwantyfikujące będą również nazywane jako reguły RIF-BLD. | + | * //Reguła kwantyfikująca (ang. quantified rule)//: Jeśli ''t'' jest regułą wynikania oraz ''?V_1, ..., ?V_n'' są zmiennymi, wtedy ''Forall ?V_1 ... ?V_n(t)'' jest dobrze sformułowaną formułą, nazywaną regułą kwantyfikującą. Wymaga się aby wszystkie wolne (t.j. nie kwantyfikujące) zmienne w ''t'' pojawiły się w prefiksie ''Forall ?V_1 ... ?V_n''. Reguły kwantyfikujące będą również nazywane jako reguły RIF-BLD. |
| - | * //Grupa (ang. group)//: Jeśli ''t'' jest ramą oraz ''p_1, ..., p_n'' są regułami RIF-BLD lub grupami formuł (mogą byc wymieszane), to ''Group t (p_1 ... p_n)'' i ''Group (p_1 ... p_n)'' formułami grupowymi. | + | * //Grupa (ang. group)//: Jeśli ''t'' jest ramą oraz ''p_1, ..., p_n'' są regułami RIF-BLD lub grupami formuł (mogą być wymieszane), to ''Group t (p_1 ... p_n)'' i ''Group (p_1 ... p_n)'' formułami grupowymi. |
| - | Formuły grupowe mają za zadanie reprezentować zbiory reguł z przypisami w meta-danych (ang. annotated with metadata). Te meta-dane są określone przy pomocy opcjonalnego termu ramowego ''t''. Warto zauważyć, że niektóre z ''p_i'' mogą być formułami grupowymi, co oznacza, że grupy mogą być zagnieżdżane. To pozwala na przypisy meta-danych to różnych podzbiorów reguł, które mogą być wewnątrz większych zbiorów reguł, do których też można dołączyć przypisy. | + | Formuły grupowe mają za zadanie reprezentować zbiory reguł z przypisami w meta-danych (ang. annotated with metadata). Te meta-dane są określone przy pomocy opcjonalnego termu ramowego ''t''. Warto zauważyć, że niektóre z ''p_i'' mogą być formułami grupowymi, co oznacza, że grupy mogą być zagnieżdżone. To pozwala na przypisy meta-danych to różnych podzbiorów reguł, które mogą być wewnątrz większych zbiorów reguł, do których też można dołączyć przypisy. |
| - | Z powyższych definicji wynika, że RIF-BLD posiada szeroki wachlarz form syntaktycznych dla termów i formuł. Zapewnia to infrastrukturę dla wymiany językowów regułowych, które wspierają bogate kolekcje form syntaktycznych. Systemy, które nie wspierają części składni bezpośrednio, mogą nadal ją wspierać poprzez transformacje syntaktyczne. Na przykład dysjunkcję w ciele reguły można wyeliminować poprzez standardową transformację, taką, jak zamiana ''p :- Or(q r)'' na parę reguł ''p :- q'', ''p :- r''. Termy z nazwanymi argumentami mogą zostać zredukowane do termów pozycjonowanych poprzez upożądkowanie argumentów po nazwach oraz włączenie ich w nazwę predykatu. Na przykład: ''p(bb->1 aa->2)'' może być przedstawiony jako ''p_aa_bb(2,1)''. | + | Z powyższych definicji wynika, że RIF-BLD posiada szeroki wachlarz form syntaktycznych dla termów i formuł. Zapewnia to infrastrukturę dla wymiany języków regułowych, które wspierają bogate kolekcje form syntaktycznych. Systemy, które nie wspierają części składni bezpośrednio, mogą nadal ją wspierać poprzez transformacje syntaktyczne. Na przykład dysjunkcję w ciele reguły można wyeliminować poprzez standardową transformację, taką, jak zamiana ''p :- Or(q r)'' na parę reguł ''p :- q'', ''p :- r''. Termy z nazwanymi argumentami mogą zostać zredukowane do termów pozycjonowanych poprzez uporządkowanie argumentów po nazwach oraz włączenie ich w nazwę predykatu. Na przykład: ''p(bb->1 aa->2)'' może być przedstawiony jako ''p_aa_bb(2,1)''. |
| Linia 186: | Linia 196: | ||
| Analizując zapis RIF w tej notacji, należy pamiętać o kilku rzeczach: | Analizując zapis RIF w tej notacji, należy pamiętać o kilku rzeczach: | ||
| - | * Składnisa logiki pierwszego rzędu (ang. first-order logic) nie jest bezkontekstowa, więc EBNF nie opisuje składni RIF-BLD dokładnie. Na przykład nie da się zapisać reguł dobrego formułowania. | + | * Składnisa logiki pierwszego rzędu (ang. first-order logic) nie jest bez kontekstowa, więc EBNF nie opisuje składni RIF-BLD dokładnie. Na przykład nie da się zapisać reguł dobrego formułowania. |
| - | * Składnia EBNF nie jest konkretna: nie opisuje szczegółów reprezentowania stałych i zmiennych, nie jest też dostatecznie dokładna co do separatorów. Zamiast tego spacja jest nieformalnie wykotrzystywana jako separator. | + | * Składnia EBNF nie jest konkretna: nie opisuje szczegółów reprezentowania stałych i zmiennych, nie jest też dostatecznie dokładna co do separatorów. Zamiast tego spacja jest nieformalnie wykorzystywana jako separator. |
| * Składnia EBNF nie jest normatywna. | * Składnia EBNF nie jest normatywna. | ||
| Linia 224: | Linia 234: | ||
| Zbiór ''TV'' wartości prawdy w RIF-BLD składa się z dwóch wartości: ''t'' oraz ''f''. | Zbiór ''TV'' wartości prawdy w RIF-BLD składa się z dwóch wartości: ''t'' oraz ''f''. | ||
| + | |||
| Linia 235: | Linia 246: | ||
| **Definicja (Struktura Semantyczna)**\\ | **Definicja (Struktura Semantyczna)**\\ | ||
| - | Struktura semantyczna, ''I'', jest to tuple //(ang.)// postaci ''<TV, DTS, D, Dind, Dfunc, IC, IV, IF, Iframe, ISF, Isub, Iisa, I=, Iexternal, Itruth>''. Gdzie ''D'' jest niepustym zbiorem elementów zwanym //domeną ''I'' (ang. domain)//, natomiast ''Dind'', ''Dfunc'' są niepustymi podzbiorami ''D''. ''Ding'' jest używany do interpretowania elementów ''Const'', oznaczających osobniki. ''Dfunc'' zawiera elementy ''Const'' oznaczające symbole funkcyjne. Jak poprzednio, ''Const'' oznacza zbiór wszystkich stałych symboli, a ''Var'' - zbiór wszystkich zmiennych symboli. ''TV'' oznacza zbiór wartości prawdy, których używa struktura semantyczna, a ''DTS'' jest zbiorem prostych typów danych używanych w ''I'' (Rozdział Primitive Data Types w RIF-FLD). | + | Struktura semantyczna, ''I'', jest to entka //(ang. tuple)// postaci ''<TV, DTS, D, Dind, Dfunc, IC, IV, IF, Iframe, ISF, Isub, Iisa, I=, Iexternal, Itruth>''. Gdzie ''D'' jest niepustym zbiorem elementów zwanym //domeną ''I'' (ang. domain)//, natomiast ''Dind'', ''Dfunc'' są niepustymi podzbiorami ''D''. ''Ding'' jest używany do interpretowania elementów ''Const'', oznaczających osobniki. ''Dfunc'' zawiera elementy ''Const'' oznaczające symbole funkcyjne. Jak poprzednio, ''Const'' oznacza zbiór wszystkich stałych symboli, a ''Var'' - zbiór wszystkich zmiennych symboli. ''TV'' oznacza zbiór wartości prawdy, których używa struktura semantyczna, a ''DTS'' jest zbiorem prostych typów danych używanych w ''I'' (Rozdział Primitive Data Types w RIF-FLD). |
| Pozostałe składowe ''I'' są odwzorowaniami zupełnymi (ang. total mappings) zdefiniowanymi następująco: | Pozostałe składowe ''I'' są odwzorowaniami zupełnymi (ang. total mappings) zdefiniowanymi następująco: | ||
| Linia 495: | Linia 506: | ||
| Wstępne przmyślenia: | Wstępne przmyślenia: | ||
| * Do nadania identyfikatorów posłuży element spoza RIF, należący do języka XML - ''id''. | * Do nadania identyfikatorów posłuży element spoza RIF, należący do języka XML - ''id''. | ||
| + | |||
| + | |||
| + | |||
| + | |||
| + | |||
| + | |||
| + | |||
| Linia 535: | Linia 553: | ||
| <then> | <then> | ||
| <Atom> <!-- specjalny predykat, sugerujący następną regułę/tablicę i wywołujący inne predykaty --> | <Atom> <!-- specjalny predykat, sugerujący następną regułę/tablicę i wywołujący inne predykaty --> | ||
| - | <op><Const type="rif:iri">xtt:concl</Const></op> | + | <op><Const type="rif:iri">xtt:next_table_rule</Const></op> |
| - | <arg> | + | <arg><Const type="xsd:string">xtt_table1</Const></arg> |
| - | <Atom> <!-- predykat podajacy wartosci 'id' nastepnej tablicy/wiersza --> | + | <arg><Const type="xsd:string">xtt_table_row1</Const></arg> |
| - | <op><Const type="rif:iri">xtt:next_table_rule</Const></op> | + | |
| - | <arg><Const type="xsd:string">xtt_table1</Const></arg> | + | |
| - | <arg><Const type="xsd:string">xtt_table_row1</Const></arg> | + | |
| - | </Atom> | + | |
| - | </arg> | + | |
| <arg> | <arg> | ||
| <!-- albo predykat do wywołania, albo predykat xtt:run_many wywołujący więcej niż jeden predykat --> | <!-- albo predykat do wywołania, albo predykat xtt:run_many wywołujący więcej niż jeden predykat --> | ||
| Linia 586: | Linia 599: | ||
| </arg> | </arg> | ||
| </Atom></code> | </Atom></code> | ||
| + | |||
| + | Zapis przyrównania zmiennej do zbioru (''X = {1,2,4}'') będzie realizowany za pomocą tagu ''Equal'': | ||
| + | <code xml><Equal> | ||
| + | <side><Var>X</Var></side> | ||
| + | <side> | ||
| + | <External> | ||
| + | <content> | ||
| + | <Expr> | ||
| + | <op><Const type="rif:iri">xtt:complex_set</Const></op> | ||
| + | <arg><Const type="xsd:decimal">1</Const></arg> | ||
| + | <arg><Const type="xsd:decimal">2</Const></arg> | ||
| + | <arg><Const type="xsd:decimal">4</Const></arg> | ||
| + | </Expr> | ||
| + | </content> | ||
| + | </External> | ||
| + | </side> | ||
| + | </Equal></code> | ||
| + | //ten zapis nie został zaimplementowany w translatorze, ze względu na brak informacji co do zapisu po stronie XTTMLa.// | ||
| === Wykorzystywane predykaty === | === Wykorzystywane predykaty === | ||
| - | W najnowszej wersji dokumentacji RIFa pojawił się dokument definiujący zarówno [[http://www.w3.org/2005/rules/wg/draft/rif-dtb/|predykaty wbudowane]], jaki i [[http://www.w3.org/2005/rules/wg/draft/rif-dtb/#Appendix:_Schemas_for_Externally_Defined_Terms|definiowanie zewnętrznych]]. | + | W najnowszej wersji dokumentacji RIFa pojawił się dokument definiujący zarówno [[http://www.w3.org/2005/rules/wg/draft/ED-rif-dtb-20080518/#List_of_Supported_Built-in_Predicates_and_Functions|predykaty wbudowane]], jaki i [[http://www.w3.org/2005/rules/wg/draft/rif-dtb/#Appendix:_Schemas_for_Externally_Defined_Terms|definiowanie zewnętrznych]]. |
| ^Predykat ^External schema ^Opis ^ | ^Predykat ^External schema ^Opis ^ | ||
| Linia 596: | Linia 627: | ||
| | xtt:next_table |''(?arg1 ?arg2; pred:next_table(?arg1, ?arg2))'' |Predykat sterujący wnioskowaniem. Pierwszy argument to ''id'' tabeli, która powinna być wywołana jako następna (''id'' taga ''Group''). Drugi parametr to operacja, jaką należy wykonać przy wykonaniu reguły. | | | xtt:next_table |''(?arg1 ?arg2; pred:next_table(?arg1, ?arg2))'' |Predykat sterujący wnioskowaniem. Pierwszy argument to ''id'' tabeli, która powinna być wywołana jako następna (''id'' taga ''Group''). Drugi parametr to operacja, jaką należy wykonać przy wykonaniu reguły. | | ||
| | xtt:run_many |''(?arg1 ?arg2 [...]; pred:run_many(?arg1, ?arg2, [...]))'' |Predykat wykorzystywany w konkluzji, służący do wywoływania więcej niż jednej operacji. | | | xtt:run_many |''(?arg1 ?arg2 [...]; pred:run_many(?arg1, ?arg2, [...]))'' |Predykat wykorzystywany w konkluzji, służący do wywoływania więcej niż jednej operacji. | | ||
| + | |||
| + | Dodatkowo wszystkie operatory ''logop'' są traktowane jako zdefiniowane operatory i występują jako predykaty z przedrostkiem ''xtt:''. Na przykład ''\in'' będzie to ''<op><Const type="rif:iri">xtt:in</Const></op>''. | ||
| **Uwagi**\\ | **Uwagi**\\ | ||
| * Każda tablica (element ''Group'') musi być w osobnym pliku (zgodność z plikami xsd). | * Każda tablica (element ''Group'') musi być w osobnym pliku (zgodność z plikami xsd). | ||
| - | |||
| - | === Przykład 1: calculations (factorial) === | ||
| - | <code> | ||
| - | |----------------------------------------------------| | ||
| - | | | | ||
| - | | x s || s | | ||
| - | |->------------ x y s || y | | ||
| - | NA ||=x --+------> ------------------- | | ||
| - | >0 ||=s-1 --| || | | ||
| - | >0 >0 || =y*s -----| | ||
| - | =0 || =1 -----------| | ||
| - | >0 =1 || -----------+------> | ||
| - | </code> | ||
| - | <code xml> | ||
| - | <Group id="xtt_table1"> | ||
| - | <sentence id="xtt_table1_row1"> | ||
| - | <Implies> | ||
| - | <if> | ||
| - | <External> | ||
| - | <content> | ||
| - | <Atom> | ||
| - | <op><Const type="rif:iri">fn:is_empty</Const></op> | ||
| - | <arg><Var>x</Var></arg> | ||
| - | </Atom> | ||
| - | </content> | ||
| - | </External> | ||
| - | </if> | ||
| - | <then> | ||
| - | <Atom> | ||
| - | <op><Const type="rif:iri">xtt:concl</Const></op> | ||
| - | <arg> | ||
| - | <External> | ||
| - | <content> | ||
| - | <Expr> | ||
| - | <op><Const type="rif:iri">xtt:next_table</Const></op> | ||
| - | <arg><Const type="xsd:string">xtt_table2</Const></arg> | ||
| - | </Expr> | ||
| - | </content> | ||
| - | </External> | ||
| - | </arg> | ||
| - | <arg> | ||
| - | <External> | ||
| - | <content> | ||
| - | <Expr> | ||
| - | <op><Const type="rif:iri">op:assign</Const></op> | ||
| - | <arg><Var>s</Var></arg> | ||
| - | <arg><Var>x</Var></arg> | ||
| - | </Expr> | ||
| - | </content> | ||
| - | </External> | ||
| - | </arg> | ||
| - | </Atom> | ||
| - | </then> | ||
| - | </Implies> | ||
| - | </sentence> | ||
| - | |||
| - | <sentence id="xtt_table1_row2"> | ||
| - | <Implies> | ||
| - | <if> | ||
| - | <External> | ||
| - | <content> | ||
| - | <Atom> | ||
| - | <op><Const type="rif:iri">op:numeric-greater-than</Const></op> | ||
| - | <arg><Var>s</Var></arg> | ||
| - | <arg><Const type="xsd:decimal">0</Const></arg> | ||
| - | </Atom> | ||
| - | </content> | ||
| - | </External> | ||
| - | </if> | ||
| - | <then> | ||
| - | <Atom> | ||
| - | <op><Const type="rif:iri">xtt:concl</Const></op> | ||
| - | <arg> | ||
| - | <External> | ||
| - | <content> | ||
| - | <Expr> | ||
| - | <op><Const type="rif:iri">xtt:next_table</Const></op> | ||
| - | <arg><Const type="xsd:string">xtt_table2</Const></arg> | ||
| - | </Expr> | ||
| - | </content> | ||
| - | </External> | ||
| - | </arg> | ||
| - | <arg> | ||
| - | <External> | ||
| - | <content> | ||
| - | <Expr> | ||
| - | <op><Const type="rif:iri">op:assign</Const></op> | ||
| - | <arg><Var>s</Var></arg> | ||
| - | <arg> | ||
| - | <External> | ||
| - | <content> | ||
| - | <Expr> | ||
| - | <op><Const type="rif:iri">op:numeric-substract</Const></op> | ||
| - | <arg><Var>s</Var></arg> | ||
| - | <arg><Const type="xsd:decimal">1</Const></arg> | ||
| - | </Expr> | ||
| - | </content> | ||
| - | </External> | ||
| - | </arg> | ||
| - | </Expr> | ||
| - | </content> | ||
| - | </External> | ||
| - | </arg> | ||
| - | </Atom> | ||
| - | </then> | ||
| - | </Implies> | ||
| - | </sentence> | ||
| - | </Group> | ||
| - | |||
| - | <Group id="xtt_table2"> | ||
| - | <sentence id="xtt_table2_row1"> | ||
| - | <Implies> | ||
| - | <if> | ||
| - | <And> | ||
| - | <formula> | ||
| - | <External> | ||
| - | <content> | ||
| - | <Atom> | ||
| - | <op><Const type="rif:iri">op:numeric-greater-than</Const></op> | ||
| - | <arg><Var>x</Var></arg> | ||
| - | <arg><Const type="xsd:decimal">0</Const></arg> | ||
| - | </Atom> | ||
| - | </content> | ||
| - | </External> | ||
| - | </formula> | ||
| - | <formula> | ||
| - | <External> | ||
| - | <content> | ||
| - | <Atom> | ||
| - | <op><Const type="rif:iri">op:numeric-greater-than</Const></op> | ||
| - | <arg><Var>s</Var></arg> | ||
| - | <arg><Const type="xsd:decimal">0</Const></arg> | ||
| - | </Atom> | ||
| - | </content> | ||
| - | </External> | ||
| - | </formula> | ||
| - | </And> | ||
| - | </if> | ||
| - | <then> | ||
| - | <Atom> | ||
| - | <op><Const type="rif:iri">xtt:concl</Const></op> | ||
| - | <arg> | ||
| - | <External> | ||
| - | <content> | ||
| - | <Expr> | ||
| - | <op><Const type="rif:iri">xtt:next_table</Const></op> | ||
| - | <arg><Const type="xsd:string">xtt_table1</Const></arg> | ||
| - | </Expr> | ||
| - | </content> | ||
| - | </External> | ||
| - | </arg> | ||
| - | <arg> | ||
| - | <External> | ||
| - | <content> | ||
| - | <Expr> | ||
| - | <op><Const type="rif:iri">op:assign</Const></op> | ||
| - | <arg><Var>y</Var></arg> | ||
| - | <arg> | ||
| - | <External> | ||
| - | <content> | ||
| - | <Expr> | ||
| - | <op><Const type="rif:iri">op:numeric-multiply</Const></op> | ||
| - | <arg><Var>y</Var></arg> | ||
| - | <arg><Var>s</Var></arg> | ||
| - | </Expr> | ||
| - | </content> | ||
| - | </External> | ||
| - | </arg> | ||
| - | </Expr> | ||
| - | </content> | ||
| - | </External> | ||
| - | </arg> | ||
| - | </Atom> | ||
| - | </then> | ||
| - | </Implies> | ||
| - | </sentence> | ||
| - | |||
| - | <sentence id="xtt_table1_row2"> | ||
| - | <Implies> | ||
| - | <if> | ||
| - | <Equal> | ||
| - | <side><Var>x</Var></side> | ||
| - | <side><Const type="xsd:decimal">0</Const></side> | ||
| - | </Equal> | ||
| - | </if> | ||
| - | <then> | ||
| - | <Atom> | ||
| - | <op><Const type="rif:iri">xtt:run_many</Const></op> | ||
| - | <arg> | ||
| - | <External> | ||
| - | <content> | ||
| - | <Expr> | ||
| - | <op><Const type="rif:iri">op:assign</Const></op> | ||
| - | <arg><Var>y</Var></arg> | ||
| - | <arg><Const type="xsd:decimal">1</Const></arg> | ||
| - | </Expr> | ||
| - | </content> | ||
| - | </External> | ||
| - | </arg> | ||
| - | <arg> | ||
| - | <External> | ||
| - | <content> | ||
| - | <Expr> | ||
| - | <op><Const type="rif:iri">xtt:return</Const></op> | ||
| - | <arg><Var>s</Var></arg> | ||
| - | <arg><Var>x</Var></arg> | ||
| - | <arg><Var>y</Var></arg> | ||
| - | </Expr> | ||
| - | </content> | ||
| - | </External> | ||
| - | </arg> | ||
| - | </Atom> | ||
| - | </then> | ||
| - | </Implies> | ||
| - | </sentence> | ||
| - | |||
| - | <sentence id="xtt_table2_row3"> | ||
| - | <Implies> | ||
| - | <if> | ||
| - | <And> | ||
| - | <formula> | ||
| - | <External> | ||
| - | <content> | ||
| - | <Atom> | ||
| - | <op><Const type="rif:iri">op:numeric-greater-than</Const></op> | ||
| - | <arg><Var>x</Var></arg> | ||
| - | <arg><Const type="xsd:decimal">0</Const></arg> | ||
| - | </Atom> | ||
| - | </content> | ||
| - | </External> | ||
| - | </formula> | ||
| - | <formula> | ||
| - | <Equal> | ||
| - | <side><Var>s</Var></side> | ||
| - | <side><Const type="xsd:decimal">1</Const></side> | ||
| - | </Equal> | ||
| - | </formula> | ||
| - | </And> | ||
| - | </if> | ||
| - | <then> | ||
| - | <Atom> | ||
| - | <op><Const type="rif:iri">xtt:return</Const></op> | ||
| - | <arg><Var>s</Var></arg> | ||
| - | <arg><Var>x</Var></arg> | ||
| - | <arg><Var>y</Var></arg> | ||
| - | </Atom> | ||
| - | </then> | ||
| - | </Implies> | ||
| - | </sentence> | ||
| - | |||
| - | </Group> | ||
| - | </code> | ||
| - | Obie tablice w formacie xml: {{:pl:miw:miw08_xtt_rif:factorial.xml|factorial.xml}}, {{:pl:miw:miw08_xtt_rif:factorial1.xml|factorial1.xml}} | ||
| - | ---- | ||
| - | Powyższy przykład został zwalidowany za pomocą dostępnych arkuszy XSD. Jedyny element, który zgłasza błędy jest to parametr ''id'', aczkolwiek ze względu na brak walidacji niektórych przykładów obecnych w dokumentacji, nie należy się tym przejmować. Nigdzie w dokumentacji nie ma wyraźnego zakazu wykorzystywania elementów standardu XML. | ||
| + | ==== Sugestie/Braki w RIF ==== | ||
| + | * Możliwość umieszczania kilku elementów ''Group'' w jednym pliku | ||
| + | * Identyfikowanie poszczególnych ''Group'', ''sentence'', np. poprzez parametr ''id'' | ||
| + | * Uproszczenie zapisu w xml ''External schema'', bo w tej chwili zapis powoduje spory rozrost pliku i zmniejsza czytelność | ||
| + | * "Wywoływanie" większej ilości predykatów w konkluzji | ||
| FIXME | FIXME | ||
| - | * runmany, etc | + | * ^_^runmany, etc |
| - | * zestawienie wprowadzonych predykatów iri:xtt_... -> odn. do ew. impl. | + | * ^_^zestawienie wprowadzonych predykatów iri:xtt_... -> odn. do ew. impl. |
| - | * ew. lista sugestii/ograniczeń w rif (id reguł) | + | * ^_^ew. lista sugestii/ograniczeń w rif (id reguł) |
| ==== Translacja XTTML => RIF ==== | ==== Translacja XTTML => RIF ==== | ||
