Both sides previous revision
Poprzednia wersja
Nowa wersja
|
Poprzednia wersja
|
pl:miw:miw08_xtt_rif [2008/05/28 11:33] 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 ===== |
| |
Ten normatywny rozdział, określa składnię RIF-BLD bezpośrednio, bez opierania się na RIF-FLD. Definiuje się składnię prezentacji oraz składnię XML. Składnia prezentacji **nie ma być konkretną składnią** dla RIF-BLD. Jest zdefiniowana przy pomocy języka matematycznego (ang. mathematical English) i powinna być wykorzystywana w przykładach i definicjach. Składnia ta celowo pomija szczegóły, takie jak separatory różnych komponentów syntaktycznych, symboli ucieczki (ang. escape symbols), **parenthesizing**, pierwszeństwo operatorów i podobne. Ponieważ RIF jest formatem wymiany, używa XML jako konkretnej składni. | Ten normatywny rozdział, określa składnię RIF-BLD bezpośrednio, bez opierania się na RIF-FLD. Definiuje się składnię prezentacji oraz składnię XML. Składnia prezentacji **nie ma być konkretną składnią** dla RIF-BLD. Jest zdefiniowana przy pomocy języka matematycznego (ang. mathematical English) i powinna być wykorzystywana w przykładach i definicjach. Składnia ta celowo pomija szczegóły, takie jak separatory różnych komponentów syntaktycznych, symboli ucieczki (ang. escape symbols), **parenthesizing**, pierwszeństwo operatorów i podobne. Ponieważ RIF jest formatem wymiany, używa XML jako konkretnej składni. |
| |
| |
| |
==== Alfabet ==== | ==== Alfabet ==== |
//[[http://www.w3.org/2005/rules/wg/draft/rif-bld/#Alphabet_of_RIF-BLD|Alphabet of RIF-BLD]]//\\ | //[[http://www.w3.org/2005/rules/wg/draft/rif-bld/#Alphabet_of_RIF-BLD|Alphabet of RIF-BLD]]//\\ |
| |
Alfabet RIF-BLD składa się z dowolnej //(ang. countably infinite)// liczby: | Alfabet RIF-BLD składa się z dowolnej //(ang. countably infinite)// liczby: |
* **stałych symboli**: ''Const'' | * **stałych symboli**: ''Const'' |
| |
| |
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: |
| |
Zbiór wszystkich przestrzeni symboli, które dzielą ''Const'' jest uważany za część **języka logiki** RIF-FLD. | Zbiór wszystkich przestrzeni symboli, które dzielą ''Const'' jest uważany za część **języka logiki** RIF-FLD. |
| |
| |
| |
==== Termy ==== | ==== Termy ==== |
| //[[http://www.w3.org/2005/rules/wg/draft/rif-bld/#Terms|Terms]]//\\ |
| |
RIF-BLD wspiera kilka rodzajów termów: //stałych// i //zmiennych//, //termów pozycjonowanych//, //termów z nazwanymi argumentami//, //równości//, //przynależności do klasy// oraz //formuł atomicznych podklasy//, i //formuły ramowe//. Słowo "term" będzie używane zastępczo do każdego z tych określeń. | RIF-BLD wspiera kilka rodzajów termów: //stałych// i //zmiennych//, //termów pozycjonowanych//, //termów z nazwanymi argumentami//, //równości//, //przynależności do klasy// oraz //formuł atomicznych podklasy//, i //formuły ramowe//. Słowo "term" będzie używane zastępczo do każdego z tych określeń. |
=== Definicja === | === Definicja === |
Termy klasyfikujące, podklas i ramowe są używane do opisu obiektów i hierarchii klas. | Termy klasyfikujące, podklas i ramowe są używane do opisu obiektów i hierarchii klas. |
| |
=== Poprawne formułowanie Termów (Well-formedness of Terms)=== | === Poprawne formułowanie Termów === |
Zbiór wyszystkich symboli, ''Const'', jest podzielony na: | //[[http://www.w3.org/2005/rules/wg/draft/rif-bld/#Well-formedness_of_Terms|Well-formedness of Terms]]//\\ |
| |
| 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. |
| |
==== Formuły ==== | ==== Formuły ==== |
| //[[http://www.w3.org/2005/rules/wg/draft/rif-bld/#Formulas|Formulas]]//\\ |
| |
Każdy term (pozycjonowany, lub z nazwanymi argumentami) postaci ''p(...)'' (lub ''External(p(...)''), gdzie ''p'' jest symbolem predykatu, jest również formułą atomiczną. Termy równościowe, klasyfikujące, podklas oraz ramowe również są formułami atomicznymi. Formuła postaci ''External(p(...))'' też jest nazywana zewnętrznie zdefiniowaną formułą atomiczną. | Każdy term (pozycjonowany, lub z nazwanymi argumentami) postaci ''p(...)'' (lub ''External(p(...)''), gdzie ''p'' jest symbolem predykatu, jest również formułą atomiczną. Termy równościowe, klasyfikujące, podklas oraz ramowe również są formułami atomicznymi. Formuła postaci ''External(p(...))'' też jest nazywana zewnętrznie zdefiniowaną formułą atomiczną. |
| |
* //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)''. |
| |
| |
| |
==== Gramatyka warstwy prezentacji (EBNF) ==== | ==== Gramatyka warstwy prezentacji (EBNF) ==== |
| //[[http://www.w3.org/2005/rules/wg/draft/rif-bld/#EBNF_Grammar_for_the_Presentation_Syntax_of_RIF-BLD|EBNF Grammar for the Presentation Syntax of RIF-BLD]]//\\ |
| |
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. |
| |
| |
===== Bezpośrednia specyfikacja semantyki RIF-BLD ===== | ===== Bezpośrednia specyfikacja semantyki RIF-BLD ===== |
==== Wartości Prawdy (Truth Values) ==== | ==== Wartości Prawdy ==== |
| //[[http://www.w3.org/2005/rules/wg/draft/rif-bld/#Truth_Values|Truth Values]]//\\ |
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''. |
| |
| |
| |
| |
==== Konstrukcje Semantyczne ==== | ==== Konstrukcje Semantyczne ==== |
| //[[http://www.w3.org/2005/rules/wg/draft/rif-bld/#Semantic_Structures|Semantic Structures]]//\\ |
| |
Kluczowym pojęciem w modelowo-teoretycznej semntyce języka logiki jest pojęcie struktury semantycznej. Definicja (poniżej) jest trochę ogólniejsza niż to potrzebne. Została tak napisana, aby lepiej można było zrozumieć związek z semantyką framewora RIF. | Kluczowym pojęciem w modelowo-teoretycznej semntyce języka logiki jest pojęcie struktury semantycznej. Definicja (poniżej) jest trochę ogólniejsza niż to potrzebne. Została tak napisana, aby lepiej można było zrozumieć związek z semantyką framewora RIF. |
| |
**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: |
| |
| |
| ==== Interpretacja Formuł ==== |
| //[[http://www.w3.org/2005/rules/wg/draft/rif-bld/#Interpretation_of_Formulas|Interpretation of Formulas]]//\\ |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
==== Interpretacja Formuł ==== | |
**Definicja oszacowania prawdy (ang. Truth valuation)**\\ | **Definicja oszacowania prawdy (ang. Truth valuation)**\\ |
Oszacowanie prawdy dla dobrze sformułowanej formuły w RIF-BLD jest wyznaczane przy pomocy następującej funkcji, oznaczanej jako ''TValI'': | Oszacowanie prawdy dla dobrze sformułowanej formuły w RIF-BLD jest wyznaczane przy pomocy następującej funkcji, oznaczanej jako ''TValI'': |
| |
==== Logical Entailment ==== | ==== Logical Entailment ==== |
| //[[http://www.w3.org/2005/rules/wg/draft/rif-bld/#Logical_Entailment|Logical Entailment]]//\\ |
| |
Pomimo, że meta-dane, związane z formułami RIF-BLD są ignorowane przez semantykę, mogą być wydobyte poprzez narzędzia XML'a. Ponieważ meta-dane są przedstawiane za pomocą termów ramowych, mogą być uzasadnione regułami RIF-BLD. | Pomimo, że meta-dane, związane z formułami RIF-BLD są ignorowane przez semantykę, mogą być wydobyte poprzez narzędzia XML'a. Ponieważ meta-dane są przedstawiane za pomocą termów ramowych, mogą być uzasadnione regułami RIF-BLD. |
| |
==== Zapis w XML języka warunkowego ==== | ==== Zapis w XML języka warunkowego ==== |
| //[[http://www.w3.org/2005/rules/wg/draft/rif-bld/#XML_for_the_RIF-BLD_Condition_Language|XML for the RIF-BLD Condition Language]]//\\ |
| |
Wykorzystujemy następujące tagi: | Wykorzystujemy następujące tagi: |
<code>- And (conjunction) | <code>- And (conjunction) |
| |
==== Zapis w XML języka reguł ==== | ==== Zapis w XML języka reguł ==== |
| //[[http://www.w3.org/2005/rules/wg/draft/rif-bld/#XML_for_the_RIF-BLD_Rule_Language|XML for RIF-BLD Rule Language]]//\\ |
| |
Jest to rozszerzenie języka warunkowego, o: | Jest to rozszerzenie języka warunkowego, o: |
<code>- Group (nested collection of sentences annotated with metadata) | <code>- Group (nested collection of sentences annotated with metadata) |
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 ==== |