1\newcommand{\eos}{\hfill{}$\cdots\diamond\cdots$\hfill{}\vspace{5mm}} 2 3\newcommand{\mathpredn}{\mathbin{-\!\!\!\mid\mid\!\rightarrow}} 4 5\newcommand{\KC}{\con{K}} 6\newcommand{\SC}{\con{S}} 7\newcommand{\bk}{\char'134} 8 9 10\chapter{Esempio: Logica Combinatoria} 11\label{chap:combin} 12 13\section{Introduzione} 14\label{sec:Introduction} 15 16Questo piccolo caso di studio � una formalizzazione di una logica 17combinatoria (priva di variabili). Questa logica � d'importanza fondamentale 18nell'informatica teorica, ed ha una ricca teoria. L'esempio 19si basa principalmente su uno sviluppo fatto da Tom Melham. Lo script 20completo per lo sviluppo � disponibile come \texttt{clScript.sml} nella 21directory \texttt{examples/ind\_def} della distribuzione. E' 22autosufficiente e cos� include le risposte agli esercizi fissati al 23termine di questo documento. 24 25Le sessioni HOL assumono che la traccia Unicode sia \emph{accesa} (cos� 26come � di default), il che significa che bench� gli input possono essere scritti in 27puro ASCII, l'output usa tuttavia degli eleganti caratteri Unicode (simboli come 28$\forall$ e $\Rightarrow$). I simboli Unicode potrebbero essere usati anche 29nell'input. 30 31 32\section{Il tipo dei combinatori} 33\label{sec:Type-Combinators} 34 35La prima cosa che dobbiamo fare � definire il tipo dei 36\emph{combinatori}. Di questi ce ne sono soltanto due, \KC{} e \SC, ma 37dobbiamo anche essere in grado di \emph{combinarli}, e per questo abbiamo bisogno 38di introdurre la nozione di applicazione. In mancanza di un simbolo ASCII 39migliore, useremo il cancelletto (\#) per rappresentare questo nella logica: 40\setcounter{sessioncount}{0} 41\begin{session} 42\begin{verbatim} 43- Hol_datatype `cl = K | S | # of cl => cl`; 44> val it = () : unit 45\end{verbatim} 46\end{session} 47Vogliamo anche che \# sia un infisso, cos� lo impostiamo come uno stretto infisso 48associativo a sinistra: 49\begin{session} 50\begin{verbatim} 51- set_fixity "#" (Infixl 1100); 52> val it = () : unit 53\end{verbatim} 54\end{session} 55 56 57% C = S (S (K S) (S (K K) S)) (K K) 58 59 60\section{Regole di riduzione dei combinatori} 61\label{sec:Comb-Reduct} 62 63La logica combinatoria � lo studio di come valori di questo tipo possono evolversi 64date varie regole che descrivono come cambiano. Di conseguenza, il nostro prossimo 65passo � di definire le riduzioni che i combinatori possono subire. Ci 66sono due regole base: 67\[\begin{array}{l@{\;\;\rightarrow\;\;}l} 68\KC\;x\;y & x\\ 69\SC\;f\;g\;x & (f x)(g x) 70\end{array}\] 71Qui, nella nostra descrizione al di fuori di HOL, usiamo la giustapposizione al posto 72del \#. Inoltre, la giustapposizione � anche associativa a sinistra, cos� che 73$\con{K}\;x\;y$ dovrebbe essere letto come $\con{K}\;\#\;x\;\#\;y$ che � a sua 74volta $(\con{K}\;\#\;x)\;\#\;y$. 75 76Dato un termine nella logica, vogliamo che queste riduzioni siano in grado di essere eseguite 77in qualsiasi punto, non solo al top level, cos� abbiamo bisogno di due ulteriori 78regole di congruenza:\[ 79\begin{array}{l} 80\infer{x\;y\;\;\rightarrow\;\;x'\;y}{x\;\;\rightarrow\;\;x'}\\[5mm] 81\infer{x\;y\;\;\rightarrow\;\;x\;y'}{y\;\;\rightarrow\;\;y'} 82\end{array}\] 83In HOL, possiamo catturare questa relazione con una definizione induttiva. 84Per prima cosa abbiamo bisogno di impostare il nostro simbolo freccia come un infisso per rendere ogni cosa 85un p� pi� elegante 86\begin{session} 87\begin{verbatim} 88- set_fixity "-->" (Infix(NONASSOC, 450)); 89> val it = () : unit 90\end{verbatim} 91\end{session} 92Rendiamo il nostro simbolo freccia non-associativo, rendendo di conseguenza un 93errore di parsing scrivere \verb!x --> y --> z!. Sarebbe carino essere in grado 94di scrivere questo e averlo con il significato di \verb!x --> y /\ y --> z!, ma questo al 95momento non � possibile con il parser di HOL. 96 97Il nostro prossimo passo � di definire di fatto la relazione con la 98funzione \ml{xHol\_reln}. In aggiunta a una quotation che specifica le 99regole per la nuova relazione, essa richiede un nome da usare come la radice per 100i teoremi che essa dimostra. Utilizziamo la stringa \ml{"redn"}\footnote{La 101 funzione correlata \ml{Hol\_reln} pu� essere usata se la scelta della radice da parte del 102 sistema � accettabile. In questo caso, \ml{Hol\_reln} non pu� gestire i 103 caratteri non-alfanumerici in \holtxt{-->} e sollever� un 104 errore.}. 105La funzione \ml{xHol\_reln} per 106fare questo restituisce tre teoremi separati, e leghiamo il primo (il 107teorema ``rules'') e il 108terzo (il teorema ``cases'') 109\begin{session} 110\begin{alltt} 111val (redn_rules, _, redn_cases) = xHol_reln "redn" 112 `(!x y f. x --> y ==> f # x --> f # y) /\bs 113 (!f g x. f --> g ==> f # x --> g # x) /\bs 114 (!x y. K # x # y --> x) /\bs 115 (!f g x. S # f # g # x --> (f # x) # (g # x))`; 116> val redn_rules = 117 |- (\(\forall\)x y f. x --> y \(\Rightarrow\) f # x --> f # y) \(\land\) 118 (\(\forall\)f g x. f --> g \(\Rightarrow\) f # x --> g # x) \(\land\) 119 (\(\forall\)x y. K # x # y --> x) \(\land\) 120 \(\forall\)f g x. S # f # g # x --> f # x # (g # x) : thm 121 val redn_cases = 122 |- \(\forall\)a0 a1. 123 a0 --> a1 \(\Leftrightarrow\) 124 (\(\exists\)x y f. (a0 = f # x) \(\land\) (a1 = f # y) \(\land\) x --> y) \(\lor\) 125 (\(\exists\)f g x. (a0 = f # x) \(\land\) (a1 = g # x) \(\land\) f --> g) \(\lor\) 126 (\(\exists\)y. a0 = K # a1 # y) \(\lor\) 127 \(\exists\)f g x. (a0 = S # f # g # x) \(\land\) (a1 = f # x # (g # x)) 128 : thm 129\end{alltt} 130\end{session} 131 132Oltre a dimostrare questi tre teoremi per noi, il pacchetto di 133definizioni induttiva li ha anche salvati sul disco. 134 135Ora, usando il nostro teorema \texttt{redn\_rules} possiamo dimostrare singoli 136passi della nostra relazione di riduzione: 137\begin{session} 138\begin{verbatim} 139- PROVE [redn_rules] ``S # (K # x # x) --> S # x``; 140Meson search level: ... 141> val it = |- S # (K # x # x) --> S # x : thm 142\end{verbatim} 143\end{session} 144Il sistema che abbiamo appena definito � potente quanto il 145$\lambda$-calcolo, le macchine di Turing, e tutti gli altri modelli standard 146di computazione. 147 148Un utile risultato circa la logica combinatoria � che � 149\emph{confluente}. Si consideri il termine $\SC\;z\;(\KC\;\KC)\;(\KC\; y\; 150x)$. Esso pu� subire due riduzioni, a $\SC\;z\;(\KC\;\KC)\;y$ e anche 151a $(z\;(\KC\;y\;x))\,(\KC\;\KC\;(\KC\;y\;x))$. Fare queste due scelte 152di riduzione significa che da questo punto in poi i termini hanno due 153storie completamente separate? In parole povere, essere confluente 154significa che la risposta a questa domanda � \emph{no}. 155 156 157\section{Chiusura transitiva e confluenza} 158\label{sec:Transitive-Clos-Conf} 159 160Una nozione cruciale a quella di confluenza � quella di \emph{chiusura 161 transitiva}. Abbiamo definito un sistema che si evolve specificando come 162un valore algebrico si pu� evolvere in possibili valori successivi in un singolo 163passo. La prossima domanda naturale � di chiedere per una caratterizzazione 164dell'evoluzione in uno o pi� passi della relazione $\rightarrow$. 165 166Di fatto, definiremo una relazione che vale tra due valori se 167il secondo pu� essere raggiunto dal primo in zero o pi� passi. Questa 168� la \emph{chiusura riflessiva, transitiva} della nostra relazione originaria. 169Comunque, piuttosto che legare la nostra definizione alla nostra relazione originaria, 170svilupperemo questa nozione in modo indipendente e dimostreremo una variet� di 171risultati che sono veri di ogni sistema, non soltanto del nostro sistema di 172logica combinatoria. 173 174Cos�, iniziamo la nostra digressione astratta con un'altra definizione 175induttiva. La nostra nuova costante � \con{RTC}, tale che 176$\con{RTC}\;R\;x\;y$ � vera se � possibile andare da $x$ a $y$ 177con zero o pi� ``passi'' della relazione $R$. (La notazione 178standard per $\con{RTC}\;R$ � $R^*$.) Possiamo esprimere quest'idea con 179solo due regole. La prima \[ \infer{\con{RTC}\;R\;x\;x}{} \] dice 180che � sempre possibile andare da $x$ a $x$ in zero o pi� 181passi. La seconda \[ 182\infer{\con{RTC}\;R\;x\;z}{R\;x\;y\qquad\con{RTC}\;R\;y\;z} 183\] dice che se si pu� fare un singolo passo da $x$ a $y$, e poi 184zero o pi� passi per andare da $y$ a $z$, allora � possibile fare 185zero o pi� passi per andare da $x$ a $z$. La realizzazione di 186queste regole in HOL � di nuovo diretta. 187 188(Come accade, \con{RTC} � una costante gi� definita nel conteso 189in cui stiamo lavorando (si trova in \texttt{relationTheory}), cos� la 190nasconderemo dalla vista prima di iniziare. Evitiamo cos� messaggi che ci dicono 191che stiamo immettendo termini ambigui. Le ambiguit� verrebbero sempre 192risolte in favore della definizione pi� recente, ma i warning 193sono fastidiosi.) 194\begin{session} 195\begin{alltt} 196val _ = hide "RTC"; 197 198val (RTC_rules, _, RTC_cases) = Hol_reln ` 199 (!x. RTC R x x) /\bs 200 (!x y z. R x y /\bs RTC R y z ==> RTC R x z)`; 201<<HOL message: inventing new type variable names: 'a>> 202> val RTC_rules = 203 |- \(\forall\)R. (\(\forall\)x. RTC R x x) \(\land\) 204 \(\forall\)x y z. R x y \(\land\) RTC R y z \(\Rightarrow\) RTC R x z : thm 205 val RTC_cases = 206 |- \(\forall\)R a0 a1. RTC R a0 a1 \(\Leftrightarrow\) (a1 = a0) \(\lor\) 207 \(\exists\)y. R a0 y \(\land\) RTC R y a1 : thm 208\end{alltt} 209\end{session} 210Ora torniamo indietro alla nozione di confluenza. Vogliamo che questo significhi 211qualcosa del tipo: ``bench� un sistema possa prendere differenti percorsi a breve 212scadenza, questi due percorsi possono sempre finire nello stesso posto''. 213Questo suggerisce che definiamo confluente nel modo seguente: 214\begin{session} 215\begin{verbatim} 216- val confluent_def = Define 217 `confluent R = 218 !x y z. RTC R x y /\ RTC R x z ==> 219 ?u. RTC R y u /\ RTC R z u`; 220\end{verbatim} 221\end{session} 222Questa propriet� afferma di $R$ che possiamo ``completare il diamante''; 223se abbiamo 224\begin{center} 225\begin{tikzpicture}[scale=.8,transform shape] 226\node (middle) {}; 227\node (x) [above=of middle] {$x$}; 228\node (y) [left=of middle] {$y$}; 229\node (z) [right=of middle] {$z$}; 230\path (x) edge [->,thick] node[auto,swap] {$*$} (y); 231\path (x) edge [->,thick] node[auto] {$*$} (z); 232\end{tikzpicture} 233\end{center} 234allora possiamo completare con un nuovo valore $u$: 235\begin{center} 236\begin{tikzpicture}[scale=.8,transform shape] 237\node (middle) {}; 238\node (x) [above=of middle] {$x$}; 239\node (y) [left=of middle] {$y$}; 240\node (z) [right=of middle] {$z$}; 241\node (u) [below=of middle] {$u$}; 242\path (x) edge [->,thick] node[auto,swap] {$*$} (y); 243\path (x) edge [->,thick] node[auto] {$*$} (z); 244\path (y) edge [->,thick,densely dotted] node[auto,swap] {$*$} (u); 245\path (z) edge [->,thick,densely dotted] node[auto] {$*$} (u); 246\end{tikzpicture} 247\end{center} 248 249Un'interessante propriet� delle relazioni confluenti � che da qualsiasi punto 250iniziale esse producono non pi� di una \emph{forma normale}, dove una forma 251normale � un valore da cui non si possono pi� fare ulteriori passi. 252\begin{session} 253\begin{alltt} 254- val normform_def = Define`normform R x = !y. ~(R x y)`; 255<<HOL message: inventing new type variable names: 'a, 'b>> 256Definition has been stored under "normform_def". 257> val normform_def = |- \(\forall\)R x. normform R x \(\Leftrightarrow\) \(\forall\)y. \(\neg\)R x y : thm 258\end{alltt} 259\end{session} 260In altre parole, un sistema ha un $R$-forma normale in $x$ se non ci sono 261connessioni attraverso $R$ ad altri valori. (Avremmo potuto scrivere 262\verb!~?y. R x y! come nostro lato destro per la definizione di sopra.) 263 264Possiamo ora dimostrare il seguente: 265\begin{session} 266\begin{alltt} 267- g `!R. confluent R ==> 268 !x y z. 269 RTC R x y /\bs normform R y /\bs 270 RTC R x z /\bs normform R z ==> (y = z)`; 271<<HOL message: inventing new type variable names: 'a>> 272> val it = 273 Proof manager status: 1 proof. 274 1. Incomplete: 275 Initial goal: 276 \(\forall\)R. 277 confluent R \(\Rightarrow\) 278 \(\forall\)x y z. RTC R x y \(\land\) normform R y \(\land\) RTC R x z \(\land\) normform R z \(\Rightarrow\) 279 (y = z) 280\end{alltt} 281\end{session} 282Riscriviamo la definizione di confluenza: 283\begin{session} 284\begin{alltt} 285- e (RW_TAC std_ss [confluent_def]); 286OK.. 2871 subgoal: 288> val it = 289 y = z 290 ------------------------------------ 291 0. \(\forall\)x y z. RTC R x y \(\land\) RTC R x z \(\Rightarrow\) \(\exists\)u. RTC R y u \(\land\) RTC R z u 292 1. RTC R x y 293 2. normform R y 294 3. RTC R x z 295 4. normform R z 296\end{alltt} 297\end{session} 298 La nostra propriet� confluenza � ora l'assunzione 0, e possiamo usarla per 299 dedurre che c'� un $u$ alla base del diamante: 300\begin{session} 301\begin{alltt} 302- e (`?u. RTC R y u /\bs RTC R z u` by PROVE_TAC []); 303OK.. 304Meson search level: ......... 3051 subgoal: 306> val it = 307 y = z 308 ------------------------------------ 309 0. \(\forall\)x y z. RTC R x y \(\land\) RTC R x z \(\Rightarrow\) \(\exists\)u. RTC R y u \(\land\) RTC R z u 310 1. RTC R x y 311 2. normform R y 312 3. RTC R x z 313 4. normform R z 314 5. RTC R y u 315 6. RTC R z u 316\end{alltt} 317\end{session} 318 Cos�, da $y$ possiamo fare zero o pi� passi per arrivare a $u$ e 319 analogamente da $z$. Ma, sappiamo anche che siamo in una $R$-forma 320 normale sia in $y$ sia in $z$. Non possiamo fare alcun passo da 321 questi valori. Possiamo concludere sia che $u = y$ sia che $u = z$, e 322 questo a sua volta significa che $y = z$, che � il nostro goal. Cos� possiamo 323 concludere con 324\begin{session} 325\begin{alltt} 326- e (PROVE_TAC [normform_def, RTC_cases]); 327OK.. 328Meson search level: .......... 329 330Goal proved. [...] 331> val it = 332 Initial goal proved. 333 |- \(\forall\)R. 334 confluent R \(\Rightarrow\) 335 \(\forall\)x y z. 336 RTC R x y \(\land\) normform R y \(\land\) RTC R x z \(\land\) normform R z \(\Rightarrow\) 337 (y = z) 338\end{alltt} 339\end{session} 340Impacchettando cos� da rimuovere i comandi del pacchetto sub-goal, possiamo 341dimostrare e salvare il teorema per l'uso futuro con: 342\begin{session} 343\begin{verbatim} 344val confluent_normforms_unique = store_thm( 345 "confluent_normforms_unique", 346 ``!R. confluent R ==> 347 !x y z. RTC R x y /\ normform R y /\ 348 RTC R x z /\ normform R z ==> (y = z)``, 349 RW_TAC std_ss [confluent_def] THEN 350 `?u. RTC R y u /\ RTC R z u` by PROVE_TAC [] THEN 351 PROVE_TAC [normform_def, RTC_cases]); 352\end{verbatim} 353\end{session} 354\eos{} 355 356Chiaramente la confluenza � una propriet� interessante per un sistema. La 357domanda � come potremmo riuscire a dimostrarla. Iniziamo definendo 358la propriet� diamante che abbiamo usato nella definizione di confluenza. 359\begin{session} 360\begin{alltt} 361- val diamond_def = Define 362 `diamond R = !x y z. R x y /\bs R x z ==> ?u. R y u /\bs R z u`; 363<<HOL message: inventing new type variable names: 'a>> 364Definition has been stored under "diamond_def". 365> val diamond_def = 366 |- \(\forall\)R. diamond R \(\Leftrightarrow\) \(\forall\)x y z. R x y \(\land\) R x z \(\Rightarrow\) \(\exists\)u. R y u \(\land\) R z u 367 : thm 368\end{alltt} 369\end{session} 370 Ora chiaramente abbiamo che la confluenza di una relazione � equivalente alla 371 chiusura riflessiva, transitiva di quella relazione che ha la 372 propriet� diamante. 373\begin{session} 374\begin{verbatim} 375val confluent_diamond_RTC = store_thm( 376 "confluent_diamond_RTC", 377 ``!R. confluent R = diamond (RTC R)``, 378 RW_TAC std_ss [confluent_def, diamond_def]); 379\end{verbatim} 380\end{session} 381 Fin qui tutto bene. Come possiamo poi mostrare la propriet� diamante per 382 $\con{RTC}\;R$? La risposta che salta alla mente � di sperare che se 383 la relazione originale ha la propriet� diamante, allora magari anche la 384 chiusura riflessiva, transitiva l'avr�. Il teorema che vogliamo � 385 \[ \con{diamond}\;R \supset \con{diamond}\,(\con{RTC}\;R)\] Graficmente, 386 questo � sperare che da 387 \[\xymatrix @R=5mm @C=2.5mm { 388& x \ar[dl] \ar[dr] & \\ 389y \ar@{.>}[dr] & & z \ar@{.>}[dl] \\ 390& u}\] 391 saremo in grado di concludere \[\xymatrix @R=4mm @C=2mm { 392& & & x \ar[dl] \ar[dr] & \\ 393& & y \ar@{.>}[dr] \ar@{-->}[ddll] & & z \ar@{.>}[dl] \ar@{-->}[ddrr] \\ 394& & & u \\ 395p \ar@{.>}[dddrrr] & & & & & & q \ar@{.>}[dddlll] \\ \\ \\ 396& & & r}\] dove le linee tratteggiate indicano che questi passi (da $x$ a $p$, 397per esempio) stanno usando $\con{RTC}\;R$. La presenza di due istanze 398di $\con{RTC}\;R$ � un'indicazione che questa dimostrazione richieder� due 399induzioni. Con la prima dimostreremo 400\[\xymatrix @R=4mm @C=2mm { 401& & & x \ar[dl] \ar[dr] & \\ 402& & y \ar@{.>}[dr] \ar@{-->}[ddll] & & z \ar@{.>}[dl] \\ 403& & & u \ar@{.>}[ddll] \\ 404p \ar@{.>}[dr] \\ 405& r}\] 406In altre parole, vogliamo mostrare che se facciamo un passo in una 407direzione (verso $z$) e molti altri passi in un'altra (verso $p$), allora la 408propriet� diamante per $R$ ci garantir� l'esistenza di $r$, 409verso cui saremo in grado di fare molti passi sia da $p$ sia da $z$. 410 411Facciamo un p� d'attenzione ad esprimere il goal cos� che dopo aver eliminato 412l'assunzione pi� esterna (che $R$ ha la propriet� diamante), esso si accorder� con il 413principio di induzione per \con{RTC}\footnote{In questa e nelle seguenti 414 dimostrazioni usando il pacchetto sub-goal, presenteremo il gestore di dimostrazione 415 come se il goal da dimostrare fosse il primo in questo stack. In 416 altre parole, abbiamo fatto una \texttt{dropn 1;} dopo ogni dimostrazione 417 di successo per rimuovere l'evidenza del goal vecchio. In pratica, non c'� 418 nulla di male nel lasciare questi goal nello stack del gestore di dimostrazione.}. 419\begin{session} 420\begin{alltt} 421- g `!R. diamond R ==> 422 !x p. RTC R x p ==> 423 !z. R x z ==> 424 ?u. RTC R p u /\bs RTC R z u`; 425<<HOL message: inventing new type variable names: 'a>> 426> val it = 427 Proof manager status: 1 proof. 428 1. Incomplete: 429 Initial goal: 430 \(\forall\)R. 431 diamond R \(\Rightarrow\) 432 \(\forall\)x p. RTC R x p \(\Rightarrow\) \(\forall\)z. R x z \(\Rightarrow\) \(\exists\)u. RTC R p u \(\land\) RTC R z u 433\end{alltt} 434\end{session} 435Per prima cosa, eliminiamo l'assunzione della propriet� diamante (due cose devono essere 436eliminate: il quantificatore universale pi� esterno e l'antecedente 437dell'implicazione): 438\begin{session} 439\begin{alltt} 440- e (GEN_TAC THEN STRIP_TAC); 441OK.. 4421 subgoal: 443> val it = 444 \(\forall\)x p. RTC R x p \(\Rightarrow\) \(\forall\)z. R x z \(\Rightarrow\) \(\exists\)u. RTC R p u \(\land\) RTC R z u 445 ------------------------------------ 446 diamond R 447\end{alltt} 448\end{session} 449Ora possiamo usare il principio d'induzione per la chiusura riflessiva e transitiva (in alternativa, eseguiamo una ``regola d'induzione''). 450Per far questo, usiamo il comando \ml{Induct\_on} che � usato anche per fare 451un'induzione strutturale su tipi di dati algebrici (come numeri e 452liste). 453Forniamo il nome della costante il cui principio d'induzione vogliamo 454usare, e la tattica fa il resto: 455\begin{session} 456\begin{alltt} 457- e (Induct_on `RTC`); 458OK.. 4591 subgoal: 460> val it = 461 (\(\forall\)x z. R x z \(\Rightarrow\) \(\exists\)u. RTC R x u \(\land\) RTC R z u) \(\land\) 462 \(\forall\)x x' p. 463 R x x' \(\land\) RTC R x' p \(\land\) (\(\forall\)z. R x' z \(\Rightarrow\) \(\exists\)u. RTC R p u \(\land\) RTC R z u) \(\Rightarrow\) 464 \(\forall\)z. R x z \(\Rightarrow\) \(\exists\)u. RTC R p u \(\land\) RTC R z u 465 ------------------------------------ 466 diamond R 467\end{alltt} 468\end{session} 469Eseguiamo uno strip del goal il pi� possibile con l'obiettivo di rendere ci� che 470rimane da dimostrare pi� facile da vedere: 471\begin{session} 472\begin{alltt} 473- e (REPEAT STRIP_TAC); 474OK.. 4752 subgoals: 476> val it = 477 \(\exists\)u. RTC R p u \(\land\) RTC R z u 478 ------------------------------------ 479 0. diamond R 480 1. R x x' 481 2. RTC R x' p 482 3. \(\forall\)z. R x' z \(\Rightarrow\) \(\exists\)u. RTC R p u \(\land\) RTC R z u 483 4. R x z 484 485 \(\exists\)u. RTC R x u \(\land\) RTC R z u 486 ------------------------------------ 487 0. diamond R 488 1. R x z 489\end{alltt} 490\end{session} 491Questo primo goal � semplice. Esso corrisponde al caso dove i passi 492principali da $x$ a $p$ sono di fatto nessun passo del tutto, e $p$ e $x$ 493sono di fatto lo stesso posto. Nell'altra direzione, $x$ ha fatto 494un passo verso $z$, e abbiamo bisogno di trovare un qualche posto raggiungibile in zero o 495pi� passi sia da $x$ sia da $z$. Dato quello che conosciamo fino ad ora, l'unico 496candidato � lo stesso $z$. Di fatto, non abbiamo nemmeno bisogno di fornire questo 497testimone in modo esplicito. \texttt{PROVE\_TAC} lo trover� per noi, purch� 498noi gli diciamo quali sono le regole che governano \con{RTC}: 499\begin{session} 500\begin{alltt} 501- e (PROVE_TAC [RTC_rules]); 502OK.. 503Meson search level: ..... 504 505Goal proved. [..] |- \(\exists\)u. RTC R p u \(\land\) RTC R z u 506Remaining subgoals: 507> val it = 508 \(\exists\)u. RTC R p u \(\land\) RTC R z u 509 ------------------------------------ 510 0. diamond R 511 1. R x x' 512 2. RTC R x' p 513 3. \(\forall\)z. R x' z \(\Rightarrow\) \(\exists\)u. RTC R p u \(\land\) RTC R z u 514 4. R x z 515\end{alltt} 516\end{session} 517 E cosa facciamo di questo goal restante? Le assunzioni uno e quattro 518 tra di loro sono la cima di un $R$-diamante. Usiamo il fatto 519 che abbiamo la propriet� diamante per $R$ e deduciamo che 520 esiste un $v$ verso cui $x'$ e $z$ possono fare entrambi singoli passi: 521\begin{session} 522\begin{alltt} 523- e (`?v. R x' v /\bs R z v` by PROVE_TAC [diamond_def]); 524OK.. 525Meson search level: ............ 5261 subgoal: 527> val it = 528 \(\exists\)u. RTC R p u \(\land\) RTC R z u 529 ------------------------------------ 530 0. diamond R 531 1. R x x' 532 2. RTC R x' p 533 3. \(\forall\)z. R x' z \(\Rightarrow\) \(\exists\)u. RTC R p u \(\land\) RTC R z u 534 4. R x z 535 5. R x' v 536 6. R z v 537\end{alltt} 538\end{session} 539Ora possiamo applicare le nostre ipotesi d'induzione (assunzione 3) per completare 540la lunga, striscia asimmetrica del diamante. Concluderemo che 541c'� un $u$ tale che $\con{RTC}\;R\;p\;u$ e $\con{RTC}\;R\;v\;u$. Di 542fatto abbiamo bisogno un $u$ tale che $\con{RTC}\;R\;z\;u$, ma poich� c'� 543un singolo passo-$R$ tra $z$ e $v$ abbiamo anche quello allo stesso modo. Tutto ci� 544di cui abbiamo bisogno di fornire a \texttt{PROVE\_TAC} sono le regole per \con{RTC}: 545\begin{session} 546\begin{alltt} 547- e (PROVE_TAC [RTC_rules]); 548OK.. 549Meson search level: ....... 550 551Goal proved. [...] 552> val it = 553 Initial goal proved. 554 |- \(\forall\)R. 555 diamond R \(\Rightarrow\) 556 \(\forall\)x p. RTC R x p \(\Rightarrow\) \(\forall\)z. R x z \(\Rightarrow\) \(\exists\)u. RTC R p u \(\land\) RTC R z u 557\end{alltt} 558\end{session} 559 Di nuovo possiamo (e dovremmo) impacchettare il lemma, evitando i 560 comandi del pacchetto sub-goal: 561\begin{session} 562\begin{verbatim} 563val R_RTC_diamond = store_thm( 564 "R_RTC_diamond", 565 ``!R. diamond R ==> 566 !x p. RTC R x p ==> 567 !z. R x z ==> 568 ?u. RTC R p u /\ RTC R z u``, 569 GEN_TAC THEN STRIP_TAC THEN Induct_on `RTC` THEN 570 REPEAT STRIP_TAC THENL [ 571 PROVE_TAC [RTC_rules], 572 `?v. R x' v /\ R z v` by PROVE_TAC [diamond_def] THEN 573 PROVE_TAC [RTC_rules] 574 ]); 575\end{verbatim} 576\end{session} 577\eos{} 578 579Ora possiamo spostarci a dimostrare che se $R$ ha la propriet� diamante, allora 580anche $\con{RTC}\;R$. Vogliamo dimostrare questo di nuovo per induzione. 581E' molto forte la tentazione di affermare il goal come l'ovvio \[ 582\con{diamond}\;R\supset\con{diamond}\,(\con{RTC}\;R) 583\] ma cos� facendo render� di fatto pi� difficile applicare il principio 584d'induzione quando � il momento giusto. E' meglio partire con una 585dichiarazione del goal che � molto vicina nella forma al principio 586d'induzione. Cos�, espandiamo manualmente il significato di \con{diamond} e dichiariamo 587il nostro prossimo goal cos�: 588\begin{session} 589\begin{alltt} 590- g `!R. diamond R ==> !x y. RTC R x y ==> 591 !z. RTC R x z ==> 592 ?u. RTC R y u /\bs RTC R z u`; 593<<HOL message: inventing new type variable names: 'a>> 594> val it = 595 Proof manager status: 1 proof. 596 1. Incomplete: 597 Initial goal: 598 \(\forall\)R. 599 diamond R \(\Rightarrow\) 600 \(\forall\)x y. RTC R x y \(\Rightarrow\) \(\forall\)z. RTC R x z \(\Rightarrow\) \(\exists\)u. RTC R y u \(\land\) RTC R z u 601\end{alltt} 602\end{session} 603 Di nuovo, eliminiamo l'assunzione della propriet� diamante, applichiamo il 604 principio d'induzione, ed eseguiamo \ml{STRIP_TAC} ripetutamente: 605\begin{session} 606\begin{alltt} 607- e (GEN_TAC THEN STRIP_TAC THEN Induct_on `RTC` THEN REPEAT STRIP_TAC); 608OK.. 6092 subgoals: 610> val it = 611 \(\exists\)u. RTC R y u \(\land\) RTC R z u 612 ------------------------------------ 613 0. diamond R 614 1. R x x' 615 2. RTC R x' y 616 3. \(\forall\)z. RTC R x' z \(\Rightarrow\) \(\exists\)u. RTC R y u \(\land\) RTC R z u 617 4. RTC R x z 618 619 \(\exists\)u. RTC R x u \(\land\) RTC R z u 620 ------------------------------------ 621 0. diamond R 622 1. RTC R x z 623\end{alltt} 624\end{session} 625Il primo goal � di nuovo uno facile, corrispondendo al caso in cui 626il percorso da $x$ a $y$ � stato uno senza alcun passo. 627\begin{session} 628\begin{alltt} 629- e (PROVE_TAC [RTC_rules]); 630OK.. 631Meson search level: ... 632 633Goal proved. [...] 634 635Remaining subgoals: 636> val it = 637 \(\exists\)u. RTC R y u \(\land\) RTC R z u 638 ------------------------------------ 639 0. diamond R 640 1. R x x' 641 2. RTC R x' y 642 3. \(\forall\)z. RTC R x' z \(\Rightarrow\) \(\exists\)u. RTC R y u \(\land\) RTC R z u 643 4. RTC R x z 644\end{alltt} 645\end{session} 646Il goal � molto simile a quello che abbiamo visto in precedenza. Abbiamo la punta di 647un diamante (``asimmetrico'') nelle assunzioni 1 e 4, cos� possiamo dedurre 648l'esistenza di una destinazione comune per $x'$ e $z$: 649\begin{session} 650\begin{alltt} 651- e (`?v. RTC R x' v /\bs RTC R z v` by PROVE_TAC [R_RTC_diamond]); 652OK.. 653Meson search level: ............ 6541 subgoal: 655> val it = 656 \(\exists\)u. RTC R y u \(\land\) RTC R z u 657 ------------------------------------ 658 0. diamond R 659 1. R x x' 660 2. RTC R x' y 661 3. \(\forall\)z. RTC R x' z \(\Rightarrow\) \(\exists\)u. RTC R y u \(\land\) RTC R z u 662 4. RTC R x z 663 5. RTC R x' v 664 6. RTC R z v 665\end{alltt} 666\end{session} 667 A questo punto nell'ultima dimostrazione eravamo stati in grado di concludere il tutto 668 appellandoci soltanto alle regole per \con{RTC}. Questa volta non � 669 cos� semplice. Quando usiamo l'ipotesi d'induzione 670 (assunzione 3), possiamo concludere che c'� un $u$ per cui sia 671 $y$ sia $v$ si possono connettere in zero o pi� passi, ma al fine di 672 mostrare che questo $u$ � raggiungibile da $z$, abbiamo bisogno di essere in grado di 673 concludere $\con{RTC}\;R\;z\;u$ quando conosciamo che 674 $\con{RTC}\;R\;z\;v$ (assunzione 6 di sopra) e 675 $\con{RTC}\;R\;v\;u$ (la nostra conseguenza dell'ipotesi 676 d'induzione). Lasciamo la dimostrazione di questo risultato generale come un 677 esercizio, e qui assumiamo che essa � gi� stata dimostrato come il teorema 678 \texttt{RTC\_RTC}. 679\begin{session} 680\begin{alltt} 681- e (PROVE_TAC [RTC_rules, RTC_RTC]); 682Meson search level: ....... 683 684Goal proved. [...] 685> val it = 686 Initial goal proved. 687 |- \(\forall\)R. 688 diamond R \(\Rightarrow\) 689 \(\forall\)x y. RTC R x y \(\Rightarrow\) \(\forall\)z. RTC R x z \(\Rightarrow\) \(\exists\)u. RTC R y u \(\land\) RTC R z u 690\end{alltt} 691\end{session} 692Possiamo impacchettare questo risultato come un lemma e poi dimostrare la versione 693pi� elegante direttamente: 694\begin{session} 695\begin{verbatim} 696val diamond_RTC_lemma = prove( 697 ``!R. 698 diamond R ==> 699 !x y. RTC R x y ==> !z. RTC R x z ==> ?u. RTC R y u /\ RTC R z u``, 700 GEN_TAC THEN STRIP_TAC THEN Induct_on `RTC` THEN 701 REPEAT STRIP_TAC THENL [ 702 PROVE_TAC [RTC_rules], 703 `?v. RTC R x' v /\ RTC R z v` by PROVE_TAC [R_RTC_diamond] THEN 704 PROVE_TAC [RTC_RTC, RTC_rules] 705 ]); 706val diamond_RTC = store_thm( 707 "diamond_RTC", 708 ``!R. diamond R ==> diamond (RTC R)``, 709 PROVE_TAC [diamond_def,diamond_RTC_lemma]); 710\end{verbatim} 711\end{session} 712 713\section{Di nuovo sui combinatori} 714\label{sec:Return-to-Land} 715 716Ora, siamo nella posizione di ritornare all'oggetto reale dello studio e 717dimostrare la confluenza per la logica combinatoria. Abbiamo fatto uno sviluppo 718astratto e stabilito che\[ 719\begin{array}{ccccc} 720\con{diamond}\;R & \supset & \con{diamond}\,(\con{RTC}\;R)\\ 721& & \land\\ 722& & \con{diamond}\,(\con{RTC}\;R) & \equiv & \con{confluent}\;R\\ 723\end{array} 724\] (Abbiamo anche stabilito un paio di utili risultati lungo 725la strada.) 726 727\newcommand{\topk}{\KC\;\SC\;(\KC\;\KC\;\KC)} Purtroppo, non si da il 728caso che $\rightarrow$, la nostra relazione di un passo per i combinatori, abbia 729la propriet� diamante. Un controesempio � $\topk$. La sua evoluzione possibile 730pu� essere descritta graficamente: \[\xymatrix @R=5mm @C=2.5mm { 731& \topk \ar[dl] \ar[dr] & \\ 732\SC & & \KC\;\SC\;\KC \ar[dl] \\ 733& \SC}\] 734Se avessimo la propriet� diamante, sarebbe possibile trovare una destinazione 735comune per $\KC\;\SC\;\KC$ e $\SC$. Tuttavia, \SC{} non ammette 736alcuna riduzione di sorta, cos� non c'� una destinazione 737comune\footnote{Di fatto il nostro contro esempio � pi� complicato 738 del necessario. Il fatto che $\KC\;\SC\;\KC$ abbia una 739 riduzione alla forma normale $\SC$ agisce anche come un contro esempio. 740 Puoi vedere perch�?}. 741 742Questo � un problema. Dovremo prendere un altro approccio. 743Definiremo un'altra strategia di riduzione (\emph{riduzione parallela}), 744e dimostreremo che la sua chiusura riflessiva, transitiva � di fatto la stessa 745relazione della nostra chiusura riflessiva, transitiva originaria. Poi 746mostreremo anche che la riduzione parallela ha la propriet� diamante. Questo 747stabilir� che anche la sua chiusura riflessiva transitiva ce l'ha. 748Poi, dal momento che sono la stessa relazione, avremo che la 749chiusura riflessiva, transitiva della nostra relazione originaria ha la propriet� 750diamante, e di conseguenza, la nostra relazione originaria sar� confluente. 751 752\subsection{Riduzione parallela} 753\label{sec:Parallel-Reduction} 754 755La nostra nuova relazione permette l'occorrenza di un qualsiasi numero di riduzioni 756in parallelo. Usiamo il simbolo \texttt{-||->} per indicare la riduzione parallela 757a causa delle sue linee parallele: 758\begin{session} 759\begin{verbatim} 760- set_fixity "-||->" (Infix(NONASSOC, 450)); 761> val it = () : unit 762\end{verbatim} 763\end{session} 764 Poi possiamo definire la riduzione parallela stessa. Le regole appaiono molto 765 simili a quelle per $\rightarrow$. La differenza � che 766 permettiamo la transizione riflessiva, e diciamo che un'applicazione di 767 $x\;u$ pu� essere trasformata in $y\;v$ se ci sono trasformazioni 768 che portano $x$ in $y$ e $u$ in $v$. Questo � il motivo per cui dobbiamo avere 769 incidentalmente la riflessivit�. Senza di essa, un termine come 770 $(\KC\;x\;y)\,\KC$ non si potrebbe ridurre perch� mentre il lato sinistro 771 dell'applicazione ($\KC\;x\;y$) si pu� ridurre, il suo lato destro non pu�. 772\begin{session} 773\begin{alltt} 774- val (predn_rules, _, predn_cases) = xHol_reln "predn" 775 `(!x. x -||-> x) /\bs 776 (!x y u v. x -||-> y /\bs u -||-> v 777 ==> 778 x # u -||-> y # v) /\bs 779 (!x y. K # x # y -||-> x) /\bs 780 (!f g x. S # f # g # x -||-> (f # x) # (g # x))`; 781> val predn_rules = 782 |- (\(\forall\)x. x -||-> x) \(\land\) 783 (\(\forall\)x y u v. x -||-> y \(\land\) u -||-> v \(\Rightarrow\) x # u -||-> y # v) \(\land\) 784 (\(\forall\)x y. K # x # y -||-> x) \(\land\) 785 \(\forall\)f g x. S # f # g # x -||-> f # x # (g # x) : thm 786 val predn_cases = 787 |- \(\forall\)a0 a1. 788 a0 -||-> a1 \(\Leftrightarrow\) 789 (a1 = a0) \(\lor\) 790 (\(\exists\)x y u v. (a0 = x # u) \(\land\) (a1 = y # v) \(\land\) 791 x -||-> y \(\land\) u -||-> v) \(\lor\) 792 (\(\exists\)y. a0 = K # a1 # y) \(\lor\) 793 \(\exists\)f g x. (a0 = S # f # g # x) \(\land\) (a1 = f # x # (g # x)) 794 : thm 795\end{alltt} 796\end{session} 797 798\subsection{Usare \con{RTC}} 799\label{sec:Using-RTC} 800 801Ora possiamo impostare un'elegante sintassi per le chiusure riflessiva e 802transitiva delle nostre due relazioni. Useremo per entrambe dei simbolo ASCII 803che consistono del simbolo originario seguito da un asterisco. Si noti 804anche come, definendo le due relazioni, dobbiamo usare il 805carattere \texttt{\$} per effettuare l'``escape'' delle normali fixity dei simboli. Questo 806� esattamente analogo al modo in cui � usata la parola chiave \texttt{op} 807dell'ML. Per prima cosa creiamo il simbolo desiderato per la sintassi concreta, 808e quindi ne effettuiamo l'``overload'' cos� che il parser lo espander� alla forma 809desiderata. 810\begin{session} 811\begin{verbatim} 812- set_fixity "-->*" (Infix(NONASSOC, 450)); 813> val it = () : unit 814 815- overload_on ("-->*", ``RTC $-->``); 816> val it = () : unit 817\end{verbatim} 818\end{session} 819We do exactly the same thing for the reflexive and transitive closure 820of our parallel reduction. 821\begin{session} 822\begin{verbatim} 823- set_fixity "-||->*" (Infix(NONASSOC, 450)); 824> val it = () : unit 825 826- overload_on ("-||->*", ``RTC $-||->``); 827> val it = () : unit 828\end{verbatim} 829\end{session} 830Incidentalmente, in congiunzione con \texttt{PROVE} possiamo ora 831dimostrare automaticamente catene di riduzioni relativamente lunghe. 832\begin{session} 833\begin{verbatim} 834- PROVE [RTC_rules, redn_rules] ``S # K # K # x -->* x``; 835Meson search level: ...... 836> val it = |- S # K # K # x -->* x : thm 837 838- PROVE [RTC_rules, redn_rules] 839 ``S # (S # (K # S) # K) # (S # K # K) # f # x -->* 840 f # (f # x)``; 841Meson search level: ........................... 842> val it = |- S # (S # (K # S) # K) # (S # K # K) # f # x -->* f # (f # x) 843 : thm 844\end{verbatim} 845\end{session} 846(L'ultima � una sequenza lunga sette riduzioni.) 847 848 849\subsection{Dimostrare che le \con{RTC} sono le stesse} 850\label{sec:Proving-RTCs-same} 851 852Iniziamo con la direzione pi� facile, e mostriamo che ogni cosa che � in 853$\rightarrow^*$ � in $\mathpredn^*$. Poich� 854\con{RTC} � monotona (fatto che � lasciato da dimostrare al lettore), 855possiamo ridurre questo per mostrare che $x\rightarrow y\supset x\mathpredn y$. 856 857Il nostro goal: 858\begin{session} 859\begin{alltt} 860- g `!x y. x -->* y ==> x -||->* y`; 861> val it = 862 Proof manager status: 1 proof. 863 1. Incomplete: 864 Initial goal: 865 \(\forall\)x y. x -->* y \(\Rightarrow\) x -||->* y 866\end{alltt} 867\end{session} 868Effettuiamo il back-chain usando il nostro risultato di monotonicit� 869\begin{session} 870\begin{alltt} 871- e (MATCH_MP_TAC RTC_monotone); 872OK.. 8731 subgoal: 874> val it = 875 \(\forall\)x y. x --> y \(\Rightarrow\) x -||-> y 876\end{alltt} 877\end{session} 878Ora possiamo eseguire l'induzione sulle regole per $\rightarrow$: 879\begin{session} 880\begin{alltt} 881- e (Induct_on `$-->`); 882OK.. 8831 subgoal: 884> val it = 885 (\(\forall\)x y f. x --> y \(\land\) x -||-> y \(\Rightarrow\) f # x -||-> f # y) \(\land\) 886 (\(\forall\)f g x. f --> g \(\land\) f -||-> g \(\Rightarrow\) f # x -||-> g # x) \(\land\) 887 (\(\forall\)x y. K # x # y -||-> x) \(\land\) 888 \(\forall\)f g x. S # f # g # x -||-> f # x # (g # x) 889\end{alltt} 890\end{session} 891Avremmo potuto dividere la congiunzione di 4 congiunti in quattro goal, ma non 892c'� una vera necessit�. E' abbastanza chiaro che ciascuno segue immediatamente dalle 893regole per la riduzione parallela. 894\begin{session} 895\begin{alltt} 896- e (PROVE_TAC [predn_rules]); 897OK.. 898Meson search level: ............ 899 900Goal proved. [...] 901> val it = 902 Initial goal proved. 903 |- \(\forall\)x y. x -->* y \(\Rightarrow\) x -||->* y : goalstack 904\end{alltt} 905\end{session} 906Impacchettata in un piccolo pacchetto libero dal pacchetto subgoal, la nostra dimostrazione � 907\begin{session} 908\begin{verbatim} 909val RTCredn_RTCpredn = store_thm( 910 "RTCredn_RTCpredn", 911 ``!x y. x -->* y ==> x -||->* y``, 912 MATCH_MP_TAC RTC_monotone THEN 913 Induct_on `$-->` THEN PROVE_TAC [predn_rules]); 914\end{verbatim} 915\end{session} 916\eos{} 917 918La nostra prossima dimostrazione � nell'altra direzione. Dovrebbe essere chiaro che 919questa volta non saremo in grado di ricorrere semplicemente alla monotonicit� di 920\con{RTC}; un passo della relazione di riduzione parallela non pu� essere riflesso 921da un passo della relazione di riduzione originale. E' chiaro che 922rispecchiare un singolo passo della relazione di riduzione parallela potrebbe richiedere molti 923passi della relazione originale. Dimostriamo dunque questo: 924\begin{session} 925\begin{alltt} 926- g `!x y. x -||-> y ==> x -->* y`; 927> val it = 928 Proof manager status: 1 proof. 929 1. Incomplete: 930 Initial goal: 931 \(\forall\)x y. x -||-> y \(\Rightarrow\) x -->* y 932\end{alltt} 933\end{session} 934Questa volta la nostra induzione sar� sulle regole che definiscono la relazione 935di riduzione parallela. 936\begin{session} 937\begin{alltt} 938- e (Induct_on `$-||->`); 939OK.. 9401 subgoal: 941> val it = 942 (\(\forall\)x. x -->* x) \(\land\) 943 (\(\forall\)x y x' y'. x -||-> y \(\land\) x -->* y \(\land\) x' -||-> y' \(\land\) x' -->* y' \(\Rightarrow\) 944 x # x' -->* y # y') \(\land\) 945 (\(\forall\)x y. K # x # y -->* x) \(\land\) 946 \(\forall\)f g x. S # f # g # x -->* f # x # (g # x) 947\end{alltt} 948\end{session} 949 Qui ci sono quattro congiunti, e dovrebbe essere chiaro che nessuno tranne 950 il secondo pu� essere dimostrato immediatamente ricorrendo alle regole per 951 la chiusura transitiva e per la stessa $\rightarrow$. Potremmo 952 dividere le congiunzioni ed inserire un ramo \texttt{THENL}. 953 Tuttavia, avremmo bisogno di ripetere la stessa tattica tre volte per 954 chiudere velocemente tre dei quattro rami. Piuttosto, usiamo il 955 tatticale \texttt{TRY} per provare ad applicare la stessa tattica a tutti e quattro 956 i rami. Se la nostra tattica fallisce sul ramo \#2, come ci aspettiamo, 957 \texttt{TRY} ci protegger� da questo fallimento e ci permetter� di 958 procedere. 959\begin{session} 960\begin{alltt} 961e (REPEAT CONJ_TAC THEN 962 TRY (PROVE_TAC [RTC_rules, redn_rules])); 963OK.. 964Meson search level: .... 965Meson search level: .... 966Meson search level: ............................... 967Meson search level: .. 9681 subgoal: 969> val it = 970 \(\forall\)x y x' y'. x -||-> y \(\land\) x -->* y \(\land\) x' -||-> y' \(\land\) x' -->* y' \(\Rightarrow\) 971 x # x' -->* y # y' 972\end{alltt} 973\end{session} 974 Si noti che avvolgere \texttt{TRY} intorno a \texttt{PROVE\_TAC} non � 975 sempre saggio. Spesso la tattica \texttt{PROVE\_TAC} richiede un tempo 976 estremamente lungo per esaurire il suo spazio di ricerca, e poi arrendersi con un 977 fallimento. Qui, ``siamo stati fortunati''. 978 979 In ogni caso, che cosa ne facciamo di quest'ultimo subgoal? Se lo osserviamo per un tempo 980 sufficiente, dovremmo vedere che � un altro fatto di monotonicit�. Pi� 981 precisamente, abbiamo bisogno di ci� che � chiamato un risultato di \emph{congruenza} per 982 \holtxt{-->*}. In questa forma, non � molto adatto per una dimostrazione semplice. 983 Andiamo via e dimostriamo \texttt{RTCredn\_ap\_monotonic} 984 separatamente. (Un altro esercizio!) Il nostro nuovo teorema dovrebbe stabilire 985\begin{session} 986\begin{verbatim} 987val RTCredn_ap_congruence = store_thm( 988 "RTCredn_ap_congruence", 989 ``!x y. x -->* y ==> !z. x # z -->* y # z /\ z # x -->* z # y``, 990 ...); 991\end{verbatim} 992\end{session} 993 Ora che abbiamo questo, il nostro sub-goal � quasi immediatamente 994 dimostrabile. Usandolo, sappiamo che \[\begin{array}{c} 995 x\;x' \rightarrow^* y\;x' \\ 996 y\;x' \rightarrow^* y\;y' 997 \end{array}\] 998 Tutto ci� che dobbiamo fare � ``cucire insieme'' le due transizioni di sopra 999 e andiamo da $x\;x'$ a $y\;y'$. Possiamo fare questo ricorrendo al nostro 1000 precedente risultato \texttt{RTC\_RTC}. 1001\begin{session} 1002\begin{alltt} 1003e (PROVE_TAC [RTC_RTC, RTCredn_ap_congruence]); 1004OK.. 1005Meson search level: ....... 1006 1007Goal proved. [...] 1008> val it = 1009 Initial goal proved. 1010 |- \(\forall\)x y. x -||-> y \(\Rightarrow\) x -->* y : goalstack 1011\end{alltt} 1012\end{session} 1013Ma dato che possiamo rifinire ci� che pensavamo essere un ramo scomodo 1014con solo un'altra applicazione di \texttt{PROVE\_TAC}, non abbiamo bisogno di 1015usare il nostro footwork con \texttt{TRY} al passo precedente. Piuttosto, 1016possiamo semplicemente fondere le liste di teoremi passate ad entrambe le invocazioni, distribuire 1017con \texttt{REPEAT CONJ\_TAC} e avere di fatto una dimostrazione con una tattica 1018molto corta: 1019\begin{session} 1020\begin{verbatim} 1021val predn_RTCredn = store_thm( 1022 "predn_RTCredn", 1023 ``!x y. x -||-> y ==> x -->* y``, 1024 Induct_on `$-||->` THEN 1025 PROVE_TAC [RTC_rules, redn_rules, RTC_RTC, RTCredn_ap_congruence]); 1026\end{verbatim} 1027\end{session} 1028\eos{} 1029 1030Ora � il momento di dimostrare che se un numero di passi di riduzione parallela 1031sono concatenati insieme, allora possiamo riflettere questo con qualche numero di 1032passi usando la relazione di riduzione originale. Il nostro goal: 1033\begin{session} 1034\begin{alltt} 1035- g `!x y. x -||->* y ==> x -->* y`; 1036> val it = 1037 Proof manager status: 1 proof. 1038 1. Incomplete: 1039 Initial goal: 1040 \(\forall\)x y. x -||->* y \(\Rightarrow\) x -->* y 1041\end{alltt} 1042\end{session} 1043Usiamo l'appropriato principio di induzione per andare a: 1044\begin{session} 1045\begin{alltt} 1046- e (Induct_on `RTC`); 1047OK.. 10481 subgoal: 1049> val it = 1050 (\(\forall\)x. x -->* x) \(\land\) 1051 \(\forall\)x x' y. x -||-> x' \(\land\) x' -||-> y* \(\land\) x' -->* y \(\Rightarrow\) x -->* z 1052\end{alltt} 1053\end{session} 1054Possiamo concludere questo in un singolo passo. La prima congiunzione � ovvia, 1055e nella seconda \verb!x -||-> y! e il nostro ultimo risultato si combinano per 1056dirci che \verb!x -->* y!. Poi questo pu� essere concatenato insieme con 1057l'altra assunzione nel secondo congiunto e abbiamo finito. 1058\begin{session} 1059\begin{alltt} 1060- e (PROVE_TAC [RTC_rules, predn_RTCredn, RTC_RTC]); 1061OK.. 1062Meson search level: ....... 1063 1064Goal proved.[...] 1065> val it = 1066 Initial goal proved. 1067 |- \(\forall\)x y. x -||->* y \(\Rightarrow\) x -->* y : proof 1068\end{alltt} 1069\end{session} 1070Impacchettata, questa dimostrazione �: 1071\begin{session} 1072\begin{verbatim} 1073val RTCpredn_RTCredn = store_thm( 1074 "RTCpredn_RTCredn", 1075 ``!x y. x -||->* y ==> x -->* y``, 1076 Induct_on `RTC` THEN PROVE_TAC [predn_RTCredn, RTC_RTC, RTC_rules]); 1077\end{verbatim} 1078\end{session} 1079\eos{} 1080 1081La nostra ultima azione � di usare ci� che abbiamo finora per concludere che 1082$\rightarrow^*$ e $\mathpredn^*$ sono uguali. Dichiariamo il nostro goal: 1083\begin{session} 1084\begin{verbatim} 1085- g `$-||->* = $-->*`; 1086> val it = 1087 Proof manager status: 1 proof. 1088 1. Incomplete: 1089 Initial goal: 1090 $-||->* = $-->* 1091\end{verbatim} 1092\end{session} 1093Vogliamo ora ricorrere all'estensionalit�. Il modo pi� semplice per far questo 1094� di riscrivere con il teorema \texttt{FUN\_EQ\_THM}: 1095\begin{session} 1096\begin{alltt} 1097- FUN_EQ_THM; 1098> val it = |- \(\forall\)f g. (f = g) \(\Leftrightarrow\) \(\forall\)x. f x = g x : thm 1099\end{alltt} 1100\end{session} 1101Cos�, riscriviamo: 1102\begin{session} 1103\begin{alltt} 1104- e (SIMP_TAC std_ss [FUN_EQ_THM]); 1105OK.. 11061 subgoal: 1107> val it = 1108 \(\forall\)x x'. x -||->* x' = x -->* x' 1109\end{alltt} 1110\end{session} 1111 1112Questo goal � una semplice conseguenza delle nostre implicazioni precedenti. 1113\begin{session} 1114\begin{verbatim} 1115- e (PROVE_TAC [RTCpredn_RTCredn, RTCredn_RTCpredn]); 1116OK.. 1117Meson search level: ...... 1118 1119Goal proved. [...] 1120> val it = 1121 Initial goal proved. 1122 |- $-||->* = $-->* : goalstack 1123\end{verbatim} 1124\end{session} 1125Impacchettata, la dimostrazione �: 1126\begin{session} 1127\begin{verbatim} 1128val RTCpredn_EQ_RTCredn = store_thm( 1129 "RTCpredn_EQ_RTCredn", 1130 ``$-||->* = $-->*``, 1131 SIMP_TAC std_ss [FUN_EQ_THM] THEN 1132 PROVE_TAC [RTCpredn_RTCredn, RTCredn_RTCpredn]); 1133\end{verbatim} 1134\end{session} 1135 1136 1137\subsection{Dimostrare una propriet� diamante per la riduzione parallela} 1138\label{sec:predn-diamond} 1139 1140Ora non ci resta che una dimostrazione sostanziale da fare. Prima ancora di poter 1141cominciare, c'� un numero di lemmi minori che abbiamo bisogno di dimostrare prima. 1142Questi sono essenzialmente delle specializzazioni del teorema 1143\texttt{predn\_cases}. Vogliamo delle caratterizzazioni esaustive delle 1144possibilit� che si possono presentare quando i seguenti termini subiscono una riduzione parallela: 1145$x\;y$, \KC, \SC, $\KC\;x$, $\SC\;x$, $\KC\;x\;y$, $\SC\;x\;y$ e 1146$\SC\;x\;y\;z$. 1147 1148Per far questo, scriveremo una piccola funzione che deriva 1149le caratterizzazioni automaticamente: 1150\begin{session} 1151\begin{verbatim} 1152- fun characterise t = SIMP_RULE (srw_ss()) [] (SPEC t predn_cases); 1153> val characterise = fn : term -> thm 1154\end{verbatim} 1155\end{session} 1156La funzione \ml{characterise} specializza il teorema 1157\ml{predn\_cases} con il termine di input, e quindi semplifica. Il 1158simpset \ml{srw\_ss()} include informazioni circa l'iniettivit� e 1159la disgiunzione [disjointness ndt] dei costruttori ed elimina le ovvie impossibilit�. 1160Per esempio, 1161\begin{session} 1162\begin{alltt} 1163- val K_predn = characterise ``K``; 1164<<HOL message: more than one resolution of overloading was possible>> 1165> val K_predn = |- \(\forall\)a1. K -||-> a1 = (a1 = K) : thm 1166 1167- val S_predn = characterise ``S``; 1168<<HOL message: more than one resolution of overloading was possible>> 1169> val S_predn = |- \(\forall\)a1. S -||-> a1 = (a1 = S) : thm 1170\end{alltt} 1171\end{session} 1172Sfortunatamente, ci� che otteniamo indietro dagli altri input non � cos� buono: 1173\begin{session} 1174\begin{alltt} 1175- val Sx_predn0 = characterise ``S # x``; 1176> val Sx_predn0 = 1177 |- \(\forall\)a1. 1178 S # x -||-> a1 = 1179 (a1 = S # x) \(\lor\) 1180 \(\exists\)y v. (a1 = y # v) \(\land\) S -||-> y \(\land\) x -||-> v : thm 1181\end{alltt} 1182\end{session} 1183Quel primo disgiunto � ridondante, come dimostra il seguente: 1184\begin{session} 1185\begin{verbatim} 1186val Sx_predn = prove( 1187 ``!x y. S # x -||-> y = ?z. (y = S # z) /\ (x -||-> z)``, 1188 REPEAT GEN_TAC THEN EQ_TAC THEN 1189 RW_TAC std_ss [Sx_predn0, predn_rules, S_predn]); 1190\end{verbatim} 1191\end{session} 1192La nostra funzione \texttt{characterise} dovr� solo aiutarci nelle 1193dimostrazioni che seguono. 1194\begin{session} 1195\begin{verbatim} 1196val Kx_predn = prove( 1197 ``!x y. K # x -||-> y = ?z. (y = K # z) /\ (x -||-> z)``, 1198 REPEAT GEN_TAC THEN EQ_TAC THEN 1199 RW_TAC std_ss [characterise ``K # x``, predn_rules, K_predn]); 1200\end{verbatim} 1201\end{session} 1202Cosa facciamo di $\KC\;x\;y$? Un poco di ragionamento dimostra che ci sono 1203in realt� due casi questa volta. 1204\begin{session} 1205\begin{verbatim} 1206val Kxy_predn = prove( 1207 ``!x y z. 1208 K # x # y -||-> z = 1209 (?u v. (z = K # u # v) /\ (x -||-> u) /\ (y -||-> v)) \/ 1210 (z = x)``, 1211 REPEAT GEN_TAC THEN EQ_TAC THEN 1212 RW_TAC std_ss [characterise ``K # x # y``, predn_rules, 1213 Kx_predn]); 1214\end{verbatim} 1215\end{session} 1216Per contro, c'� solo un caso per $\SC\;x\;y$ perch� esso 1217non � ancora un ``redex'' al livello alto. 1218\begin{session} 1219\begin{verbatim} 1220val Sxy_predn = prove( 1221 ``!x y z. S # x # y -||-> z = 1222 ?u v. (z = S # u # v) /\ (x -||-> u) /\ (y -||-> v)``, 1223 REPEAT GEN_TAC THEN EQ_TAC THEN 1224 RW_TAC std_ss [characterise ``S # x # y``, predn_rules, 1225 Sx_predn]); 1226\end{verbatim} 1227\end{session} 1228Poi, la caratterizzazione per $\SC\;x\;y\;z$: 1229\begin{session} 1230\begin{verbatim} 1231val Sxyz_predn = prove( 1232 ``!w x y z. S # w # x # y -||-> z = 1233 (?p q r. (z = S # p # q # r) /\ 1234 w -||-> p /\ x -||-> q /\ y -||-> r) \/ 1235 (z = (w # y) # (x # y))``, 1236 REPEAT GEN_TAC THEN EQ_TAC THEN 1237 RW_TAC std_ss [characterise ``S # w # x # y``, predn_rules, 1238 Sxy_predn]); 1239\end{verbatim} 1240\end{session} 1241Infine, vogliamo una caratterizzazione per $x\;y$. Ci� che 1242\texttt{characterise} ci da questa volta non pu� essere migliorato, 1243per quello che potremmo considerare a partire dai quattro disgiunti. 1244\begin{session} 1245\begin{alltt} 1246- val x_ap_y_predn = characterise ``x # y``; 1247> val x_ap_y_predn = 1248 |- \(\forall\)a1. 1249 x # y -||-> a1 = 1250 (a1 = x # y) \(\lor\) 1251 (\(\exists\)y' v. (a1 = y' # v) \(\land\) x -||-> y' \(\land\) y -||-> v) \(\lor\) 1252 (x = K # a1) \(\lor\) 1253 \(\exists\)f g. (x = S # f # g) \(\land\) (a1 = f # y # (g # y)) : thm 1254\end{alltt} 1255\end{session} 1256\eos{} 1257 1258\noindent Ora siamo pronti per dimostrare il goal finale. Esso � 1259\begin{session} 1260\begin{alltt} 1261- g `!x y. x -||-> y ==> 1262 !z. x -||-> z ==> ?u. y -||-> u /\bs z -||-> u`; 1263> val it = 1264 Proof manager status: 1 proof. 1265 1. Incomplete: 1266 Initial goal: 1267 \(\forall\)x y. x -||-> y \(\Rightarrow\) \(\forall\)z. x -||-> z \(\Rightarrow\) \(\exists\)u. y -||-> u \(\land\) z -||-> u 1268\end{alltt} 1269\end{session} 1270Possiamo ora condurre un'induzione e suddividere il goal nei suoi congiunti individuali: 1271\begin{session} 1272\begin{alltt} 1273- e (Induct_on `$-||->` THEN REPEAT CONJ_TAC); 1274OK.. 12754 subgoals: 1276> val it = 1277 \(\forall\)f g x z. S # f # g # x -||-> z \(\Rightarrow\) 1278 \(\exists\)u. f # x # (g # x) -||-> u \(\land\) z -||-> u 1279 1280 1281 \(\forall\)x y z. K # x # y -||-> z \(\Rightarrow\) \(\exists\)u. x -||-> u \(\land\) z -||-> u 1282 1283 1284 \(\forall\)x y u v. 1285 x -||-> y \(\land\) 1286 (\(\forall\)z. x -||-> z \(\Rightarrow\) \(\exists\)u. y -||-> u \(\land\) z -||-> u) \(\land\) 1287 u -||-> v \(\land\) 1288 (\(\forall\)z. u -||-> z \(\Rightarrow\) \(\exists\)u. v -||-> u \(\land\) z -||-> u) \(\Rightarrow\) 1289 \(\forall\)z. x # u -||-> z \(\Rightarrow\) \(\exists\)u. y # v -||-> u \(\land\) z -||-> u 1290 1291 1292 \(\forall\)x z. x -||-> z \(\Rightarrow\) \(\exists\)u. x -||-> u \(\land\) z -||-> u 1293\end{alltt} 1294\end{session} 1295Il primo goal � facilmente smaltito. Il testimone che forniremmo 1296per questo caso � semplicemente \texttt{z}, ma \texttt{PROVE\_TAC} far� 1297il lavoro per noi: 1298\begin{session} 1299\begin{verbatim} 1300- e (PROVE_TAC [predn_rules]); 1301OK.. 1302Meson search level: ... 1303 1304Goal proved. [...] 1305\end{verbatim} 1306\end{session} 1307 Il goal successivo include due istanze di termine della forma 1308 \verb!x # y -||-> z!. Possiamo ora usare il nostro teorema \verb!x_ap_y_predn! 1309 qui. Tuttavia, se riscriviamo in modo indiscriminato con esso, 1310 confonderemo in realt� il goal. Vogliamo riscrivere soltanto 1311 l'assunzione, non l'istanza al di sotto del quantificatore 1312 esistenziale. Iniziare il tutto applicando ripetutamente \ml{STRIP\_TAC} non ci 1313 pu� portare troppo fuori strada. 1314\begin{session} 1315\begin{alltt} 1316- e (REPEAT STRIP_TAC); 1317OK.. 13181 subgoal: 1319> val it = 1320 \(\exists\)u. y # v -||-> u \(\land\) z -||-> u 1321 ------------------------------------ 1322 0. x -||-> y 1323 1. \(\forall\)z. x -||-> z \(\Rightarrow\) \(\exists\)u. y -||-> u \(\land\) z -||-> u 1324 2. u -||-> v 1325 3. \(\forall\)z. u -||-> z \(\Rightarrow\) \(\exists\)u. v -||-> u \(\land\) z -||-> u 1326 4. x # u -||-> z 1327\end{alltt} 1328\end{session} 1329Abbiamo bisogno di suddividere l'assunzione 4. Siamo in grado di estrarla dalla 1330lista delle assunzioni usando il theorem-tactical \texttt{Q.PAT\_ASSUM}. Scriveremo. 1331\begin{verbatim} 1332 Q.PAT_ASSUM `x # y -||-> z` 1333 (STRIP_ASSUME_TAC o SIMP_RULE std_ss [x_ap_y_predn]) 1334\end{verbatim} 1335La quotation specifica il pattern su cui vogliamo effettuare il matching. Il secondo 1336argomento specifica come trasformeremo il teorema. Leggendo 1337le composizioni da destra a sinistra, prima semplificheremo con il 1338teorema \verb!x_ap_y_predn! e poi assumeremo il risultato indietro 1339nelle assunzioni, eliminando le disgiunzioni e gli esistenziali mentre andiamo 1340avanti\footnote{Un'alternativa alo posto di usare \texttt{PAT\_ASSUM} � di usare 1341 \texttt{by}: ci sarebbe da dichiarare per proprio conto la disgiunzione 1342 di quattro disgiunti, ma la dimostrazione sarebbe pi� ``dichiarativa'' nello 1343 stile, e bench� pi� verbosa, sarebbe pi� manutenibile.}. 1344 1345Sappiamo gi� che fare questo produrr� quattro nuovi sub-goal 1346(c'erano quattro disgiunti nel teorema \verb!x_ap_y_predn!). Al meno 1347uno di questi dovrebbe essere banale perch� corrisponder� al caso 1348in cui la riduzione parallela � semplicemente un passo ``non fare nulla''. Proviamo 1349ad eliminare i casi semplici con una chiamata ``speculativa'' a 1350\texttt{PROVE\_TAC} avvolta all'interno di un \texttt{TRY}. E prima di far 1351questo, dovremmo fare alcune riscritture per essere sicuri che le uguaglianze nelle 1352assunzioni sono eliminate. 1353 1354So: 1355\begin{session} 1356\begin{alltt} 1357- e (Q.PAT_ASSUM `x # y -||-> z` 1358 (STRIP_ASSUME_TAC o SIMP_RULE std_ss [x_ap_y_predn]) THEN 1359 RW_TAC std_ss [] THEN 1360 TRY (PROVE_TAC [predn_rules])); 1361OK.. 1362Meson search level: ............................... 1363Meson search level: ............................... 1364Meson search level: .................. 1365Meson search level: ..... 13662 subgoals: 1367> val it = 1368 \(\exists\)u'. y # v -||-> u' \(\land\) f # u # (g # u) -||-> u' 1369 ------------------------------------ 1370 0. S # f # g -||-> y 1371 1. \(\forall\)z. S # f # g -||-> z \(\Rightarrow\) \(\exists\)u. y -||-> u \(\land\) z -||-> u 1372 2. u -||-> v 1373 3. \(\forall\)z. u -||-> z \(\Rightarrow\) \(\exists\)u. v -||-> u \(\land\) z -||-> u 1374 1375 \(\exists\)u. y # v -||-> u \(\land\) z -||-> u 1376 ------------------------------------ 1377 0. K # z -||-> y 1378 1. \(\forall\)z'. K # z -||-> z' \(\Rightarrow\) \(\exists\)u. y -||-> u \(\land\) z' -||-> u 1379 2. u -||-> v 1380 3. \(\forall\)z. u -||-> z \(\Rightarrow\) \(\exists\)u. v -||-> u \(\land\) z -||-> u 1381\end{alltt} 1382\end{session} 1383Splendido! Abbiamo gi� eliminato due dei quattro disgiunti. Ora 1384il nostro prossimo goal rappresenta un termine \verb!K # z -||-> y! nelle assunzioni. 1385Abbiamo un teorema che riguarda proprio questa situazione. Ma prima 1386di applicarlo volenti o nolenti, proviamo ad immaginare esattamente qual � la 1387situazione. Un diagramma della situazione corrente potrebbe apparire come 1388\shorthandoff{"} 1389\[\xymatrix @C=2cm { 1390*+<4pt>[F--]\txt{\fbox{\texttt{K\kern2mm \#\kern2mm z}} \texttt{\#} \fbox{\texttt{u}}} \ar[r] & \txt{\texttt{z}} \ar@{.>}[d] \\ 1391*+<4pt>[F--]\txt{\fbox{\texttt{y}} \texttt{\#} \fbox{\texttt{v}}} \ar@{.>}[r] & \txt{\texttt{?u?}} 1392\ar "1,1"!<-12pt,0pt>;"2,1"!<-12pt,0pt> 1393\ar "1,1"!<28pt,0pt>;"2,1"!<11pt,0pt> 1394} \] 1395\shorthandon{"} 1396Il nostro teorema ci dice che \texttt{y} deve di fatto essere della forma 1397\verb!K # w! per qualche \texttt{w}, e che ci deve essere una freccia 1398tra \texttt{z} e \texttt{w}. Cos�: 1399\begin{session} 1400\begin{alltt} 1401- e (`?w. (y = K # w) /\bs (z -||-> w)` by PROVE_TAC [Kx_predn]); 1402OK.. 1403Meson search level: ...... 14041 subgoal: 1405> val it = 1406 \(\exists\)u. y # v -||-> u \(\land\) z -||-> u 1407 ------------------------------------ 1408 0. K # z -||-> y 1409 1. \(\forall\)z'. K # z -||-> z' \(\Rightarrow\) \(\exists\)u. y -||-> u \(\land\) z' -||-> u 1410 2. u -||-> v 1411 3. \(\forall\)z. u -||-> z \(\Rightarrow\) \(\exists\)u. v -||-> u \(\land\) z -||-> u 1412 4. y = K # w 1413 5. z -||-> w 1414\end{alltt} 1415\end{session} 1416 Ispezionando, appare chiaro che \texttt{u} deve essere 1417 \texttt{w}. Il primo congiunto richiede \verb!K # w # v -||-> w!, 1418 che abbiamo perch� questo � ci� che fa \KC{}, e il secondo 1419 congiunto � gi� nella lista delle assunzioni. Riscrivendo 1420 (eliminando prima quell'uguaglianza nella lista delle assunzioni 1421 render� il lavoro di \texttt{PROVE\_TAC} molto pi� facile), e poi il ragionamento al 1422 primo ordine risolver� questo goal: 1423\begin{session} 1424\begin{alltt} 1425- e (RW_TAC std_ss [] THEN PROVE_TAC [predn_rules]); 1426OK.. 1427Meson search level: ... 1428 1429Goal proved. [...] 1430Remaining subgoals: 1431> val it = 1432 \(\exists\)u'. y # v -||-> u' \(\land\) f # u # (g # u) -||-> u' 1433 ------------------------------------ 1434 0. S # f # g -||-> y 1435 1. \(\forall\)z. S # f # g -||-> z \(\Rightarrow\) \(\exists\)u. y -||-> u \(\land\) z -||-> u 1436 2. u -||-> v 1437 3. \(\forall\)z. u -||-> z \(\Rightarrow\) \(\exists\)u. v -||-> u \(\land\) z -||-> u 1438\end{alltt} 1439\end{session} 1440This case involving \SC{} is analogous. Here's the tactic to apply: 1441\begin{session} 1442\begin{alltt} 1443- e (`?p q. (y = S # p # q) /\bs (f -||-> p) /\bs (g -||-> q)` 1444 by PROVE_TAC [Sxy_predn] THEN 1445 RW_TAC std_ss [] THEN PROVE_TAC [predn_rules]); 1446OK.. 1447Meson search level: ........ 1448Meson search level: ........... 1449 1450Goal proved.[...] 1451Remaining subgoals: 1452> val it = 1453 \(\forall\)f g x z. S # f # g # x -||-> z \(\Rightarrow\) 1454 \(\exists\)u. f # x # (g # x) -||-> u \(\land\) z -||-> u 1455 1456 1457 \(\forall\)x y z. K # x # y -||-> z \(\Rightarrow\) \(\exists\)u. x -||-> u \(\land\) z -||-> u 1458\end{alltt} 1459\end{session} 1460Questo prossimo goal rappresenta un termine \verb!K # x # y -||-> z! per cui 1461abbiamo gi� un teorema. E di nuovo, usiamo in modo speculativo una chiamata a 1462\texttt{PROVE\_TAC} per eliminare i casi semplici immediatamente 1463(\verb!Kxy_predn! � un disgiunto cos� otteniamo due sub goal se non 1464eliminiamo nulla). 1465\begin{session} 1466\begin{alltt} 1467- e (RW_TAC std_ss [Kxy_predn] THEN 1468 TRY (PROVE_TAC [predn_rules])); 1469OK.. 1470Meson search level: .. 1471Meson search level: ... 1472 1473Goal proved. [...] 1474Remaining subgoals: 1475> val it = 1476 \(\forall\)f g x z. S # f # g # x -||-> z \(\Rightarrow\) 1477 \(\exists\)u. f # x # (g # x) -||-> u \(\land\) z -||-> u 1478\end{alltt} 1479\end{session} 1480Ancora meglio! Abbiamo ottenuto entrambi i casi immediatamente, e ci siamo spostati sull'ultimo 1481caso. Possiamo provare la stessa strategia. 1482\begin{session} 1483\begin{alltt} 1484- e (RW_TAC std_ss [Sxyz_predn] THEN PROVE_TAC [predn_rules]); 1485OK.. 1486Meson search level: .. 1487Meson search level: ........... 1488 1489Goal proved.[...] 1490> val it = 1491 Initial goal proved. 1492 |- \(\forall\)x y. x -||-> y \(\Rightarrow\) \(\forall\)z. x -||-> z \(\Rightarrow\) 1493 \(\exists\)u. y -||-> u \(\land\) z -||-> u : goalstack 1494\end{alltt} 1495\end{session} 1496La dimostrazione finale del goal pu� essere impacchettata in: 1497\begin{session} 1498\begin{verbatim} 1499val predn_diamond_lemma = prove( 1500 ``!x y. x -||-> y ==> 1501 !z. x -||-> z ==> ?u. y -||-> u /\ z -||-> u``, 1502 Induct_on `$-||->` THEN REPEAT CONJ_TAC THENL [ 1503 PROVE_TAC [predn_rules], 1504 REPEAT STRIP_TAC THEN 1505 Q.PAT_ASSUM `x # y -||-> z` 1506 (STRIP_ASSUME_TAC o SIMP_RULE std_ss [x_ap_y_predn]) THEN 1507 RW_TAC std_ss [] THEN 1508 TRY (PROVE_TAC [predn_rules]) THENL [ 1509 `?w. (y = K # w) /\ (z -||-> w)` by PROVE_TAC [Kx_predn] THEN 1510 RW_TAC std_ss [] THEN PROVE_TAC [predn_rules], 1511 `?p q. (y = S # p # q) /\ (f -||-> p) /\ (g -||-> q)` by 1512 PROVE_TAC [Sxy_predn] THEN 1513 RW_TAC std_ss [] THEN PROVE_TAC [predn_rules] 1514 ], 1515 RW_TAC std_ss [Kxy_predn] THEN PROVE_TAC [predn_rules], 1516 RW_TAC std_ss [Sxyz_predn] THEN PROVE_TAC [predn_rules] 1517 ]); 1518\end{verbatim} 1519\end{session} 1520\eos{} 1521 1522Siamo in dirittura di arrivo. Il lemma pu� essere trasformato in una dichiarazione 1523che coinvolge direttamente la costante \con{diamond}: 1524\begin{session} 1525\begin{verbatim} 1526val predn_diamond = store_thm( 1527 "predn_diamond", 1528 ``diamond $-||->``, 1529 PROVE_TAC [diamond_def, predn_diamond_lemma]); 1530\end{verbatim} 1531\end{session} 1532 1533Ed ora possiamo dimostrare che la nostra relazione originale � confluente in 1534un modo analogo: 1535 1536\begin{session} 1537\begin{verbatim} 1538val confluent_redn = store_thm( 1539 "confluent_redn", 1540 ``confluent $-->``, 1541 PROVE_TAC [predn_diamond, confluent_diamond_RTC, 1542 RTCpredn_EQ_RTCredn, diamond_RTC]); 1543\end{verbatim} 1544\end{session} 1545 1546 1547 1548\section{Esercizi} 1549 1550Se necessario, le risposte ai primi tre esercizi si possono trovare 1551esaminando il file sorgente in \texttt{examples/ind\_def/clScript.sml}. 1552 1553\begin{enumerate} 1554\item Dimostrare che \[\con{RTC}\;R \;x\; y \;\;\land \;\; 1555 \con{RTC}\;R\;y\;z\;\;\;\supset\;\;\; \con{RTC}\;R\;x\;z 1556\] Si avr� bisogno di dimostrare il goal per induzione, e si avr� probabilmente 1557 bisogno di massaggiarlo prima leggermente per ottenere che si accordi all'appropriato 1558 principio d'induzione. Archiviare il teorema sotto il nome 1559 \texttt{RTC\_RTC}. 1560\item Un'altra induzione. Mostrare che \[ 1561 (\forall x\,y.\; R_1\;x\;y\supset R_2\;x\;y) \supset 1562 (\forall x\,y.\; \con{RTC}\;R_1\;x\;y \supset \con{RTC}\;R_2\;x\;y) 1563\] Chiamare il teorema risultante \texttt{RTC\_monotone}. 1564\item Ancora un'altra induzione \con{RTC}, ma dove $R$ non � pi� 1565 astratta, ed � piuttosto la relazione di riduzione originale. Dimostrare 1566\[ 1567x \rightarrow^* y \;\;\;\supset\;\;\; 1568\forall z.\;\; x\;z \rightarrow^* y \;z \land 1569z\;x \rightarrow^* z\;y 1570\] Chiamarla \texttt{RTCredn\_ap\_congruence}. 1571 1572 1573\item Fornire un controesempio per la seguente propriet�: \[ 1574\begin{array}{c} 1575 \left( 1576 \begin{array}{ll} 1577 \forall x\,y\,z. & 1578 R\;x\;y\;\;\land\;\; R\;x\;z \;\;\;\supset\\ 1579 & \exists u.\;\con{RTC}\;R\;y\;u \;\;\land\;\;\con{RTC}\;R\;z\;u 1580 \end{array}\right)\\ 1581 \supset\\ 1582 \con{diamond}\;(\con{RTC}\;R) 1583 \end{array} 1584 \] 1585\end{enumerate} 1586 1587%%% Local Variables: 1588%%% mode: latex 1589%%% TeX-master: "tutorial" 1590%%% End: 1591