1 \chapter{Principi Avanzati di Definizione}\label{HOLdefinitions}
4 \index{definizioni di tipo, nella logica HOL@definizioni di tipo, nella logica \HOL{}!tipi algebrici}
6 \index{tipi di dato algebrici|see{\ml{Hol\_datatype}}}
7 \index{tipi di dato!definizione in HOL@definizione in \HOL{}}
8 \index{tipi di dato!definizione in HOL@definizione in \HOL{}|seealso{\ml{Hol\_datatype}}}
10 Nonostante la logica \HOL{} fornisca principi primitivi di definizione
11 che permettono di introdurre nuovi tipi, il livello di dettaglio �
12 a grana molto fine. Lo stile delle definizioni di datatype nei linguaggi
13 di programmazione funzionale fornisce una motivazione per un interfaccia di
16 La funzione \verb+Hol_datatype+ supporta la definizione di tali
17 tipi di dato; le specifiche dei tipi possono essere ricorsive, mutuamente
53 \caption{Dichiarazione di Datatype}\label{datatype}
59 \index{definizioni di tipo, nella logica HOL@definizioni di tipo, nella logica \HOL{}!mantenimento della TypeBase@mantenimento della \ml{TypeBase}}
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
74 \item teorema di analisi dei casi
76 \item teorema di congruenza per la costante case
86 La seguente dichiarazione ML di un tipo di dati di alberi binari
100 \noindent La notazione \holtxt{=>} in una descrizione di datatype HOL
101 � intesa sostituire \holtxt{*} in una descrizione di datatype ML,
102 e evidenzia il fatto che, in HOL, i costruttori sono di default
103 curried. Si noti anche che non � menzionato alcun parametro di tipo
104 per il nuovo tipo: le variabili di tipo sono sempre in ordine alfabetivo.
106 Vale la pena ripetere questo punto delicato: il formato delle definizioni di datatype
108 argomenti per gli operatori di tipo introdotti. Cos�, quando si definisce un tipo
109 che � polimorfico in pi� di un argomento, c'� la questione di
120 costruttore \ml{Left} o \ml{Right}? Il sistema sceglie di far apparire
123 dato, l'\ml{'a} di \ml{('a,'b)sum} sar� l'argomento \ml{Left}
124 perch� \ml{left} viene prima di \ml{right} nell'ordine alfabetico
129 Nel seguito, daremo una panoramica del genere di tipi che
130 possono essere definiti per mezzo di \ml{Hol\_datatype}.
156 Spostandoci ai tipi ricorsivi, abbiamo gi� visto un tipo di alberi
169 formato curried usato di sopra.
171 La sintassi di base del lambda calcolo denominato � facile da descrivere:
196 Gli alberi arbitrariamente ramificanti possono essere definiti permettendo a un nodo di mantenere
197 la lista dei suoi sotto-alberi. In un tale caso, i nodi foglia non hanno bisogno di essere
207 Un tipo di `termini del primo ordine' pu� essere dichiarato nel modo seguente:
218 da Elsa Gunter da Definition of Standard ML, cattura un sottoinsieme di
258 L'uso di tipi record pu� essere ricorsivo. Per esempio, la seguente
271 \subsection{Definizioni di tipo che falliscono}
275 pu� essere incorporato nella logica HOL, ma \ml{Hol\_datatype} non � in grado di rendere
301 \ml{Hol\_datatype} non � in grado di definire tipi algebrici che
312 La ricorsione sulla sinistra deve fallire per ragioni di cardinalit�. Per
313 esempio, HOL non permette il seguente tentativo di modellare il lambda
327 \subsection{Teoremi che sorgono da una definizione di datatype}
329 Le conseguenze di un'invocazione di \ml{Hol\_datatype} sono archiviate nell'attuale segmento di teoria e nella \ml{TypeBase}.
330 Le principali conseguenze di una definizione di datatype sono i teoremi di ricorsione primitiva e d'induzione.
331 Questi forniscono la capacit� di definire semplici funzioni sul tipo, e un principio d'induzione per il tipo.
332 \index{teoremi d'induzione, nella logica HOL@teoremi d'induzione, nella logica \HOL{}!per tipi di dato algenrico}
333 Cos�, per un tipo denominato \holtxt{ty}, il teorema di ricorsione primitiva � archiviato sono \ml{ty\_Axiom} e il teorema d'induzione � messo sotto \ml{ty\_induction}.
335 Una versione `degenerata' di \ml{ty\_induction} � anche archiviata sotto \ml{ty\_nchotomy}: essa prevede ragionamenti per casi sulla costruzione degli elementi di \ml{ty}.
336 Infine, sono archiviati alcuni teoremi per scopi speciali: per esempio, \ml{ty\_case\_cong} mantiene un teorema di congruenza per enunciati ``case'' su elementi di \ml{ty}.
396 Una definizione di tipo mutuamente ricorsiva ha come risultato che i
397 teoremi e le definizioni di sopra sono aggiunte per ognuno dei tipi definiti.
400 \index{definizioni di tipo, nella logica HOL@definizioni di tipo, nella logica \HOL{}!tipi record}
403 I tipi record sono dei modi convenienti d'impacchettare insieme un numero di
404 tipi componenti, e di dare a questi componenti dei nomi cos� da facilitare
406 tipi coppia (prodotto), ma la possibilit� di etichettare i campi con nomi di
411 Costruiti correttamente, i tipi record forniscono utili funzionalit� di manutenibilit�.
412 Se si pu� sempre accedere al campo {\tt fieldn} di un tipo record
414 risultano nell'aggiunta o cancellazione di altri campi non invalideranno
417 (funzionali) dei record. L'implementazione HOL permette di scrivere
423 che sostituisce il vecchio valore di {\tt fieldn} nel record {\tt rec}
442 a definire il tipo (chiamato {\tt person}), la funzione di definizione
443 di datatype definisce anche due altre insiemi di costanti. Queste sono le
444 funzioni di accesso al campo e le funzioni di aggiornamento funzionale. Le funzioni
445 di accesso al campo hanno nomi della forma
448 di accesso ai campi per accedere ai valori del campo di un record. Cos�,
450 di restituire il valore del campo {\tt employed} di {\tt bob}.
452 stampata usando la prima sintassi, con il punto.\index{tipi record!notazione di selezione dei campi}
454 Alle funzioni di aggiornamento funzionale sono dati i nomi
474 Inoltre, c'� un addolcimento sintattico disponibile per permettere di scrivere un
476 fatto usando l'operatore \holtxt{:=} al posto di
487 teoria \texttt{combin}. Perci�, l'esempio di sopra � in realt�
495 che a sua volta � una forma pi� carina di
503 Se si desidera una catena di aggiornamenti, allora gli aggiornamenti multipli possono essere
504 specificati all'interno di coppie \holtxt{<|}-\holtxt{|>}, separati da
513 Entrambe le forme di aggiornamento (usando \texttt{updated\_by} e \texttt{:=}) possono essere
514 usati in una catena di aggiornamenti.
518 Il parser accetta liste di specifiche di campo tra coppie
520 Queste sono tradotte in sequenze di aggiornamenti di un valore arbitrario
530 \paragraph{Usare i teoremi prodotti da definizioni di record}
532 Oltre a definire il tipo e le funzioni descritti di sopra, una definizione
533 di tipo record dimostra anche una suite di utili teoremi. Questi sono tutti
544 tipo. La lista di sotto � un esempio dei teoremi dimostrati. Le
546 fine di generare il nome finale del teorema.
553 \item[\texttt{\_accessors}] Le definizioni delle funzioni di accesso.
555 \item[\texttt{\_fn\_updates}] Le definizioni delle funzioni di aggiornamento
566 \item[\texttt{\_fupdcanon}] Un teorema che stabilisce i risultati di commutativit�
567 	per tutte le possibili coppie di aggiornamenti di campo. Essi sono costruiti in
569 	le sequenze di aggiornamenti. Cos�, per tutti gli $i < j$, � generato \[
576 \paragraph{Record grandi} La dimensione di certi teoremi dimostrati nel
577 pacchetto tipi record cresce come il quadrato del numero di campi nel
578 record. (In particolare, i teoremi di canonicalizzazione dell'aggiornamento e
587 Sfortunatamente, la rappresentazione di record grandi ha lo svantaggio che
588 ogni funzione di aggiornamento e di accesso ha due forme: termini differenti che
591 ammette l'uso di teoremi pi� piccoli quando dei valori record sono
593 dall'utente che menzionano campi di record grandi o aggiornamenti di campi passino
594 attraverso una fase di semplificazione (\texttt{SIMP\_RULE}), applicando le
595 riscritture della \texttt{TypeBase}, prima di essere salvati.
597 Il pretty-printing di record grandi pu� essere controllato con il
598 flag di trace \texttt{pp\_bigrecs}.
603 \index{definizioni di tipo, nella logica HOL@definizioni di tipo, nella logica \HOL{}!quozienti|(}
604 \index{tipi quoziente, definizione di}
607 di tipi esistenti, rispetto alle relazioni di equivalenza parziale.
614 La definizione di nuovi tipi corrispondenti ai quozienti di
615 tipi esistenti per relazioni di equivalenza � chiamata ``sollevare''
627 manipolano i valori di questi tipi, e anche le nuove versioni dei
628 teoremi che descrivono le propriet� di queste costanti. Ognuna di queste
634 strumento principale di questo pacchetto.
658 {\it types\/} � una lista di record, ognuno dei quali contiene due campi:
659 {\it name}, che � il nome di un nuovo tipo quoziente da creare, e
663 � una relazione di equivalenza
672 un teorema che {\it R\/} � una relazione di equivalenza parziale non vuota,
681 Il processo di formare i nuovi tipi quoziente � descritto
684 {\it defs\/} � una lista di record che specifica le costanti da sollevare.
688 {\it fname\/} � il nome della nuova costante da definire come la versione sollevata di {\it func}.
694 processo di definire le costanti sollevate
697 {\it tyop\_equivs\/} � una lista di teoremi di equivalenza condizionali
698 per operatori di tipo (si veda [HOQ] \S 4.1).
700 i teoremi sui nuovi operatori di tipo, cos� che essi possono essere sollevati
703 {\it tyop\_quotients\/} � una lista di teoremi quoziente condizionali
704 per operatori di tipo (si veda [HOQ] \S 5.2).
707 {\it tyop\_simps\/} � una lista di teoremi per semplificare relazioni operatori di tipo
712 Il resto degli argomenti si riferisce al processo generale di sollevare i teoremi
716 {\it respects\/} � una lista di teoremi circa il rispetto delle
721 {\it poly\_preserves\/} � una lista di teoremi circa la preservazione di
730 {\it poly\_respects\/} � una lista di teoremi che mostra il rispetto
736 {\it old\_thms\/} � una lista di teoremi che concernono i tipi e le costanti pi� basse,
742 {\tt define\_quotient\_types} restituisce una lista di teoremi, che sono le
747 record con gli stessi campi di sopra eccetto per {\it old\_thms},
748 e restituisce una funzione SML di tipo {\tt thm -> thm}.
777 pi� conveniente quando la generalit� di {\tt define\_quotient\_types}
779 Questa funzione � definita in termini di {\tt define\_quotient\_types} come
793 \index{definizioni di tipo, nella logica HOL@definizioni di tipo, nella logica \HOL{}!quozienti|)}
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.
800 Questo � modellato sui costrutti case nei linguaggi di programmazione funzionale come lo Standard ML.
801 Tali espressioni case possono semplificare l'espressione di rami complicati tra casi differenti o combinazioni di casi.
810 La scelta nella regola per il primo caso ($\mathit{case}_1$) permette l'uso di una sintassi pi� uniforme, dove ciascun caso � preceduto da una barra verticale.
813 Sulla base del valore di una espressione di test, sono considerate in sequenza una lista di
814 espressioni pattern per vedere se si accordano con l'espressione di test.
834 Oltre ai letterali come pattern, come di sopra, i pattern possono essere
847 \HOL{} supporta una ricca struttura di espressioni case che usano una singola
848 notazione. Il formato � legato a quello delle definizioni di funzioni
851 elementi di pattern pi� profondamente annidati.
853 Le espressioni case possono testare valori di qualsiasi tipo. Se l'espressione test
856 nell'esempio di sopra. Una variabile libeera all'interno del pattern costruttore,
858 corrispondente valore all'interno del valore dell'espressione di test, e
863 definizione di datatype descritta nella Sezione~\ref{sec:datatype},
866 Sia che l'espressione di testi sia un tipo con costruttori o meno,
867 i pattern possono essere espressi usando i letterali appropriati di quel tipo,
876 Qui c'� un esempio di questo genere di miscuglio improprio.
891 Cancellare uno dei due gruppi di righe risolverebbe il conflitto,
907 Questo mostra l'annidamento di pattern option all'interno di un pattern coppia,
908 e anche l'uso di una wildcard \ml{\_} per matchare i casi non forniti.
910 Se l'insieme di pattern � rado [sparse nel testo originale (ndt)], ci possono essere alcune nuove righe generate
933 Questo � soltanto una breve descrizione di alcune delle
935 Molti altri esempi di pattern sono forniti nella Sezione~\ref{TFL}
943 \HOL{} fornisce una meccanismo di definizione di funzione basato sul
944 teorema di ricorsione benfondata fornito in \theoryimp{relationTheory},
945 discusso nella Sezione~\ref{relation}.  \ml{Define} prende una specifica di alto livello,
946 possibilmente ricorsiva, di una funzione e tenta di
950 dell'attivit� di \ml{Define}. Questo teorema d'induzione segue la struttura
951 ricorsiva della funzione, e pu� essere utile quando di dimostrano propriet�
952 della funzione. \ml{Define} non ha sempre successo nel tentare di
953 eseguire la definizione specificata, di solito perch� una dimostrazione
954 automatica di terminazione fallisce: in quel caso, si pu� usare un altro punto d'entrata,
955 \ml{Hol\_defn}, rinvia la dimostrazione di terminazione all'utente.
963 congiunzione di equazioni. La (o le) funzione (funzioni) specificate possono essere formulate
991 \caption{Sintassi della Dichiarazione di Funzione}\label{define:syntax}
995 \paragraph{Espansione di Pattern}
996 In generale, \ml{Define} tenta di derivare esattamente la congiunzione
997 di equazioni specificata. Tuttavia, la ricca sintassi dei pattern ammette
1011 dall'elaborazione del congiunto destro. Quindi, nell'esempio di sopra, il
1012 valore di \holtxt{f 0 0} � \holtxt{1}. Nell'implementazione,
1014 sistematicamente in un passo di pre-elaborazione.
1016 Un altro caso di ambiguit� nei pattern � mostrato di sotto: la specifica
1020 \holtxt{ARB}. Questo passo di `completamento del pattern' � un modo di trasformare le descrizioni
1021 di funzioni parziali in funzioni totali adatte per HOL. Tuttavia,
1039 dall'equazioni ambigue e incomplete di sopra. Gli strani
1040 nomi delle variabili sono dovuti ai passi di pre-elaborazione descritti di sopra. Il
1041 risultato di sopra � solo un valore intermedio: nel risultato finale restituito
1055 Durante l'elaborazione della specifica di una funzione ricorsiva, \ml{Define}
1056 deve eseguire una dimostrazione di terminazione. Essa costruisce automaticamente
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
1060 il pattern ricorsione di un datatype HOL dichiarato in precedenza, allora questa
1062 segmento attuale di teoria.
1064 un'istanza di ricorsione primitiva, e il dimostratore di terminazione pu�
1065 avere successo o fallire. Se la dimostrazione di terminazione fallisce, allora \ml{Define} fallisce.
1067 segmento di teoria. E' anche archiviato nell'attuale segmento di teoria un teorema d'induzione
1074 \paragraph{Archiviare le definizioni nel segmento di teoria}
1083 mutuamente ricorsive, dove c'� una scelta di nomi, � preso il nome della funzione
1086 Dal momento che i nomi usati per archiviare elementi nel segmento attuale di teoria
1088 richiesto che ogni invocazione di \ml{Define} generi nomi che sono
1090 nomi alfanumerici di funzione. Se si desidera definire identificatori
1103 \subsection{Esempi di definizione di funzione}
1104 Daremo un numero di esempi che mostrano la gamma di funzioni
1133 relativamente complesso. Tralasciamo di esaminare il teorema
1153 espansione di caratteri jolly e pre-elaborazione di pattern-matching.
1188 Per esempio, possiamo definire un datatype di proposizioni e una funzione per
1190 Prima definiamo un datatype, chiamato \ml{prop}, di formule booleane:
1245 con un pattern-matching complesso. La pre-elaborazione del pattern-matching di
1247 grande numero di equazioni. Per esempio:
1265 Se la dimostrazione di terminazione per una definizione potenziale
1266 fallisce, l'invocazione di \ml{Define} (o \ml{xDefine}) fallisce. In tali
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
1291 \paragraph{Esempio.} Un'invocazione di {\small\verb+Define+} sulle
1293 dimostrazione di terminazione � attualmente oltre le capacit� del dimostratore elementare
1294 di terminazione. Piuttosto, eseguiamo un'applicazione di {\small\verb+Hol_defn+}:
1308 che restituisce il seguente valore di tipo \ml{defn}, ma non tenta di
1339 di sopra � tipico, mostrando i componenti di una \ml{defn} in un formato
1340 comprensibile. Bench� sia possibile lavorare direttamente con elementi di
1342 \ml{Defn.tgoal}, che imposta una dimostrazione di terminazione in un goalstack.
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
1379 benfondatezza della relazione di terminazione
1382 coppia di goal semplici. Una volta che entrambi i goal sono dimostrati, possiamo incapsulare
1383 la relazione di terminazione con \ml{tDefine}, che prende una quotation
1384 (che rappresenta l'equazioni di ricorsione desiderate) e una tattica $t$,
1385 definisce la funzione specificata, calcola le condizioni di terminazione,
1386 e applica $t$ ad esse. Se le condizioni di terminazione sono dimostrate da
1387 $t$ allora l'equazioni di ricorsione e il teorema d'induzione sono archiviati
1388 nel segmento di teoria attuale prima che le equazioni di ricorsione siano restituite:
1430 Ci sono due problemi da affrontare quando di tenta di dimostrare la terminazione.
1433 essere in grado di formulare questo in \HOL. In ci� che segue, daremo alcuni
1434 esempi di come questo � fatto.
1436 C'� un certo numero di strumenti base e avanzati per specificare relazioni
1437 benfondate. Il punto di partenza pi� comune per trattare i problemi
1438 di terminazione per funzioni ricorsive � trovare qualche funzione, conosciuta come una
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
1443 di una funzione che calcola il massimo comun divisore di due
1466 \holtxt{n MOD m} sia pi� piccolo di \holtxt{m}. Il modo di formulare la
1467 terminazione di \holtxt{gcd} in HOL � di usare una funzione `misura'
1468 per mappare dal dominio di \holtxt{gcd}---una coppia di numeri---a un numero.
1469 La definizione di {misura} in \HOL{} � equivalente a
1477 Ora dobbiamo scegliere la posizione di argomento da misurare e
1491 \paragraph{Funzioni di Ponderazione}
1493 A volte, si ha bisogno di una funzione di misura che sia essa stessa ricorsiva. Per
1494 esempio, si consideri un tipo di alberi binari e una funzione che
1524 definizione di \holtxt{Unbal}, una semplice misura di dimensione non funziona. Piuttosto,
1525 possiamo assegnare dei pesi ai nodi nell'albero tali che le chiamate ricorsive di
1554 Le tecniche di `ponderazione' di nodi in un datatype al fine di dimostrare
1555 la terminazione vanno anche sotto il nome di \emph{interpretazione polinomiale}. Bisogna
1557 di terminazione � pi� un'arte che una scienza. Tipicamente, si fa una congettura e
1558 si prova la dimostrazione di terminazione per vedere se funziona.
1562 Saltuariamente, c'� una combinazione di fattori che complica
1563 l'argomento di terminazione. Per esempio, la seguente specifica
1564 descrive un ingenuo algoritmo di pattern matching su stringhe (qui
1593 controlla se la testa del pattern $p$ � la stessa della testa di
1595 coda di $p$ e la coda di $\mathit{rst}$. Se no, questo significa che $p$ ha
1596 fallito il match, cos� l'algoritmo avanza di un carattere in avanti in
1597 $\mathit{s}$ e inizia il matching dall'inizio di $p_0$. Se
1600 cercare: $\mathit{rst}$ � una versione `locale` di $s$: eseguiamo una ricorsione in
1606 sono due chiamate ricorsive. La prima chiamata riduce la dimensione di $p$ e $\mathit{rst}$, e
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
1622 lessicografica, e la lunghezza di $\mathit{rst}$ come il secondo
1624 argomenti in una combinazione lessicografica di relazioni.
1625 Questo � permesso da \holtxt{inv\_image} di \ml{relationTheory}:
1634 di numeri $(m,n)$, dove $m$ � la lunghezza del quarto argomento, e
1636 confrontate dal punto di vista lessicografico rispetto a minore-di ($<$).
1655 Il primo subgoal ha bisogno di un case-split su \holtxt{s} prima di essere dimostrato per
1658 \subsubsection{Come sono sintetizzate le condizioni di terminazione}
1660 \index{regole di congruenza!nelle analisi di terminazione|(}
1662 \ml{Hol\_defn} costruisce i vincoli di terminazione. In alcuni casi, �
1663 persino necessario che gli utenti influenzino questo processo al fine di avere estratti
1664 dei vincoli di terminazione corretti. Il processo � guidato dai cosiddetti
1665 \emph{teoremi di congruenza} per particolari vincoli \HOL{}.
1666 Per esempio, si consideri la seguente definizione ricorsiva di fattoriale:
1674 In assenza di una conoscenza di come il costrutto `if-then-else`
1676 estrarrebbe i vincoli di terminazione:
1686 stato preso in considerazione. Questo esempio di fatto non � un problema per HOL,
1687 dal momento che il seguente teorema di congruenza � conosciuto da \ml{Hol\_defn}:
1700 di istruzioni da seguire quando l'estrattore di condizioni di terminazione
1703 incontrata mentre l'estrattore passa attraverso la definizione di funzione,
1707 \item Traversa $B$ ed estrae le condizioni di terminazione
1711 \item Assume $B'$ ed estrae le condizioni di terminazione da ogni
1715 \item Assume $\neg B'$ ed estrae le condizioni di terminazione da ogni
1731 Le condizioni di terminazione sono accumulate fino a quando
1732 il processo di terminazione non finisce, ed appaiono come ipotesi nel risultato
1733 finale. Cos� le condizioni di terminazione estratte per \holtxt{fact} sono
1742 e sono facili da dimostrare. La nozione di \emph{contesto} di una chiamata ricorsiva
1743 � definita dall'insieme di regole di congruenza usate nell'estrazione delle condizioni
1744 di terminazione. Questo insieme si pu� ottenere invocando \holtxt{DefnBase.read\_congs},
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.
1748 \index{regole di congruenza!nelle analisi di terminazione|(}
1753 \paragraph{Ricorsione di Ordine Superiore e Regole di Congruenza}
1755 Una ricorsione di `ordine superiore' � una in cui una funzione di ordine superiore �
1756 usata per applicare la funzione ricorsiva agli argomenti. Al fine di
1757 dimostrare le condizioni di terminazione corrette per una tale ricorsione,
1758 le regole di congruenza per la funzione di ordine superiore devono essere conosciute
1759 dal meccanismo di estrazione delle condizioni di terminazione. Le regole di congrueza per
1760 funzioni di ordine superiore comuni, ad esempio \holtxt{MAP}, \holtxt{EVERY}, and
1762 meccanismo. Tuttavia, a volte, di deve dimostrare ed installare manualmente un
1763 teorema di congruenza per una nuova funzione di ordine superiore definita dall'utente.
1765 Per esempio, supponiamo di definire una funzione di ordine superiore \holtxt{SIGMA} per
1766 sommare i risultati di una funzione in una lista.
1776 Usiamo poi \holtxt{SIGMA} nella definizione di una funzione per
1777 sommare i risultati di una funzione in un albero
1792 � chiamata una \emph{ricorsione di ordine superiore}. Dal momento che la chiamata ricorsiva di
1794 speciali per estrarre le condizioni di terminazione corrette. Altrimenti,
1814 \index{regole di congruenza!nelle analisi di terminazione|(}
1815 Le condizioni di terminazione per \holtxt{ltree\_sigma} sembrano
1816 richiedere di trovare una relazione benfondata \holtxt{R} tale che la coppia
1817 \holtxt{(f,a)} � \holtxt{R}-minore di
1820 che entrambi sono \holtxt{ltree}. L'estrattore di condizioni di terminazione
1821 non ha funzionato in modo appropriato, perch� non conosceva una regola di congruenza
1822 per \holtxt{SIGMA}. Una tale teorema di congruenza � il seguente:
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}.
1855 \subsection{Schemi di Ricorsione}
1857 Nella logica di ordine superiore, possono essere definiti pattern molto generali di ricorsione, conosciuti come
1858 \emph{schemi di ricorsione} o a volte \emph{schemi di programma}.
1868 \konst{linRec} di implementare funzioni ricorsive differenti. In questo,
1869 \konst{linRec} � come molte altre funzioni di ordine superiore. Tuttavia,
1871 $g(x) = x$, allora l'istanziazione risultante di
1878 Questo, comunque, non � derivabile in \HOL{}, perch� gli schemi di ricorsione
1879 sono definiti istanziando il teorema di ricorsione benfondata, e
1880 pertanto sorgono certi vincoli astratti di terminazione che
1881 devono essere soddisfatti prima che le equazioni di ricorsione possano essere usati senza
1886 la definizione di uno schema):
1906 di terminazione. Un teorema d'induzione vincolato in modo simile �
1907 anche archiviato nel segmento attuale di teoria.
1916 Questi vincoli sono astratti, dal momento che pongono dei requisiti di terminazione
1931 term quotation come input e tenta di definire le relazioni li
1932 specificate. La term quotation di input deve essere parsata a un termine che
1943    \nonterm{con}          &::=& \mbox{una nuova costante di relazione}
1945 I termini (opzionali) $\mathit{sv}_i$ che appaiono dopo il nome di una costante
1951 del processo di definizione, e sar� emesso un messaggio di warning.
1957 Un'invocazione di successo di \ml{Hol\_reln} restituisce tre teoremi
1959 segmento di teoria attuale.
1961 \item $\mathit{rules}$ � una congiunzione di implicazioni
1962 	che sar� la stessa della term quotation di input; il teorema �
1967 \item $\mathit{cases}$ � il cosiddetto teorema dei `casi' o di `inversione'
1972    (!a0 .. an.  R1 a0 .. an = <Prima regola di possibilit� di R1> \/
1973                               <Seconda regola di possibilit� di R1> \/ ...)
1975    (!a0 .. am.  R2 a0 .. am = <Prima regola di possibilit� di R2> \/
1976                               <Seconda regola di possibilit� di R2> \/ ...)
1982 possibili modi di ottenerlo dalle regole.
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}.
1997 nuove costanti. \ml{Hol\_reln} tenter� di dimostrare automaticamente tali
1998 risultati di monotonicit�, usando un insieme di teoremi mantenuti in una reference
1999 \ml{IndDefLib.the\_monoset}. I teoremi di monotonicit� devono essere della forma
2011 dove il vettore di variabili $\vec{v}$ pu� essere vuoto, e dove i
2012 $\mathit{arg}$ e $\mathit{arg}'$ possono essere di fatto invertiti (come nella
2015 Per esempio, la regola di monotonicit� per la congiunzione �
2020 La regola di monotonicit� per l'operatore \holtxt{EVERY} nella teoria delle
2026 Con un risultato di monotonicit� disponibile per un operatore come
2032 I risultati di monotonicit� che l'utente deriva possono essere archiviati nella variabile
2034 Questa funzione prende una stringa che nomina un teorema nel segmento di teoria
2035 attuale, e aggiunge quel teorema ai teoremi di monotonicit�
2041 Un semplice esempio di definizione di due relazioni mutuamente ricorsive �
2079 transitiva di una relazione $R$. Si noti che \holtxt{R}, come una
2082 induttiva, \holtxt{RTC} di per s�.
2105 come nella definizione di \holtxt{EVEN} e \holtxt{ODD}. Le relazioni
2107 non hanno bisogno di essere contigue.
2112 Il teorema ``regole'' di una definizione induttiva fornisce un modo diretto di dimostrare argomenti che appartengono a una relazione.
2113 Se ci si trova di fronte a un goal della forma \holtxt{R~x~y}, si potrebbe fare progressi eseguendo una \ml{MATCH\_MP\_TAC} (o magari, una \ml{HO\_MATCH\_MP\_TAC}) con una delle implicazioni nel teorema ``regole''.
2116 Dal momento che il lato destro di questo teorema includer� spesso altre occorrenze della relazione, non � in generale sicuro riscrivere semplicemente con esso.
2118 \index{Once (controllo delle applicazioni di riscrittura)@\ml{Once} (controllo delle applicazioni di riscrittura)}
2119 Qui possono essere usate le direttive di controllo-di-riscrittura \ml{Once}, \ml{SimpLHS} e \ml{SimpRHS}.
2121 Inoltre, il teorema ``casi'' pu� essere usato come una forma di eliminazione: se si ha un'assunzione della forma \holtxt{R~x~y}, riscrivere questo (magari con \ml{FULL\_SIMP\_TAC} se il termine occorre nelle assunzioni del goal) nei possibili modi in cui pu� essere avvenuto � spesso un buon approccio.
2130 L'approccio di basso livello a goal di questa forma � di applicare
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}.)

Indexes created Tue Sep 03 12:52:19 MDT 2024