IT/Description/libraries.tex

76 del parser. Inoltre, la struttura del parser � esposta cos� che
80 comportamento del parser e del prettyprinter di conseguenza � di solito alterato
122 	in modo differente (alla sinistra, alla destra, o non associare del tutto). Gli utenti possono
168 In quello che segue, esploriamo alcune delle capacit� del
172 \subsubsection{Architettura del parser}
231 allora questa fase del parser non tratter� le stringhe come parte di una
245 	del fatto che l'infisso pi� non ha un argomento
246 	sinistro. Quando il risultato di successo del parsing � passato alla
262 	eseguire qualunque cambiamento sia appropriato. Come tutti gli altri aspetti del
269 	Questo processo risulta in un valore del tipo di dati \ml{Preterm}, che
331 	controlla che il tipo del primo argomento sia una funzione il cui
332 	dominio � uguale al tipo del secondo argomento.) Il lavoro del
344 	quel tipo al tipo del \ml{term} � per lo pi� semplice. L'utente
416 influenza il comportamento del lexer quando incontra delle stringhe di
447 il resto del termine dato. Se la lista risultante contiene pi� di
482 sottostante del termine in memoria, esso sar� di fatto stampato come
493 non costruisca un valore \ml{Absyn}, questo processo inverte la fase del parsing
503 \footnote{Il matching eseguito � del primo ordine; per contro il matching di ordine superiore
507 variabili del pattern.) Se questo risulta ancora in pi� possibilit�, ugualmente
509 pi� recentemente. (Gli utenti possono cos� manipolare le preferenze del printer
513 \holtxt{\~{}(?x = ?y)}, dove i punti interrogativi, indicano variabili del pattern
581 ed elaborato dal parser come un'applicazione del'identificatore simbolico \holtxt{\$=:} alla
590 Al posto del \holtxt{\$}, si possono anche usare le parentesi per rimuovere dai lessemi
616 di tipo, alle variabili di tipo non vincolate sono assegnati dei nomi da parte del sistema.
635 del termine. Per esempio, il simbolo `tilde' (\holtxt{\~{}})
701 il binding del costrutto. Questa � una soluzione elegante ed uniforme.
719 a sinistra o non associare del tutto. (Se \holtxt{+} fosse non-associativo, allora
721 \holtxt{(3 + 4) + 5} o \holtxt{3 + (4 + 5)} a seconda del significato
755 Questo operatore infisso lega pi� strettamente, cos� che quando si scrive $f\,x + y$, il risultato del parser � $(f\cdot{}x) + y$\footnote{Ci sono operatori infissi che legano pi� strettamente, il punto nella selezione di campo fa s� che $f\,x.fld$ sia elaborato dal parser come $f\cdot(x.fld)$.\index{tipi record!notazione di selezione del campo}}.
789 \multicolumn{1}{c}{\mbox{Risultato del parsing}}\\
810 \subsubsection{Trucchi e magia del parser}
949 \REFERENCE{} per maggiori dettagli, inclusa una spiegazione del tipo
973 \index{sistema HOL@sistema \HOL{}!adattamento dell'interfaccia utente del}
977 \subsubsection{Adattare la profondit� del pretty-print}
1101 L'uso principale del caret � d'introdurre le \emph{quntiquotation} (come
1182 Questa sezione del manuale documenta il cambiamento (esteso) fatto al
1184 release HOL3) e al di l� del punto di vista di un utente che non
1229 molti stati intermedi; il goalstack si prende cura del necessario mantenimento
1304 che si sbarazza del tentativo di dimostrazione corrente, e \ml{dropn}, che
1316 \subsection{Visualizzare lo stato del proof manager}
1329 Per visualizzare lo stato del proof manager in qualsiasi momento, si possono
1399 quel tipo. Le regole di riscrittura del datatype sono costruite a partire dai
1440 sono spostate dalle assunzioni alla conclusione del goal, e tutte
1525 \ml{RW\_TAC} solleva le espressioni-\holtxt{let} all'interno del goal cos� che
1565 alle assunzioni del goal originale; cos� la dimostrazione procede con
1574 contraddizione assumendo la negazione del goal e spostando la
1581 \index{procedure di decisione!logica del primo ordine}
1583 La dimostrazione del primo ordine � una potente tecnica di dimostrazione di teoremi che pu�
1592 \index{metodo model elimination per la logica del primo ordine}
1594 La libreria \ml{meson} � un'implementazione del
1596 del primo ordine. Ci sono tre entry-point principali:
1612 \texttt{MESON\_TAC} ignora le assunzioni del goal; gli altri due
1613 entry-point includono le assunzioni come pare del sequente da
1616 I parametri extra a \ml{GEN\_MESON\_TAC} forniscono un controllo extra del
1637 \index{metodo di risoluzione per la logica del primo ordine}
1639 La libreria \ml{metis} � un'implementazione del metodo di risoluzione
1640 per trovare dimostrazioni di goal nella logica del primo ordine. Ci sono due
1659 ordinata e il calcolo di paramodulazione ordinata per la logica del primo ordine,
1670 interattiva. Come strumenti di riscrittura, il ruolo generale del semplificatore
1724 dimensione del termine (ci sono due occorrenze di $p$ al lato destro
1725 del teorema). Ci� nonostante, � chiaro che questo teorema pu� pu�
1763 del goal come regole di riscrittura extra. Cos�:
1799 assunzione � ri-aggiunta alla lista di assunzioni del goal con la
1808 del goal. Tipicamente quindi, la prima assunzione da semplificare
1836 apparse nell'ordine opposto, solo la \holtxt{x} del goal sarebbe
1868 semplificato il resto del goal.
1880 	anche con le assunzioni del goal.
1922 dei \simpset{} che includano tutte le riscritture ``appropriate'' del contesto
1941 non contiene del tutto teoremi di riscrittura, e gioca il ruolo di una tabula
2035 Questi due aspetti del \simpset{} \ml{arith\_ss} sono dimostrati
2047 sembrare non intuitivi. In particolare, la normalizzazione del coefficiente non pu�
2066 riscritture includono i fatti ovvi circa i costruttori del tipo lista
2094 efficiente, ma meno generale del semplificatore. Per esempio:
2178 del suo contesto, cos� come codice per fare calcoli standard
2252 Una descrizione completa per i vari campi del record passato a
2265 La riscrittura � l'``operazione core'' del semplificatore. Questa sezione
2275 il semplificatore eseguir� una scansione dall'alto verso il basso del termine di input $t$,
2287 L'attraversamento del termine da semplificare � ripetuto fino a quando non si trova
2288 alcun match ulteriore per le regole di riscrittura del semplificatore. La
2301   Eseguire una ricorsione sui sotto termini del termine. Il modo in cui i termini sono
2318 cose. Una caratteristica particolarmente potente del semplificatore � che
2325 del termine, tenta di scaricare la condizione $P$. Se il
2357 pu� causare un considerevole degrado delle performance del semplificatore, dal momento
2393 ad ognuno dei teoremi prodotti dal filtro del \simpset{} esistente.
2471 combinato $f(a)$ matcher� qualsiasi termine del tipo appropriato fino a quando le
2525 Questa sezione descrive alcune delle caratteristiche avanzate del semplificatore.
2532 Esse forniscono anche un meccanismo per mezzo del quale possono essere
2533 aggiunte al contesto del semplificatore assunzioni aggiuntive, che rappresentano informazione circa il
2547 Quando si specifica l'azione del semplificatore, queste regole dovrebbero essere
2605 ramo-vero del condizionale, e di assumere la sua negazione quando si
2676 del semplificatore non � specificato. Tuttavia, la forma
2701 il loro proprio codice gli utenti possono personalizzare il comportamento del
2718 I campo \ml{name} e \ml{trace} sono usati quando il tracing del semplificatore
2719 � acceso. Se la conversione � applicata, e se il livello di traccia del
2724 Il campo \ml{key} del record di sopra � usato per specificare i
2728 pattern fornito. Il primo componente del pattern � una lista di
2730 del pattern. Il secondo componente � il pattern di termine stesso. Il matching
2741 fatto ignorando i primi due parametri del campo \ml{conv} Per una
2754 condizioni collaterali all'invocazione ricorsiva del semplificatore.
2761 \paragraph{Procedure di decisione consapevoli del contesto}
2803 chiamata dal meccanismo di attraversamento del semplificatore per dare ad ogni
2810 anche alla funzione \ml{addcontext}. (Naturalmente, � del tutto a carico
2820 dall'utente. La potenza dell'astrazione del riduttore � di avere accesso a
2826 possibili. Questo significa che bench� la riscrittura del semplificatore avvenda in un maniera che va
2836 Si pu� accedere ad alcune delle caratteristiche del semplificatore in un modo
2841 A due delle caratteristiche avanzate del semplificatore, la normalizzazione-AC e
2881 la tecnologia di congruenza del semplificatore pu� essere usata per forzare il
2960 poi lavora su un termine, non applicher� mai pi� del numero dato
2985   Si immagini, per esempio, che si debba impostare un ``profondo incorporamento'' del
3031 (sotto le assunzioni che i termini $u$ e $v$ siano variabili del
3049 I campo del record che � il primo argomento sono:
3062 	Questi sono usati per aumentare il risultante ``filtro'' del \simpset{} cos� che
3079 produrr� un \texttt{ss} aumentato che ha tutti i comportamenti del
3094 di esercitare tutto il potere del processo di riscrittura,
3374 lunghezza del word e del valore numerico. Il pretty-printer di default (installato quando si carica \theoryimp{wordsLib}) stampa valori piccoli in decimale e valori grandi in esadecimale.
3475 Molti di questi frammenti \emph{simpset} hanno delle conversioni corrispondenti. Per esempio, la conversione \ml{WORD\_ARITH\_CONV} � basata si \ml{WORD\_ARITH\_EQ\_ss}, tuttavia, fa del lavoro extra per assicurare che \holtxt{``a = b``} e \holtxt{``b = a``} si convertano nella stessa espressioni. Di conseguenza, questa conversione � adatta per ragionare circa l'eguaglianza delle espressioni aritmetiche word.
3601 Ci sono anche tattiche bit-blasting: \ml{BBLAST\_TAC} e \ml{FULL\_BBLAST\_TAC}; dove solo la seconda fa uso delle assunzioni del goal.