10 Nonostante la logica \HOL{} fornisca principi primitivi di definizione
16 La funzione \verb+Hol_datatype+ supporta la definizione di tali
62 \HOL{} mantiene un database sottostante di fatti datatype chiamata la
64 di dimostrazione di alto livello (si veda la Sezione~\ref{sec:bossLib}), ed � aumentato ogni volta
66 definito per mezzo di \verb+Hol_datatype+, la seguente informazione � derivata
76 \item teorema di congruenza per la costante case
81 si avvia, la \ml{TypeBase} contiene gi� le voci rilevanti per
106 Vale la pena ripetere questo punto delicato: il formato delle definizioni di datatype
109 che � polimorfico in pi� di un argomento, c'� la questione di
197 la lista dei suoi sotto-alberi. In un tale caso, i nodi foglia non hanno bisogno di essere
249 Tipi record semplici possono essere introdotti usando la notazione \holtxt{<| ... |>}.
258 L'uso di tipi record pu� essere ricorsivo. Per esempio, la seguente
276 la definizione.
299 I tipi non possono eseguire la ricorsione su entrambi i lati delle frecce funzione. La ricorsione
300 sulla destra � coerente (si veda la teoria \theoryimp{inftree}), ma
302 la richiedono. Cos�, esempi come il seguente falliranno:
314 calcolo non tipizzato come un insieme (si noti la \holtxt{->} nella clausola per il
331 Questi forniscono la capacit� di definire semplici funzioni sul tipo, e un principio d'induzione per il tipo.
334 Altre conseguenze includono la distinzione dei costruttori (\ml{ty\_distinct}), e l'iniettivit� dei costruttori (\verb+ty_11+).
406 tipi coppia (prodotto), ma la possibilit� di etichettare i campi con nomi di
416 permettono la stessa manutenibilit� quando sono interessati degli aggiornamenti
429 I tipi record sono definiti con la funzione \texttt{Hol\_datatype}, come
442 a definire il tipo (chiamato {\tt person}), la funzione di definizione
447 Queste funzioni possono essere usate direttamente, o si pu� usare la notazione standard
452 stampata usando la prima sintassi, con il punto.\index{tipi record!notazione di selezione dei campi}
460 il campo specificato ha avuto la funzione applicata ad esso per
461 generare il nuovo valore per quel campo. Esse possono essere scritte con la
519 \holtxt{<|}-\holtxt{|>} senza la parola chiave \holtxt{with}.
541 \ml{SRW\_TAC} (si veda la Sezione~\ref{sec:simpLib}).
587 Sfortunatamente, la rappresentazione di record grandi ha lo svantaggio che
589 sono stampati allo stesso modo. Una forma � una semplice costante, ed � la forma
609 Order Logic''} [HOQ], da cui � presa la seguente descrizione.
686 {\it func\/} � un termine HOL, che deve essere una singola costante, che � la
688 {\it fname\/} � il nome della nuova costante da definire come la versione sollevata di {\it func}.
689 {\it fixity\/} � la fixity HOL della nuova costante da creare,
691 {\it def\_name} � il nome sotto il quale deve essere archiviata la definizione nella nuova costante
721 {\it poly\_preserves\/} � una lista di teoremi circa la preservazione di
759 � anche fornita la seguente funzione:
777 pi� conveniente quando la generalit� di {\tt define\_quotient\_types}
799 All'interno della logica \HOL{}, le espressioni case forniscono una notazione molto compatta e conveniente per la selezione multi-way tra i valori di pi� espressioni.
811 Omettendo la barra, che � ci� che fa il pretty-printer quando la sintassi � stampata, si conforma con la sintassi usata dall'SML.
831 ma l'espressione case � molto pi� compatta e pulita, con la
845 (Questo esempio usa la barra opzionale all'inizio del primo caso.)
896 la funzione \ml{parents} restituisce una coppia contenente il padre della persona
897 e/o la madre, dove ciascuno � rappresentato da \ml{NONE} se deceduto.
911 automaticamente per compilarlo, e possibilmente alcune nuove variabili o la
947 definire la funzione nella logica. \ml{Define} pu� essere usato per definire
950 dell'attivit� di \ml{Define}. Questo teorema d'induzione segue la struttura
953 eseguire la definizione specificata, di solito perch� una dimostrazione
955 \ml{Hol\_defn}, rinvia la dimostrazione di terminazione all'utente.
965 \ml{Define `}\textit{spec}\ml{`} dovrebbe conformarsi con la grammatica nella Tabella
996 In generale, \ml{Define} tenta di derivare esattamente la congiunzione
997 di equazioni specificata. Tuttavia, la ricca sintassi dei pattern ammette
1009 gli interpreti per i linguaggi funzionali: cio�, la congiunzione delle
1010 equazioni � trattata come fosse applicata prima la congiunzione sinistra, seguita
1016 Un altro caso di ambiguit� nei pattern � mostrato di sotto: la specifica
1022 dal momento che l'utente non specificato in modo completo la funzione, il sistema
1023 lo prende come un suggerimento che l'utente non � interessato nell'usare la
1057 delle condizioni di terminazione per la funzione, e invoca un dimostratore
1058 di terminazione nel tentativo di dimostrare le condizioni di terminazione. Se la
1063 Altrimenti, la funzione non �
1065 avere successo o fallire. Se la dimostrazione di terminazione fallisce, allora \ml{Define} fallisce.
1068 customizzato per la funzione specificata. Si noti, tuttavia, che
1076 \ml{Define} genera automaticamente nomi con i quali archiviare la
1078 attuale. Il nome per archiviare la definizione � costruito
1087 sono trasformati in binding ML dopo che la teoria � esportata, �
1091 simbolici, si dovrebbe usare la funzione ML \ml{xDefine}.
1101 si archivia la definizione nella teoria attuale.
1104 Daremo un numero di esempi che mostrano la gamma di funzioni
1263 \subsection{Quando la terminazione non � dimostrata automaticamente}
1265 Se la dimostrazione di terminazione per una definizione potenziale
1267 situazioni, si dovrebbe usare la funzione \ML{} \ml{Hol\_defn}.
1277 \ml{Hol\_defn} esegue la definizione richiesta, ma rinvia la dimostrazione di
1278 terminazione all'utente. Per la creazione di dimostrazioni di terminazione, esistono
1288 risultato di \ml{Hol\_defn} e creare un goal per dimostrare la terminazione
1292 seguenti equazioni per Quicksort attualmente fallir�, dal momento che la
1309 dimostrare la terminazione.
1361 iniziare la dimostrazione di terminazione. Chiaramente, \ml{qsort} termina perch� la lista
1362 argomento diventa pi� piccola. L'invocazione di \ml{WF\_REL\_TAC} con la funzione di misura
1378 L'esecuzione di \ml{WF\_REL\_TAC} ha dimostrato automaticamente la
1383 la relazione di terminazione con \ml{tDefine}, che prende una quotation
1385 definisce la funzione specificata, calcola le condizioni di terminazione,
1409 primo argomento denota una teoria; la teoria attuale pu� essere specificata da \texttt{"-"}.}.
1425 essere applicato da \ml{recInduct}. Si veda la Sezione \ref{sec:bossLib} per i dettagli.
1428 \subsubsection{Tecniche per dimostrare la terminazione}
1430 Ci sono due problemi da affrontare quando di tenta di dimostrare la terminazione.
1432 perch� la funzione in considerazione termina. Secondo, si deve
1439 \emph{misura} sotto la quale gli argomenti di una chiamata di funzione sono pi� grandi
1442 Per un esempio di partenza molto semplice, si consideri la seguente definizione
1466 \holtxt{n MOD m} sia pi� piccolo di \holtxt{m}. Il modo di formulare la
1477 Ora dobbiamo scegliere la posizione di argomento da misurare e
1523 Dal momento che la dimensione dell'albero non � modificata nell'ultima clausola nella
1555 la terminazione vanno anche sotto il nome di \emph{interpretazione polinomiale}. Bisogna
1556 ammettere che trovare la ponderazione corretta per una dimostrazione
1558 si prova la dimostrazione di terminazione per vedere se funziona.
1563 l'argomento di terminazione. Per esempio, la seguente specifica
1569 Il quarto argomento, $s$, � la stringa che viene cercata.
1590 trovato un match; la funzione restituisce \holtxt{T}. La seconda clausola rappresenta il caso
1591 dove $s$ � esaurito ma $p$ no, in questo caso la funzione restituisce
1592 \holtxt{F}. Il caso rimanente � quando c'� pi� ricerca da fare; la funzione
1593 controlla se la testa del pattern $p$ � la stessa della testa di
1594 $\mathit{rst}$. Se s�, allora la ricerca procede ricorsivamente, usando la
1595 coda di $p$ e la coda di $\mathit{rst}$. Se no, questo significa che $p$ ha
1599 $\mathit{rst}$ e $s$ rappresentano entrambi la stringa da
1602 se la ricerca alla fine fallisce, allora $s$, che `ricorda` dove la ricerca
1603 � iniziata, � usata per riavviare la ricerca.
1606 sono due chiamate ricorsive. La prima chiamata riduce la dimensione di $p$ e $\mathit{rst}$, e
1607 lascia l'altro argomento invariato. La seconda chiamata pu� accrescere la
1608 dimensione di $p$ e $\mathit{rst}$, ma riduce la dimensione di $s$. Questa � una classica situazione
1619 Nella seconda chiamata ricorsiva, la lunghezza di \holtxt{s} � ridotta, e nella
1620 prima rimane uguale. Questo spinge ad avere la lunghezza della
1622 lessicografica, e la lunghezza di $\mathit{rst}$ come il secondo
1634 di numeri $(m,n)$, dove $m$ � la lunghezza del quarto argomento, e
1635 $n$ � la lunghezza del secondo argomento. Queste lunghezze sono poi
1666 Per esempio, si consideri la seguente definizione ricorsiva di fattoriale:
1703 incontrata mentre l'estrattore passa attraverso la definizione di funzione,
1747 Le funzioni `add' e `drop' influenzano solo lo stato attuale del database di congruenza; per contro, la funzione `export' fornisce un modo per le teorie di specificare che un particolare teorema dovrebbe essere aggiunto al database di congruenza in tutte le teorie discendenti.
1756 usata per applicare la funzione ricorsiva agli argomenti. Al fine di
1758 le regole di congruenza per la funzione di ordine superiore devono essere conosciute
1792 � chiamata una \emph{ricorsione di ordine superiore}. Dal momento che la chiamata ricorsiva di
1795 risulta la seguente infelice situazione:
1816 richiedere di trovare una relazione benfondata \holtxt{R} tale che la coppia
1833 Una volta che a \ml{Hol\_defn} � stato fornito questo teorema, attraverso le funzioni \ml{add\_cong} o \ml{export\_cong} di \ml{DefnBase}, le condizioni di terminazione estratte per la definizione sono ora dimostrabili, dal momento che \holtxt{a} � un sottotermine proprio di \holtxt{Node v tl}.
1886 la definizione di uno schema):
1927 Le definizioni induttive sono fatte con la funzione \ml{Hol\_reln}, che si trova
1947 seguire tutte le costanti nuove in tutta la definizione. Queste variabili
1953 le variabili libere, ma � anche ammissibile usare la quantificazione
1962 	che sar� la stessa della term quotation di input; il teorema �
1987 Se lo ``stem'' della prima costante definita in un insieme di clausole � tale che i binding \ML{} risultanti in un file di teoria esportato risulteranno in un codice \ML{} non legale, allora si dovrebbe usare la funzione \ml{xHol\_reln}.
1988 La funzione \ml{xHol\_reln} � analoga alla funzione \ml{xDefine} per definire funzioni ricorsive (si veda la Sezione~\ref{TFL}).
1991 Le cosiddette versioni ``complete'' dei principi d'induzione (in cui le istanze della relazione da definire appaiono come ipotesi extra), sono dimostrate automaticamente quando � fatta una definizione con \ml{Hol\_reln}. Il principio d'induzione completa per una relazione � usato quando � usata la tattica \ml{Induct\_on}.
2013 regola per la negazione).
2015 Per esempio, la regola di monotonicit� per la congiunzione �
2021 liste (si veda la Sezione~\ref{avra_list}), �
2033 globale \ml{the\_monoset} usando la funzione \ml{export\_mono}.
2037 la teoria attuale � successivamente ricaricata.
2078 Il prossimo esempio mostra come definire induttivamente la chiusura riflessiva e
2081 appropriato perch� � \holtxt{RTC R} che ha la caratterizzazione
2124 Poich� una relazione induttiva � la relazione minima che soddisfa le regole date, si pu� usare l'induzione per mostrare goal della forma
2135 Un approccio leggermente di pi� alto livello � di usare la tattica \ml{Induct\_on}.
2136 (Questa tattica � anche usata per eseguire induzioni strutturali su tipi di dato algebrici; si veda la Sezione~\ref{sec:bossLib}.)
2137 Quando si esegue una regola d'induzione, la quotation passata a \ml{Induct\_on} dovrebbe essere della costante usata.
2138 Per questioni estetiche, la costante pu� anche essere applicata a degli argomenti.

Indexes created Tue Jul 09 22:07:09 MDT 2024