IT/Description/definitions.tex

103 curried. Si noti anche che non � menzionato alcun parametro di tipo
107 non ha abbastanza informazione per determinare sempre l'ordine degli
145 Altri tipi non ricorsivi possono essere definiti cos�:
197 la lista dei suoi sotto-alberi. In un tale caso, i nodi foglia non hanno bisogno di essere
273 Ora ci rivolgiamo ad alcuni tipi che non possono essere dichiarati con \ml{Hol\_datatype}.
274 In alcuni casi essi non possono esistere del tutto in HOL; in altri, il tipo
275 pu� essere incorporato nella logica HOL, ma \ml{Hol\_datatype} non � in grado di rendere
278 Per prima cosa, un tipo vuoto non � permesso in HOL, cos� il seguente tentativo
288 I cosiddetti `tipi annidati', che occasionalmente sono piuttosto utili, non possono
299 I tipi non possono eseguire la ricorsione su entrambi i lati delle frecce funzione. La ricorsione
301 \ml{Hol\_datatype} non � in grado di definire tipi algebrici che
313 esempio, HOL non permette il seguente tentativo di modellare il lambda
314 calcolo non tipizzato come un insieme (si noti la \holtxt{->} nella clausola per il
414 risultano nell'aggiunta o cancellazione di altri campi non invalideranno
415 questo riferimento. Una mancanza nei tipi record dell'SML � che non
441 L'ordine in cui i campi sono inseriti non � significativo. Oltre
618 alcuni dettagli che sono evidenti al livello inferiore non sono pi�
621 Formare semplicemente un nuovo tipo non completa l'operazione quoziente.
625 pi� alto, e pi� astratto. Questo include non solo i nuovi
672 un teorema che {\it R\/} � una relazione di equivalenza parziale non vuota,
778 non � necessaria.
802 La sintassi base (dove il $\mathit{term}$ non-terminale sta per qualsiasi termine \HOL{}) �
871 Tuttavia, i letterali e i costruttori non possono essere mischiati come alternative
908 e anche l'uso di una wildcard \ml{\_} per matchare i casi non forniti.
952 della funzione. \ml{Define} non ha sempre successo nel tentare di
1017 � incompleta dal momento che non dice come \holtxt{f} dovrebbe comportarsi quando
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
1027 In sintesi, \ml{Define} deriver� le equazioni non ambigue e
1042 da \ml{Define}, l'ultima equazione � rimossa dal momento che non � stata
1063 Altrimenti, la funzione non �
1069 non � archiviato un teorema d'induzione per le funzioni ricorsive primitive, dal
1119 Dal momento che \holtxt{fact} non �
1170 Poi facciamo una definizione ricorsiva primitiva. Si noti che, in questo caso, non
1235 \ml{Define} pu� anche essere usata per definire funzioni non-ricorsive.
1244 \ml{Define} pu� essere usata anche per definire funzioni non-ricorsive
1263 \subsection{Quando la terminazione non � dimostrata automaticamente}
1308 che restituisce il seguente valore di tipo \ml{defn}, ma non tenta di
1465 dal momento che sappiamo che \holtxt{m} non � 0, si da il caso che
1523 Dal momento che la dimensione dell'albero non � modificata nell'ultima clausola nella
1524 definizione di \holtxt{Unbal}, una semplice misura di dimensione non funziona. Piuttosto,
1685 che non sono dimostrabili, perch� il \emph{contesto} delle chiamate ricorsive non �
1686 stato preso in considerazione. Questo esempio di fatto non � un problema per HOL,
1732 il processo di terminazione non finisce, ed appaiono come ipotesi nel risultato
1793 \holtxt{ltree\_sigma} non � applicata in modo completo, bisogna fare degli sforzi
1818 \holtxt{(f, Node v tl)}. Tuttavia, questo � un compito senza speranza, dal momento che non c'� alcuna
1821 non ha funzionato in modo appropriato, perch� non conosceva una regola di congruenza
1878 Questo, comunque, non � derivabile in \HOL{}, perch� gli schemi di ricorsione
1917 su variabili che non sono state ancora istanziate. Una volta che sono trovate
1948 e i nomi delle costanti-to-be non devono essere quantificate in
1949 ciascuna {\nonterm{clausola}}. Una {\nonterm{clausola}} non dovrebbe avere
1954 esistenziale nelle ipotesi. Se una clausola non ha variabili libere,
1955 � ammissibili non avere alcuna quantificazione universale.)
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}.
2080 variabile schematica, non � quantificata nelle regole. Questo �
2107 non hanno bisogno di essere contigue.
2116 Dal momento che il lato destro di questo teorema includer� spesso altre occorrenze della relazione, non � in generale sicuro riscrivere semplicemente con esso.