X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmathql%2Fgrammar.txt;h=5622761a3381db959570f04bbd778f456bc1d31f;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=2c53c2a1d07d4118ba6498a5aed968810afce66c;hpb=3b401fbefb3830d4f3cdce189ac31559c0219a0d;p=helm.git diff --git a/helm/mathql/grammar.txt b/helm/mathql/grammar.txt index 2c53c2a1d..5622761a3 100644 --- a/helm/mathql/grammar.txt +++ b/helm/mathql/grammar.txt @@ -1,131 +1,148 @@ GRAMMATICA PER QUERY SU DOCUMENTI MATEMATICI MATHEMATICAL QUERY LANGUAGE (MathQL) - := (* clausola iniziale *) + := (* clausola iniziale *) + + := ( ) (* parentesizzazione *) + | (* var per insieme singoletto + di una risorsa *) + | (* var per insieme di risorse + (insieme di valori) *) + | REF (* oggetto/i referenziato/i da + URI esplicita/e *) + | PATTERN (* oggetto/i referenziato/i da + URI ottenute da espansione + del pattern *) + | SELECT IN WHERE (* selezione *) + | LET BE IN (* assegnazione a set-var in + contesto *) + | LET BE IN (* assegnamento a value-var + in contesto*) + | RELATION ATTR + (* unione insieme risorse in + relazione specificata con le + risorse in set, ognuna con + attributi (ATTR) *) + | UNION (* unione *) + | INTERSECT (* intersezione *) + | DIFF (* differenza *) + + := "" (* relazione (proprieta') *) + | SUB (* proprieta' e + sotto-proprieta' *) + | SUPER (* proprieta' e + super-proprieta' *) + + := + (* relazione (proprieta') *) + | "/" + (* insieme di stringhe: + proprieta' strutturata *) + + := + | , - := ( ) (* parentesizazione *) - | UNION (* unione *) - | INTERSECT (* intersezione *) - | DIFF (* differenza *) - | SELECT IN WHERE (* selezione *) - | EXISTS IN WHERE (* esistenziale *) - | USE POSITION (* unione lista backward *) - | USEDBY POSITION (* unione lista forward *) - | CONTRUCTORS (* unione costruttori della - lista oggetti*) - | PATTERN (* espansione del pattern *) - | INTHEORY ITEMTYPE (* unione oggetti lista teorie *) - | THEORYREFTO (* unione teorie che fanno - riferimento a lista oggetti *) - | OFTYPE (* unione oggetti in base a - classi *) - | OFSUPERTYPE (* unione oggetti in base a - classi e loro superclassi *) - | OFSUBTYPE (* unione oggetti in base a - classi e loro sottoclassi *) := ( ) (* parentesizzazione *) - | AND (* congiunzione *) - | OR (* disgiunzione *) - | NOT (* negazione *) | TRUE (* vero *) | FALSE (* falso *) - | IS (* case sensitive matching *) - | EQUAL (* uguaglianza tra liste *) - - := <"-quoted-constant-string> (* pattern costante *) - - := <'-quoted-constant-string> (* costante letterale *) - | CONCLUSION | HYPOTHESIS | BODY (* costanti simboliche *) - | MAINCONCLUSION | MAINHYPOTHESIS - | (* variabile *) - | (* variabile *) - | (* applicazione di funzione *) - - := NAME (* URIREF -> nome_oggetto *) - | + | NOT (* negazione *) + | AND (* congiunzione *) + | OR (* disgiunzione *) + | EQ (* uguaglianza tra insiemi + stringhe (case sensitive) *) + | SUB (* operazione di sottoinsieme + tra insiemi stringhe *) + | MEET (* operazione di meet tra + insiemi stringhe *) + | EX (* existential on attributes + of references *) + := ( ) (* parentesizzazione *) + | {} (* insieme vuoto*) + | (* stringa singoletto *) + | {}(* insieme stringhe *) + | REFOF (* insieme riferimenti *) + | . (* variabile per insieme + stringhe, relativa a + riferimento *) + | + (* applicazione di funzione + specificata a riferimento + o insiemi di rif. o var*) + | (* vvar introduced by LET *) + + := + | , + (* lista di stringhe *) + + := FUN (* funzione generale *) + | - := THEORY (* URIREF -> valore_Proprieta' *) - | TITLE (* URIREF -> valore_Prop_DC *) - | CONTRIBUTOR - | CREATOR - | PUBLISHER - | SUBJECT - | DESCRIPTION - | DATE - | TYPE - | FORMAT - | IDENTIFIER - | LANGUAGE - | RELATION - | SOURCE - | COVERAGE - | RIGHTS - | INSTITUTION - | CONTACT - | FIRSTVERSION - | MODIFIED - | + := ATTRIBUTE (* funzione proprieta': restituisce + suoi valori (anche strutturati) + (e delle sotto-proprieta' o + super-proprieta' *) - := SUB (* proprieta' e sotto-proprieta' - di *) - | SUPER (* proprieta' e super-proprieta' - di *) - := (* variabile per risorse *) - := $ (* variabile per stringhe *) + := @ (* variabile per riferimento *) + := $ (* variabile per insiemi + stringhe *) + := % (* variabile per insiemi + riferimenti *) -- () = lista vuota (?) + +- Idea di base: grammatica del linguaggio semplice e permissiva (duttile) +- MEET e' definito come "esiste almeno un elemento che appartiene + all'interserzione tra due insiemi" - le stringhe sono "case sensitive" - la funzione non definita sull'argomento restituisce la stringa nulla - le si presuppongono essere istanziate come URI references costituite - da un URI e da un fragment identifier opzionalecomplete; esse identificano - risorse -- ogni binding lega una variabile libera (nuova) + da un URI e da un fragment identifier opzionale complete; i riferimenti + identificano risorse - Precedenza operatori: NOT (+) DIFF AND INTERSECT OR (-) UNION -- Possibili tipi di RELATION e DEPENDENCE sono rappresentati dalle loro - subproperties -- FUTURO: thesauri di parole e sinonimi per ricerche testuali, ordinamenti sui - risultati, caratteri jolly. Una volta reperito l'oggetto si possono - visualizzare le info associate. -- FUTURO: in output numeri ad esempio a fini statistici, aggiungendo anche - operatori aritmetici e di confronto (< = >). Es. Quante proofs di un certo - teorema ci sono? - L'ordinamento di default e' quello alfabetico crescente in base al nome delle rvar -- Note su - Contiene un'espressione regolare per selezionare delle "reference" - (cioe` delle uri eventualmente seguite da un fragment identifier) - L'espressione regolare contiene i seguenti costrutti: - - costrutto semanticamente fa match con - ? un singolo carattere diverso da / # : - * la piu' lunga sottostringa che non contiene / # : - ** la piu' lunga sottostringa che non contiene # : - altro carattere solo se' stesso - - costrutto puo' appareire in - ? "body" - * dovunque - ** "body" e "fragment" - altro carattere dovunque - - "body" parte compresa fra le occorrenze di ":/" e "#1" escluse - "fragment" parte successiva all'occorrenza "#1" -- FUTURO: operatore di ordinamento sul risultato finale della query. - SORTEDBY (* unione lista ordinata secondo - ordine e valore funzione *) - := DESC (* ordinamento decrescente *) - | ASC (* ordinamento crescente *) - DTD: - - - - - -- RILASSAMENTO degli operatori UNION e INTERSECT. Operatori fuzzy con - introduzione di pesi associati ai risultati. \ No newline at end of file +- REF aumenta performance perche' NON accede al data base (costoso). +- l'argomento di PATTERN ha sintassi di una espressione regolare + POSIX 1003.2-1992 +- Possibile FUN (): + NAME (* URIREF -> nome_oggetto *) +- MEET aumenta performance nel caso si verifichi (a in S) oppure + (b in S) = ({a,b} meet S) perche' valuta S una volta sola + Il MEET codifica inoltre l'esistenziale su risorse (URI) in un certo + insieme che soddisfa certe condizioni +- record . serve per disambiguare nomi uguali di variabili +- Operatori (come EQ) hanno nomi abbreviati rispetto ai costrutti del + linguaggio +- EX verfica che la sua condizione sia vera per almeno un insieme di attributi + associato all'URI in rvar +- Possibili RELATION sono: + USE con attributo POSITION (riferimenti backward) e valori MAINHYPOTHESIS, + HYPOTHESIS, MAINCONCLUSION, CONCLUSION, BODY + USEBY con attributo POSITION (riferimenti forward) e valori MAINHYPOTHESIS, + HYPOTHESIS, MAINCONCLUSION, CONCLUSION, BODY + CONSTRUCTORS + INTHEORY con attributo ITEMTYPE (riferimenti oggetti contenuti in teorie) + THEORYREFTO con attributo ITEMTYPE (riferimenti teorie referenti a oggetti) +- invece di come argomento di poiche' la REF non + e' piu' restrittiva su argomento/i e quindi e' inutile imporne l'uso quando + si passano i riferimenti alle funzioni. Con l'utente e' libero + di passare direttamente le stringhe dei riferimenti. +- Il costrutto di ordinamento: + SORTEDBY (* unione insieme ordinato secondo + valore funzione e ordine *) + := DESC (* ordinamento decrescente *) + | ASC (* ordinamento crescente *) + perde di senso nel caso di metadati, poiche' per definizione le proprieta' + in RDF possono essere ripetute quindi restituiscono (come anche le funzioni + in generale) valori multipli per ogni riferimento (ambiguita' nell'ordine) +- Possibili proprieta' (): + le DC: TITLE, CONTRIBUTOR, CREATOR, PUBLISHER, SUBJECT, DESCRIPTION, DATE, + TYPE, FORMAT, IDENTIFIER, LANGUAGE, RELATION, SOURCE, COVERAGE, RIGHTS, + RIGHTS; and INSTITUTION, CONTACT, FIRSTVERSION, MODIFIED, THEORY +- Il concetto di Classe, sottoclasse, superclasse, puo' essere visto come una + particolare proprieta' (type o tipo) di una risorsa, e quindi codificabile + da RELATION \ No newline at end of file