IT/Description/theories.tex

31 Per un elenco completo degli assiomi, definizioni e teoremi in \HOL, si vedano le risorse online distribuite con il sistema.
32 In particolare, il file HTML \url{help/HOLindex.html} � un buon punto di partenza per esplorare le teorie disponibili.
94 logica \HOL{}, includendo le operazioni booleane e
114 per la logica di ordine superiore. Questi assiomi, insieme con le regole
125 differenza pi� grande � che nella formulazione di Church le variabili di tipo
273 Gli altri tre assiomi della teoria \theoryimp{bool}, le regole
289 La teoria \theoryimp{bool} fornisce anche le definizioni di un numero di
313 completa di come le espressioni \holtxt{let} sono tradotte, si veda
342 sono le restrizioni dei quantificatori esistenziale e universale:
364 Per completezza, sono fornite le versioni ristrette dell'esistenza unica e
379 predicati arbitrari per restringere le variabili di binding. Il parser \HOL{}
380 permette la quantificazione ristretta su tutte le variabili di una sequenza di variabili
430 valori (di tipo \ml{term}) come le altre quotation nella stessa riga.
587 per le congiunzioni, le disgiunzioni, e le implicazioni rispettivamente.
645 contiene le definizioni della composizione di funzione (\ml{o} infisso),
699 Non ci sono teoremi circa \ml{:>}; il suo uso � una sintassi conveniente per le applicazioni di funzione.
700 Per esempio, le catene di update possono perdere qualche parentesi se scritte
706 Questa presentazione rende anche l'ordine in cui le funzione sono applicate da sinistra a destra.
750 converte le espressioni di tipo della forma \holtxt{:$\sigma_1$\#$\sigma_2$}
773 $\sigma_1$\holtxt{\#}$\sigma_2$. Di solito, le coppie sono scritte all'interno
815 Poi, sono introdotte le funzioni di rappresentazione e astrazione \holtxt{REP\_prod}
848 Skolemizzando {\small\verb+ABS_PAIR_THM+} e facendo le specifiche di costante
871 Questa conversione � compiuta attraverso le funzioni \holtxt{CURRY} e
906 rimpiazzare le variabili con tuple di variabili. I seguenti teoremi
925 funzioni ricorsive. Per le coppie, la combinazione lessicografica
1071 applica ripetutamente le trasformazioni:
1090 le operazioni di de-costruzione. Per esempio:
1108 I lettori sono incoraggiati a convincersi che le traduzioni dei
1173 con le funzioni discriminatore \ml{ISL} e \ml{ISR}:
1228 Il nome di questo valore � \holtxt{the\_value}, ma il parser e il pretty-printere sono impostati cos� che per il tipo \holtxt{$\alpha$~itself}, \holtxt{the\_value} pu� essere scritto come \holtxt{(:$\alpha$)} (la sintassi include le parentesi).
1263 Le option possono essere usate per modellizzare le funzioni parziali. Se una funzione di tipo
1269 Come tipo induttivo, le option hanno un teorema di ricorsione che supporta la
1302 \index{mapping di funzioni, nella logica HOL@mapping di funzioni, nella logica \HOL{}!per le option}
1331 di questo, in \theoryimp{arithmetic} � sviluppata un'ampia teoria che tratta le operazioni aritmetiche
1341 teoria, sono definite le costanti \ml{0}
1376 le definizioni arbitrariamente ricorsive
1391 importante sono le funzioni \emph{ricorsive primitive}\footnote{Nella
1467 \noindent dove tutte le variabili libere nei termini $t_1$,
1502 per denotare la funzione ricorsiva che soddisfa le due equazioni nel corpo
1515 soddisfa le equazioni di definizione ricorsiva primitiva date dal teorema mostrato
1548 fare queste dimostrazioni per le ricorsioni primitive.
1554 giustificare le definizioni ricorsive. Per esempio, la teoria
1612 La teoria \HOL{} \theoryimp{arithmetic} contiene le definizioni ricorsive
1660 modulo ({\small\verb+MOD+}, infisso) � usata una specifica di costante, insieme con le loro
1813 aritmetiche, che usano i nomi usuali per le operazioni, ad esempio \verb|+|,
1839 come prefisso le stringhe \holtxt{0b} e \holtxt{0x} rispettivamente. Le
1840 `cifre' A--F nei numeri esadecimali possono essere scritte con le lettere maiuscole o
1841 minuscole. I numeri binari hanno le loro cifre pi� significative pi� a sinistra. Ai
1848 (\ml{\_}). Questi possono essere usati per raggruppare le cifre per aggiungere leggibilit�
2003 componente non deve essere zero. Per rendere le cose pi� semplici nella teoria \HOL\,
2032 I teoremi nella teoria dei numeri razionali includono le propriet� del campo,
2033 le regole aritmetiche la manipolazione delle (in)equazioni e la loro riduzione a
2034 (in)equazioni tra interi, le propriet� delle relazioni minore-di e la
2084 le sequenze.
2101 Sono definite le operazioni aritmetiche standard, con dimostrati gli appropriati teoremi che le riguardano.
2118 un intero positivo $N$, e restituisce un intero $n$ nel range $0\le
2119 n < N$, selezionato uniformemente a caso tra le scelte possibili. Questa
2143 2005\footnote{La teoria attuale sussume teorie di parola precedenti -- si � evoluta da uno sviluppo basato su una costruzione di classi di equivalenza. La teoria di parola di Wai Wong, che era basata sulla teoria \ml{rich\_list} di Paul Curzon, non � pi� distribuita con HOL. I principali vantaggi della teoria attuale sono che c'� un'unica teoria per tutte le dimensioni di parole e che non sono richiesti effetti secondari della lunghezza delle parole.}
2167 \holtxt{y} sono uguali se, e solo se, tutte le loro componenti \oo{x}{i} e
2186 \ml{FCP\_ETA} mostra che si pu� eliminare un binding quando tutte le componenti
2289 e tutte le operazioni aritmetiche sono definite usando i numeri
2294 a destra, dove sono necessarie le varianti con segno e senza segno. Quando
2304 Sono fornite le operazioni booleane bit field standard, cio� la negazione bitwise
2398 Sono forniti tutti gli ordinamenti parola standard, con le versioni con e senza
2540 le liste. Il parser \HOL{}
2561 \index{assiomi!non-primitivi, della logica HOL@non-primitivi, della logica \HOL{}!per le liste}
2562 \index{teoremi d'induzione, nella logica HOL@teoremi d'induzione, nella logica \HOL{}!per le liste}
2563 \index{teorema caratterizzante!per le liste}
2583 \index{teorema di ricorsione primitiva!per le liste}
2596 Il teorema d'induzione per le liste, \ml{list\_INDUCT}, fornisce lo strumento
2605 sono usati per il ragionamento equazionale circa le liste.
2609 \index{selettori, nella logica HOL@selettori, nella logica \HOL{}!per le liste}
2624 \noindent Nella teoria \ml{list} sono definite anche le seguenti funzioni.
2736 Il comportamento di \holtxt{MAP2} nel caso in cui le siano date liste di
2829 quando le liste non sono della stessa lunghezza. L'operazione inversa,
2907 e ogni membro ha lo stesso numero di occorrenze in entrambe le liste. Una
2927 utile nelle dimostrazioni circa le permutazioni.
3001 teoria delle liste, le analoghe funzioni \ml{HD} e \ml{TL} hanno
3134   \item gli elementi testa di $l_3$ e $l_4$ sono gli stessi, e le
3202 C'� sempre un tale elemento, e le equazioni di definizione sono
3325 Tutte le funzioni e i predicati sulle liste sono cos� disponibili per l'uso
3360 I letterali stringa possono essere costruiti usando le varie speciali sequenze
3376 le stringhe che restituisce un tipo opzione.
3400 Una tale espressione � di fatto un'espressione case sulla lista sottostante, e cos� la costante sottostante � quella per le liste.
3436 $\alpha \to \konst{bool}$, cio�, essi sono le cosiddette funzioni
3612 Come menzionato, le operazioni su insiemi si applicano sia a insiemi finiti che
3628 \theoryimp{pred\_set}, le propriet� delle operazioni su insiemi finiti devono
3711 con le altre, ma non esprimono al cun teorema profondo della teoria degli insiemi.
3769 essere le variabili libere dell'altro termine. Se entrambi hanno variabili
3771 in cui le variabili sono elencate nella struttura di variabili
3849 le variabili menzionate in \holtxt{vs} devono soddisfare il vincolo
3882 sollever� un errore. (Inoltre, le parentesi pi� esterne intorno
3948 $b_2$ a condizione che ogni elemento in $b_1$ occorra almeno le stesse volte in
4031 Lo spostamento tra bag e insiemi si ottiene con le seguenti due
4267 Da queste definizioni, si possono recuperare le regole iniziali.
4374 definita induttivamente, da essa possono essere derivate le sue regole, il teorema di analisi dei casi e
4400 sequenza di chiamate ricorsive � $R$-decrescente, allora le equazioni
4401 di ricorsione specificano un'unica funzione totale e le equazioni possono essere
4423 {\small\verb+WFREC_COROLLARY+} sono usati per automatizzare le definizioni
4425 di base per le relazioni benfondate, insieme con i teoremi che affermano
4474 le sostituzioni e gli array. Il tipo rappresentate � $\alpha\to\beta +
4484 (\holtxt{FAPPLY}), e il dominio di una mappa (\holtxt{FDOM}) sono le
4618 Per quanto possibile, le mappe finite dovrebbero essere come funzioni ordinarie.
4642 le funzioni composte sono mappe finite o no. La composizione di due
4722 le istanziazione per \verb+B+ e \verb+C+ devono essere conosciute prima