Opis

Projekt zakończony

Mateusz Mazur, m-a-t-i@o2.pl

translacja XTTML → RIF

Projekt

Sprawozdanie


W oparciu o dokumentację z 15.04.2008 (rif_bld_fld_freez.zip)


Wprowadzenie do RIF

Format RIF jest ciągle w fazie rozwoju, jedyne dostępne dokumenty są to szkice specyfikacji poszczególnych modułów (Working Draft). Do rozwijanych dokumentów należą m.in. (istotne według mnie dla projektu):

Już w obecnej fazie prac, można znaleźć projekty zainteresowane wykorzystaniem RIFa.

Od strony teoretycznej RIF-BLD (the Basic Logic Dialect of the Rule Interchange Format) odpowiada językowi klauzul Horna z równością oraz standardową semantyką aksjomatyczną (ang. definite Horn rules with equality and with a standard first-order semantics). RIF-BLD jest definiowany na dwa sposoby. Po pierwsze jako specjalizacja RIF-FLD (the RIF Framework for Logic-based Dialects) - jest to bardzo zwięzły opis, ale wymaga znajomości RIF-FLD. FLD dostarcza ogólnego frameworku - zarówno syntaktycznego i semantycznego, co umożliwia definiowanie dialektów RIFa. Drugi sposób jest to definiowanie RIF-BLD niezależnie od frameworku. Korzyścią tego podejścia jest szybsze pojęcie składni formatu, lecz mniejsza znajomość możliwości jego rozszerzania.

Bezpośrednia specyfikacja składni RIF-BLD

Direct Specification of RIF-BLD Syntax

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

Alphabet of RIF-BLD

Alfabet RIF-BLD składa się z dowolnej (ang. countably infinite) liczby:

  • stałych symboli: Const
  • zmiennych symboli (rozłącznych z Const): Var
  • nazw argumentów (rozłącznych z Const i Var): ArgNames
  • łączników: And, Or, :-
  • kwantyfikatorów: Exists, ForAll
  • symboli: =, #, ##, oraz External
  • symbolu grupującego: Group
  • pomocniczych symboli: np. „(”, „)”, „[”, „]” oraz „^^

Zbiór łączników, kwantyfikatorów, =, itp., jest rozłączny z Const oraz Var. Nazwy argumentów w ArgNames są zapisywane jako stringi w Unicode i nie mogą zaczynać się od „?”. Zmienne są zapisywane jako stringi w Unicode poprzedzone przez „?”.

Stałe są zapisywane jako „literal”^^symspace, gdzie literal jest sekwencją znaków Unicode, a symspace jest identyfikatorem przestrzeni symboli. Przestrzeni symboli są zdefiniowane w Rozdziale Symbol Spaces dokumentu RIF-FLD. Ostatecznie definicja Przestrzeni symboli będzie się znajdować w dokumencie Data Types and Builtins.

Symbole =, # oraz ## są używane w formułach, które definiują równość, przynależenie do klas oraz związki pomiędzy podklasami. Symbol jest wykorzystywany w termach, które mają nazwane argumenty oraz w formułach ramowych (ang. frame forumula). Symbol External wskazuje, że formuła atomiczna albo term funkcji (ang. function term) jest zdefiniowany na zewnątrz (np. jest wbudowany).

Symbol Group używa się do organizowania reguł RIF-BLD w kolekcje oraz do dodawania adnotacji w postaci meta-danych (ang. annotate them with metadata).

Język RIF-BLD jest zbiorem formuł zbudowanych przy pomocy alfabetu i zgodnie z regułami podanymi poniżej.

Przestrzenie symboli (z RIF-FLD)

W tym dokumencie będziemy używać następujących prefiksów:

Skłania typu xsd:string powinna być rozumiana jako zwarty URI (CURIE) - makro, które jest rozwija związek ciągu znaków oznaczaną przez prefiks xsd oraz string string. Notacja zwartych URI nie jest częścią składni RIF, lecz zabiegiem zaoszczędzającym miejsce w zapisie.

Zbiór wszystkich stałych symboli w dialekcie RIF jest podzielony na podzbiory, zwane przestrzeniami symboli, wykorzystywanymi do reprezentowania typów danych w schematach XML, oraz typów danych zdefiniowanych w innych specyfikacjach W3C, jak rdf:XMLLiteral. Są one również używane do odróżniania zbiorów stałych. Wszystkie stałe symbole mają składnię (czasem również semantykę), narzuconą przez przestrzeń symboli, do której należą.

Definicja przestrzeni symboli
Przestrzeń symboli jest nazwanym podzbiorem zbioru wszystkich stałych, Const. Aspekty semantyczne przestrzeni symboli będą opisane w rozdziale Semantic Framework. Każdy symbol z Const należy do dokładnie jednej przestrzeni symboli.

Każda przestrzeń symboli posiada związaną przestrzeń leksykalną, unikalny identyfikator oraz, prawdopodobnie, jeden lub więcej alias. Dokładniej:

  • Przestrzeń leksykalna przestrzeni symboli, jest niepustym zbiorem ciągów znaków (string) Unicode.
  • Identyfikator przestrzeni symboli jest sekwencją znaków Unicode, które tworzą kompletne IRI.
  • Alias jest również sekwencją znaków Unicode, ale nie musi mieć postaci kompletnego IRI.
  • Inne przestrzenie symboli nie mogą posiadać tych samych identyfikatorów czy aliasów.

Identyfikatory i aliasy przestrzeni symboli nie są same w sobie symbolami stałymi w RIF.

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:

"literal"^^symspace

Gdzie literal to część leksykalna symbolu, a symspace, jest identyfikatorem lub aliasem przestrzeni symboli. W tym wypadku literal jest sekwencją znaków Unicode, która musi być elementem z przestrzeni leksykalnej, należącej do przestrzeni symboli symspace. Na przykład „1.2”^^xsd:decimal oraz „1”^^xsd:decimal są prawidłowymi symbolami, ponieważ 1.2 oraz 1 należą do przestrzeni leksykalnej typu danych xsd:decimal schematu XML. Z drugiej strony „a+2”^^xsd:decimal nie jest poprawnym symbolem, ponieważ a+2 nie należy do przestrzeni leksykalnej xsd:decimal.

Zbiór wszystkich przestrzeni symboli, które dzielą Const jest uważany za część języka logiki RIF-FLD.

Termy

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ń.

Definicja

Podstawową konstrukcją języka są termy. Wyróżniamy:

  • Stałe i zmienne. Jeśli t należy do Const albo t należy do Var to t jest prostym termem (ang. simple term).
  • Termy pozycjonowane (ang. positional terms). Jeśli t należy do Const oraz t_1, …, t_n są termami prostymi, pozycjonowanymi lub z nazwanymi argumentami, to t(t_1 … t_n) jest termem pozycjonowanym.
  • Termy z nazwanymi argumentami (ang. terms with named arguments). Są to termy postaci t(s_1→v_1 … s_n→v_n), gdzie t należy do Const oraz t_1, …, t_n są termami prostymi, pozycjonowanymi lub z nazwanymi argumentami oraz s_1, …, s_npairwise, różnymi symbolami ze zbioru ArgNames.

Term t reprezentuje predykat bądź funkcję; s_1, …, s_n to nazwy argumentów; v_1 , …, v_n - wartości argumentów. Termy z nazwanymi argumentami są jak zwykłe termy pozycjonowane, z tym że argumenty są nazwane a ich kolejność jest nieistotna. Warto zauważyć, że term bez argumentów, np. f(), jest zarówno pozycjonowany jak i z nazwanymi argumentami.

  • Termy równościowe (ang. equality terms). Jeśli t oraz s są termami prostymi, pozycjonowanymi lub z nazwanymi argumentami, to t = s jest termem równościowym.
  • Termy klasyfikujące (ang. class membership terms/just membership terms). t#s jest termem klasyfikującym, jeśli t oraz s są termami prostymi, pozycjonowanymi lub z nazwanymi argumentami.
  • Termy podklas (ang. subclass terms). t##s jest termem podklasy jeśli t oraz s są termami prostymi, pozycjonowanymi lub z nazwanymi argumentami.
  • Termy ramowe (ang. frame terms). t[p_1→v_1 … p_n→v_n] jest termem ramowym (ramą) jeśli t, p_1, …, p_n, v_1, …, v_n, n >= 0, są termami prostymi, pozycjonowanymi lub z nazwanymi argumentami.
  • Termy zdefiniowane zewnętrznie (ang. externally defined terms). Jeśli t jest termem, to External(t) jest termem zdefiniowanym zewnętrznie.

Takie termy są wykorzystywane do reprezentowania wbudowanych funkcji oraz predykatów, jak również „dołączanych proceduralnie” termów czy predykatów, które mogą istnieć w różnych systemach regułowych, ale nie są określone przez RIFa.

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

Zbiór wszystkich symboli, Const, jest podzielony na:

  • Pozycjonowane symbole predykatów (ang. positional predicate symbols)
  • Symbole predykatów z nazwanymi argumentami (ang. predicate symbols with named arguments)
  • Pozycjonowane symbole funkcji (ang. positional function symbols)
  • Symbole funkcji z nazwanymi argumentami (ang. function symbols with named arguments)
  • Osobniki (ang. individuals).

Symbole w Const, które są wspieranymi przez RIF typami danych są osobnikami.

Każdy symbol predykatu i funkcji ma dokładnie jedną arność.

  • Dla symboli pozycjonowanych, arność to nieujemna liczba całkowita (integer), mówiąca ile argumentów dany symbol przyjmuje.
  • 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ź osobnika) nie jest określona w RIF-BLD kategorycznie. Przeciwnie, jest ona wnioskowana jak następuje:

  • 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 symbol funkcji o określonej arności
    • jako symbol predykatu o określonej arności.
  • 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.

Dla termu postaci External(t) bycie dobrze sformułowanym oznacz, że t musi być instancją zewnętrznego schematu (ang. external schema), np. schematem zewnętrznie określonego termu, jak to zostało zdefiniowane w Rozdziale Schemas for Externally Defined Terms of RIF-FLD.

Jeśli term postaci External(p(…)) pojawi się jako formuła atomiczna, to p jest uważane za predykat. Definicja zewnętrznych schematów (ang. external schemas) ostatecznie pojawi się w dokumencie Data Types and Builtins.

Formuły

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ą.

Proste termy (stałe i zmienne) nie są formułami. Nie wszystkie formuły atomiczne są dobrze sformułowane (ang. well-formed). Dobrze sformułowana formuła atomiczna, to taka, która jest również dobrze sformułowanym termem. Bardziej ogólne formuły są budowane z formuł atomicznych z pomocą łączników logicznych (ang. logical connectives).

Definicja dobrze sformułowanej formuły

Dobrze sformułowana formuła posiada jedną z poniższych postaci:

  • 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.
  • 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.

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(…)).
  • 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ą 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ż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ę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)

EBNF Grammar for the Presentation Syntax of RIF-BLD

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 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 wykorzystywana jako separator.
  • Składnia EBNF nie jest normatywna.

Definicja języka warunkowego:

  FORMULA        ::= 'And' '(' FORMULA* ')' |
                     'Or' '(' FORMULA* ')' |
                     'Exists' Var+ '(' FORMULA ')' |
                     ATOMIC |
                     'External' '(' ATOMIC ')'
  ATOMIC         ::= Atom | Equal | Member | Subclass | Frame
  Atom           ::= UNITERM
  UNITERM        ::= Const '(' (TERM* | (Name '->' TERM)*) ')'
  Equal          ::= TERM '=' TERM
  Member         ::= TERM '#' TERM
  Subclass       ::= TERM '##' TERM
  Frame          ::= TERM '[' (TERM '->' TERM)* ']'
  TERM           ::= Const | Var | Expr | 'External' '(' Expr ')'
  Expr           ::= UNITERM
  Const          ::= '"' UNICODESTRING '"^^' SYMSPACE
  Name           ::= UNICODESTRING
  Var            ::= '?' UNICODESTRING
  SYMSPACE       ::= UNICODESTRING

Definicja reguł RIF-BLD:
Składnia prezentacji dla reguł Horna, rozszerza definicje języka warunkowego o następujące produkcje:

  Group    ::= 'Group' IRIMETA? '(' (RULE | Group)* ')'
  IRIMETA  ::= Frame
  RULE     ::= 'Forall' Var+ '(' CLAUSE ')' | CLAUSE
  CLAUSE   ::= Implies | ATOMIC
  Implies  ::= ATOMIC ':-' FORMULA

Przykłady zapisu, można znaleźć tutaj.

Bezpośrednia specyfikacja semantyki RIF-BLD

Wartości Prawdy

Truth Values

Zbiór TV wartości prawdy w RIF-BLD składa się z dwóch wartości: t oraz f.

Konstrukcje Semantyczne

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.

Definicja (Struktura Semantyczna)
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:

  1. IC odwzorowuje Const na D. To odwzorowanie objaśnia stałe symbole. Dodatkowo:
    • Jeśli stała c należy do Const, oznacza osobnika, to jest wymagane, by IC© należało do Dind.
    • Jeśli stała c należy do Const, oznacza symbol funkcyjny (pozycjonowany, lub z nazwanymi argumentami), to jest wymagane, by IC© należało do Dfunc.
  2. IV odwzorowuje Var na Dind. To odwzorowanie objaśnia zmienne symbole.
  3. IF odwzorowuje D na funkcje D*ind → D (tutaj D*ind jest zbiorem wszystkich sekwencji dowolniej skończonej długości na zbiorze Dind). To odwzorowanie objaśnia termy pozycjonowane. Dodatkowo:
    • Jeśli d należy do Dfunc, to IF(d) musi być funkcją D*ind → Dind.
    • Oznacza to, że kiedy symbol funkcyjny jest stosowany do argumentów, które są osobnymi obiektami, to wynik jest również osobnym obiektem.
  4. ISF jest zupełnym odwzorowaniem z D na zbiór zupełny funkcji postaci SetOfFiniteSets(ArgNames x Dind) → D. To odwzorowanie określa symbole funkcyjne z nazwanymi argumentami. Dodatkowo:
    • Jeśli d należy do Dfunc, to ISF(d) musi być funkcją SetOfFiniteSets(ArgNames x Dind) → Dind.
    • Jest to analogiczne do interpretacji termów pozycjonowanych, z dwoma różnicami: *
      • Każda para <s,v> należąca do ArgNames x Dind reprezentuje pary argument/wartość, zamiast reprezentować tylko wartość w wypadku termu pozycjonowanego.
      • Argumenty termu z nazwanymi argumentami stanowią skończony zbiór par argumentów/wartości, a nie skończoną listę elementów. Więc kolejność elementów nie ma znaczenia.
  5. Iframe jest zupełnym odwzorowaniem z Dind na zupełny zbiór funkcji postaci SetOfFiniteBags(Dind x Dind) → D.
    • To odwzorowanie przedstawia termy ramowe. Argument d należący do Dind do Iframe reprezentuje obiekt oraz skończoną rodzinę zbiorów (ang. bag) {<a1,v1>, …, <ak,vk>} przedstawiającą rodzinę zbiorów par atrybutów-wartości dla d. Niedługo zobaczymy jak Iframe jest wykorzystywany do określania oszacowania prawdy termu ramowego (ang. truth valuation of frame terms).
    • Rodziny zbiorów (multi-zbiory) są tu użyte, ponieważ kolejność par atrybut/wartość w ramie jest nieistotna a pary mogą się powtarzać: o[a→b a→b]. Takie powtórzenia powstają oczywiści kiedy pod zmienne są podstawiane stałe. Na przykład, o[?A→?B ?A→?B] staje się o[a→b a→b] jeśli pod zmienną ?A zostanie podstawiony symbol a, a pod ?B symbol b.
  6. Isub nadaje znaczenie relacji podklasom. Jest to zupełna funkcja Dind x Dind → D.
    • Operator ## jest musi być przechodni, t.j., c1 ## c2 i c2 ## c3 z tego musi wynikać c1 ## c3. Jest to zapewnione poprzez obostrzenie w rozdziale dotyczącym interpretacji fotmuł (Interpretation of Formulas).
  7. Iisa nadaje znaczenie przynależeniu do klas. Jest to zupełna funkcja Dind x Dind → D.
    • Przynależności # oraz ## muszą posiadać własność, że wszyscy członkowie podklasy są również członkami klasy wyżej (ang. superclass), t.j. o # cl oraz cl ## scl z tego musi wynikać o # scl. Jest to zapewnione prze obostrzenie w rozdziale dotyczącym interpretacji fotmuł (Interpretation of Formulas).
  8. I= jest to zupełna funkcja Dind x Dind → D. Daje ona znaczenie operatorowi równości.
  9. Itruth jest zupełnym odwzorowaniem D → TV. Jest wykorzystywane do definiowania oceny prawdziwości formuł.
  10. Iexternal to odwzorowanie z koherentnego zbioru schematów (ang. schemas) dla zewnętrznie zdefiniowanych funkcji, do funkcji zupełnych D* → D. Dla każdego zewnętrznego schematu s = (?X1 … ?Xn; t) w koherentnym zbiorze takich schematów związanych z językiem, Iexternal(s) jest funkcją postaci Dn → D.
    • Dla każdego zewnętrznego schematu s, związanego z językiem, zakłada się, że Iexternal(s) jest określone w jakimś zewnętrznym dokumencie (stąd nazwa zewnętrzny schemat). W szczególności, jeśli s jest schematem wbudowanego predykatu lub funkcji RIFa, Iexternal(s) jest określone w dokumencie Data Types and Builtins, po to aby:
      • Jeśli s jest schematem wbudowanej funkcji, to Iexternal(s) musi być funkcją zdefiniowaną we wspomnianym dokumencie.
      • Jeśli s jest schematem wbudowanego predykatu, to Itruth ο (Iexternal(s)) (złożenie Itruth i Iexternal(s), funkcja prawdziwa) musi być określona w Data Types and Builtins.

Dla wygody zostały również zdefiniowane odwzorowania I z termów na D:

  • I(k) = IC(k), jeśli k jest symbolem ze zbioru Const
  • I(?v) = IV(?v), jeśli ?v jest symbolem ze zbioru Var
  • I(f(t1 … tn)) = IF(I(f))(I(t1),…,I(tn))
  • I(f(s1→v1 … sn→vn)) = ISF(I(f))({<s1,I(v1)>,…,<sn,I(vn)>}) - Tutaj używamy {…} aby oznaczyć zbiór par argumentów/wartości.
  • I(o[a1→v1 … ak→vk]) = Iframe(I(o))({<I(a1),I(v1)>, …, <I(an),I(vn)>}) - Tutaj używamy {…} aby oznaczyć worek par atrybutów/wartości.
  • I(c1##c2) = Isub(I(c1), I(c2))
  • I(o#c) = Iisa(I(o), I©)
  • I(x=y) = I=(I(x), I(y))
  • I(External(t)) = Iexternsl(σ)(I(s1), …, I(sn)), jeśli t jest instancją zewnętrznego schematu s = (?X1 … ?Xn; t) przez podstawienie ?X1/s1 … ?Xn/s1.

Warto zauważyć, że z definicji, External(t) jest dobrze sformułowany tylko, jeśli t jest instancją zewnętrznego schematu. Ponadto, z definicji koherentnych zbiorów zewnętrznych schematów, wynika, że t może być instancją co najwyżej jednego schematu, aby I(External(t)) było dobrze sformułowane.

Wynik typów danych (ang. The effect of data types). Typy danych w DTS nakładają bastępujące ograniczenia. Jeśli dt jest identyfikatorem przestrzeni symboli typów danych, niech LSdt oznacza leksykalną przstrzeń dt, VSdt oznacza przestrzeń wartości oraz Ldt: LSdt → VSdt odwzorowanie przstrzeni leksykalnej w przestrzeń wartości (definicje tych pojęć są w rozdziale Primitive Data Types, RIF-FLD). To musi być zachowane:

  • VSdt jest podzbiorem lub równa się Dind; oraz
  • Dla każdej stałej „lit”^^dt należy do LSdt, IC(„lit”^^dt) = Ldt(lit).

To znaczy, że IC musi odwzorowywać stałe typów danych zgodnie z Ldt.

RIF-BLD nie nakłada ograniczeń na IC dla stałych w przestrzni leksykalnej, które nie odpowiadają podstawowym typom danych w DTS.

Interpretacja Formuł

Interpretation of Formulas

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:

  1. Pozycjonowane formuły atomiczne: TValI(r(t1 … tn)) = Itruth(I(r(t1 … tn))).
  2. Formuły atomiczne z nazwanymi argumentami: TValI(p(s1→v1 … sk→vk)) = Itruth(I(p(s1→v1 … sk→vk))).
  3. Równość: TValI(x = y) = Itruth(I(x = y)).
    • Aby zapewnić, że równość ma spodziewne własności, wymagane jest by:
      • Itruth(I(x = y)) = t wtedy i tylko wtedy, gdy I(x) = I(y) oraz, że Itruth(I(x = y)) = f w przeciwnym razie.
    • Jest to równoważne powiedzeniu, że TValI(x = y) = t if I(x) = I(y).
  4. Podklasa: TValI(sc ## cl) = Itruth(I(sc ## cl)).
    • Aby zapewnić, żeby operator ##był przechodni, musi być spelnione:
      • Dla wszystkich c1, c2, c3 należących do D, jeśli TValI(c1 ## c2) = TValI(c2 ## c3) = t to TValI(c1 ## c3) = t.
  5. Przynależność: TValI(o # cl) = Itruth(I(o # cl)).
    • Aby zapenić, że wszyscy członkowie podklas, są też członkami klasy głównej, wymagane jest:
      • Dla wszystkich o, cl, scl należących do D, jeśli TValI(o # cl) = TValI(cl ## scl) = t to TValI(o # scl) = t.
  6. Rama: TValI(o[a1→v1 … ak→vk]) = Itruth(I(o[a1→v1 … ak→vk])).
    • Ponieważ rózne pary atrybut/wartość powinny być rozumiane jako kombinacje, wymaga się by:
      • TValI(o[a1→v1 … ak→vk]) = t wtedy i tylko wtedy, gdy TValI(o[a1→v1]) = … = TValI(o[ak→vk]) = t.
  7. Zewnętrznie zdefiniowana formuła atomiczna: TValI(External(t)) = Itruth(Iexternal(s)(I(s1), …, I(sn))), jeśli t jest formułą atomiczną, która jest instancją zewnętrznego schematu s = (?X1 … ?Xn; t) poprzez podstawienie ?X1/s1 … ?Xn/s1.
    • Warto zauważyć, że zgodnie z definicją, External(t) jest dobrze sformułowany, jeśli t jest instancją zewnętrznego schematu. Ponadto, z definicji koherentnych zbiorów zewnętrznych schematów, t może być instancją co najwyżej jednego schemtu, aby I(External(t)) było dobrze sformułowane.
  8. Koniunkcja: TValI(And(c1 … cn)) = t wtedy i tylko wtedy, gdy TValI(ci) = t, dla wszystkich i = 1, …, n. W innym wypadku, TValI(And(c1 … cn)) = f.
    • Pusta koniunkcja jest traktowana jako tautologia, więc TValI(And()) = t.
  9. Alternatywa (Dysjunkcja): TValI(Or(c1 … cn)) = f wtedy i tylko wtedy, gdy TValI(ci) = f, dla wszystkich i = 1, …, n. W innym wypadku, TValI(And(c1 … cn)) = t.
  10. Kwantyfikacja:
    • TValI(Exists ?v1 … ?vn (s)) = t wtedy i tylko wtedy, gdy dla pewnego I*, opisanego poniżej, TValI*(s) = t.
    • TValI(Forall ?v1 … ?vn (s)) = t wtedy i tylko wtedy, gdy dla każego I*, opisanego poniżej, TValI*(s) = t.
    • I* jest to struktura semantyczna postaci <TV, DTS, D, Dind, Dfunc, IC, I*V, IF, Iframe, ISF, Isub, Iisa, I=, Iexternsl, Itruth>, która jest identyczna z I, poza tym, że odwzorowanie I*V, jest uzywane zamiast IV. I*V jest zdefiniowane tak, by pokrywać się z IV na wszystkich zmienny poza , possibly, on ?v1,…,?vn.
  11. Implikacja reguł:
    • TValI(conclusion :- condition) = t, jeśli TValI(conclusion)=t lub TValI(condition)=f.
    • TValI(conclusion :- condition) = f w innym wypadku.
  12. Grupy reguł:
    • Jeśli P jest grupową formułą postaci Group t (s1 … sn) lub Group (s1 … sn) to:
      • TValI(P) = t wtedy i tylko wtedy, gdy TValI(s1) = t, …, TValI(sn) = t.
      • TValI(P) = f w innym wypadku.
    • Oznacza to, że grupa reguł jest traktowana jako kombinacja. Meta-dane są ignorowane na potrzeby semantyki RIF-BLD.

Model grupy reguł, P, jest strukturą semantyczną I taką, że TValI(P) = t. W takim wypadku piszemy I |= P.

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.

Serializacja XML RIFa

Wszystkie tagi XML są podzielone na:

  • deskryptory klas (ang. class descriptors), zwane tagami typów (type tags),
  • deskryptory właściwości (ang. property descriptors), zwane tagami ról (role tags).

Będziemy używać nazw napisanych dużymi literami dla tagów typów, oraz małymi literami dla tagów ról.

Zapis w XML języka warunkowego

XML for the RIF-BLD Condition Language

Wykorzystujemy następujące tagi:

- And       (conjunction)
- Or        (disjunction)
- Exists    (quantified formula for 'Exists', containing declare and formula roles)
- declare   (declare role, containing a Var)
- formula   (formula role, containing a FORMULA)
- Atom      (atom formula, positional or with named arguments)
- External  (external call, containing a content role)
- content   (content role, containing an Atom, for predicates, or Expr, for functions)
- Member    (member formula)
- Subclass  (subclass formula)
- Frame     (Frame formula)
- object    (Member/Frame role, containing a TERM or an object description)
- op        (Atom/Expr role for predicates/functions as operations)
- arg       (positional argument role)
- upper     (Member/Subclass upper class role)
- lower     (Member/Subclass lower instance/class role)
- slot      (Atom/Expr/Frame slot role, containing a Prop)
- Prop      (Property, prefix version of slot infix '->')
- key       (Prop key role, containing a Const)
- val       (Prop val role, containing a TERM)
- Equal     (prefix version of term equation '=')
- Expr      (expression formula, positional or with named arguments)
- side      (Equal left-hand side and right-hand side role)
- Const     (individual, function, or predicate symbol, with optional 'type' attribute)
- Name      (name of named argument)
- Var       (logic variable)

Składnie XML dla przestrzeni symboli wykorzystuje atrybut typu, związany z elementami termów, jak Const. Na przykład <Const type=„xsd:dateTime”>2007-11-23T03:55:44-02:30</Const>.

Przykład 3a
Przykład ten obrazuje serializację XML dla warunkór RIFa.

Przykład 3b
Opisuje serializację warunku RIF, zawierającego termy z nazwanymi argumentami.

Zapis w XML języka reguł

XML for RIF-BLD Rule Language

Jest to rozszerzenie języka warunkowego, o:

- Group    (nested collection of sentences annotated with metadata)
- meta     (meta role, containing metadata, which is represented as a Frame)
- sentence (sentence role, containing RULE or Group)
- Forall   (quantified formula for 'Forall', containing declare and formula roles)
- Implies  (implication, containing if and then roles)
- if       (antecedent role, containing FORMULA)
- then     (consequent role, containing ATOMIC)

Przykład
Przykład prezentuje serializację reguły z przykładu 3, dotyczącego warstwy prezentacji.

Translacja pomiędzy składnią prezentacji a zapisem XML

Bardzo przejrzysty opis translacji pomiedzy tymi dwoma rodzajami zapisu jest umieszczony w dokumentacji do RIF-BLD. Jest on na tyle przejrzysty, że nie wymaga tłumaczenia na język polski.

Thermostat w RIF

Przykład reguł termostatu, zapisany za pomocą składni XML formatu RIF, znajduje się tutaj. Plik XML z thrermostatem: thermostat_v2.xml.

Próba werbalizacji RIF'a na przykładzie thermostatu

Opierając się o zapisane reguły thermostatu w RIF, udało mi się za pomocą XSLT wykonać prostą werbalizację:

If dayofweek is Monday or dayofweek is Tuesday or dayofweek is Wednesday or dayofweek is Thursday or dayofweek is Friday 
then thrm:is-workday( var dayofweek).

If dayofweek is Saturday or dayofweek is Sunday 
then thrm:is-weekend( var dayofweek).

If thrm:is-weekend(External fn:get-dayOfWeek-from-DateTime(var today)) is true 
And External op:numeric-between(External fn:hours-from-dateTime(var today), 9am, 5pm) is true 
then thrm:is-during-business-hours( var today).

If thrm:is-workday(External fn:get-dayOfWeek-from-DateTime(var today)) is true 
And External op:numeric-less-than(External fn:hours-from-dateTime(var today), 9am) is true 
then thrm:is-not-during-business-hours(var today).

If thrm:is-workday(External fn:get-dayOfWeek-from-DateTime(var today)) is true 
And External op:numeric-greater-than(External fn:hours-from-dateTime(var today), 5pm) is true 
then thrm:is-not-during-business-hours( var today).

If thrm:is-weekend(External fn:get-dayOfWeek-from-DateTime(var today)) is true 
then thrm:is-not-during-business-hours(var today).

If month is January or month is February or month is December then thrm:is-summer(var month).

If month is March or month is April or month is May then thrm:is-atumn(var month).

If month is June or month is July or month is August then thrm:is-winter(var month).

If month is September or month is October or month is November then thrm:is-spring(var month).

If thrm:is-spring(External fn:month-from-dateTime(var date)) is true 
And thrm:is-during-buisness-hours(var date) is true then thrm:thermostat-setting(20).

If thrm:is-spring(External fn:month-from-dateTime(var date)) is true 
And thrm:is-not-during-buisness-hours(var date) is true then thrm:thermostat-setting(15).

If thrm:is-summer(External fn:month-from-dateTime(var date)) is true 
And thrm:is-during-buisness-hours(var date) is true then thrm:thermostat-setting(24).

If thrm:is-summer(External fn:month-from-dateTime(var date)) is true 
And thrm:is-not-during-buisness-hours(var date) is true then thrm:thermostat-setting(27).

If thrm:is-atumn(External fn:month-from-dateTime(var date)) is true 
And thrm:is-during-buisness-hours(var date) is true then thrm:thermostat-setting(20).

If thrm:is-atumn(External fn:month-from-dateTime(var date)) is true 
And thrm:is-not-during-buisness-hours(var date) is true then thrm:thermostat-setting(16).

If thrm:is-winter(External fn:month-from-dateTime(var date)) is true 
And thrm:is-during-buisness-hours(var date) is true 
then thrm:thermostat-setting(18).

If thrm:is-winter(External fn:month-from-dateTime(var date)) is true 
And thrm:is-not-during-buisness-hours(var date) is true then thrm:thermostat-setting(14).

Treść arkusza XSLT znajduje się tutaj. Plik do pobrania: RIFverb.xml

Próba wizualizacji reguł RIF'a na przykładzie thermostatu

Kolejną podjętą przeze mnie próbą było wizualizowanie reguł.
:pl:miw:miw08_xtt_rif:rifvis.png
Arkusz XSLT służący do wizualizacji znajduje się tutaj. Plik do pobrania: RIFvis.xml

XTT Minicases

Analiza i próba zapisu za pomocą RIFa.

Wnioski:

  • Aby konkluzja mogła składać się z więcej niż jednego predykatu/zmiennej, trzeba stworzyć predykat, który to umożliwi.
  • Do sterowanie wnioskami można wykorzystać właściwość języka XML - nadawać elementom Group oraz sentence identyfikatory za pomocą id i odwoływać się do nich w jakimś predykacie (nie znalazłem informacji, żeby nie można było użyć id).
  • Do zapisu wielowartościowych atrybutów proponuję:
    • termy z nazwanymi argumentami dla zbiorów wartości.
    • termy pozycjonowane dla list wartości.

RIF a XTTML

Wstępne przmyślenia:

  • Do nadania identyfikatorów posłuży element spoza RIF, należący do języka XML - id.

Proponowany zapis

<Group id="xtt_table1"> <!-- definicja tabeli xtt -->
 <sentence id="xtt_table_row1"> <!-- definicja wiersza tabeli -->
  <Implies>
   <if>
    <!-- warunki łączone za pomocą 'and' bądź 'or' -->
   </if>
   <then>
    <Atom> <!-- specjalny predykat, sugerujący następną regułę/tablicę i wywołujący inne predykaty -->
     <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>
     <arg>
      <!-- albo predykat do wywołania, albo predykat xtt:run_many wywołujący więcej niż jeden predykat -->
     </arg>
    </Atom>
   </then>
  </Implies>
 </sentence>
 
 <sentence id="xtt_table_row2">
  ...
 </sentence>
 
 ...
 
</Group>

Niuanse zapisu XTT w RIF

Jeśli któryś z wierszy ma być zawsze wykonywany (dla dowolnej wartości zmiennej na wejściu), to część warunkowa powinna wyglądać następująco:

<if>
 <And></And>
</if>

Pusty And zwraca zawszę prawdę. (Patrz rozdział Formuły: Dobrze sformułowane formuły)

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.

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ą:

<Atom>
 <op><Const type="rif:iri">xtt:complex_set</Const></op>
 <arg>
  <External>
   <content>
    <Expr>
     <op><Const type="rif:iri">xtt:set</Const></op>
     <arg><Const type="xsd:decimal">a</Const></arg>
     <arg><Const type="xsd:decimal">b</Const></arg>
    </Expr>
   </content>
  </External>
 </arg>
 <arg>
  <Const type="xsd:decimal">C</Const>
 </arg>
</Atom>

Zapis przyrównania zmiennej do zbioru (X = {1,2,4}) będzie realizowany za pomocą tagu Equal:

<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>

ten zapis nie został zaimplementowany w translatorze, ze względu na brak informacji co do zapisu po stronie XTTMLa.

Wykorzystywane predykaty

W najnowszej wersji dokumentacji RIFa pojawił się dokument definiujący zarówno predykaty wbudowane, jaki i definiowanie zewnętrznych.

Predykat External schema Opis
xtt:set (?arg1 ?arg2; pred:set(?arg1, ?arg2)) Predykat definiuje zbiór liczb z zakresu. Odpowiednik {arg1, arg2}.
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.
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.
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.

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

  • Każda tablica (element Group) musi być w osobnym pliku (zgodność z plikami xsd).

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

  • ^_^runmany, etc
  • ^_^zestawienie wprowadzonych predykatów iri:xtt_… → odn. do ew. impl.
  • ^_^ew. lista sugestii/ograniczeń w rif (id reguł)

Translacja XTTML => RIF

Po zaproponowaniu wstępnej postaci zapisu XTT w RIF, nadszedł czas na stowrzenie translatora XTTML ⇒ RIF. Translator można pobrać tutaj: XTTtoRIF.xml.

Sposób zapisu w RIFie mniejwiecej zgadza się z przedstawionym powyżej. Dokonałem jedynie pewnych uproszczeń, ułatwiających translacje. Za pomocą powyższego arkusza XSLT dokonałem translacji przykładu, która znajduje się tutaj. Z powodu składni RIFa stosunkowo prosty i czytelny przykład rozrósł się dość znacznie.

Materiały

pl/miw/miw08_xtt_rif.txt · ostatnio zmienione: 2019/06/27 15:50 (edycja zewnętrzna)
www.chimeric.de Valid CSS Driven by DokuWiki do yourself a favour and use a real browser - get firefox!! Recent changes RSS feed Valid XHTML 1.0