Lines Matching defs:di
20 manipolare valori di questi tipi. Su questa base � implementata la logica
26 \HOL{} � quello di applicare le regole d'inferenza ad assiomi o a teoremi esistenti;
27 di conseguenza la coerenza della logica � preservata.
29 Il proposito del meta-linguaggio \ML\ � di fornire un ambiente
30 di programmazione in cui costruire strumenti di dimostrazione per assistere nella
31 costruzione di dimostrazioni. Quando il build del sistema \HOL{} � eseguito, una variet� di
32 utili teoremi � pre-dimostrato e un insieme di strumenti pre-definito. Il sistema
33 di base cos� offre un ricco ambiente iniziale; gli utenti lo possono arricchire ulteriormente
41 di una variabile \HOL{}
44 \index{variabili, nella logica HOL@variabili, nella logica \HOL{}!nomi di|(}
46 pu� essere qualsiasi stringa \ML{}, ma il meccanismo di quotation eseguir� il parsing solo
47 di nomi che sono identificatori (si veda la Sezione~\ref{ident} di sotto). Usare dei non-identificatori come nomi di variabili � sconsigliato eccetto in circostanze
50 esistenti). Il nome di una variabile di tipo
52 \index{variabili di tipo, nella logica HOL@variabili di tipo, nella logica \HOL{}!nomi di}
56 per degli esempi). Il nome di una costante di tipo o di un termine costante nella
58 in modo speciale dal parser e dal printer di HOL e dovrebbero quindi essere
66 un identificatore \HOL{} pu� essere di due forme:
68 \item Una sequenza finita di \emph{alfanumerici} che cominciano con una lettera. Il
69 carattere di underscore � considerato un carattere numerico, e cos� pu�
70 occorrere dopo la prima lettera di un identificatore. I caratteri greci (approssimativamente
76 Le cifre sono i caratteri ASCII 0--9, il carattere di underscore, e i
77 sottoscritti e i soprascritti Unicode. Il carattere di apostrofo
81 Non � una lettera, ma pu� comparire come parte di un identificatore di termine
83 nome di una variabile di tipo, e pu� anche apparire nel contesto di un termine come
84 una sequenza di apostrofi per conto proprio.
88 simboli ASCII di base sono
92 L'uso del segno di omissione e del carattere di accento circonflesso � complicato dal fatto
94 di quotation; si veda la Sezione~\ref{sec:quotation-antiquotation}. I simboli
95 ASCII di raggruppamento (graffe, quadre, e parentesi tonde), e i caratteri
103 caratteri non si combinano tra di loro o con altri caratteri
110 come simboli. Nessuno di questi � non-aggregante.
112 \item Un \emph{numero} � una stringa di una o pi� cifre. Se non � la
114 fornire una spaziatura. Al fine di distinguere differenti generi di numeri
139 dei booleani, e di conseguenza anche in tutte le teorie discendenti. Essi non
140 dovrebbero essere usati come il nome di una variabile o di una costante a meno che l'utente sia
141 molto confidente della propria abilit� di perdere tempo con le grammatiche
147 \paragraph {Nomi di variabili di tipo}\label{tyvars}
149 Il nome di una variabile di tipo nella logica \HOL{} � una stringa
152 di variabili di tipo eccetto l'ultimo:
161 In generale, un utente \HOL{} ha una grande quantit� di libert� di creare la sua propria sintassi, richiedendo token speciali a prescindere dalle variabili e dai nomi per le costanti.
164 ha token speciali (l'``if'', il ``then'' e l'``else'') che non sono nomi per le variabili, n� per le costanti (la costante sottostante � di fatto chiamata \holtxt{COND}).
165 Per essere sicuro che le operazioni di stampa e parsing dei token siano appropriatamente l'una l'inverso dell'altra, gli utenti non dovrebbero creare token che includono spazi vuoti o le stringhe di commento (\ml{(*} and \ml{*)}).
170 I tipi ammessi dipendono da quali costanti di tipo
172 \index{costanti di tipo, nella logica HOL@costanti di tipo, nella logica \HOL{}}
175 per i dettagli di come tali dichiarazioni sono fatte. Ci sono due funzioni
179 \index{costruttori di tipo!nella logica HOL@nella logica \HOL{}}
181 che fungono da costruttori per valori di tipo \ml{hol\_type}:
193 La funzione \ml{mk\_vartype} costruisce una variabile di tipo
195 \index{variabili di tipo, nella logica HOL@variabili di tipo, nella logica \HOL{}!costruttori per}
198 per una variabile di tipo (cio� non � un \ml{'} seguito da un alfanumerico).
204 che rappresenta il nome di un operatore di tipo, \ml{Thy} � una stringa
206 � una lista di tipi che rappresentano gli argomenti dell'operatore.
212 La valutazione di
225 \index{valori di verit�, nella logica HOL@valori di verit�, nella logica \HOL{}}
227 � valutato a un valore \ML{} di tipo \ml{hol\_type} che rappresenta il tipo
232 Le costanti di tipo possono essere
233 legate a valori \ML\ e non hanno bisogno di essere costruiti ripetutamente, ad esempio il tipo costruito da\linebreak
236 con la funzione infissa \ML\ \ml{-->}. Alcune variabili di tipo comuni
238 � la variabile di tipo \ml{'a} e \ml{beta} � la variabile di tipo
239 \ml{'b}. Cos� il codice \ML\ \ml{alpha --> bool} � uguale a, ma molto pi� conciso di
255 \index{de-costruttori di tipo, nella logica HOL@de-costruttori di tipo, nella logica \HOL{}}
257 che fungono da de-costruttori per valori di tipo \ml{hol\_type}:
270 \index{variabili di tipo, nella logica HOL@variabili di tipo, nella logica \HOL{}!de-costruttori per}
273 estrae il nome di una variabile di tipo. Un tipo composto � de-costruito
275 di tipo, il nome della teoria in cui esso fu dichiarato, e una lista dei
277 le inverse di \ml{mk\_vartype} e \ml{mk\_thy\_type}, rispettivamente.
282 Le quattro specie primitive di termini della logica sono descritte in
294 \index{costruttori di termini, nella logica HOL@costruttori di termini, nella logica \HOL{}}
295 che fungono da costruttori per valori di tipo \ml{term}:
321 \item $c$ non � il nome di una costante nella teoria $\mathit{thyname}$;
322 \item $\sigma$ non � un'istanza del tipo generico di $c$
323 (il tipo generico di una costante � stabilito quando la costante � definita;
335 \index{applicazione di funzione, nella logica HOL@applicazione di funzione, nella logica \HOL{}!costruttore per}
343 \item il tipo di $t_1$ non ha la forma \ml{$\sigma'$->$\sigma$};
344 \item il tipo di $t_1$ ha la forma \ml{$\sigma'$->$\sigma$}, ma il
345 tipo di $t_2$ non � uguale a $\sigma'$.
358 \index{astrazione di funzione, nella logica HOL@astrazione di funzione, nella logica \HOL{}!costruttore per}
363 Le quattro funzioni primitive di de-costruzione sui termini sono:
365 \index{de-costruttori di termini, nella logica HOL@de-costruttori di termini, nella logica \HOL{}}
369 \index{astrazione di funzione, nella logica HOL@astrazione di funzione, nella logica \HOL{}!de-costruttori per}
370 \index{applicazione di funzione, nella logica HOL@applicazione di funzione, nella logica \HOL{}!de-costruttori per}
387 Queste sono le inverse di \ml{mk\_var}, \ml{mk\_thy\_const},
389 a termini della forma sbagliata. Altre utili funzioni di de-costruzione sono
407 \index{tipi, nella logica HOL@tipi, nella logica \HOL{}!determinazione di}
408 di un termine. La funzione
416 \noindent implementa il test di $\alpha$-convertibil� per
419 \index{$\alpha$-convertibil�, nella logica HOL@$\alpha$-convertibil�, nella logica \HOL{}!determinazione di}
421 Dal punto di vista della logica \HOL{}, i termini $\alpha$-convertibili
422 sono identici. Una variet� di altre funzioni sono disponibili per
424 (\ml{eta\_conv}), la sostituzione (\ml{subst}), l'istanziazione di tipo (\ml{inst}), la computazione delle variabili libere (\ml{free\_vars}) e
440 \index{parsing, della logica HOL@parsing, della logica \HOL{}!delle quotation di sintassi}
441 per tipi e termini \HOL{} che permettono di immettere
444 valore (con tipo \ML\ \ml{hol\_type}) di
457 \index{astrazione di funzione, nella logica HOL@astrazione di funzione, nella logica \HOL{}}
459 pu� essere usata al posto di\footnote{Per poter essere elaborata con successo
491 di tipo \ml{hol\_type} che rappresenta
500 Un segno iniziale di due punti � usato per distinguere una quotation di tipo da una quotation di termine:
506 le capacit� delle funzioni di parsing e stampa di termini e tipi
507 nel sistema. Il resto di questa sezione fornisce una breve
508 panoramica di ci� che � possibile.
511 \subsection{Inferenza di tipo}
512 \index{inferenza di tipo!nel parser HOL@nel parser \HOL{}|(}
514 Si noti che non c'� alcuna informazione esplicita di tipo in
517 Da questa informazione esso pu� inferire che entrambe le occorrenze di \ml{x} in
519 l'unica assegnazione di tipo possibile; per esempio, la prima occorrenza di
524 l'unico modo di costruire in termine con questa seconda assegnazione di tipo �
568 di sopra per inferire un tipo sensato per tutte le variabili che occorrono in un termine.
570 \index{vincoli di tipo!nella logica HOL@nella logica \HOL{}} A volte,
571 l'utente pu� voler controllare il tipo esatto di un sottotermine. Per supportare tale
573 termine un simbolo di due punti e poi un tipo. Per esempio, dato
588 Il comportamento del parser e del printer di \HOL{} � determinato
590 della collezione standard di teorie di \HOL{} se si vuole usare
596 usata nel contesto di avvio di \HOL{} ha gli operatori di tipo
618 differenti precedenze: \verb+#+ (con 70) lega in modo pi� forte di
619 \verb|+| (60), che lega pi� forte di \verb+->+ (50). Tutti gli
620 operatori di tipo suffissi (con 100) legano pi� fortemente di quelli infissi.
624 nell'ambiente di avvio di \HOL{}. L'output omesso include un elenco
625 di tutte le costanti conosciute dal sistema, inclusi gli operatori prefissi,
627 varia da operatori di binding con forza di binding molto bassa (0),
628 fino all'applicazione di funzione (2000) e alla selezione di record (2500),
686 \subsection{Controllo di namespace}
689 l'ambiguit�. L'overload di letterali numerici � discusso nella
697 l'operatore minore-di.
707 parser quando fornito nella sua forma ``fully-qualified''. Dal punto di vista sintattico, a tali
709 concreta di \HOL.
711 \index{costanti, nella logica HOL@costanti, nella logica \HOL{}!nomi di ... fully-qualified}
713 \section{Modi di Costruire Tipi e Termini}
715 \index{variabili di tipo, nella logica HOL@variabili di tipo, nella logica \HOL{}!costruttori per}
716 \index{costruttori di tipo!nella logica HOL@nella logica \HOL{}}
717 \index{costruttori di termine, nella logica HOL@costruttori di termine, nella logica \HOL{}|(}
719 La tabella di sotto mostra l'espressioni \ML\ per varie specie di quotazioni
720 di tipo\index{quotation, nella logica HOL@quotation, nella logica \HOL{}!di tipi}.
727 \index{ variabili di tipo, nella logica HOL@\ml{'a,\,'b,\,}$\ldots$ (variabili di tipo, nella logica \HOL{})}
729 \index{ operatore di tipo funzione, nella logica HOL@\ml{->} (operatore di tipo funzione, nella logica \HOL{})}
732 \index{virgolette di tipo, in ML@\ml{`:$\cdots$`} (virgolette di tipo, in \ML)}
737 {\it Specie di tipo} & {\it quotation \ML} & {\it Espressione costruttore} \\ \hline
739 Variabile di tipo &
741 Costante di tipo & $:op$ & {\small\verb+mk_type("+}$op${\small\verb+",[])+} \\ \hline
764 Modi equivalenti di immettere le quattro specie di termini primitivi sono mostrati nella
773 \index{quotation, nella logica HOL@quotation, nella logica \HOL{}!di termini primitivi}
774 \index{astrazione di funzione, nella logica HOL@astrazione di funzione, nella logica \HOL{}!symbol for}
775 \index{applicazione di funzione, nella logica HOL@applicazione di funzione, nella logica \HOL{}!costruttori per}
776 \index{applicazione di funzione, nella logica HOL@applicazione di funzione, nella logica \HOL{}!sintassi delle}
787 {\it Specie di termine} & {\it quotation \ML} &
807 \index{type checking, nella logica HOL@type checking, nella logica \HOL{}!delle quotation di sintassi|)}
809 In aggiunta alle specie di termini nella tabella di sopra, il parser supporta
844 In \LOGIC, la nozione di deduzione � stata introdotta in termini di
852 \index{conclusioni!di sequenti}
854 e il cui primo componente � un insieme di formule
857 \index{ipotesi!di sequenti}
859 Su questo era basata la nozione di un \textit{sistema
864 un insieme di coppie, il cui secondo componente � un sequente, e il cui primo
865 componente � un insieme di sequenti\footnote{Si noti che questi sequenti formano
866 una lista, non un insieme; cio�, sono ordinati.}. Fu quindi definito il concetto di un sequente
871 un insieme di sequenti attraverso un sistema deduttivo: un sequente
872 segue da un insieme di sequenti se il sequente � l'ultimo elemento di
873 qualche catena di sequenti, ognuno dei cui elementi o � nell'insieme,
879 insieme di sequenti $\Delta$, attraverso un sistema deduttivo ${\cal D}$, �
885 Un sequente che segue dall'insieme vuoto di sequenti attraverso un sistema
886 deduttivo � chiamato un \textit{teorema} di quel sistema deduttivo. In altre
891 � l'ultimo elemento di una \textit{dimostrazione}
895 (nel senso di \LOGIC) dall'insieme vuoto di sequenti. Quando una coppia
915 di tipo \holtxt{:bool} � usato per rappresentare un membro dell'insieme di
916 ipotesi di un sequente; e allo stesso modo per rappresentare la conclusione di un
937 \noindent che restituisce una coppia che consiste, rispettivamente, di una lista delle
939 \index{ipotesi!di teoremi}
941 \index{conclusioni!di teoremi}
943 di un teorema. Non si dovrebbe fare affidamento sull'ordine delle assunzioni
944 nella lista. Le ipotesi di un teorema sono disponibili anche nella forma
945 di insieme con la funzione
954 Usando \ml{dest\_thm}, sono derivate ulteriori funzioni di
968 di un teorema. Il tipo \ML\ non ha
969 una funzione costruttore primitiva. In questo modo, il sistema di tipi \ML{} protegge
972 di teoremi, che comprometterebbero
980 In \LOGIC � stato menzionato che il sistema deduttivo di \HOL{}
981 include quattro assiomi\footnote{Questa � una semplificazione: di fatto i
982 vari assiomi sono un'estensione della logica di base.}. In quel
986 di sotto). Per esempio, l'assioma \ml{BOOL\_CASES\_AX} menzionato in
999 Si noti lo speciale formato di stampa,
1007 \ml{|-}, usata per indicare lo status di tipo \ML{} \ml{thm}; insieme con
1008 l'assenza dei segni di quotation \HOL{}
1010 \index{ segno di teorema, nella logica HOL@\ml{"|-} (segno di teorema, nella logica \HOL{})}
1012 nel contesto \ml{|-}. La sessione di sotto illustra l'uso delle
1013 funzioni di de-costruzione:
1033 \noindent In aggiunta alle convenzioni di stampa menzionate di sopra, la
1034 stampa di teoremi stampa le ipotesi
1036 come dei punti (cio� un singolo punto di conclusione o dei puntini). Il flag \ml{show\_assums}
1037 \index{show_assums@\ml{show\_assums}} permette di stampare i teoremi
1039 teorema inferito, a scopo di esempio, da un altro assioma menzionato
1063 $t_1$, $t_2$, e cos� via. Nella logica \HOL{}, infinite famiglie di
1065 schemi primitivi di inferenza. %
1069 Ciascuna famiglia contiene tutte le istanze concrete di un particolare
1090 sistema \HOL{} sono descritte di sotto. E' usata qui la stessa notazione
1097 \index{conclusioni!delle regole d'inferenza} di sotto. Per le costanti logiche � usata
1100 \subsection{Introduzione di assunzione}
1102 \index{introduzione di assunzione, nella logica HOL@introduzione di assunzione, nella logica \HOL{}!funzione ML per@funzione \ML{} per}
1119 Fallisce se $t$ non � di tipo \ml{bool}.
1160 \item dove $t_1[t_2/x]$ denota il risultato di sostituire $t_2$ per $x$
1175 \subsection{Sostituzione}\index{regola di sostituzione, nella logica HOL@regola di sostituzione, nella logica \HOL{}!funzione ML per@funzione \ML\ per|(}\index{SUBST@\ml{SUBST}|(}
1197 $t[t'_1,\ldots,t'_n]$ denota il risultato di sostituire simultaneamente ciascuna
1198 di tali occorrenze di $t_i$ con $t'_i$ (per $1{\leq}i {\leq} n$),
1207 un template di termine $t[x_1,\ldots,x_n]$ in cui le occorrenze della variabile
1224 \item il tipo di $x_i$ non � uguale al tipo di $t_i$ per qualche
1226 \end{myenumerate}\index{SUBST@\ml{SUBST}|)}\index{regola di sostituzione, nella logica HOL@regola di sostituzione, nella logica \HOL{}!funzione ML per@funzione \ML\ per|)}
1228 \subsection{Astrazione}\index{regola di astrazione, nella logica HOL@regola di astrazione, nella logica \HOL{}!funzione ML per@funzione \ML\ per}
1229 \index{astrazione di funzione, nella logica HOL@astrazione di funzione, nella logica \HOL{}!regola d'inferenza per}
1258 \subsection{Istanziazione di tipo}
1259 \index{istanziazione di tipo, nella logica HOL@istanziazione di tipo, nella logica \HOL{}!funzione ML per@funzione \ML\ per}
1260 \index{tipi, nella logica HOL@tipi, nella logica \HOL{}!istanziazione di}
1279 denota il risultato di sostituire (in parallelo) i tipi $\sigma_1$,
1280 $\ldots$\ , $\sigma_n$ per le variabili di tipo $\alpha_1$, $\ldots$\ ,
1282 ,\sigma_n/\alpha_1,\ \ldots\ ,\alpha_n]$ denota il risultato di
1289 ,$\ldots$,$\alpha_n$~|->~$\sigma_n$]~$th$} restituisce il risultato di
1290 sostituire ciascuna occorrenza di $\alpha_i$ nel teorema $th$ con
1292 � una variabile di tipo.
1302 \subsection{Scaricamento di un'assunzione}\index{scaricamento di assunzioni, nella logica HOL@scaricamento di assunzioni, nella logica \HOL{}!funzione ML per@funzione \ML\ per}
1327 \ml{DISCH} fallisce se il termine dato come suo primo argomento non � di
1351 {\small\verb+MP+} prende due teoremi (nell'ordine mostrato di sopra) e restituisce
1358 \HOL{} estende la tradizione \LCF\ permettendo l'uso di un
1359 meccanismo di \emph{oracolo}, consentendo che formule arbitrarie diventino
1360 elementi del tipo \ml{thm}. Per mezzo dell'uso di questo meccanismo, \HOL{} pu�
1361 utilizzare i risultati di procedure di dimostrazione arbitrarie. Nonostante questa
1363 degli oggetti ML di tipo \ml{thm}.
1370 tag componenti del teorema. Un teorema dimostrato senza l'uso di
1393 Oltre a fornire un accesso di principio ai risultati di ragionatori
1394 esterni, i tag sono usati per implementare alcune utili operazioni di `sistema'
1397 teorema creato con questa chiamata. Questo permette agli utenti di creare direttamente
1398 utili teoremi, ad esempio, da usare come dati di test per regole d'inferenza
1400 di validit�' per le tattiche.
1417 stampata di un teorema: i primi due\footnote{I tag sono usati anche per
1418 tenere traccia dell'uso di assiomi nelle dimostrazioni.} comprendono i tag componenti e il
1419 terzo � la lista standard di assunzioni. Il tag componente di un teorema
1440 \index{teorie, nella logica HOL@teorie, nella logica \HOL{}!rappresentazione di|(}
1452 la struttura di tipo di ${\cal T}$;
1454 la firma di ${\cal T}$;
1456 l'insieme di assiomi di ${\cal T}$;
1457 \item ${\sf Theorems}_{\cal T}$ � l'insieme di
1458 teoremi di ${\cal T}$.
1461 Nell'implementazione di \HOL, le teorie sono strutturate in modo gerarchico
1462 per rappresentare sequenze di estensioni chiamate
1465 \index{segmenti di teoria}
1467 di una teoria iniziale chiamata \ml{min}\index{min@\ml{min}}. Un segmento di
1473 \index{genitori, di teorie HOL@genitori, di teorie \HOL{}}
1475 La teoria rappresentata da un segmento � ottenuta prendendo l'unione di
1478 raggiungibili seguendo i puntatori ai genitori. Questa collezione di
1482 \index{teorie, nella logica HOL@teorie, nella logica \HOL{}!gerarchie di}
1486 \index{teorie, nella logica HOL@teorie, nella logica \HOL{}!rappresentazione di|)}
1491 Un tipico\index{sistema HOL@sistema \HOL{}!lavoro tipico in} pezzo di lavoro
1492 con il sistema \HOL{} consiste in un numero di sessioni\index{sessioni
1493 con il sistema HOL@sessioni, con il sistema \HOL{}}. Nella prima di queste, � creata
1494 una nuova teoria, diciamo ${\cal T}$, importando qualche segmento di teoria
1495 esistente, facendo una serie di definizioni, e magari dimostrando e
1498 $name$\ml{Theory} il cui contenuto � il segmento di teoria attuale
1500 desiderata ${\cal T}$. Le sessioni di lavoro successive possono accedere alle
1501 definizioni e ai teoremi di ${\cal T}$ importando $name$\ml{Theory};
1502 questo evita di dover caricare gli strumenti e rieseguire
1509 $thy$ � il nome dell'attuale segmento di teoria quando l'elemento fu
1511 funzioni \ml{new\_axiom}, \ml{new\_definition}, di sotto). Elementi differenti
1513 Cos� ciascun segmento di teoria fornisce un namespace separato di binding ML di
1517 di teoria, incluso lo status di parsing delle costanti (ad esempio se
1523 rappresentata dal segmento di teoria attuale insieme con la sua
1524 stirpe. Il nome del segmento di teoria attuale � restituito dalla funzione
1534 gi� nel contesto logico. L'insieme esatto di teorie nel
1539 L'esatto insieme di teorie caricate pu� essere determinato con il
1550 della gerarchia delle teorie. L'argomento � il nome di una teoria (o
1568 \paragraph{Creare un segmento di teoria}
1570 \index{teorie, nella logica HOL@teorie, nella logica \HOL{}!creazione di|(}
1572 Nuovi segmenti di teoria sono creati con una chiamata a \ml{new\_theory}.
1582 di teoria hanno effetto. Se la teoria attuale (diciamo $thy_1$) al momento
1583 di una chiamata a {\small\verb+new_theory +}$thy_2$ non � vuota, cio�, � stato
1587 il segmento attuale di teoria � gi� chiamato $thy$, allora questo �
1588 interpretato semplicemente come una richiesta di ripulire l'attuale segmento di teoria
1598 \item se � necessario esportare il segmento attuale prima di creare
1599 il nuovo e il tentativo di export fallisce.
1602 All'avvio, il segmento di teoria attuale di \HOL{} � chiamato \ml{scratch},
1603 che � una teoria vuota, che ha un'utile collezione di teorie nella
1607 Il segmento attuale di teoria agisce come una sorta di blocco di appunti. Gli elementi archiviati
1609 cancellati completamente. Ogni elemento di teoria che fosse stato sovrascritto
1618 \index{teorie, nella logica HOL@teorie, nella logica \HOL{}!creazione di|)}
1624 un segmento di teoria esistente semplicemente importando il modulo corrispondente.
1635 {\small\verb+loadPath+}. Qualunque antenato di
1636 $name$ sar� caricato prima che il caricamento di $name${\small\verb+Theory+}
1643 Le seguenti funzioni \ML{} aggiungono tipi e termini al segmento di teoria
1645 necessarie dal momento che funzionalit� di definizione di pi� alto livello invocheranno queste
1646 in caso di necessit�. Tuttavia, queste funzioni possono essere utili per coloro che scrivono
1647 strumenti di dimostrazione e principi derivati di definizione.
1658 un nuovo operatore di tipo\index{operatori di tipo, nella logica HOL@operatori di
1659 tipo, nella logica \HOL{}!dichiarazione di} $n$-ario nella teoria attuale. Se
1671 $c_{\sigma'}$ una nuova costante\index{costanti, nella logica HOL@costanti, nella logica \HOL{}!dichiarazione di} della teoria attuale,
1672 per ogni $c_{\sigma'}$ dove $\sigma'$ � un'istanza di $\sigma$.
1675 HOL@tipi generici, nella logica \HOL{}} di $c$.
1687 \ml{(\lb\rb{},$t$)} essere un assioma\index{assiomi!dichiarazione di, nella logica HOL@dichiarazione di, nella logica \HOL{}} della teoria attuale con nome $name$.
1690 \item il tipo di $t$ non � \verb+bool+.
1693 tipi che sono stati ri-dichiarati dopo che � stato eseguito il build di $t$.
1709 \index{teoremi, nella logica HOL@teoremi, nella logica \HOL{}!salvataggio di}
1712 $\mathit{th}$ con nome $\mathit{name}$ nel segmento di teoria
1717 Una volta che un segmento di teoria � stato costruito, pu� essere scritto su un
1729 teoria. Il segmento di teoria attuale � scritto sul file
1730 $name${\small{\tt Theory.sml}} nell'attuale directory di lavoro. Anche il
1731 file $name${\small{\tt Theory.sig}}, che documenta il contenuto di
1732 $name$, � scritto nell'attuale directory di lavoro. Si noti che
1735 le dipendenze tra collezioni di segmenti di teoria \HOL{}.
1743 Gli argomenti di tipo \ML{} \ml{string} a \ml{new\_axiom},
1746 funzioni \ml{axiom}, \ml{definition}, ecc., descritte di sotto.
1757 Ci sono varie funzioni per caricare il contenuto dei file di teoria:
1770 \noindent Il primo argomento � il nome di una teoria (che deve essere nella
1771 stirpe dell'attuale segmento di teoria); il risultato � una lista delle
1775 \index{ abbreviazione, di parte dei nomi di teoria HOL@\ml{-} (abbreviazione, di parte dei nomi di teoria \HOL{})}
1780 Nel caso di \ml{types} � restituita una lista di coppie ariet�-nome.
1797 una lista di tutti gli assiomi, definizioni e teoremi della teoria con
1814 \index{stampa, nella logica HOL@stampa, nella logica \HOL{}!di teorie}
1822 \index{teorie, nella logica HOL@teorie, nella logica \HOL{}!estensione di|(}
1825 Ci sono tre specie di estensioni definizionali:
1826 definizioni di costante, specifiche di costane e definizioni di tipo.
1828 \subsubsection{Definizioni di costante}
1831 In \LOGIC{} una definizione di costante
1833 \index{estensione, della logica HOL@estensione, della logica \HOL{}!per definizione di costante}
1834 \index{estensione per definizione di costante, della logica HOL@estensione per definizione di costante, della logica \HOL{}!funzione ML per@funzione \ML\ per}
1839 \item $c$ non � il nome di alcuna costante in $\Sigma_{\Omega}$;
1841 \item tutte le variabili di tipo che occorrono in $t_{\sigma}$ occorrono in $\sigma$.
1844 In \HOL, le definizioni possono essere leggermente pi� generali di questo, nel senso che
1850 strutture variabili (cio� tuple di variabili distinte). Una tale equazione �
1855 \noindent che � una definizione nel senso di \LOGIC{} se valgono (i),
1858 La seguente funzione \ML\ crea\index{meccanismi di definizione, per la logica HOL@meccanismi di definizione, per la logica \HOL{}} una nuova definizione nella
1872 \ml{(\lb\rb{},$c = \lambda v_1\ \cdots\ v_n.\ t$)} essere una definizione di costante
1881 \item c'� una variabile di tipo in $v_1$, $\dots$, $v_n$ o $t$
1882 che non occorre nel tipo di $c$.
1885 \subsubsection{Specifiche di costante}
1888 \index{specifica di costanti, nella logica HOL@specifica di costanti, nella logica \HOL{}|(}
1890 \index{estensione, della logica HOL@estensione, della logica \HOL{}!per specifica di costante}
1892 In \LOGIC{} una specifica di costante\index{estensione per specifica di costante, della logica HOL@estensione per specifica di costante, della logica \HOL{}!funzione ML per@funzione \ML\ per} per una teoria ${\cal T}$
1911 La seguente funzione \ML\ � usata per fare specifiche di costante nel
1938 con nome $name$, come una definizione nell'attuale segmento di teoria. Una chiamata a
1942 \item il teorema argomento non ha una lista vuota di assunzioni;
1945 \item il tipo di qualche $c_i$ non contiene tutte le variabili
1946 di tipo che occorrono nel termine
1950 \index{specifica di costanti, nella logica HOL@specifica di costanti, nella logica \HOL{}|)}
1952 \subsubsection{Definizioni di tipo}
1955 \index{estensione, della logica HOL@estensione, della logica \HOL{}!per definizione di tipo|(}
1957 \index{definizioni di tipo, nella logica HOL@definizioni di tipo, nella logica \HOL{}|(}
1962 \index{definizioni di tipo, nella logica HOL@definizioni di tipo, nella logica \HOL{}!introduzione di}
1963 \index{estensione per definizione di tipo, nella logica HOL@estensione per definizione di tipo, nella logica \HOL{}!funzione ML per@funzione \ML\ per|(}
1966 consiste nell'introdurre $\ty{op}$ come un nuovo operatore di tipo $n$-ario e
1971 che caratterizza\index{predicato caratteristico, di definizioni di tipo} un
1972 sottoinsieme non vuoto di un tipo esistente $\sigma$. Formalmente, una definizione di tipo
1983 \item \ty{op} � il nome di una costante di tipo in ${\sf Struc}_{\cal T}$.
1984 \item $p\in{\sf Terms}_{\cal T}$ � un termine chiuso di
1990 La seguente funzione \ML\ esegue una definizione di tipo nel sistema \HOL{}.
1998 \noindent Se $t$ � un termine di tipo
1999 $\sigma$\ml{->bool} contenente $n$ distinte variabili di tipo, allora
2009 \noindent risulta nella dichiarazione di \ty{op} come un nuovo operatore di tipo $n$-ario
2011 definizionale\index{operatori di tipo, nella logica HOL@operatori di tipo, nella logica \HOL{}!assiomi definizionali per}:
2036 \index{estensione, della logica HOL@estensione, della logica \HOL{}!per definizione di tipo|)}
2037 \index{teorie, nella logica HOL@teorie, nella logica \HOL{}!estensione di|)}
2038 \index{estensione per definizione di tipo, nella logica HOL@estensione per definizione di tipo, nella logica \HOL{}!funzione ML per@funzione \ML\ per|)}
2039 \index{definizioni di tipo, nella logica HOL@definizioni di tipo, nella logica \HOL{}|)}
2042 \index{definizioni di tipo, nella logica HOL@definizioni di tipo, nella logica \HOL{}!definire le biezioni per|(}
2044 Il risultato di una definizione di tipo usando \ml{new\_type\_definition} � un teorema
2045 che asserisce solo l'{\it esistenza\/} di una
2046 biezione\index{biezione di tipi, nella logica HOL@biezione di tipi, nella logica \HOL{}}
2047 dal tipo che esso definisce al corrispondente sottoinsieme di un tipo esistente. Per
2048 introdurre costanti che di fatto denotano una tale biezione e la sua inversa, �
2061 la definizione di costante (di fatto, una specifica di costante) fatta da
2062 {\small\verb!define_new_type_bijections!} sar� archiviata nel segmento di teoria
2067 teorema fornito, e il tipo rappresentante di questo tipo
2091 \noindent Questo teorema, che � la propriet� di definizione per le costanti
2093 di teoria. Esso � anche il valore restituito da \ml{define\_new\_type\_bijections}.
2094 Il teorema dichiara che \m{abs} � l'inversa sinistra di \m{rep} e---per
2095 valori che soddisfano \ml{P}---che \ml{rep} � l'inversa sinistra di \m{abs}.
2105 \index{definizioni di tipo, nella logica HOL@definizioni di tipo, nella logica \HOL{}!definire biezioni per|)}
2107 \paragraph{Propriet� delle biezioni di tipo}
2109 \index{definizioni di tipo, nella logica HOL@definizioni di tipo, nella logica \HOL{}!propriet� delle biezioni per|(}
2127 \noindent Il teorema argomento a ciascuna di queste funzioni deve essere un teorema
2135 \noindent Se \m{th} � un teorema di questa forma, allora valutare
2144 sopra (onto [n.d.t]) l'insieme di valori che soddisfano \m{P}:
2170 abbia la forma di un teorema restituito da \ml{define\_new\_type\_bijections}.
2171 Nessuna di queste funzioni salva alcunch� nella teoria attuale.
2173 \index{definizioni di tipo, nella logica HOL@definizioni di tipo, nella logica \HOL{}!propriet� delle biezioni per|)}