Both sides previous revision
Poprzednia wersja
Nowa wersja
|
Poprzednia wersja
|
pl:miw:miw08_xtt_rif [2008/05/28 11:42] miw |
pl:miw:miw08_xtt_rif [2019/06/27 15:50] (aktualna) |
====== Opis ====== | ====== Opis ====== |
| __**Projekt zakończony**__ |
| |
Mateusz Mazur, <m-a-t-i@o2.pl> | Mateusz Mazur, <m-a-t-i@o2.pl> |
| |
* 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 ====== |
//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 ===== |
| |
| |
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: |
//[[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) |
* 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. |
* //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)''. |
| |
| |
| |
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. |
| |
| |
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''. |
| |
| |
| |
| |
**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: |
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''. |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
<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 --> |
Parametry ''id'' zostały dodane do tag'ów ''Group'' oraz ''sentence''. Ich zadaniem jest oznaczenie poszczególnych tablic i wierszy, aby można było sterować wnioskowaniem (XTT link). Do sterowania wnioskowaniem w części wynikowej reguły używany jest predykat ''xtt:concl/2'' pierwszy argument to ''xtt:next_table_rule/2'' lub ''xtt:next_table/1''. Drugim argumentem jest wywołanie dowolnego predykatu. Aby wywołać więcej niż jeden, można użyć ''xtt:run_many''. | Parametry ''id'' zostały dodane do tag'ów ''Group'' oraz ''sentence''. Ich zadaniem jest oznaczenie poszczególnych tablic i wierszy, aby można było sterować wnioskowaniem (XTT link). Do sterowania wnioskowaniem w części wynikowej reguły używany jest predykat ''xtt:concl/2'' pierwszy argument to ''xtt:next_table_rule/2'' lub ''xtt:next_table/1''. Drugim argumentem jest wywołanie dowolnego predykatu. Aby wywołać więcej niż jeden, można użyć ''xtt:run_many''. |
| |
Aby zapisać warunek gdzie zmienna należy do np. ''{1,5}u8'' w RIF posłużono się następującą konstrukcją: | Jako, że XTT posługuje się również parametrami będącymi zbiorami (zapisywane przez ''{V}''), należało stworzyć konstrukcję o podobnym działaniu w RIF. Moja propozycja jest taka, aby taki parametr identyfikować predykatem ''xtt:set/2'' definiujący zbiór od liczby ''a'' do ''b''. Aby zapisać znienną ''{a,b}uC'', gdzie C jest pojedyńczym elementem, bądź innym przedziałem, w RIF posłużono się następującą konstrukcją: |
<code xml><Atom> | <code xml><Atom> |
<op><Const type="rif:iri">in</Const></op> <!-- przynależność do zbioru --> | <op><Const type="rif:iri">xtt:complex_set</Const></op> |
<arg><Var>att_0</Var></arg> | <arg> |
<arg> <!-- {1,5} --> | |
<External> | <External> |
<content> | <content> |
<Expr> | <Expr> |
<op><Const type="rif:iri">xtt:set</Const></op> | <op><Const type="rif:iri">xtt:set</Const></op> |
<arg><Const type="xsd:decimal">1</Const></arg> | <arg><Const type="xsd:decimal">a</Const></arg> |
<arg><Const type="xsd:decimal">5</Const></arg> | <arg><Const type="xsd:decimal">b</Const></arg> |
</Expr> | </Expr> |
</content> | </content> |
</External> | </External> |
</arg> | </arg> |
<arg><Const type="xsd:decimal">8</Const></arg> <!-- u8 --> | <arg> |
| <Const type="xsd:decimal">C</Const> |
| </arg> |
</Atom></code> | </Atom></code> |
| |
**Uwagi**\\ | Zapis przyrównania zmiennej do zbioru (''X = {1,2,4}'') będzie realizowany za pomocą tagu ''Equal'': |
* Każda tablica (element ''Group'') musi być w osobnym pliku (zgodność z plikami xsd). | <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.// |
| |
=== Przykład 1: calculations (factorial) === | === Wykorzystywane predykaty === |
<code> | 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]]. |
|----------------------------------------------------| | |
| | | |
| 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"> | ^Predykat ^External schema ^Opis ^ |
<Implies> | | xtt:set |''(?arg1 ?arg2; pred:set(?arg1, ?arg2))'' |Predykat definiuje zbiór liczb z zakresu. Odpowiednik ''{arg1, arg2}''. | |
<if> | | xtt:complex_set |''(?arg1 ?arg2 [...]; pred:complex_set(?arg1, ?arg2, [...]))'' |Predykat definiuje złożony zbiór. Za argumenty może przyjmować nie tylko liczby całkowite, ale również predykaty ''xtt:set''. | |
<External> | | xtt:next_table_rule |''(?arg1 ?arg2 ?arg3; pred:next_table_rule(?arg1, ?arg2, ?arg3))'' |Predykat sterujący wnioskowaniem. Pierwszy argument to ''id'' tabeli, która powinna być wywołana jako następna (''id'' taga ''Group''). Drugi - ''id'' konkretnego wiersza owej tabeli (''id'' taga ''sentence''). Ostatni parametr to operacja, jaką należy wykonać przy wykonaniu reguły. | |
<content> | | 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. | |
<Atom> | | 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. | |
<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"> | 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>''. |
<sentence id="xtt_table2_row1"> | |
<Implies> | **Uwagi**\\ |
<if> | * Każda tablica (element ''Group'') musi być w osobnym pliku (zgodność z plikami xsd). |
<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 ==== |