IT/Description/theories.tex

84 \noindent Nella teoria \theoryimp{min} non si trova alcun teorema o assioma.
268 s� stesso che non � suriettiva. Questo implica che il tipo \holtxt{ind}
276 in linea di principio, l'utente del sistema \HOL{} non dovrebbe avere mai bisogno
282 non-definizionale. In pratica, � spesso molto allettante correre il rischio di
392 \index{quotation, nella logica HOL@quotation, nella logica \HOL{}!of non-primitive terms|(}
444 \index{termini, nella logica HOL@termini, nella logica \HOL{}!non-primitivi}
468 \multicolumn{4}{|c|}{\bf Termini non-primitivi} \\
594 \index{quotation, nella logica HOL@quotation, nella logica \HOL{}!di termini non-primitivi|)}
713 talvolta non � conveniente perch� spesso essi sono desiderati come nomi
797 un $\beta$-redex non ridotto al fine di soddisfare l'interfaccia
806 L'operatore di tipo {\small\verb%prod%} � definito invocando \ml{new\_type\_definition}\index{new_type_definition@\ml{new\_type\_definition}} con questo teorema che risulta nell'asserazione nella teoria \ml{pair} dell'assioma definizionale \index{assiomi!non-primitivi, della logica HOL@non-primitivi, della logica \HOL{}!per prodotti} \index{assiomi!nella teoria bool@nella teoria \ml{bool}} \ml{prod\_TY\_DEF} mostrato di sotto.
982 \noindent fino a quando non rimane pi� alcuna struttura variabili. Per esempio:
1000 \ml{\bs(x,y).x+y}, non � un sottotermine della astrazione
1264 $\alpha\rightarrow\beta$ non valori $\beta$ utili per tutti
1347 \index{assiomi!non-primitivi, della logica HOL@non-primitive, della logica \HOL{}!per i numeri naturali}
1364 \ml{INDUCTION} non potrebbe essere enunciato come un singolo assioma nella logica del
1365 primo ordine perch� i predicati (ad esempio \holtxt{P}) non possono essere quantificati.
1380 non sono permesse. Per esempio, non c'� alcuna funzione $f$ (di tipo
1431 	di conseguenza contiene la seguente definizione non ricorsiva di \ml{<}:
1445 contiene {\small\verb%m%} ma non {\small\verb%n%}.
1540 definizioni ricorsive primitive su un range di tipi, non solo sui
1545 primitiva, insieme con altri stili di ricorsione, e non richiede
1547 richiedere di eseguire dimostrazioni di terminazione; fortunatamente, non � necessario
1571 benfondatezza di una relazione $R$ � quello di dire che non ha infinite
1764 numerali: \ml{1}, \ml{2}, \ml{3}, \etc. Tuttavia, la logica \HOL{} non ha
1842 fini della retro-compatibilit� i numeri ottali non sono
1849 e non hanno alcun effetto semantico.
2003 componente non deve essere zero. Per rendere le cose pi� semplici nella teoria \HOL\,
2052 {\small\verb+hrealTheory+}, ma non � usata una volta che i reali sono stati
2111 non a tutti gli insiemi pu� essere assegnata una probabilit� (il paradosso di
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.}
2280 L'operazione \holtxt{word\_concat:\worda\rarr\wordb\rarr\wordc} concatena parole. Si noti che il tipo restituito non � vincolato. Questo significa che due parole di sedici bit possono essere concatenate per dare una parola di qualsiasi lunghezza -- che pu� essere pi� piccola o pi� grande del valore atteso di 32. La funzione correlata \holtxt{word\_join} restituisce una parola della lunghezza attesa, cio� di tipo fcp{\bool}{$\alpha+\beta$}; comunque, l'operazione di concatenazione � pi� utile perch� spesso vogliamo \fcp{\bool}{\ty{32}} e non il logicamente distinto \fcp{\bool}{\ty{16}+\ty{16}}.
2285 in complemento a due) o come non aventi segno. Tuttavia, questo non �
2286 reso esplicito all'interno della teoria\footnote{Le parole non sono etichettate come
2287 	aventi/non aventi segno. Sono forniti mapping a/da interi (\holtxt{w2i} e
2292 sotto la rappresentazione in complemento a due. Questo tuttavia non avviene
2561 \index{assiomi!non-primitivi, della logica HOL@non-primitivi, della logica \HOL{}!per le liste}
2604 non possono dare origine alla stessa struttura. Insieme, questi tre teoremi
2631 un lista vuota o non vuota hanno la sintassi di superficie (grossomodo presa in prestito
2715 o uguale a $n$, il risultato di \holtxt{EL~$n$~$\ell$~} non �
2750 di tutti gli elementi in una lista che non soddisfano il predicato dato
2828 l'operazione {\small\verb+ZIP+}. Il risultato non � specificato
2829 quando le liste non sono della stessa lunghezza. L'operazione inversa,
2849 (\holtxt{LAST}) di una lista non vuota in modo diretto. L'ultimo elemento
2850 di una lista non vuota � eliminato attraverso \holtxt{FRONT}.
2862 Concatenare la parte frontale e l'ultimo elemento di una lista non vuota porta
2864 sono non specificate su liste vuote.
2885 lista (clausola 1); che nessuna lista non vuota � un prefisso della lista vuota
2886 (clausola 2); e che una lista non vuota � un prefisso di un'altra lista
2887 non vuota se i primi elementi delle liste sono gli stessi, e se la coda
3002 semplicemente dei valori non specificati quando applicate alle liste vuote.)
3004 Il tipo \ml{llist} non � induttivo, e non c'� alcun teorema di
3210 Dall'altro lato, la funzione \ml{last} non ha sempre un
3222 valore di \ml{last} su tali percorsi non � specificato:
3390 un termine sia una stringa vuota o non vuota possono essere scritte con la
3481 Il simbolo Unicode per $\mathbb{U}$ � U+1D54C, e potrebbe non esistere in molti set di font.
3595 Un insieme � infinito sse non � finito, e c'� un'abbreviazione nel sistema che esegue il parsing di \holtxt{\holquote{INFINITE~s}} in \holtxt{\holquote{\td{}FINITE~s}}.
3615 cardinalit� di un insieme infinito non � specificata.
3708 TCi sono molte altre definizioni in \theoryimp{pred\_set}, ma non sono
3711 con le altre, ma non esprimono al cun teorema profondo della teoria degli insiemi.
3768 $t$ o $p$ non hanno variabili libere, allora $x_1, \ldots, x_n$ sono considerate
3770 libere, ma non c'� sovrapposizione, allora risulta un errore. L'ordine
3839 \paragraph{Comprensioni d'insieme non ambigue} C'� anche una sintassi
3840 della comprensione d'insieme non ambigua, che permetter all'utente di
3856 � l'insieme dei numeri da \holtxt{y} fino a ma non incluso
3868 Il componente \holtxt{vs} della notazione non ambigua deve essere una singola
3885 La notazione non ambigua � stampata dal pretty-printere ogni volta che
3886 l'insieme da stampare non pu� essere espressa con la notazione di default, o
3906 Il multinsieme vuoto non ha elementi. Cos�, la funzione che lo implementa
3996 di mezzo rispetto all'ultimo. Questa non � la stessa cosa di usare
4016 dove tutti gli elementi che non sono nell'insieme sono stati rimossi.
4047 del multinsieme. Tuttavia, c'� un problema se $f$ non � iniettiva
4052 stipulare che la funzione sia solo finitamente non-iniettiva, o che
4148 generalit� extra non fa male.) La teoria \theoryimp{relation}
4360 Una relazione $R$ � benfondata ({\small\verb+WF+}) se ogni insieme non-vuoto
4600 (\holtxt{FUNION\_DEF}) non � simmetrica: il dominio della prima mappa
4670 funzioni totali, permetta la definizione di funzioni che non sembrano
4690 la seguente funzione totale e non-ricorsiva: