La formalizzazione del concetto di algoritmo: rassegna e...

Alma Mater Studiorum · Universita diBologna

FACOLTA DI SCIENZE MATEMATICHE, FISICHE E NATURALICorso di Laurea in Informatica

La formalizzazione delconcetto di algoritmo:rassegna e confronto

Tesi di Laurea in Paradigmi di Programmazione

Relatore:Chiar.mo Prof.Simone Martini

Presentata da:Tudor Alexandru Lascu

I SessioneAnno Accademico 2006-2007

A mio padre,che mi ha insegnato a sentire anche,

nel trambusto della vita,la cincia allegra cantare

Indice

1 Introduzione 71.1 Formulazione del problema . . . . . . . . . . . . . . . . . . . . 7

1.1.1 Le origini . . . . . . . . . . . . . . . . . . . . . . . . . 71.1.2 Il problema . . . . . . . . . . . . . . . . . . . . . . . . 81.1.3 Perche e interessante . . . . . . . . . . . . . . . . . . . 91.1.4 Il nostro lavoro . . . . . . . . . . . . . . . . . . . . . . 9

1.2 Due soluzioni . . . . . . . . . . . . . . . . . . . . . . . . . . . 101.2.1 Gurevich → Abstract State Machines . . . . . . . . . . 101.2.2 Moschovakis → Ricorsori . . . . . . . . . . . . . . . . . 13

2 Approccio operazionale 172.1 Presentazione . . . . . . . . . . . . . . . . . . . . . . . . . . . 17

2.1.1 Differenze tra la Tesi di Turing e la ASM–Thesis . . . . 192.2 Requisiti e loro analisi . . . . . . . . . . . . . . . . . . . . . . 19

2.2.1 Comportamento → Tempo sequenziale . . . . . . . . . 192.2.2 Struttura → Stati Astratti . . . . . . . . . . . . . . . . 212.2.3 Quantita di lavoro → Esplorazione limitata . . . . . . 252.2.4 Definizione di algoritmo sequenziale . . . . . . . . . . . 31

2.3 Programmi ASM e Teorema di caratterizzazione . . . . . . . . 322.3.1 Programmi ASM . . . . . . . . . . . . . . . . . . . . . 322.3.2 Teorema di caratterizzazione . . . . . . . . . . . . . . . 352.3.3 Alcune considerazioni . . . . . . . . . . . . . . . . . . . 37

2.4 Estensioni delle Abstract State Machines . . . . . . . . . . . . 422.4.1 Abstract State Machines non-deterministiche . . . . . . 422.4.2 Abstract State Machines parallele . . . . . . . . . . . . 452.4.3 Abstract State Machines distribuite . . . . . . . . . . . 46

2.5 Successi delle Abstract State Machines . . . . . . . . . . . . . 50

3 Approccio denotazionale 533.1 Presentazione . . . . . . . . . . . . . . . . . . . . . . . . . . . 533.2 Macchine astratte e definizioni ricorsive . . . . . . . . . . . . . 54

5

6 INDICE

3.2.1 Mergesort . . . . . . . . . . . . . . . . . . . . . . . . . 543.2.2 Macchine astratte . . . . . . . . . . . . . . . . . . . . . 573.2.3 Teoria delle equazioni ricorsive . . . . . . . . . . . . . . 593.2.4 Funzionali e ricorsori . . . . . . . . . . . . . . . . . . . 623.2.5 Implementazioni . . . . . . . . . . . . . . . . . . . . . 663.2.6 Algoritmi . . . . . . . . . . . . . . . . . . . . . . . . . 68

3.3 FLR - Sintassi . . . . . . . . . . . . . . . . . . . . . . . . . . . 703.3.1 Tipi . . . . . . . . . . . . . . . . . . . . . . . . . . . . 703.3.2 Oggetti tipati . . . . . . . . . . . . . . . . . . . . . . . 703.3.3 Sintassi . . . . . . . . . . . . . . . . . . . . . . . . . . 713.3.4 Congruenza e termini speciali . . . . . . . . . . . . . . 743.3.5 FLR - Riduzione . . . . . . . . . . . . . . . . . . . . . 75

3.4 FLR - Semantica . . . . . . . . . . . . . . . . . . . . . . . . . 813.4.1 Semantica denotazionale su strutture funzionali . . . . 813.4.2 Semantica intensioniale . . . . . . . . . . . . . . . . . . 84

4 Confronto e conclusioni 914.1 Moschovakis vs. Gurevich . . . . . . . . . . . . . . . . . . . . 91

4.1.1 Moschovakis critica Gurevich . . . . . . . . . . . . . . 924.1.2 La risposta di Gurevich . . . . . . . . . . . . . . . . . . 934.1.3 Gurevich critica Moschovakis . . . . . . . . . . . . . . 97

4.2 Confronto e conclusioni . . . . . . . . . . . . . . . . . . . . . . 984.2.1 Implementazioni . . . . . . . . . . . . . . . . . . . . . 984.2.2 Assiomatica vs. Teoria degli insiemi . . . . . . . . . . . 994.2.3 Critica a Moschovakis . . . . . . . . . . . . . . . . . . 1004.2.4 Critica a Gurevich . . . . . . . . . . . . . . . . . . . . 1004.2.5 Conclusioni . . . . . . . . . . . . . . . . . . . . . . . . 108

Bibliografia 111

Capitolo 1

Introduzione

1.1 Formulazione del problema

1.1.1 Le origini

La problematica che ci accingiamo a studiare trae origine dall’intensa atti-vita di ricerca, svolta negli anni Trenta, orientata alla soluzione del famosoEntscheidungsproblem formulato da Hilbert ed Ackermann nel 1928.La domanda che Hilbert aveva posto e la seguente: esiste un procedimentoeffettivo che in un numero finito di passi ci permetta di stabilire se una dataproposizione espressa in un linguaggio formale sia dimostrabile all’interno deldato formalismo (che costituisca quindi un teorema)?Un procedimento di questo genere, meccanico-effettivo e che termini in unnumero finito di passi, prendera poi, ufficialmente quanto informalmente, ilnome di algoritmo.Per rispondere a tale domanda era prima necessario chiarire che cosa si in-tendesse per procedimento di calcolo effettivo: si cercava, quindi, un’adeguataformalizzazione del concetto informale di funzione calcolabile in modo effet-tivo. Le prime risposte giunsero indipendentemente da Alonzo Church edAlan Turing nel 1936, rispettivamente in [14], [13] e [42]: entrambi giunge-vano, per vie notevolmente diverse, ad una formalizzazione del concetto difunzione calcolabile e, a partire da essa, assumendola corretta, dimostravanoche non puo esistere un procedimento meccanico che risponda ai requisiti po-sti da Hilbert. L’Entscheidungsproblem divenne cosı uno dei primi problemiad essere dichiarati indecidibili.I formalismi proposti da Church e Turing, pur profondamente diversi, venne-ro dimostrati equivalenti da Turing stesso in una postilla al proprio articolo

7

8 CAPITOLO 1. INTRODUZIONE

del ’36. In seguito vennero proposti numerosi altri formalismi1 che, sorpren-dentemente, data la notevole varieta, risultarono essere equivalenti.Quest’osservazione porto alla formulazione di quella che per molti versi eun’ipotesi di lavoro valida a tutt’oggi e universalmente accettata dalla comu-nita scientifica: la Tesi di Church–Turing. Essa sostiene, essenzialmente, cheil concetto (informale) di funzione calcolabile e stato correttamente forma-lizzato (si puo addirittura scegliere il formalismo che si preferisce, dato chesono tutti equivalenti).La Tesi di Turing afferma che per ogni funzione calcolabile (in modo effet-tivo) esiste un’opportuna Macchina di Turing che la calcola. Cio significache il formalismo delle MdT rappresenta un formalismo universale rispettoal concetto di funzione calcolabile.

1.1.2 Il problema

Il problema della formalizzazione del concetto di funzione calcolabile e dun-que stato risolto lasciando pero aperto il problema della formalizzazione delconcetto di algoritmo.Per comprendere la differenza tra i due problemi basta notare che la funzioneche un certo algoritmo calcola ne esprime l’estensione (cio che esso calcola)ma tralascia completamente l’aspetto intensionale dello stesso (il come vieneeffettuato il calcolo).Un esempio tanto semplice quanto chiaro e quello degli algoritmi di ordi-namento. Consideriamo il Mergesort ed il Quicksort, e chiaro che essi sonoprofondamente diversi ma e altresı chiaro che, per definizione, essi calcolanola stessa funzione: data una sequenza di numeri essi restituiscono la sequenzaordinata per valore.Vi e tutta una serie di caratteristiche di non secondaria importanza per lequali la definizione di funzione calcolabile risulta essere eccessivamente gros-solana: basandoci su di essa due algoritmi cosı diversi risulterebbero indi-stinguibili!Vorremmo un formalismo in grado di catturare tutta questa serie di aspetticaratterizzanti; vorremmo, inoltre, che questo formalismo avesse carattereuniversale e cioe che ogni algoritmo fosse definibile all’interno di esso.Si vuole qui analizzare se possa esistere un tale formalismo e passare inrassegna le possibili soluzioni che sono state proposte negli ultimi anni.

1I principali formalismi alternativi sono: la teoria delle funzioni ricorsive sviluppatada Godel, Herbrand e Kleene; la logica combinatoria (sistema S-K) sviluppata indipen-dentemente da Schonfinkel e Curry; i sistemi di riscrittura di Post ed infine gli algoritminormali sviluppati da Markov.

1.1. FORMULAZIONE DEL PROBLEMA 9

1.1.3 Perche e interessante

Il problema enunciato, formalizzare il concetto di algoritmo, risulta esseredi grande interesse da molti punti di vista. Se consideriamo il fatto che inambiente scientifico gran parte del lavoro (di routine e di ricerca) si basa sualgoritmi e sulle loro proprieta: e quasi sconcertante notare che nessuno sisia proposto prima di approfondire questo concetto in quanto tale ed even-tualmente di cercare una caratterizzazione che vada oltre la pratica comunedi limitarsi ad un elenco di caratteristiche (piu o meno ambigue). Sostan-zialmente lavoriamo con delle entita senza conoscerne la loro natura ulti-ma! Tale curiosita, oltre all’aspetto storico/epistemologico, riveste anche ungrande significato nell’ambito della ricerca sui fondamenti della matematicae dell’informatica; quello di algoritmo e infatti uno dei concetti fondanti diqueste discipline ma, sorprendentemente, esso stesso non e fondato2. Non daultimo bisogna anche considerare le conseguenze “pratiche” che una defini-zione formale di algoritmo potrebbe avere sulla teoria della calcolabilita.Vogliamo sottolineare che non e detto che sia possibile fondare in modo rigo-roso la teoria degli algoritmi ma che in ogni caso uno studio che si propongauno scopo di tale genere e spesso in grado di mettere in luce degli aspettipotenzialmente nuovi del concetto in esame o di chiarirne in modo inequivo-cabile degli aspetti noti.

1.1.4 Il nostro lavoro

Come abbiamo gia avuto modo di accennare, e piuttosto sorprendente notareche in numerosi testi (anche autorevoli) di teoria della calcolabilita si affermache il concetto di algoritmo e stato formalizzato da Church e Turing! Versola meta degli anni Ottanta la fondatezza di tale affermazione e stata messa indubbio da due studiosi che hanno ridato vita all’interesse verso l’aspetto fon-dazionale della teoria degli algoritmi: Yuri Gurevich e Yiannis Moschovakis.Analogamente a quanto successo nel 1936, essi hanno lavorato indipenden-temente l’uno dall’altro e percorso strade notevolmente diverse, giungendociascuno a risposte originali: il primo ha fornito una assiomatizzazione delconcetto di algoritmo mentre il secondo ne ha fornito un modello di teoriadegli insiemi.Scopo del presente studio e prendere in esame le soluzioni da essi sviluppatee confrontarle per cercare di capire se e in che misura sia stata fornita unarisposta soddisfacente al suddetto problema.

2Naturalmente la letteratura sull’analisi degli algoritmi e piu fiorente che mai ma essaconsidera il concetto di algoritmo come primitivo, preesistente.


Come vedremo, dall’analisi che e stata fatta emerge che in entrambi i casi citroviamo di fronte ad una soluzione non appieno soddisfacente.Nel caso del lavoro svolto da Moschovakis si tratta principalmente di proble-mi di scalabilita dal modello nel caso di algoritmi sequenziali3 al modello pertipi piu generali di algoritmo, algoritmi parallelli e distribuiti.Per quanto riguarda la soluzione proposta da Gurevich, invece, si tratta di unproblema di correttezza, nel senso che nel suo formalismo e possibile definireanche oggetti che non sono algoritmi. Cercando di approfondire lo studiodi questo aspetto, inoltre, abbiamo sviluppato una argomentazione sul per-che, a nostro parere, non sia possibile ovviare a tale problema rimanendoall’interno dell’impostazione generale adottata da Gurevich; esso e legato acaratteristiche intrinseche del modello stesso ed in quanto tale risulta ine-liminabile. Allo scopo di verificare la validita di tale osservazione abbiamocontattato il professor Gurevich ed il professor Egon Borger; tale discussioneverra presentata nel capitolo 4, dedicato al confronto ed alle conclusioni.

1.2 Due soluzioni

Le soluzioni qui presentate e messe a confronto si iscrivono in due delleprincipali correnti che hanno marcato la trattazione formale dei linguaggidi programmazione (spesso in contrapposizione l’una all’altra): l’approcciooperazionale e quello denotazionale. Gurevich con le sue Abstract State Ma-chines ha seguito il primo mentre Moschovakis coi suoi Ricorsori ha seguitoil secondo. Di seguito forniremo una breve presentazione dei due approc-ci in modo da fornire fin dall’inizio una chiave intepretativa che preceda lapresentazione dei singoli formalismi e dei loro tecnicismi.

1.2.1 Gurevich → Abstract State Machines

Il lavoro di Gurevich parte dalla ricerca di un modello operazionale univer-sale rispetto agli algoritmi: in sostanza una modello di macchina tale che,dato un algoritmo qualsiasi, si possa “costruire” una macchina che lo simulipasso–passo.Il modello cercato da Gurevich si basa quindi sul concetto di stato; per as-sicurarsi di catturare tutti gli algoritmi (non importa quanto astratti) egliconsidera il concetto piu generale di stato: in matematica esso e rappresen-tato dalle strutture (del primo ordine) introdotte da Tarski [41]. Si tratta

3Intendiamo che i passi della computazione vengono eseguiti in sequenza, da un soloagente di calcolo.

1.2. DUE SOLUZIONI 11

sostanzialmente di una collezione di funzioni, suddivisa in insiemi disgiun-ti detti universi; per uniformita gli elementi base possono essere visti comefunzioni ad arieta nulla e le relazioni come funzioni a valori nell’universo deiBooleani, formato dai soli elementi true e false. L’esperienza di oltre mezzosecolo mostra che ogni realta (matematica) statica puo essere adeguatamen-te modellata attraverso una struttura di Tarski; e importante notare che sitratta di entita astratte matematiche, nel senso che una struttura puo conte-nere anche insiemi infiniti (l’insieme N dei numeri naturali) oppure elementinon discreti come il numero “esatto”

√2, con la sua espansione infinita di

decimali.Gurevich utilizza proprio le strutture di Tarski per gli stati dell’automa colquale modellare un qualsiasi sistema di calcolo (algoritmico); tale scelta efondamentale in quanto e questa a garantirgli la massima liberta nel fissare,di volta in volta a seconda delle esigenze, il grado di astrazione che vuoleconsiderare. La novita di questo approccio sta proprio nel fatto che non ci sipreoccupa che le entita–stato possano trascendere il finito oppure il discreto!Anzi ci si avvantaggia di quello che potrebbe sembrare un limite per riuscirea gestire potenzialmente qualsiasi sistema, non importa quanto astratto es-so sia. Tale impostazione e cosı centrale da aver contribuito a buona partedel nome; le Abstract State (Machines) sono macchine i cui stati sono, perl’appunto, entita matematiche astratte non legate (e che non legano il pro-grammatore) ad alcun vincolo di rappresentabilita.

Abbiamo detto che gli stati astratti servono a descrivere realta statiche,la computazione e pero qualcosa di intrinsecamente dinamico. Usando leparole stesse di Gurevich prese da [21]:

Il modello ASM e un tentativo di incorporare la dinamica nellanozione di struttura.

Il calcolo puo essere dunque visto come evoluzione dello stato. Il minimocambiamento di uno stato lo si ottiene cambiando il valore di una funzionein un punto: questa istruzione, che prende il nome di aggiornamento, saral’istruzione base della nostra macchina astratta (del nostro automa) da consi-derarsi atomica, inscindibile in sottopassi. Prendendo in esame la transizioneda uno stato al successivo, l’idea fondamentale delle ASM e che se il compor-tamento del sistema di calcolo che stiamo considerando e algoritmico, allorala transizione da ciascuno stato al suo successore puo essere decomposta in unnumero finito di aggiornamenti; possiamo quindi modellare il procedimentodi calcolo con degli aggiornamenti regolati da delle condizioni. Dal momen-to che abbiamo verificato bastare un insieme finito di aggiornamenti e che


ogni regola (vista come aggiornamento + condizione) e finitamente rappre-sentabile, un programma ASM e sostanzialmente un’unica regola compostache descrive un passo della computazione che si vuole modellare. Esso forni-sce una rappresentazione simbolica della funzione di transizione dell’automaconsiderato.

Facciamo un esempio concreto, sfruttando il classico algoritmo per il cal-colo del massimo comun divisore che risale ad Euclide, che applicato a duenumeri naturali a e b restituisce in d il risultato:

1. Se a = 0 allora poni d = b, stop

2. altrimenti poni a = b mod a, b = a, torna al punto 1.

Il programma ASM corrispondente e il seguente:

if a = 0 then d := belseif a = 1 then d := 1.else

do in-parallel

a := b mod ab := a

enddo

endif

Il programma in se pare sufficientemente chiaro ma ci sono alcune pro-prieta importanti che e bene sottolineare; esse costituiscono delle caratteristi-che fondamentali del modello di calcolo (e del conseguente paradigma di pro-grammazione) sviluppato da Gurevich che possono, a prima vista, apparirebizzarre poiche si discostano dal modo standard di concepire il procedimentodi calcolo e la sua programmazione:

1. Tutti gli aggiornamenti (le cui guardie valutano a true) vengono esegui-ti simultaneamente; di default si tratta quindi di un tipo di program-mazione parallela in cui il grado di parallelismo e limitato, fissato apriori4.

2. Il programma ASM, corrispondente alla regola principale, che abbiamodetto descrivere un solo passo della computazione, va pensato da iterarefino a che non vengono generati nuovi aggiornamenti.

4Nel capitolo 2 in cui presenteremo in dettaglio le Abstract State Machines tratteremoanche delle estensioni del modello base che permettono grado di parallelismo illimitato.


3. Un altro aspetto caratteristico di questo approccio e che spetta al pro-grammatore curarsi del fatto che le entita coinvolte, stati e funzioni,appartengano al dominio dell’implementabile e rispettivamente del cal-colabile e questo avviene solo nel momento in cui egli debba tradurrein realta un certo modello 5.

4. Legato all’aspetto precedente bisogna sottolineare che scrivendo un pro-gramma ASM vogliamo tenere a mente che si tratta di simulare un datoalgoritmo il piu fedelmente possibile: ad un passo dell’algoritmo devecorrispondere una “mossa” dell’automa. Per rendere questo posssibilee necessario che, prima di ogni cosa, fissiamo un volta per tutte il li-vello di astrazione che vogliamo trattare; questo significa identificare leentita “significative”, esplicitandole e separandole da quelle che non losono. Rifacendoci all’esempio precedente, il fatto di come venga effet-tuato il calcolo dell’operazione mod, al livello che abbiamo scelto, none importante e per questo ci limitiamo a dire che vogliamo che in unqualche modo venga calcolato il valore a mod b. Possiamo immaginarequesto procedimento come la scelta del livello di dettaglio in cui fornirela descrizione di un certo oggetto: tutto cio che risulta piu specificonon e significativo e complicherebbe inutilmente la nostra descrizione.

La programmazione ASM e stata anche chiamata, in maniera eloquente,“pseudo-codice su strutture astratte” [17]; come abbiamo visto, scrivendoun programma ASM descriviamo un passo nella transizione da uno stato alsuccessivo senza dover scendere in tutti i dettagli: il testo di un programmaASM puo spesso apparire come pseudo–codice mentre esso costituisce un veroe proprio linguaggio di programmazione, dotato di una semantica precisa edeseguibile con vari strumenti 6.

1.2.2 Moschovakis → Ricorsori

In questa sezione ci rifacciamo alla presentazione di Moschovakis del propriolavoro contenuta in [33].Immaginiamo di lavorare nel contesto della struttura

A = (N, 0, zero, pred, plus);

5Nel senso che restando a livello di specifica si possono anche considerare entitairrealizzabili.

6Tra di essi ricordiamo: l’interprete ASM–Gofer [1] e ed il linguaggio AsmL per definirespecifiche eseguibili in ambiente .NET [3]. Per un elenco completo si rimanda alla sezioneTools di [2].


sull’insieme dei numeri naturali, abbiamo cioe a disposizione la costante 0,l’operazione di test su 0 7 e le operazioni per calcolare il predecessore di unnumero e la somma tra due numeri. Consideriamo ora il classico algoritmoper calcolare il quadrato di un numero:

sq(x) = times(x, x) where (1)times(u, v) = if zero(v) then 0

else plus(times(u, pred(v)), u).

Naturalmente la (1) letta come definizione ci appare come la definizionenon di un algoritmo ma bensı di una funzione; nell’approccio di Moschovakissi vuole invece mostrare che tale equazione puo anche essere interpretata co-me la definizione di un procedimento di calcolo, un algoritmo per l’appunto.Come punto di partenza per questa impostazione possiamo considerare lacoppia di funzionali:

f0(times, x) ' times(x, x),f1(u, v, times, x) ' if zero(v) then 0 else plus(times(u, pred(v)), u),

dove times varia nell’insieme delle funzioni parziali (binarie) su N. Pos-siamo vedere questa coppia come una prima aprossimazione dell’algoritmoche riteniamo “contenuto” nell’equazione (1). Per “eseguire” questo algorit-mo e calcolare il valore x2 dobbiamo prima di tutto calcolare il minimo puntofisso 8 dell’equazione:

times(u, v) ' f1(u, v, times).

A questo punto, denotato con times tale punto fisso, basta porre:

x2 = times(x, x).

Cosı facendo pero stiamo dando per scontato che f1 possa essere calcolatoin un solo passo nella struttura A e perdiamo quindi di vista come vengaeffettuato il calcolo a partire dalle operazioni base (che abbiamo a disposizio-ne in A). Vorremmo quindi esplicitare il procedimento di calcolo; dobbiamoespandere la definizione (1) in forma piu esplicita:

7L’operazione unaria zero(x) restituisce true se x vale 0 e false altrimenti (in questocontesto l’insieme dei Booleani e le operazioni base su di esso definite vanno consideratipredefiniti).

8Nella sezione 3.2.3 enunceremo il risultato che ci garantisce che e sempre possibilecalcolare il minimo punto fisso, in generale, di un sistema di equazioni di questo tipo.


sq(x) = times(x, x) where (2){times(u, v) ' if test(v) then initvalue( ) else loop(u, v),test(v) ' zero(v),initvalue( ) ' 0,loop(u, v) ' plus(loop1(u, v), u),loop1(u, v) ' times(u, loop2(v)),loop2(v) ' pred(v)}

Ora possiamo dire di aver modellato l’algoritmo “sottinteso” da (1), inA, tramite la tupla di funzionali:

sq = [g0, g1, . . . , g6],

dove g0 = f0 ed i restanti gi sono i punti fissi delle equazioni presenti in (2),ad esempio:

g4(u, v, times, test, initvalue, loop, loop1, loop2) ' plus(loop1(u, v), u).

L’oggetto sq e un ricorsore puro 9. Vedremo che esso e l’interpretazione(intensionale) su A di un certo termine appartenente ad un particolare lin-guaggio formale, FLR o Formal Language of Recursion; tale linguaggio con-sidera la ricorsione come operazione primitiva. E importante notare che sitratta di un oggetto semantico, definito all’interno della teoria degli insiemi,indipendente dai simboli utilizzati in (1) e che individua determinate pro-prieta semantiche (sulla struttura A in cui e definito). Un esempio e datodal fatto che cambiando l’ordine in cui eseguiamo la somma otteniamo, comevedremo, lo stesso oggetto poiche l’operazione di somma e commutativa inA; l’espressione:

sq′(x) = times(x, x) wheretimes(u, v) = if zero(v) then 0

else plus(u, times(u, pred(v))),

definisce lo stesso ricorsore individuato da (1) e dunque , in questo senso,lo stesso “algoritmo”.

9L’aggettivo puro si riferisce al fatto che esso non da luogo ad effetti collaterali (privodi side effect).


La tesi avanzata da Moschovakis e che i ricorsori possono modellare glialgoritmi, nel senso che ne catturano tutte le proprieta matematiche essen-ziali: se il formalismo delle funzioni ricorsive generali sono sufficientementepotenti da catturare tutte le funzioni calcolabili in modo effettivo allora unformalismo basato sulla ricorsione (generalizzata) deve essere in grado dicatturare tutti gli algoritmi. Abbiamo visto che un’equazione come (1) puoessere interpretata come un procedimento di calcolo, in generale avremo siste-mi di equazioni e il modo piu naturale e di considerare che essi contenganogia, in maniera implicita, tutte le informazioni necessarie per ottenere deiprocedimenti di calcolo e per derivarne le caratteristiche salienti.

Capitolo 2

Approccio operazionale

2.1 Presentazione

Il lavoro intrapreso da Gurevich puo essere visto, egli stesso lo suggerisce in[21], come un “affinamento della Tesi di Turing”.La Tesi di Turing afferma che per ogni funzione calcolabile in modo effettivoesiste una opportuna Macchina di Turing che la calcola.Dall’analisi condotta da Turing nel suo famoso articolo del 1936 [42] e dal-l’argomentazione informale che egli porta a favore della sua congettura nasceun ulteriore risultato, piu forte, che egli non enuncia in modo esplicito mache risulta ugualmente convincente: ogni procedimento di calcolo effettivo(algoritmo) puo essere simulato da una opportuna Macchina di Turing.Questo risultato e noto in letteratura con il nome di Tesi implicita di Turinged e a questa Tesi che si riferisce Gurevich ed e, quindi, questa Tesi che eglisi propone di “affinare”.Si parla di affinamento nel senso che Gurevich va alla ricerca di un model-lo di calcolo, una macchina, in grado di simulare qualsiasi algoritmo il piufedelmente possibile. Questo modello ci dovrebbe permettere di passare dauna descrizione informale di un algoritmo A ad una sua formalizzazione, inessenza una macchinaM, che risulti equivalente, dal punto di vista compor-tamentale, ad A.Un tale modello costituirebbe un modello universale rispetto agli algoritmiallo stesso modo in cui il formalismo delle Macchine di Turing costituisce unmodello universale rispetto alle funzioni calcolabili.Nel 1985, in una nota alla American Mathematical Society [25], Gurevichpresenta “una nuova tesi”: ogni algoritmo puo essere simulato da un’oppor-

17

18 CAPITOLO 2. APPROCCIO OPERAZIONALE

tuna struttura dinamica in tempo reale1.In seguito le strutture dinamiche di cui sopra prenderanno il nome di AbstractState Machines e la “nuova tesi” diventera nota col nome di Abstract StateMachine Thesis, abbreviato ASM–Thesis.La ASM–Thesis nella sua forma originaria era limitata agli algoritmi sequen-ziali, da intendersi qui come gli algoritmi “classici” in contrapposizione agli(ai piu moderni) algoritmi paralleli e distribuiti.Ammettendo che un modello del genere possa esistere, Gurevich procede adun’analisi dettagliata dei requisiti che una tale “macchina” deve presentare:sono questi ad indicargli il percorso da seguire per formalizzare il concetto dialgoritmo.Ad esempio, per garantire che un algoritmo e la corrispettiva macchina chelo simula si “comportino” allo stesso modo, uno dei requisiti fondamentali eche ad ogni passo dell’algoritmo debba corrispondere un solo passo compiu-to dalla macchina in questione: cosı facendo saremo autorizzati a scambiarel’uno con l’altra in qualsiasi contesto che richieda un adeguato grado di for-malizzazione.Gurevich compila una lista di tre requisiti che e facile verificare necessariaffinche un algoritmo sia rappresentabile da una ASM. A coronamento diquesto approccio, nel 2000, giunge un risultato [21] in cui si dimostra che talirequisiti sono anche sufficienti affinche un algoritmo sia caratterizzabile nelformalismo delle ASM.Rinfrancata da questo ed altri successi 2 la comunita di ricercatori delle ASMsi “lancia” quindi nel tentativo di estendere la ASM–Thesis anche alle classidi algoritmi paralleli e distribuiti e, se possibile, di ottenere risultati analoghia quello precedentemente enunciato.

Nella sezione 2.2 affronteremo l’analisi dei requisiti fondamentali in mo-do che la comprensione delle scelte che sono state fatte per il formalismodelle ASM, presentato nella sezione 2.3, risulti piu intuitiva; alla fine dellasezione 2.2 daremo una definizione di algoritmo sequenziale a partire dai re-quisiti base analizzati nella sezione precedente. Nella sezione 2.3 illustreremoil teorema (di caratterizzazione degli algoritmi sequenziali) che dimostra chei requisiti considerati sono (necessari e) sufficienti e per finire nella sezio-ne 2.4 presenteremo le estensioni del modello sequenziale alle altre classi dialgoritmi (non-deterministici, paralleli e distribuiti).

1Per una definizione formale di simulazione in tempo reale si veda la nota 12 nellasezione 2.3.3

2Si veda il capitolo 3 in cui ci occuperemo di confrontare i due approcci.

2.2. REQUISITI E LORO ANALISI 19

2.1.1 Differenze tra la Tesi di Turing e la ASM–Thesis

Prima di iniziare l’esposizione sistematica del modello delle ASM e beneprecisare alcuni aspetti per i quali differiscono le due Tesi:

1. La prima differenza e costituita dal fatto che la Tesi di Turing fornisceuna caratterizzazione delle funzioni calcolabili in modo effettivo e quin-di si concentra sull’aspetto estensionale degli algoritmi; la ASM–Thesis,al contrario, si propone di investigare anche l’aspetto intensionale e diarrivare ad una caratterizzazione degli algoritmi stessi.

2. (rispetto alla Tesi implicita di Turing) La seconda differenza riguardail livello di astrazione: e certamente vero che in linea di principio ognialgoritmo e simulabile da una Macchina di Turing ma questa formaliz-zazione non ci sarebbe di grande aiuto dal momento che si tratterebbedi “scendere” al livello dei singoli bit, mentre abbiamo gia accenna-to al fatto di come sia di vitale importanza per i nostri intenti chead un “passo” dell’algoritmo in questione corrisponda una ed una sola“mossa” della macchina. E chiaro che per simulare anche una sem-plice operazione, come la somma tra due interi, una MdT dovrebbeeffettuare un grande numero di “mosse”: quest’osservazione e sufficien-te a chiarire che abbiamo bisogno di un modello, per certi versi, “piuastratto”.

2.2 Requisiti e loro analisi

In questa sezione ci concentreremo sugli algoritmi sequenziali “classici”, ri-servandoci di discutere l’estensione del modello alle altre classi di algoritminella sezione seguente: una volta compreso il modello base, il passaggio allesue estensioni risultera piu intuitivo.Seguendo l’impostazione di Gurevich, facciamo conto che esista un modellooperazionale, un automa cioe, in grado di “catturare” qualsiasi algoritmo evediamo quali caratteristiche ci aspettiamo che esso soddisfi: a ciascuna diesse corrispondera un postulato nella caratterizzazione proposta da Gurevich.

2.2.1 Comportamento → Tempo sequenziale

Prima di tutto, associato ad un dato algoritmo A, ci aspettiamo di avere uninsieme di stati SA ed un suo sottoinsieme IA, gli stati iniziali, entrambi nonvuoti.Potremmo introdurre, come si fa solitamente, anche l’insieme degli stati di


terminazione oppure potremmo limitarci agli stati raggiungibili da I ma sce-gliamo di non farlo perche la trattazione non subisce modifiche sostanziali esi preferisce mantenere il massimo grado di generalita.Avremo poi una funzione di transizione τA : S → S.Un procedimento di calcolo algoritmico implica che ogni “passo” e ottenutoa partire dal precedente iterando il procedimento, cioe: Si+1 = τA(Si).(Per ogni stato S di terminazione avremo che: τA(S) = S.)A partire da uno stato iniziale S0 ∈ I la sequenza di stati σ := S0S1S2 . . . ,potenzialmente infinita, generata dall’iterazione di τA “costituisce” una ese-cuzione.Il flusso logico di esecuzione e in questo senso sequenziale, da cui il termi-ne Tempo sequenziale utilizzato per denotare i sistemi che godono di questaproprieta.Permettiamo che anche esecuzioni infinite facciano parte del nostro mo-dello perche non vogliamo escludere quegli algoritmi per i quali la non-terminazione e condizione normale; un esempio e rappresentato dall’algo-ritmo che, applicando il crivello di Eratostene per valori crescenti dell’ar-gomento, produce via via la successione dei numeri primi: si tratta di unalgoritmo che per definizione non termina.Essenzialmente stiamo dicendo che si trattera sicuramente di un tipo di siste-ma di transizione, cosa che non ci sorprende affatto considerato che quest’ul-timo rappresenta uno dei modelli piu generali per la semantica operazionale.I pochi elementi che abbiamo discusso ci permettono gia di definire unarelazione di equivalenza tra algoritmi:

1 Definizione (Equivalenza tra algoritmi). Due algoritmi A e B sidicono equivalenti se: SA = SB, IA = IB e τA = τB.

E facile notare che due algoritmi equivalenti sono “identici” dal punto divista comportamentale. La definizione fornita e molto “stretta” ed e naturalechiedersi se non sia “troppo stretta”: in effetti in base ad essa gli algoritmiseguenti risultano “diversi”:

• begin x := 1, y := 2 end

• begin y := 2, x := 1 end

Per il momento scegliamo di non occuparci di questo aspetto dal momentoche piu e “stretta” la definizione piu il risultato presentato nella sezione 2.3risulta “forte”.

Postulato del Tempo Sequenziale Ogni algoritmo sequenziale soddisfail requisito di Tempo Sequenziale.


Nota sulla terminologia (algoritmi a tempo sequenziale vs. algo-ritmi sequenziali) Generalmente il termine algoritmo sequenziale vieneutilizzato per indicare la classe degli algoritmi in cui c’e un solo agente dicalcolo e ogni passo ha una complessita limitata, fissata a priori; questo per-mette di distinguere gli algoritmi “classici” da quelli a paradigma parallelo(un agente di calcolo solo che puo eseguire piu linee di computazione) e di-stribuito (piu agenti di calcolo).Bisogna sottolineare che il termine algoritmo sequenziale e piu restrittivo nelsenso che non e detto che un algoritmo che soddisfa il postulato del TempoSequenziale sia sequenziale. Ad esempio, il seguente algoritmo, che determi-na se ci sono nodi isolati in un grafo:

if ∀x∃y : Edge(x, y) thenOutput := false

elseOutput := true

end if

soddisfa il suddetto postulato ma non si tratta di un algoritmo sequenzialeperche richiede di esplorare in un solo passo l’intero grafo (la cui ampiezzanon e a priori limitata).Per formalizzare la richiesta che un algoritmo sequenziale presenti un limitesuperiore al numero di azioni che puo eseguire in un passo, in una transizioneda uno stato al successivo, dobbiamo “investigare” meglio che cosa siano glistati del nostro automa: e quello di cui ci occuperemo nella prossima sezione.

2.2.2 Struttura → Stati Astratti

Il postulato trattato in questa sezione, che chiameremo Postulato degli StatiAstratti, riguarda gli stati dell’automa ed e composto di quattro parti. Leanalizzeremo una per una, per poi presentarle in forma unificata.

1) StatiChe tipo di “oggetti” sono gli stati del nostro automa?Per descrivere una realta statica l’oggetto matematico piu naturale e costi-tuito dal concetto di struttura del primo ordine introdotto da Tarski [41] (ladefinizione tradizionale viene leggermente modificata in modo da permetterealcune semplificazioni).


Sintassi Una segnatura, o vocabolario, Σ e una collezione finita di simbolida interpretare come “nomi di funzione”. Ciascuna funzione ha una arietafissata; funzioni ad arieta 0 si dicono costanti. Assumiamo che ogni segnaturaΣ contenga i seguenti simboli: =, true, false, undef, il simbolo unarioBoole e tutti i simboli delle operazioni booleane classiche. Nella definizioneclassica di struttura del primo ordine tutte le funzioni sono totali: la costanteundef ci permette di considerare anche funzioni parziali.Un Σ-termine e definito induttivamente:1. un nome di funzione ad arieta 0 e un Σ-termine,2. sia f un nome di funzione n-ario e siano t1, t2, . . . , tn Σ-termini, alloraf(t1, t2, . . . , tn) e un Σ-termine.

Semantica Una struttura X su una segnatura Σ e l’associazione tra uninsieme non vuoto BX (l’insieme base di X) e l’interpretazione dei nomi difunzione di Σ in BX . Indicheremo con Fun(X), la segnatura corrispondentealla struttura X. Un nome di funzione ad arieta n > 0 viene interpretato co-me una funzione f : BX

n → BX ; l’interpretazione di un nome di funzione adarieta 0 e un elemento di BX . I nomi di funzione si dividono in due categorie:quelli la cui interpretazione e passibile di cambiamento, dinamici e quelli chenon lo sono, statici. Nel caso di un nome di funzione ad a arieta 0 se e staticolo chiameremo costante mentre se e dinamico prendera il nome di variabile.Tra le richieste aggiungiamo che alle costanti true, false, undef debbanocorrispondere interpretazioni a due a due differenti. Funzioni con codomi-nio pari a {true, false} si chiamano relazioni. Una relazione unaria prendeil nome di universo e la sua interpretazione e quella di un sottoinsieme di BX .

Il valore V alX(t) 3 di un termine t in una struttura X la cui segnaturacontiene tutti i simboli di t e definito induttivamente:1. se t e un nome di funzione ad arieta 0, allora V alX(t) = c, dove c e l’ele-mento di X corrispondente a t che scriveremo come tX2. se t = f(t1, t2, . . . , tn), allora V alX(t) = fX(V alX(t1), V alX(t2), . . . , V alX(tn))

Se un certo termine t valuta a true nello stato S, se cioe V alS(t) = true,scriveremo S |= t.E da notare che noi lavoreremo con strutture dinamiche4 nel senso che ilvalore di una funzione in un punto puo cambiare e tipicamente lo fara, ri-

3Ove non risulti ambiguo, indicheremo V alX(t) anche con tX .4Nella nota presentata nel 1985, in cui Gurevich formula per la prima volta la sua Tesi,

viene utilizzato proprio il termine strutture dinamiche; in seguito, per un certo periodo ditempo, il nome cambiera in Evolving Algebras sempre in riferimento al fatto che, in questocontesto, i valori di una funzione sono passibili di cambiamento.


specchiando l’evoluzione della computazione; in particolare le variabili rive-stono il significato delle variabili nei linguaggi di programmazione (da nonconfondersi con le variabili della logica).La restrizione dell’insieme Fun(X) ai nomi di funzione statici prende il nomedi Carrier(X).

Esempio Per chiarire le idee facciamo un esempio in cui mostriamo comeappaiono gli stati di una Macchina di Turing nel formalismo delle AbstractState Machines.L’insieme base e formato dall’unione di tre universi disgiunti:Controllo ∪ Alfabeto ∪ Nastro

(a sua volta disgiunto da {true, false, undef}).– Controllo rappresenta l’insieme degli stati finiti che controllano la macchi-na. Ad elementi diversi in Controllo corrispondono nomi diversi. Abbiamopoi un elemento dinamico ControlloCorrente che potra essere aggiornatoad un nuovo valore (il nuovo stato di controllo appunto).– Alfabeto e l’alfabeto del nastro. Tutti gli elementi in Alfabeto sono di-stinguibili. Esiste un elemento che denotiamo con Blank.– Nastro possiamo identificarlo con l’insieme degli interi: ciascun intero rap-presenta/identifica una casella del nastro (infinito in entrambe le direzioni).Abbiamo bisogno di due funzioni/operazioni unarie, Succ e Pred, e di unafunzione dinamica (ad arieta 0), Testina, definita su Nastro.Per finire abbiamo la funzione Contenuto: Nastro → Alfabeto

Contenuto assegna Blank a tutti gli elementi di Nastro fuorche ad un numerofinito (qualsiasi elemento al di fuori del dominio viene mappato su undef).Ogni istruzione della Macchina di Turing puo essere rappresentata dal se-guente programma:

if ControlloCorrente = q1 and Contenuto(Testina) = σ1 then

do-in-parallel

ControlloCorrente := q2

Contenuto(Testina) := σ2

Testina := Succ(Testina)

2) Segnatura unicaNel paragrafo precedente abbiamo visto come ad ogni stato, in quanto strut-tura del primo ordine, sia associata una certa segnatura. Adesso vogliamoargomentare che gli stati, la cui successione costituisce una esecuzione (cor-rispondente ad un dato algoritmo A), condividono la stessa segnatura. Gli


elementi della segnatura corrispondono alle “entita essenziali” coinvolte inA. E sensato? Se la caratterizzazione e stata scelta in modo opportuno lasegnatura riflette solo gli elementi invarianti coinvolti nella computazione,quest’ultima vista come evoluzione dello stato.In generale, se abbiamo bisogno, man mano che la computazione avanza,di un numero sempre maggiore di elementi (funzioni) ad arieta n possiamogestire il problema tramite una funzione ad arieta n + 1.

3) Insieme base costanteIn base al punto precedente abbiamo che tutti gli stati condividono la stessasegnatura: e naturale chiedersi che cosa accada all’insieme base di ciascunastruttura-stato. Ad esempio: il nome di funzione sqr puo essere interpretatoin un certo stato S1 come la radice quadrata e in un altro stato S2 come ilvalore assoluto. E ovvio che cosı debbano stare le cose ma il problema sorgenel momento in cui S1 ed S2 occorrono nella stessa esecuzione: dobbiamonecessariamente garantire che l’interpretazione sia coerente!Fissati un livello di astrazione ed uno stato iniziale di partenza, ad ogni ese-cuzione di un dato algoritmo A viene quindi associato un insieme (base) chepossiamo denotare con BA.A livello di computazione vista come evoluzione di stato, questo significa chela funzione di transizione τA lascia inalterato l’insieme base BA. Gli elemen-ti di BA costituiscono “l’universo del discorso” (ed in effetti in letteratural’insieme base e anche noto col nome di superuniverse per distinguerlo dallerelazioni unarie anche note come universe).Supporremo, inoltre, di avere un insieme Riserva da cui andiamo ad estrarrenuovi elementi se ne abbiamo bisogno: cio equivale a lanciare il comandonew di certi linguaggi di programmazione che richiede l’allocazione di nuovospazio in memoria. E come se l’ambiente ci fornisse dall’esterno questi nuovielementi ma per semplificare certi tecnicismi si preferisce stipulare che taleinsieme faccia parte dell’insieme base. Lo stesso procedimento e stato segui-to quando abbiamo richiesto che gli elementi true, false, e undef fosserosempre inclusi nell’insieme base di qualsiasi stato.

4) Chiusura rispetto ad isomorfismiUn isomorfismo tra due strutture X e Y , con la stessa segnatura Σ, e unafunzione biiettiva dall’insieme base di X nell’insieme base di Y , ζ : BX → BY ,tale che per ogni f in Σ abbiamo:f(x1, ..., xn) = x0 in X ⇒ f(ζ(x1), ..., ζ(xn)) = ζ(x0) in Y .

Cio che ci interessa veramente e quello che un certo stato “rappresenta”:se ho una funzione che trasforma una certa struttura X in un’altra struttura


Y da essa indistinguibile, al livello di astrazione che sto considerando, allorase X e uno stato “valido” deve esserlo anche Y . La trasformazione che stia-mo considerando e proprio un isomorfismo tra strutture, come conseguenzal’insieme degli stati S(A), e l’insieme degli stati iniziali I(A), associati all’al-goritmo A, devono essere chiusi rispetto ad isomorfismi.Ma non basta, secondo quanto detto prima la funzione di transizione preser-va l’insieme base, cioe X e τA(X) hanno lo stesso insieme base e dunque glistessi elementi: l’isomorfismo ζ preserva anche le funzioni di τA(X)? Faccia-mo vedere che la domanda e ben posta:data una funzione f : X → Y , dove X e Y sono stati isomorfi, allora restadefinita la f : τA(X)→ τA(Y ) (dato che BX = BτA(X) e BY = BτA(Y ), dominioe codominio coincidono).Ragioniamo a livello di rappresentazione: dato un isomorfismo ζ tra due statiX e Y , essi rappresentano lo stesso stato. Un elemento x ∈ X e rappresen-tato dall’elemento ζx ∈ Y . Poniamo che τA setti il valore f(a) a c in X:avremo f(a) = c in τA(X). Consideriamo la ζ-rappresentazione di X, cioeY , τA pone f(ζa) a ζc da cui: f(ζa) = ζc in τA(Y ).

Possiamo finalmente raccogliere le quattro osservazioni sin qui fatte in ununico enunciato:

Postulato degli Stati Astratti:

1. gli stati di un algoritmo sono strutture del primo ordine;

2. tutti gli stati (di una esecuzione) di un algoritmo condividono la stessasegnatura;

3. la funzione di transizione non modifica l’insieme base di alcuno stato(appartenente ad una certa esecuzione);

4. gli insiemi S(A) e I(A), l’insieme degli stati e l’insieme degli statiiniziali associati all’algoritmo A, sono chiusi rispetto ad isomorfismi.Inoltre se f e un isomorfismo tra due stati X e Y , allora e ancheisomorfismo tra τA(X) e τA(Y ).

2.2.3 Quantita di lavoro → Esplorazione limitata

Abbiamo precedentemente accennato a come, nel caso sequenziale, sia ne-cessario specificare in qualche modo che la “quantita di lavoro” compiuta adogni passo da un algoritmo abbia un limite superiore fissato a priori (dunquecostante).


Questo limite si riferisce necessariamente al numero di “azioni base” ma qualisono le azioni base (elementari) nel contesto che stiamo considerando? Cia-scuno Σ-stato5 S e univocamente determinato dal valore (interpretazione)delle funzioni nell’insieme base X di S. Il cambiamento minimo e ottenutoa partire da X cambiando il valore di una funzione in un punto (stiamo la-vorando con funzioni dinamiche!).Per formalizzare il discorso introduciamo il concetto di aggiornamento.Dato un nome di funzione f ad arieta n, in Σ, e una n-upla a di elementidell’insieme base X, la coppia l = (f, a) prende il nome di locazione6; ad(f, a) viene associato il valore assunto dal termine f(a) in X che chiameremocontenuto di l e denoteremo con ContentX(f, a).Un aggiornamento e un cambiamento del contenuto di una locazione l:se b e un elemento in X, la tripla u = (f, a, b) e un aggiornamento di X.La semantica di un aggiornamento e quella di sostituire il contenuto dellalocazione (f, a) col valore b.Un insieme di aggiornamenti si dice coerente se non contiene aggiornamentidiversi sulla stessa locazione, aggiornamenti del tipo: (f, a, b1), (f, a, b2), conb1 6= b2.La semantica di un insieme coerente di aggiornamenti e quella di eseguiretutti gli aggiornamenti simultaneamente mentre la semantica di un insiemeincoerente di aggiornamenti e di non causare alcuna modifica.Denotiamo un insieme di aggiornamenti con ∆ ed il corrispettivo risultato(dell’applicazione di ∆ allo stato X) con X + ∆.

Osservazione Siano X e Y strutture definite a partire dalla stessa segna-tura e con lo stesso insieme base, allora l’insieme (coerente) di aggiornamenti∆ che trasforma l’una nell’altra (Y = X + ∆) e unico. Per verificare che ecosı e sufficiente notare che X e Y hanno le stesse locazioni, per cui bastadefinire:

∆ =def {(f, a, b) : b = ContentY (f, a) 6= ContentX(f, a)}.

Denoteremo questo insieme di aggiornamenti con Y −X.

Insieme di aggiornamenti generato da un algoritmo Partiamo dauno stato X associato ad un algoritmo A, sappiamo che X e τA(X) hanno

5Stato definito a partire dalla segnatura Σ.6In effetti e possibile vedere uno stato S come un dispositivo di memorizzazione da-

to dall’insieme delle associazioni tra un indirizzo (nome di funzione + interpretazionedei termini a cui viene applicata) ed il valore ivi salvato (il valore assunto dal terminecomposto).


gli stessi elementi e le stesse locazioni (ce lo garantisce il postulato degli StatiAstratti).Possiamo definire l’insieme degli aggiornamenti generato dall’algoritmo Asullo stato X:

∆(A, X) =def τA(X)−X.

Risulta: τA(X) = X + ∆(A, X).

Insieme caratteristico Notiamo che gli elementi coinvolti negli aggior-namenti di ∆(A, X) sono Σ-termini; cio significa che la transizione da unostato X al suo successore τA(X) puo essere specificata da un insieme di talitermini. Se si potesse trovare un unico insieme T di termini in grado dirappresentare la transizione da ogni stato al suo successore allora si potrebbedescrivere ∆(A, X) tramite gli elementi di T . In questo caso diremo che T ecaratteristico per τ .Per un tale insieme T e ragionevole richiedere che se a due stati X e Ycorrispondono insiemi di aggiornamenti diversi (∆(A, X) 6= ∆(A, Y )), allorasignifica che esiste almeno un termine t in T la cui interpretazione, nei duestati, differisce (tX 6= tY ).Per cui se T e caratteristico per τ deve valere la seguente proprieta:se per ogni t in T vale tX = tY , allora ∆(A, X) = ∆(A, Y ).

Di seguito presenteremo prima il terzo postulato nella sua forma origi-naria, come presentato in [21], per poi esporne i limiti e passare ad un’altraformulazione, piu generale, trattata in [26].

Sia τA la funzione di transizione corrispondente all’algoritmo A e sia Tun insieme di termini; come nella discussione precedente (caratteristico perτA) se T e finito diciamo che τA e ad esplorazione limitata.Col termine esplorazione limitata viene suggerito che ad ogni passo l’algo-ritmo A agisce solamente su un numero di elementi limitato a priori (che eproprio il requisito da cui eravamo partiti).In questo caso l’insieme T prende anche il nome di testimone di esplorazionelimitata.

Postulato dell’esplorazione limitata (prima versione) Esiste un in-sieme finito T di Σ-termini tale che ∆(A, X) = ∆(A, Y ) ogni volta che X eY coincidono su T (∀t ∈ T : tX = tY ).


Il postulato precedente sembra ragionevole e abbastanza chiaro ma pre-senta un problema notevole: richiede di abbandonare l’impostazione, assuntaa paradigma, che avevamo adottato col Postulato degli Stati Astratti. Nellaprima versione del postulato, infatti, lavoriamo con due stati specifici X e Ye non con le loro classi di ismorfismo e incappiamo quindi in una incoerenzadi approccio che vorremmo eliminare.La seconda versione, presentata in [26], e in questo senso piu generale.Per comprenderlo abbiamo prima bisogno di introdurre un po’ di terminolo-gia ed alcuni risultati.

Sia T un insieme di Σ-termini chiuso rispetto a sottotermini7.Denoteremo con XT l’insieme {V alX(t) : t ∈ T} (l’insieme dei valori assuntiin X quando t spazia in T ).La relazione, rappresentata dall’insieme di coppie:

{(V alX(t), V alY (t)) : t ∈ T},

prende il nome di relazione di T -similarita tra X e Y e viene indicata con RT .Risulta naturale considerare la seguente relazione di equivalenza sui Σ-termini:

2 Definizione (Tipo di T -similarita). Il Tipo di T-similarita dello statoX e la relazione di equivalenza ∼X definita su T nel seguente modo:

s ∼X t ⇐⇒ V alX(s) = V alX(t).

Possiamo denotare con EX il Tipo di T-similarita di X.Indotta da questa relazione di equivalenza ne rimane definita un’altra, questavolta sugli stati:

3 Definizione (T -similarita). Due stati X e Y si dicono T-simili se i loroTipi di T-similarita coincidono (se vale cioe EX = EY ).

1 Lemma. Se due stati X e Y sono T -simili, allora RT e una funzionebiiettiva da XT in YT .

Dimostrazione. Dobbiamo verificare che per ogni x ∈ XT risulti:

se (x, y) ∈ RT e (x, z) ∈ RT , allora y = z.

Sia x = V alX(s), abbiamo xRT V alY (s) (per definizione di RT ).Supponiamo che esista un termine t in T , con t 6= s, tale che xRT V alY (t),cioe: V alX(s)RT V alY (t). Per come abbiamo definito RT , due elementi sonoin RT -relazione se sono interpretazione (in generale in strutture diverse) dellostesso termine, allora deve esistere un termine r in T tale che:

7Se t1 ∈ T e t2 e un suo sottotermine, allora anche t2 ∈ T .


1. V alX(r)RT V alY (r), e

2. V alX(s) = V alX(r) e V alY (r) = V alY (t).

Osserviamo ora che:

1. V alX(s) = V alX(r) =⇒ r ∼X s =⇒ s ∈ [r]∼X

2. V alY (r) = V alY (t) =⇒ r ∼Y t =⇒ t ∈ [r]∼Y

Per ipotesi X e Y sono T -simili, questo significa che le classi di equivalenzaindotte da X, EX , e quelle indotte da Y , EY , coincidono: ∼X =∼Y , da cui[r]∼X

= [r]∼Y. Risulta che s e t sono nella stessa classe di equivalenza (sia in

X che in Y ): s ∼Y t, da cui otteniamo, per definizione, V alY (s) = V alY (t).Per verificare che RT sia biiettiva basta mostrare che la relazione inversa diRT e anch’essa una funzione, cosa che si dimostra allo stesso modo.

4 Definizione (T -isomorfismo). Una funzione biiettiva F : XT → YT

prende il nome di T -isomorfismo da X in Y se per ogni termine f(t1, . . . , tn)in T risulta:

F (fX(V alX(t1), . . . , V alX(tn))) = fY (F (V alX(t1)), . . . , F (V alX(tn))).

2 Lemma. Siano X e Y due stati T -simili, allora RT e una funzione biiettivaed e un T -isomorfismo da X in Y .

Dimostrazione. Per il lemma precedente non ci resta che mostrare che RT

e un T -isomorfismo da X in Y . Sia t = f(t1, . . . , tn) un termine in T , siaxi = V alX(ti) per i = 1, . . . , n, allora:

RT (fX(V alX(t1), . . . , V alX(tn))) = RT (V alX(t)), ma

RT (V alX(t)) = V alY (t) = fY (RT (x1), . . . , RT (xn)), da cui risulta:

RT (fX(V alX(t1), . . . , V alX(tn))) = fY (RT (x1), . . . , RT (xn)).

3 Lemma. Se RT : XT → YT e una funzione biiettiva, allora X e Y sonoT -simili.

Dimostrazione. Dobbiamo far vedere che:

t1 ∼X t2 ⇐⇒ t1 ∼Y t2, per ogni t1, t2 in T .

Basta mostrare solo un verso dell’implicazione perche quello contrario e sim-metrico. Sia, per ipotesi, t1 ∼X t2. Allora per definizione di RT abbiamo cheV alX(t1) = V alX(t2). Da cui, applicando RT ad entrambi i lati, otteniamo:


RT (V alX(t1)) = RT (V alX(t2)), e quindi:

V alY (t1) = RT (V alX(t1)) = RT (V alX(t2)) = V alY (t2).

Sempre per definizione di RT , risulta t1 ∼Y t2.

5 Definizione (T -accessibilita). Un elemento a di uno stato X e T-accessibile se esiste un termine t ∈ T tale che a = V alX(t).Un aggiornamento (f, (a1, . . . , an), a0) si dice T-accessibile se ogni elementoai e T-accessibile, con i = 0, 1, . . . , n. Un insieme ∆ di aggiornamenti si diceT-accessibile se ogni aggiornamento in ∆ e T-accessibile.

Ora abbiamo tutti gli elementi per dare la nuova formulazione del postu-lato.

Postulato dell’esplorazione limitata (nuova versione) Esiste un in-sieme finito T di Σ-termini tale che:

1. per ogni stato X di A, ∆(A, X) e T -accessibile;

2. se gli stati X e Y sono T -simili, f(t1, . . . , tn) ∈ T e, adottando lanotazione ai = V alX(ti) e bi = V alY (ti), allora(f, (a1, . . . , an), a0) ∈ ∆(A, X) ⇐⇒ (f, (b1, . . . , bn), b0) ∈ ∆(A, Y ).

Il postulato afferma che basta un insieme finito di termini per distinguereinsiemi di aggiornamenti diversi e per caratterizzare quindi la transizione, daogni stato al successore, dell’automa che stiamo considerando. Inoltre notia-mo che, a differenza della prima versione, lavoriamo con classi di isomorfismo(individuate dalla relazione di T -similarita).Questo e il requisito fondamentale perche a partire da esso saremo in grado difornire una rappresentazione sintattica (basata su Σ-termini) di un sistemadi transizione in grado di simulare passo-passo un algoritmo dato.

Possiamo richiedere che, dato un insieme T di termini caratteristico, se adue stati X e Y corrispondono insiemi di aggiornamenti diversi, allora esistealmeno un termine t in T la cui interpretazione, nei due stati, differisce; talerichiesta, che aveva portato alla prima formulazione del postulato, e moltonaturale: vorremmo quindi verificare che rimanga valida a fronte della nuovaformulazione. Facciamo vedere che se e verificato il postulato nella versionenuova (PN) allora lo e anche in quella vecchia8.

8Esiste anche una dimostrazione del verso contrario dell’implicazione. Tramite essaviene stabilita l’equivalenza tra le due versioni del postulato, in presenza dei primi due.Si e scelto, tuttavia, di omettere tale dimostrazione per non appesantire ulteriormentel’esposizione.


Sia T un testimone di esplorazione limitata tale che sia verificato PN, si trattadi mostrare che se X e Y coincidono su T , allora vale: ∆(A, X) = ∆(A, Y ).X e Y sono banalmente T -simili e la funzione RT e la funzione identita.PN garantisce che vale:

(f, (a1, . . . , an), a0) ∈ ∆(A, X) ⇐⇒ (f, (b1, . . . , bn), b0) ∈ ∆(A, Y ),

dove ai = V alX(ti) e bi = V alY (ti). Ma, per ipotesi, V alX(ti) = V alY (ti),per ogni ti ∈ T . Risulta che ∆(A, X) = ∆(A, Y ).

Prima di procedere illustriamo un corollario del Postulato dell’esplorazio-ne limitata che verra sfruttato nella dimostrazione del Teorema di caratteriz-zazione, presentato nella sezione seguente.

Immagine di un aggiornamento via un isomorfismo Siamo interessatia mettere in relazione gli insiemi di aggiornamenti corrispondenti a statiisomorfi. Per far cio dobbiamo prima dire che cosa sia l’immagine di unaggiornamento via un isomorfismo.Siano X e Y due stati e sia ζ : X → Y un isomorfismo, consideriamo unaggiornamento su X, δ = (f, a, b), allora:

ζ(δ) = ζ((f, a, b)) = ζ((f, (a0, . . . , an), b)) =def (f, (ζ(a0), . . . , ζ(an)), ζ(b)).

Possiamo ora dire che cos’e l’immagine di un insieme di aggiornamenti ∆ viaun isomorfismo: ζ(∆) =def {ζ(δ) : δ ∈ ∆}.

4 Lemma. Siano X ed Y due stati T -simili, allora RT (∆(A, X)) = ∆(A, Y ).

Dimostrazione. RT e un ismorfismo in quanto X e Y sono T -simili. Laseconda parte del postulato ci dice che:

(f, (V alX(t1), . . . , V alX(tn)), V alX(t0)) ∈ ∆(A, X) ⇐⇒(f, (V alY (t1), . . . , V alY (tn)), V alY (t0)) ∈ ∆(A, Y ),

dove f(t1, . . . , tn) ∈ T . Ma per ogni i, V alY (ti) e esattamente RT (V alX(ti)),da cui otteniamo: RT (∆(A, X)) = ∆(A, Y ).

2.2.4 Definizione di algoritmo sequenziale

Analizzando ciascuno di essi separatamente, abbiamo visto come i requisitiprecedenti risultino abbastanza naturali per un algoritmo sequenziale qual-siasi.


Lanciamo ora una sorta di provocazione: diamo una definizione di algoritmosequenziale (a partire dai postulati individuati dai tre requisiti).

6 Definizione (Algoritmo sequenziale). Un oggetto che soddisfi i trepostulati:

1. Tempo Sequenziale

2. Stati Astratti

3. Esplorazione Limitata

e un algoritmo sequenziale.

Naturalmente la suddetta definizione, per il momento, non e nient’altroche una congettura e come tale soggetta al “dubbio scientifico” ma nella se-zione seguente illustreremo un risultato che mostra che questa “scommessa”e, quanto meno, ragionevole.

2.3 Programmi ASM e Teorema di caratte-

rizzazione

2.3.1 Programmi ASM

Vogliamo, adesso, trovare degli elementi sintattici (costrutti o regole), la cuicombinazione sia in grado di “rappresentare” la funzione di transizione asso-ciata ad un certo algoritmo A.Abbiamo visto che il “costituente elementare” di ogni transizione e costitui-to dall’aggiornamento, per cui ad esso dovra corrispondere la regola base deiprogrammi che stiamo considerando.Il modo piu naturale di rappresentare un aggiornamento e tramite un’istru-zione di assegnamento α sulla segnatura Σ:

f(t1, . . . , tn) := t0

dove f e un nome di funzione n-aria in Σ e t0, t1, . . . , tn sono Σ-termini.Una istruzione di assegnamento e anche nota come regola di aggiornamento.La semantica dell’assegnamento α sulla struttura X (con segnatura Σ) e laseguente: calcolare il valore (in X) corrispondente ad ogni termine presentein α, ai =not V alX(ti), e poi eseguire l’aggiornamento (f, (a1, . . . , an), a0) su

2.3. PROGRAMMI ASM E TEOREMA DI CARATTERIZZAZIONE 33

X.Ricordiamo che ∆(A, X) e l’insieme di aggiornamenti generato dall’algoritmoA sullo stato X.Per essere precisi, dobbiamo dimostrare che ogni aggiornamento δ in ∆(A, X)e rappresentabile da una regola, ovvero che ogni elemento in δ e T -accessibile,ottenuto cioe dalla valutazione di un certo Σ-termine in T (dove T e un te-stimone di esplorazione limitata). Riprendendo la notazione precedentemen-te introdotta, XT =not {V alX(t) : t ∈ T}, dobbiamo dimostrare che ognielemento in δ e in XT .

5 Lemma. Sia δ = (f, (a1, . . . , an), a0) un aggiornamento in ∆(A, X), alloraciascun elemento ai in δ e T -accessibile, con T testimone di esplorazionelimitata.

Dimostrazione. Supponiamo, per assurdo, che un certo ai non sia T -accessibilee costruiamo uno stato Y , isomorfo a quello di partenza, ottenuto sostituen-do l’elemento ai con un nuovo elemento b (il fatto che questo sia a tutti glieffetti uno stato ci e garantito dal Postulato degli Stati Astratti).Ovviamente, non avendo modificato alcun termine in T , abbiamo:V alX(t) = V alY (t),∀t ∈ T .Abbiamo precedentemente dimostrato (alla fine della sezione precedente) cheil Postulato dell’Esplorazione Limitata implica che se X e Y coincidono suT , allora ∆(A, X) = ∆(A, Y ).Per cui, dev’essere: (f, (a1, . . . , an), a0) ∈ ∆(A, Y ).Ma ai non compare in Y . Il Postulato degli Stati Astratti ci garantisce chel’insieme base non cambia, per cui ai non puo comparire nemmeno in τA(Y ),da cui risulta che ai non compare in ∆(A, Y ) = τA(Y )− Y .Quindi: (f, (a1, . . . , an), a0) 6∈ ∆(A, Y ). Assurdo.

A questo punto siamo sicuri che ad ogni aggiornamento δ in ∆(A, X)corrisponde un assegnamento e constatiamo che per rappresentare l’interoinsieme di aggiornamenti ∆(A, X) abbiamo bisogno di una regola che ci per-metta di eseguire molteplici assegnamenti simultaneamente.Siano R1, . . . , Rk Σ-regole9 (con k numero naturale), allora la seguente:

do-in-parallel

R1

R2...

Rk

9Regole definite sulla segnatura Σ.


enddo-in-parallel

e una Σ-regola. La semantica di questa regola e quella, sottintesa, di eseguirein parallelo le R1, . . . , Rk. Ove non risulti ambiguo ometteremo il termina-tore enddo-in-parallel.

Nell’eseguire un algoritmo A ogni stato e ottenuto dal precedente perapplicazione della funzione di transizione τA: per “rappresentare” corretta-mente τA abbiamo quindi bisogno di un unico “programma” che, iterato,simuli ciascuna transizione da uno stato al successore. Dal momento cheil programma e unico dobbiamo avere un modo per distinguere uno statodall’altro: la soluzione piu naturale e cercare un termine che, valutato, resti-tuisca true solo in corrispondenza dello stato in questione.Quest’osservazione ci suggerisce che abbiamo bisogno anche di un costruttoche ci permetta di eseguire una determinata azione solo nel caso in cui risultiverificata una certa condizione.Sia ϕ un Σ-termine booleano (valutato assume valori nell’universo Boole) esiano R1, R2 due Σ-regole, allora la seguente:

if ϕ then R1

else R2

endif

e una Σ-regola (regola condizionale). La semantica di questa regola e quelladi valutare il termine ϕ (la guardia) e, a seconda della sua validita, di ese-guire R1 oppure R2.

Possiamo ora definire, induttivamente, l’insieme degli aggiornamenti ge-nerati da una Σ-regola R, denotato con ∆(R,X):

1. se R e un assegnamento, f(t1, . . . , tn) := t0, e ai = V alX(ti) (per i =0, 1, . . . , n), allora ∆(R,X) =def {(f, (a1, . . . , an), a0)}.

2. se R e un regola di tipo do-in-parallel, con R1, . . . , Rk come sotto-regole, allora ∆(R,X) =def ∆(R1, X) ∪ · · · ∪∆(Rk, X).

3. se R e un regola condizionale, con guardia ϕX ed R1, R2 come sottore-gole, allora

∆(R,X) =def

{∆(R1, X) se ϕX = true∆(R2, X) se ϕX = false


Un programma ASM e sostanzialmente una Σ-regola R che applicata aduna stato (iniziale) genera, per iterazione, una successione di stati (esecuzio-ne): esso descrive un solo passo nella transizione individuata dall’esecuzionedi un algoritmo.Ciascuno stato e ottenuto a partire dal precedente applicando gli aggiorna-menti individuati dalle sottoregole di R.In questo modo ci si assicura di mantenere lo stesso livello di astrazione, cosache abbiamo visto essere fondamentale per questo approccio.A partire da un programma Π possiamo considerare la funzione di transizioneda esso generata:

τΠ(X) =def X + ∆(Π, X).

Abbiamo, quindi, dei costrutti sintattici in grado di rappresentare l’evoluzio-ne della computazione di un procedimento algoritmico: ci basta? E sufficienteper risolvere l’intera problematica?Nella prossima sezione mostreremo un risultato potente che sembra avallareuna risposta affermativa.

2.3.2 Teorema di caratterizzazione

Non e difficile condividere l’opinione che i requisiti presentati nella sezioneprecedente debbano costituire condizione necessaria affinche un algoritmo(sequenziale) sia rappresentabile da un modello operazionale.In questa sezione dimostriamo che tali requisiti sono anche sufficienti.La definizione proposta di algoritmo, presentata nella sezione 2.2.4, risultaquindi ben fondata.Questo ci dice che esiste un modello operazionale (un automa) in grado disimulare passo-passo ogni algoritmo sequenziale.

Prima di tutto facciamo vedere che per ogni funzione di transizione corri-spondente ad un algoritmo esiste un programma ASM in grado di descriverla(la cui interpretazione generi lo stesso insieme di aggiornamenti).

6 Lemma. Per ogni algoritmo sequenziale A, definito sulla segnatura Σ,esiste un programma ASM Π, sempre definito su Σ, tale che:∆(A, X) = ∆(Π, X), per ogni stato X di A.

Dimostrazione. Partiamo da uno stato qualsiasi X di A. Sia T un testimonedi esplorazione limitata per A.


La prima parte del Postulato di esplorazione limitata ci dice che ∆(A, X) e ac-cessibile, per cui per ogni aggiornamento δ = (f, (a1, . . . , an), a0) ∈ ∆(A, X)possiamo considerare i termini ti

δ tali che V alX(tiδ) = ai, per i = 0, 1, . . . , n.

A partire da questi costruiamo l’assegnamento f(t1δ, . . . , tn

δ) := t0δ, denota-

to con Rδ. Sia RX la regola do-in-parallel con sottoregole costituenti leRδ, per tutti i δ ∈ ∆(A, X).Per ogni stato Y di A, T -simile ad X, per il Lemma 2, RT e un T -isomorfismoda X in Y . Abbiamo che:

∆(RX , Y ) = RT (∆(RX , X)) = RT (∆(A, X)) = ∆(A, Y ).

La prima uguaglianza e verificata per definizione di RT , la seconda per comeabbiamo costruito RX e l’ultima corrisponde al Lemma 4.Abbiamo ottenuto: ∆(RX , Y ) = ∆(A, Y ).Essendo T finito (per definizione di testimone di esplorazione limitata), ilnumero di relazioni di equivalenza sui termini in T (in particolare la T -similarita) risulta anch’esso finito. E quindi possibile fissare un insieme distati {X1, . . . , Xm} (di A) con cardinalita massimale tale che tra essi non visiano stati T -simili.Indichiamo con ϕi il termine:∧

{s = t : s, t ∈ T ∧ V al(s, Xi) = V al(t,Xi)}∧

∧{s 6= t : s, t ∈ T ∧ V al(s, Xi) 6= V al(t,Xi)}

Dove, per maggior chiarezza, abbiamo utilizzato la notazione V al(t,X), alposto di quella usuale V alX(t), per indicare il valore assunto dal termine tnello stato X.Ricordiamo che il fatto che due stati X ed Y siano T -simili significa che iltermine s = t vale in X (interpretato valuta a true) se e solo se vale in Y .Il termine ϕi “afferma” che la relazione di equivalenza sui termini in T eesattamente la relazione di equivalenza EX e dunque valutera a true se esolo se interpretato in uno stato T -simile ad X.Il programma ASM R che stiamo cercando e dunque il seguente:

do-in-parallel

if ϕ1 then RX1

if ϕ2 then RX2

...

if ϕm then RXm

Ora, sia Y uno stato di A qualsiasi, la semantica dell’esecuzione di R e laseguente:

∆(R, Y ) = {RXi: ϕi = true in Y }.


Per come abbiamo costruito l’insieme {X1, . . . , Xm}, Y sara T -simile ad uncerto stato Xi e l’unica guardia che valutera a true sara quindi ϕi.Risulta:

∆(A, Y ) = ∆(RXi, Y ) = ∆(R, Y ),

che era esattamente cio che dovevamo mostrare.

Diamo una definizione di Abstract State Machine per poi mostrare il ri-sultato che lega la classe degli algoritmi sequenziali al formalismo delle ASM.

7 Definizione (Abstract State Machine). Una Abstract State MachineM definita sulla segnatura Σ e data da:

• un programma Π definito sulla segnatura Σ

• un insieme SM di strutture del primo ordine (definite sulla segnaturaΣ) chiuse rispetto ad isomorfismi ed alla funzione di transizione τΠ,definita a partire da Π

• un suo sottoinsieme IM

• la funzione τM, restrizione di τΠ ad SM

Non e difficile mostrare che una ASM soddisfa i tre postulati: secondo laDefinizione 6, risulta essere un algoritmo.

Ricordiamo che la Definizione 1 fornisce una nozione di equivalenza traalgoritmi dal punto di vista comportamentale. E questa l’equivalenza di cuisi parla nel teorema seguente.

Teorema di caratterizzazione. Per ogni algoritmo sequenziale A esisteuna Abstract State Machine M equivalente. In particolare, M simula Apasso-passo.

Dimostrazione. Per il lemma precedente abbiamo che esiste un programmaASM Π tale che ∆(Π, X) = ∆(A, X), per ogni stato X di A. Per terminarela dimostrazione basta porre SM = SA e IM = IA.

2.3.3 Alcune considerazioni

Prima di procedere alla trattazione delle estensioni del formalismo delle Ab-stract State Machines e bene mettere a fuoco alcune idee per comprenderemeglio il significato di cio che stiamo facendo.


Rappresentabilita degli stati Uno dei punti cruciali di questo approccioe dato dal fatto che si sceglie di astrarre dalla rappresentabilita degli stati diun algoritmo. Nello studio dei requisiti, infatti, non vi e traccia di imposizionisu come gli stati possano/debbano essere rappresentati: potremmo non esse-re in grado di fornirne una caratterizzazione simbolica finita semplicementeperche abbiamo a che fare con strutture naturalmente infinite. Pensiamo, adesempio, di avere un programma P in cui si usa la costante Pi e consideriamolo stato S in cui l’interpretazione di tale nome sia proprio il numero π la cuirappresentazione decimale richiederebbe una espansione infinita di cifre: eovvio che tale valore non e rappresentabile in termini “finitistici” e da cio nederiva che l’intero stato S non puo avere una rappresentazione finita. Pos-siamo affermare che S non e implementabile10, eppure esso viene accettatocome stato perfettamente valido.In questo contesto basta che uno stato S fornisca un’interpretazione per ogninome presente nel programma P affinche possiamo applicare P ad S.E proprio a questo aspetto che fa riferimento il termine Abstract State delnome: gli stati sono strutture matematiche astratte.L’idea fondamentale e che e sufficiente trovare una rappresentazione simboli-ca finita della funzione di transizione per caratterizzare l’algoritmo, in quantoessa “descrive” il comportamento di un algoritmo al di la dei dati su cui essoopera. In quest’ottica il requisito essenziale e quello dell’Esplorazione Limita-ta perche ci dice che basta un insieme finito di termini per distinguere insiemidi aggiornamenti diversi: questo ci permette di caratterizzare la transizioneda uno stato al successivo.

Rappresentabilita della funzione di transizione Un altro problemariguarda le funzioni coinvolte in un programma ASM: in effetti non si par-la da nessuna parte di calcolabilita. Il formalismo delle ASM ci consente apriori di interpretare il nome sqr anche come la funzione che dato un numeronaturale n, che e il codice di una Macchina di Turing M, ed una stringa iche rappresenta un possibile input, restituisce il valore 1 se M con input isi arresta e 0 altrimenti; tale funzione sarebbe quindi in grado di risolvere ilProblema della Terminazione, indecidibile!A prima vista puo risultare sconcertante che tra le funzioni definibili in questocontesto siano ammessi anche simili “mostri” ma questo fatto apparentemen-te bizzarro si inscrive nell’impostazione generale di questo approccio che equella di lasciare il massimo grado di liberta: per la descrizione ad alto livellodi certi sistemi puo tornare utile una simile liberta di astrazione rispetto a

10Nel senso che non siamo in grado di costruire alcuna macchina (fisica) in grado dicontenere una struttura dati che fornisca una rappresentazione precisa di tale stato.


problematiche implementative.Volendo, potremmo imporre il vincolo che tutte le funzioni di un programmaASM debbano essere calcolabili; ad ogni modo discuteremo piu in dettagliodella ragionevolezza di questo aspetto nel capitolo 3 in cui metteremo a con-fronto i due modelli, quello operazionale e quello denotazionale, analizzandopro e contro di ciascuno di essi.

Potere espressivo Dopo il modello operazionale della Macchina di Turingnumerosi studiosi si sono posti il problema se fosse possibile “lavorare” conmacchine piu potenti ed i vantaggi che questo avrebbbe apportato. Nel corsodegli anni sono quindi state proposte macchine dotate di istruzioni base viavia piu complesse, tra di esse ricordiamo alcune tra le piu significative:

1. Macchina di Kolmogorov-Uspensky - 1953 [29]Sostanzialmente si tratta di una MdT in cui il nastro viene sostituitoda un grafo che, essendo riconfigurabile, fornisce una maggiore liberta;in particolare lavoriamo con un grafo diretto, simmetrico, con un nu-mero massimo fissato di archi entranti ed uscenti. A priori non e deltutto chiaro come si sia giunti a questo modello; un’ipotesi plausibilee che Kolmogorov ed Uspensky abbiano pensato alla gestione dell’in-formazione, nel senso che ogni arco uscente dal nodo A ed entrantenel nodo B sta a significare che il nodo A possiede delle informazionisu B. Questo spiegherebbe anche il limite fissato sul numero di archi,dato che la quantita d’informazione contenuta da ciascun nodo deveper forza essere limitata.La Macchina di Kolmogorov-Uspensky e una prima generalizzazionedelle MdT ed anche se le funzioni calcolabili da questa macchina sonoesattamente quelle calcolabili da una MdT, questo rappresenta il primotentativo di dare una definizione formale del concetto di algoritmo. Aquesto proposito Gurevich in [8] cita il seguente passaggio significativo,tratto da [29]:

Ci sembra plausibile che un procedimento algoritmico qual-siasi soddisfi la nostra definizione di algoritmo. Vorremmosottolineare che non stiamo parlando di una riduzione di unalgoritmo qualsiasi ad un algoritmo nel senso della nostra de-finizione ma che stiamo dicendo che ogni11 algoritmo soddisfala definizione proposta.

11Corsivo aggiunto dal traduttore.


Grigoriev, in [20], ha dimostrato che le MdT non possono simula-re in tempo reale12 la Macchina di Kolmogorov-Uspensky e quindi,quest’ultima puo essere considerata, in questo senso, piu potente.

2. Storage Modification Machine di Schonhage - 1970 [38] e [39]Rilassando una delle restrizioni precedenti, e cioe permettendo un nu-mero arbitrario di archi entranti, otteniamo un’ulteriore generalizzazio-ne; per comprendere il significato di questo e utile riprendere l’analogiaadoperata per spiegare il modello di Kolmogorov-Uspensky: bisognaconsiderare gli archi dal punto di vista della quantita di informazione.Abbiamo detto che gli archi uscenti da un certo nodo A rappresentanoinformazioni che tale nodo possiede riguardo ai nodi “vicini”, svilup-pando il ragionamento gli archi entranti in A rappresentano informa-zioni che i nodi “vicini” possiedono su A. Ora e chiaro che man manoche la computazione procede e vengono aggiunti nuovi nodi e ragione-vole pensare che essi possano contere informazioni sui nodi vecchi: perquesto motivo, a priori, non possiamo sapere quanti nodi conterrannoinformazioni su (“punteranno” a) un dato nodo.Quest’ultima osservazione ci permette di vedere tale macchina anchecome una macchina a puntatori ed in effetti il nome suggerito da Knuthche l’aveva proposto indipendentemente come modello di computazionein [16] e quello di Pointer Machine; purtroppo in letteratura c’e un po’di confusione e di anarchia riguardo a questo nome e di conseguenzanon e chiaro che cosa sia una Pointer Machine.

3. Macchina di Blum, Shub e Smale - 1989 [30]Un altro modello interessante e molto potente e rappresentato da unamacchina astratta pensata per sviluppare la teoria della calcolabilitasu di una struttura algebrica di anello R qualsiasi13. Nell’articolo inquestione in particolare viene sviluppata la teoria della calcolabilitasull’anello R dei numeri reali; questo approccio, a detta degli autori:

12Concetto introdotto da Schonhage in [39]. Diciamo che una macchina M ′ simulaun’altra macchina M in tempo reale, denotato con M ; M ′, se esiste una costante c taleche per ogni sequenza di input x, vale: se x fa sı che M legga un simbolo dall’input oche stampi un simbolo di output o che si fermi agli istanti 0 = t0 < t1 < · · · < tn, allorax fa sı che M ′ si comporti allo stesso modo agli istanti 0 = t0

′ < t1′ < · · · < tn

′ dovetj′ − tj−1

′ ≤ c(tj − tj−1) per 1 ≤ j ≤ n. A livello di classi di macchineM,M′,M;M′

significa che per ogni M ∈M esiste M ′ ∈M′ tale che M ; M ′.13Naturalmente se R e Z, l’anello degli interi, otteniamo esattamente le stesse entita

della teoria della calcolabilita classica: le funzioni calcolabili sono quelle classiche, gliinsiemi R.E. sono quelli classici, ecc. . .


fornisce un’impostazione naturale per studiare le questionifondazionali riguardanti algoritmi in analisi numerica.

Inoltre:

C’e un altro vantaggio nello sviluppare una teoria delle mac-chine su di un anello. Questo ci costringe ad adottare unapproccio piu algebrico, piu vicino alla matematica classicarispetto all’approccio derivato dalla logica.

Per rendersi conto di quanto sia potente questo modello basta notareche in esso lavoriamo direttamente con numeri reali (a rappresentazio-ne, in generale, infinita) e che la moltiplicazione tra due numeri nondipende dalla loro dimensione!

Abbiamo quindi una gerarchia di modelli di computazione via via piu potentima il problema essenziale rimane: comunque sia, il livello di astrazione, perquanto alto, e, ad ogni modo, fissato a priori una volta per tutte. Il modelloproposto da Gurevich rispetto a questo e rivoluzionario perche fa della pos-sibilita di scegliere, a piacimento, il livello di astrazione piu adatto, uno deipunti fondamentali: quello delle Abstract State Machine supera i modelli dicomputazione classici in quanto non c’e un livello di astrazione imposto dalmodello stesso.

Indipendenza dalla rappresentazione dei dati Un’altra caratteristicafondamentale e che, dandoci la liberta di fissare a piacere il livello di astra-zione che vogliamo considerare, questo modello ci permette di lavorare divolta in volta con i dati di cui necessitiamo indipendentemente dalla lororappresentazione. Dover specificare quest’ultima significherebbe addentrarsiin dettagli implementativi (per quanto ad alto livello) che potrebbero non es-sere significativi per l’algoritmo che stiamo considerando. Un facile esempioe dato dagli algoritmi che operano sui grafi; il seguente verifica se un grafoha punti isolati:

if ∀x∃y : Edge(x, y) thenOutput := false

elseOutput := true

end if

Il fatto se abbiamo scelto la rappresentazione dei grafi con matrici di adia-cenza o con liste non ci dice, a questo livello, nulla in piu sull’algoritmo in


se. Questo aspetto ci offre quindi il vantaggio di poter “ignorare” tutto cioche va oltre il livello di astrazione di quello che stiamo considerando.

2.4 Estensioni delle Abstract State Machines

In questa sezione vogliamo trattare le estensioni base del formalismo delleASM deterministico-sequenziali precedentemente presentato.Prima di tutto prenderemo in esame la gestione del non-determinismo, perpoi occuparci del passaggio dal modello sequenziale ai paradigmi parallelo edistribuito. In ciascuno di questi casi ci limiteremo a fornire un’intuizionedi quali siano le problematiche da affrontare e delle soluzioni proposte senzaentrare in dettaglio poiche la trattazione formale delle estensioni del modellosequenziale delle ASM esula dagli scopi di questo studio. E importante peronotare che l’approccio di fondo utilizzato nella dimostrazione del Teorema diCaratterizzazione di tutte le estensioni e lo stesso: esse si basano su alcuniprincipi base che servono a formalizzare la tipologia di algoritmo che si staanalizzando.

2.4.1 Abstract State Machines non-deterministiche

In molte situazioni (il piu delle volte si tratta di descrizioni ad alto livello diun certo algoritmo) risulta utile sfruttare il non-determinismo.Nell’algoritmo che verifica se tutti i nodi di un grafo sono connessi, ad esem-pio, si sceglie un nodo qualsiasi di partenza per poi esaminare il resto: aquesto livello la scelta da operare e un esempio di comportamento non-deterministico in quanto non importa da che nodo partiamo e, proprio perquesto motivo, l’algoritmo non fornisce alcun criterio che indichi quale nodoscegliere.Vorremmo, quindi, poter gestire/modellare un comportamento di questo ti-po; abbiamo due modi per farlo: uno in cui la scelta viene operata implici-tamente e l’altro in cui essa viene operata esplicitamente.

Gestione implicita - ambiente interattivo

L’idea e che nel momento in cui dobbiamo effettuare una scelta di questo tipo(in mancanza di criteri) facciamo appello ad un “agente” esterno, rappresen-tato dal classico tiro di dado o lancio di moneta, che operi la scelta al postonostro. Chi gioca il ruolo dell’agente esterno? L’ambiente o per meglio dire

2.4. ESTENSIONI DELLE ABSTRACT STATE MACHINES 43

alcune funzioni gestite dall’ambiente. Per formalizzare il discorso introducia-mo una tassonomia delle funzioni del nostro ambiente di lavoro: abbiamo giavisto che i nomi di funzione si dividono in statici e dinamici a seconda chela loro interpretazione possa cambiare o meno; consideriamo ora solamentele funzioni dinamiche14, esse si suddividono in interne, esterne e condivise aseconda che possano essere modificate solo dal programma, solo dall’ambien-te oppure da entrambi. Di seguito riportiamo una tabella che riassume leproprieta di ciascun tipo di funzione utilizzando la classica terminologia chesi usa per le variabili in programmazione: RO significa Read-Only, il valoredella funzione puo essere solamente letto, mentre RW sta per Read-Writable,il valore puo anche essere modificato.

statiche interne esterne condiviseprogramma RO RW RO RWambiente RO RO RW RW

Nel caso in cui l’ambiente entri in gioco interagendo con l’algoritmo che stia-mo considerando si parla di ambiente interattivo. Un altro esempio classicodi questo tipo di ambiente e quello dato dagli algoritmi che si aspettano deidati in input: possiamo pensare che questi ultimi vengano “caricati” attra-verso apposite funzioni gestite, per l’appunto, dall’ambiente15. In un certosenso e come se, ogni volta che ce ne fosse bisogno, interrogassimo un oraco-lo che ci fornisce un valore o che opera una scelta che serve per proseguirel’esecuzione.

Gestione esplicita

A volte, invece, e preferibile rendere esplicite le scelte, operate cioe dall’al-goritmo stesso. Per consentire cio bisogna cambiare alcuni concetti base eintrodurre un nuovo costrutto sintattico che rispecchi questo tipo di non-determinismo.Come succede ogni volta che passiamo dal determinismo al non-determinismo,le funzioni diventano relazioni: nel nostro caso, non lavoreremo piu con unafunzione di transizione ma bensı con una relazione di transizione, binaria, τA

definita sull’insieme degli stati SA. Dobbiamo inoltre modificare il Postulatodegli Stati Astratti, le ultime due condizioni vanno riformulate nel seguentemodo:

14Le funzioni corrispondenti a nomi di funzione dinamici.15Possiamo anche considerare ambienti interattivi autorizzati ad agire anche sugli stati,

modificando l’esecuzione di un algoritmo (si parla allora di esecuzioni interattive) ma peri nostri scopi questo aspetto non e significativo e quindi non lo approfondiremo.


• se (X, X ′) ∈ τA allora X ed X ′ hanno lo stesso insieme base

• SA ed IA sono chiusi rispetto ad ismorfismi. Inoltre se ζ e un isomor-fismo tra uno stato X ed uno stato Y , allora per ogni stato X ′ taleche (X, X ′) ∈ τA, esiste uno stato Y ′ tale che (Y, Y ′) ∈ τA e ζ e unisomorfismo tra X ′ ed Y ′

A livello sintattico, alle regole gia presentate dobbiamo aggiungere il costrut-to corrispondente all’azione da scegliere; in particolare abbiamo due tipi discelta: quella tra un insieme di elementi e quella tra un insieme di regole. Icostrutti corrispondenti sono i seguenti:

• choose v : g(v)R(v)

endchoose

La guardia g(v) e un termine booleano, tipicamente si tratta dell’ap-partenenza ad un certo insieme (universo) e R(v) e una regola (il corpodel costrutto). Ad esempio la scelta arbitraria di un nodo di un grafosi puo fare con la regola:

choose v : Node(v)Source := v

endchoose

• choose among

R1

R2

· · ·Rk

endchoose

dove k e un numero naturale fissato. In questo caso stiamo prendendoin esame algoritmi con un grado limitato di non-determinismo (c’e unlimite superiore al numero di regole tra le quali scegliere)16. La seman-tica e quella di scegliere arbitrariamente, ed eseguire, una delle k regoleed e ben fondata perche, a partire dai postulati modificati, si dimostrache per ogni algoritmo non-deterministico A esiste un certo valore ktale che per ogni stato X ∈ SA, l’insieme {Y : (X, Y ) ∈ τA} ha almassimo k elementi.

16Il caso di non-determinismo con grado illimitato puo essere trattato combinando questaestensione con la seguente, che riguarda gli algoritmi paralleli.


2.4.2 Abstract State Machines parallele

Prima di tutto e bene chiarire che tipo di parallelismo s’intende trattare. Nelpresentare le ASM deterministico-sequenziali abbiamo incontrato la regola:

do-in-parallel

R1

R2...

Rk

enddo-in-parallel

che dato un numero finito k di regole, le esegue simultaneamente (eseguecioe gli aggiornamenti corrispondenti). Il nostro formalismo, quindi, esibiscegia un tipo di parallelismo, soltanto che il grado di parallelismo e limitato.In questa sezione vogliamo estendere il modello base ad un grado di paralle-lismo potenzialmente illimitato17. E necessaria un’ulteriore precisazione: glialgoritmi che vogliamo poter modellare sono algoritmi per i quali il numerodi linee di esecuzione e illimitato mentre il numero di “azioni” corrispondentia ciascuna di esse e invece limitato. Per chiarire meglio le cose diamo unesempio di un algoritmo di questo tipo:

1. Per ogni nodo x esegui:

se ogni nodo y con un arco diretto in x e segnato,

allora segna anche x.

2. Ripeti il passo 1 finche vengono segnati nuovi nodi.

che applicato ad un grafo orientato G individua la parte ben fondata di G.Notiamo che non sappiamo, a priori, quanti nodi fanno parte del grafo Ge quindi non possiamo dire quante linee di esecuzione verranno “generate”,tuttavia il numero di “azioni” in ciascuna di esse e limitato.Per gestire questo tipo di parallelismo dobbiamo estendere il nostro modello:

• Prima di tutto bisogna ampliare l’insieme dei termini anche a terminidel primo ordine. Siano v una variabile, g(v) ed s(v) termini booleani,allora:(∀v : g(v))s(v), (∃v : g(v))s(v)sono termini booleani.Cosı facendo si possono introdurre dei problemi dovuti alla non calco-labilita di certe funzioni: potremmo non essere in grado di stabilire seuna certa proprieta e verificata per ogni elemento di un insieme oppu-

17Nel senso che non c’e un limite superiore fissato a priori.


re se esiste una soluzione di una certa equazione. Come al solito e ilprogrammatore a dover assicurare la calcolabilita e/o trattabilita dellefunzioni coinvolte.

• Sia v una variabile, sia g(v) un termine booleano e sia R(v) una regola,allora la seguente:

do-for-all v : g(v)R(v)

enddo-for-all

e una regola. Come al solito, in mancanza di possibili ambiguita omet-teremo il terminatore enddo-for-all.

Il seguente programma ASM “implementa” l’algoritmo di cui sopra:do-for-all x ∈ Nodes

if {y : y ∈ Nodes : Edge(y, x) ∧ ¬(M(y))} = ∅then M(x) := true

Nel 2003, in [7], e stato dimostrato un risultato analogo al Teorema di ca-ratterizzazione degli algoritmi sequenziali: anche questo si basa su alcunipostulati/principi base. Ovviamente il Postulato dell’Esplorazione limitata,che caratterizzava la classe degli algoritmi sequenziali, va abbandonato.

2.4.3 Abstract State Machines distribuite

Come gia fatto nella sezione precedente, prima di ogni cosa chiariamo chetipo di algoritmi distribuiti vogliamo prendere in esame: focalizzeremo lanostra attenzione sugli algoritmi distribuiti in cui gli agenti di calcolo sonodeterministici e possono interagire con l’ambiente solo tra un passo e l’altrodi computazione18. Vedremo che l’estensione del modello base a questo tipodi algoritmi risulta sufficiente per la presente trattazione.

18Questo tipo di interazione prende il nome di inter-step per distinguerlo da intra-stepin cui l’interazione tra gli agenti di calcolo e l’ambiente puo avvenire anche durante lostesso passo. La formalizzazione del secondo tipo di interazione e stata analizzata in [9]ed altri articoli ulteriori [5] e [6].


Definizione base

Dal momento che ci sono vari agenti che, potenzialmente, eseguono lo stessoprogramma19 in contemporanea, abbiamo bisogno di un modo che permettaa ciascun agente di individuare se stesso in mezzo a tutti quelli in esecuzione.Aggiungiamo quindi al vocabolario base, un nome di funzione ad arieta 0,Self, che verra interpretato in modo diverso da ciascun agente: l’agente ainterpretera Self con a.

Una Abstract State Machine distribuita A e individuata da:

• Un insieme finito di programmi πν , detti moduli20. Ciascun moduloe identificato da un’etichetta, il nome del modulo, che e un nome difunzione statico ad arieta 0.

• Un vocabolario Υ = Fun(A) che comprende tutti i simboli in Fun(πν)ma non contiene Self. Υ contiene inoltre un nome di funzione unarioMod.

• Un insieme di Υ-strutture, gli stati iniziali di A, che soddisfano leseguenti condizioni:

1. A nomi di modulo diversi corrispondono elementi diversi.

2. C’e un numero finito di elementi a tali che, fissato un nome dimodulo ν, Mod(a) = ν.

Ogni stato S, definito a partire dal vocabolario Fun(A), per essere “le-gale” deve soddisfare le condizioni 1 e 2 di cui sopra. Un elemento a e unagente su S se esiste un nome di modulo ν tale che S |= Mod(a) = ν; ilprogramma corrispondente ad a, Prog(a), e πν .L’esecuzione di una mossa, da parte di un agente a, nello stato S, signi-fica eseguire il programma Prog(a) sullo stato locale rappresentato dallostato globale “visto” da a; tale insieme viene denotato, per l’appunto, conV iewa(S) e formalmente si tratta della restrizione di S al vocabolario Fun(a)dove Self viene interpretato con a. L’insieme degli aggiornamenti generati eil seguente:

∆(a, S) =def ∆(Prog(a), V iewa(S)).

Dobbiamo ora definire che cosa sia l’esecuzione di una ASM distribuita.Abbiamo due tipi di esecuzioni: esecuzioni sequenziali ed esecuzioni con unordine parziale.

19In seguito lo chiameremo modulo.20Ciascuno di essi e un programma che va pensato eseguito da un agente..


Esecuzioni sequenziali

Una esecuzione sequenziale pura di una ASM distribuita e una sequenza distati in cui, a partire da uno stato iniziale S0, ogni stato Si+1 e ottenutodall’esecuzione di una mossa da parte di un agente nello stato (precedente)Si.Abbiamo spiegato che cosa voglia dire eseguire una mossa, ci resta da chiari-re che cosa intendiamo col termine pura: l’esecuzione, la successione di stati,e completamente determinata dalla ASM, non c’e alcun intervento da par-te dell’ambiente. E bene specificare inoltre che anche in questo caso sonoammesse successioni infinite di stati.

Esecuzioni con un ordine parziale

Una esecuzione con un ordine parziale pura di una ASM distribuita A e unatripla (M, A, σ) dove:

• (M,≤) e un insieme parzialmente ordinato (abbreviato poset), gli ele-menti di M sono le mosse effettuate dagli agenti durante l’esecuzione.

• A e una funzione che ad ogni mossa x in M associa un elemento A(x)dell’insieme base degli stati della ASM che stiamo considerando. A(x)rappresenta l’agente che ha effettuato la mossa x.

• σ e una funzione che ad ogni segmento iniziale21 finito X di M asso-cia uno stato della ASM, denotato con σ(X). σ(X) e lo stato in cuiarriviamo dopo che sono state effettuate tutte le mosse in X.

L’ordine parziale ≤ si riferisce all’ordine temporale di esecuzione: y < xsignifica che la mossa y deve terminare prima che abbia inizio x.Gli elementi che costituiscono la tripla devono inoltre soddisfare le seguenticondizioni:

• Per ogni x ∈ M , l’insieme {y ∈ M : y ≤ x} e finito. Alla luce dellaspiegazione della relazione d’ordine e chiaro che il numero delle mosseche precedono una data mossa x dev’essere finito.

• Per ogni a, il sottoinsieme di M , {x ∈ M : A(x) = a}, e totalmenteordinato (rispetto alla relazione d’ordine ≤). Tale insieme rappresental’insieme delle mosse effettuate da un singolo agente: e chiaro che essedevono avvenire in un ordine ben preciso, squenzialmente.

21Un segmento iniziale X di un insieme parzialmente ordinato O e un sottoinsieme diO chiuso verso il basso, vale cioe la seguente proprieta: se x ∈ O e y < x, allora y ∈ O.


• σ(∅) e un stato iniziale.

• Sia X un segmento iniziale finito di M , sia x un elemento massimale22

di X e sia Y = X r {x}, allora A(x) e un agente nello stato σ(Y ) eσ(X) e ottenuto da σ(Y ) effettuando la mossa x.

Il significato dell’ultima condizione puo risultare poco chiaro. L’idea e che,come gia detto, σ(X) dev’essere lo stato che raggiungiamo effettuando tuttele mosse in X disposte in qualsivoglia ordine a patto pero che venga rispettatol’ordinamento parziale ≤. Ogni elemento massimale x (di X) puo costituire“l’ultima mossa” di X: prima di effettuare questa mossa lo stato in cui citroviamo e dato da σ(Y ) dove Y = X r {x}. Per questo motivo dobbiamoassicurarci che A(x) sia un agente in σ(Y ), la cui mossa ci porta in σ(X).In sostanza una esecuzione puo essere vista come la parte comune delle di-verse storie di esecuzione, corrispondenti a tutti i possibili modi di ordi-nare temporalmente, in modo coerente, le mosse non confrontabili rispettoall’ordinamento parziale ≤.

Esecuzioni sequenziali come esecuzioni con un ordine parziale

Adesso mettiamo in relazione i due tipi di esecuzione precedentemente espo-sti. E sufficientemente chiaro che il secondo tipo di esecuzione e piu generalee ci aspettiamo quindi che il primo possa essere visto come caso particolaredi quest’ultimo. In effetti, abbiamo che:

1. Nel caso in cui l’ordinamento parziale sia anche totale, e facile verificareche le due nozioni coincidono.

2. E possibile trasformare un’esecuzione con ordine parziale in una se-quenziale, linearizzando l’ordine parziale ≤, trasformando cioe l’ordineparziale in un ordine totale. Per far cio, sostanzialmente, basta prende-re elementi a due a due non confrontabili rispetto all’ordine ≤ e imporretra di essi un ordine arbitrario23. Volendo formalizzare quest’intuizio-ne si tratta di estendere/raffinare la relazione d’ordine ≤, ottenendoun’altra relazione d’ordine ≤′ tale che ∀x, y : x ≤ y ⇒ x ≤′ y. Eevidente che ogni segmento iniziale rispetto a ≤′ e anche segmento ini-ziale rispetto a ≤. Partendo da un’esecuzione (M, A, σ), considerandolo stesso insieme M e la stessa funzione A, rimpiazzando l’ordine ≤

22Un elemento a di un insieme parzialmente ordinato (S,≤) si dice elemento massimaledi S se l’unico elemento x ∈ S tale che a ≤ x, e a stesso.

23Naturalmente bisogna sempre sincerarsi che questo nuovo ordine sia coerente, nel sensoche se due elementi y e z tali che y < z, sono entrambi non confrontabili con l’elementox, non possiamo porre x < y e z < x!


con ≤′ e restringendo il dominio di σ all’insieme dei segmenti inizialidi (M,≤′), ammesso che, per ogni x, l’insieme {y ∈ M : y ≤′ x} siafinito, otteniamo una nuova esecuzione. Se ≤′ e un’estensione linearedi ≤ con segmenti iniziali finiti, allora quest’esecuzione e sequenziale.

Teoremi di caratterizzazione

Negli ultimi anni (alcuni articoli sono ancora in via di pubblicazione) sonostati dimostrati dei Teoremi di caratterizzazione anche per questa classe dialgoritmi. Abbiamo utilizzato il termine vago “dei” perche a tutt’oggi none ben chiaro che cosa sia un algoritmo distribuito nella sua massima genera-lita, per numerose tipologie di algoritmi distribuiti sono stati dimostrati deiteoremi analoghi a quello esposto nella sezione 2.3.2.

2.5 Successi delle Abstract State Machines

Abbiamo detto che il formalismo delle Abstract State Machines, grazie allaliberta di scegliere il livello di astrazione fornita, costituisce uno strumentomolto potente. A supporto di questa affermazione, riportiamo alcune tra leapplicazioni in cui sono state utilizzate le ASM:

• Linguaggi di programmazione Uno dei primi ambiti in cui si sono appli-cate le ASM con successo e quello della trattazione formale dei linguaggidi programmazione, in particolare si trattava di fornirne una semanticatramite questo formalismo. Tra i linguaggi che sono stati oggetto distudio sono: C, C++, Java, Prolog, Occam, VHDL. Di particolare suc-cesso e risultata la formalizzazione della semantica dinamica del Prolog,che e stata poi estesa ad una trattazione dell’intero linguaggio; questatrattazione e poi stata adottata dall’ISO come definizione standard delProlog.

• Protocolli Il protocollo di rete Kermit per il trasferimento di file ed ilprotocollo, noto come Bakery algorithm, sviluppato da L. Lamport, pergestire la mutua esclusione sono alcuni dei protocolli modellati tramitele ASM.

• Architettura e macchine virtuali Uno dei primi studi mirava a dimostra-re la correttezza della gestione degli hazard nel meccanismo di pipeli-neing della macchina DLX 24. Tra le macchine virtuali invece citiamoil lavoro svolto sulla PVM, Parallel Virtual Machine.

24Macchina RISC sviluppata da Patterson ed Hennessy.

2.5. SUCCESSI DELLE ABSTRACT STATE MACHINES 51

• Applicazioni industriali Nel corso degli anni si e riscontrato che le ASMrappresentano un metodo formale che puo essere anche applicato inambito industriale, esterno a quello accademico. Le applicazioni inquesto ambito sono oramai numerose, ne citiamo un paio che mostranoche le ASM si sono dimostrate all’altezza della produzione di software alivello industriale. Prima di tutto, presso la Siemens e stato sviluppatoil progetto FALKO per la gestione delle ferrovie 25. In secondo luogo, apartire dal 1998 Gurevich lavora alla Microsoft in un gruppo di ricercache si prefigge di incorporare le ASM nell’ambiente .NET e che hasviluppato il linguaggio di programmazione AsmL [3].

Per una lista completa si veda la coppia di articoli [11] e [12], quest’ultimocontiene anche una bibliografia commentata degli articoli di ricerca sulleASM.

25A partire dal quale e stato generato il programma che gestisce il Vienna SubwayOperator.

Capitolo 3

Approccio denotazionale

3.1 Presentazione

Come anticipato, in questa sezione presenteremo l’approccio, alla problema-tica della definizione formale di algoritmo, adottato da Yiannis N. Moscho-vakis e sviluppato nel corso degli anni e di numerosi articoli a partire dal19841, anno di pubblicazione di “Abstract recursion as a foundation of thetheory of algorithms” [32]. Abbiamo utilizzato l’aggettivo denotazionale perdescrivere il suo approccio e prima di incominciare con la sua trattazione ebene chiarire che tale aggettivo e qui da intendersi in senso ampio; in genereil termine in questione si riferisce alla semantica denotazionale, sviluppatada Scott e Strachey a partire da [40], in cui i costrutti di un linguaggio diprogrammazione vengono interpretati come oggetti appartenenti a spazi difunzioni (come funzioni quindi definite su particolari domini). Come vedremonella sezione 3.2.3 gli strumenti impiegati in questa semantica si basano sudi un teorema di punto fisso per un determinato tipo di operatore che sonogli stessi utilizzati da Moschovakis per sviluppare la sua formalizzazione delconcetto di algoritmo: per questo motivo ci siamo sentiti autorizzati ad usarel’aggettivo denotazionale anche per l’approccio adottato da Moschovakis.Abbiamo visto una caratteristica che accomuna il lavoro di Scott e Strachey equello di Moschovakis, per non trarre in inganno il lettore e altresı importantesottolineare una differenza sostanziale tra i due: la semantica sviluppata daScott riguarda l’aspetto estensionale, che abbiamo visto essere troppo gene-rico per caratterizzare gli algoritmi2. Moschovakis cerca quindi di sviluppare

1E interessante notare che Moschovakis e Gurevich iniziano ad interessarsi al problemanello stesso periodo!

2Riprendendo il nostro esempio guida, si dice che i due algoritmi Mergesort e Quicksort(e di fatti tutti gli algoritmi di ordinamento) denotano la medesima funzione.

53

54 CAPITOLO 3. APPROCCIO DENOTAZIONALE

una semantica adeguata che tenga conto degli aspetti intensionali degli algo-ritmi e che prendera dunque il nome di semantica intensionale.

Nella sezione 3.2 introdurremo informalmente le tematiche principali e lelinee guida di questo approccio mentre nella sezioni 3.3 e 3.4 entreremo nelmerito di un particolare linguaggio formale la cui semantica intensionale ci“dira” che cosa sono gli algoritmi.

3.2 Macchine astratte e definizioni ricorsive

3.2.1 Mergesort

Ricordiamo che, dato un alfabeto L con una relazione di ordine totale su diesso definita, denotata con ≤, e utilizzando L∗ per indicare l’insieme di tuttele stringhe (sequenze finite di elementi di L) definite sull’alfabeto L, diciamoche una stringa u = 〈u0, . . . , un−1〉 e ordinata se vale: u0 ≤ u1 ≤ · · · ≤ un−1.Possiamo definire la funzione sort che data una stringa u ∈ L∗, ridispone glielementi di u in modo che la stringa risultante u′ sia ordinata:

sort(u) =df 〈uσ(0), . . . , uσ(n−1)〉, (3.1)

dove σ e una permutazione di {0, . . . , n− 1} tale che:

uσ(0) ≤ uσ(1) ≤ · · · ≤ uσ(n−1).

L’algoritmo Mergesort si basa sul fatto che la funzione sort soddisfa la se-guente equazione:

sort(u) =

{u se |u| ≤ 1,merge(sort(h1(u)), sort(h2(u))) altrimenti

(3.2)

dove: |u| indica la lunghezza di u; h1 ed h2 corrispondono alle due meta(sottostringhe) della stringa u e la funzione merge e cosı definita:

merge(u, v) =

u se v = ∅,v altrimenti, se u = ∅,〈u0〉 ∗merge(tail(u), v) altrimenti, se u0 ≤ v0,〈v0〉 ∗merge(u, tail(v)) altrimenti

(3.3)

dove: ∅ indica la stringa (sequenza) vuota; ∗ indica l’operatore di concate-nazione tra stringhe e la funzione tail e quella che, data una stringa (nonvuota), restituisce la stringa cui e stato rimosso il primo elemento.

3.2. MACCHINE ASTRATTE E DEFINIZIONI RICORSIVE 55

Di seguito dimostriamo alcune proprieta base che riguardano le funzionisort e merge e che ci permetteranno di dimostrare il risultato principale cheriguarda l’analisi del Mergesort e cioe che, data una stringa di lunghezza n,essa viene ordinata, secondo l’algoritmo presentato, effettuando non piu din · log2(n) confronti 3.

Lemma 1. La funzione individuata dall’equazione (3.3) e tale che se u e vsono due stringhe ordinate, allora vale:

merge(u, v) = sort(u ∗ v).

Dimostrazione. Procediamo per induzione sulla somma delle lunghezze delledue stringhe, |u| + |v|. Se una delle due stringhe e vuota, senza perdere digeneralita supponiamo si tratti di v, allora:

merge(u, ∅) = u = sort(u) = sort(u ∗ ∅).

Se entrambe le stringhe sono non vuote, supponiamo di essere nel caso u0 ≤v0, allora secondo l’equazione (3.3) abbiamo che:

merge(u, v) = 〈u0〉 ∗merge(tail(u), v),

da cui applicando l’ipotesi induttiva:

merge(tail(u), v) = sort(tail(u) ∗ v),

otteniamo il risultato desiderato. L’altro caso si risolve allo stesso modo.

Lemma 2. Per due stringhe qualsiasi u e v, abbiamo che, applicando il pro-cedimento specificato dall’equazione (3.3), la computazione di merge(u, v)non utilizza piu di |u|+ |v| − 1 confronti.

Dimostrazione. Sempre per induzione sulla somma delle lunghezze delle duestringhe: |u|+ |v|. Se una delle due stringhe e vuota, supponiamo sia v = ∅,allora, secondo l’equazione (3.3), otteniamo il risultato merge(u, ∅) = u senzaeffettuare confronti. Se, invece, entrambe le stringhe sono non vuote, alloraper calcolare merge(u, v) dobbiamo effettuare il confronto u0 ≤ v0 a cui andrapoi sommato il numero di confronti necessario per calcolare merge(tail(u), v)(oppure merge(u, tail(v)), a seconda dei casi) che, secondo l’ipotesi induttiva,e pari a |u|+ |v| − 2.

Lemma 3. La funzione sort, definita da (3.2), soddisfa la specifica datadall’equazione (3.1).

3Tenuto conto del fatto che tale misura rappresenta anche il limite inferiore della com-plessita computazionale per quanto riguarda la classe degli algoritmi di ordinamento cheoperano per solo confronto, questo ci dice che il Mergesort e asintoticamente ottimo.


Dimostrazione. Andiamo per casi. Se |u| ≤ 1, allora sort(u) = u che e,banalmente ordinata. Se invece siamo nel secondo caso di (3.2), applicandoil Lemma 1, otteniamo:

merge(sort(h1(u)), sort(h2(u))) = sort(sort(h1(u)), sort(h2(u))) = sort(u).

Lemma 4. Sia |u| = 2n, allora sort(u) puo essere calcolata secondo lo schemain equazione (3.2) utilizzando non piu di n · 2n confronti.

Dimostrazione. Per induzione su n. Per n = 0, la stringa u ha lunghez-za 20 = 1, e dall’equazione (3.2) otteniamo sort(u) = u, senza effettuareconfronti. Supponiamo ora che sia |u| = 2n+1, allora ciascuna delle due sot-tostringhe h1(u) e h2(u) ha lunghezza 2n e l’ipotesi induttiva ci garantisce chepossiamo calcolare sort(h1(u)) e sort(h2(u)) utilizzando non piu di n ·2n con-fronti ciascuna, che sommati danno luogo a n · 2n+1 confronti. Applicando ilLemma 2, abbiamo che e possibile calcolare merge(sort(h1(u)), sort(h2(u)))utilizzando non piu di 2n + 2n − 1 = 2n+1 − 1 confronti.In totale abbiamo quindi: n · 2n+1 + 2n+1 − 1 < (n + 1) · 2n+1.

Teorema 1. Data una stringa qualsiasi u di lunghezza n, e possibile calcolaresort(u), secondo lo schema in equazione (3.2), utilizzando non piu di

|u| · log2(|u|)

confronti, dove log2(m) =df “il piu piccolo n tale che m ≤ 2n”.

Dimostrazione. Basta applicare il Lemma 4 con |u| = n.

Discussione Tra i risultati precedentemente esposti, alcuni, in particolarei lemmi 1 e 3, si riferiscono alle funzioni sort e merge definite a partire dalleequazioni (3.2) e (3.3) mentre i restanti si riferiscono ai procedimenti di cal-colo che “sembrano” implicitamente specificati dalle suddette equazioni. Ecome se avessimo due livelli di interpretazione ed e interessante notare comeil passaggio dall’uno all’altro piano risulti naturale. Da un lato abbiamo laspecifica di una funzione, dall’altro la specifica di un procedimento per cal-colare in modo effettivo tale funzione. Letta come definizione matematicadi una funzione la (3.2) individua una funzione, di ordinamento su stringhe,che e la medesima individuata da qualsiasi procedimento di ordinamento.Dandone un’ulteriore interpretazione semantica, chiamiamola interpretazio-ne procedurale, potremmo invece leggere le due equazioni (3.2) e (3.3) nelseguente modo:


1. Per calcolare merge(u, v): se u = ∅, restituisci v; altrimenti se v = ∅,restituisci u; altrimenti se u0 ≤ v0, calcola z = merge(tail(u), v) erestituisci 〈u0〉 ∗ z; altrimenti calcola z = merge(u, tail(v)) e restituisci〈v0〉 ∗ z.

2. Per ordinare una stringa u: effettua il controllo |u| ≤ 1, se e vero resti-tuisci la stringa u, altrimenti ordina separatamente le due meta (sot-tostringhe) di u e poi fanne il merge seguendo la procedura presentatadallo schema precedente.

Chiamiamo la specifica di questo procedimento P , per procedura. Ora epossibile tradurre tale procedimento in un programma P di un qualsiasi lin-guaggio di programmazione che supporti la ricorsione; se adottassimo unlinguaggio a paradigma funzionale, come il Lisp, tale traduzione consiste-rebbe praticamente nel ricopiare la (3.2) e la (3.3) specificando i vari casitramite il costrutto cond. Che rapporto c’e’ tra P e P? Siano P1 e P2 latraduzione in due linguaggi di programmazione diversi, diciamo in Lisp ed inC, di P ; che rapporto c’e’ tra P1 e P2? Ponendo queste domande a qualsiasiinformatico, otterremmo le risposte attese: per quanto riguarda la prima “Pimplementa l’algoritmo P” e per quanto riguarda la seconda “P1 e P2 sonodue implementazioni dell’algoritmo P”. Ma che cosa significa implementare?Che cos’e una implementazione? E che cos’e in effetti un algoritmo? Qualisono le caratteristiche che un “oggetto” deve soddisfare per qualificarsi comealgoritmo? Il fatto che si possa discutere informalmente di questi concetti,perche intuitivamente chiari, rischia di offuscare la necessita di una tratta-zione formale di questi concetti che costituiscono alcuni fra i concetti basedell’informatica.

3.2.2 Macchine astratte

Alla domanda fondazionale “che cos’e un algoritmo?” un informatico teoricopotrebbe rispondere che e cio che viene calcolato da una Macchina di Turingma come abbiamo gia visto questo modello si limita all’estensionalita deglialgoritmi, inoltre ci sono degli aspetti importanti della complessita del pro-cedimento di calcolo che non vengono “catturati” da questo modello: bastipansare che la codifica binaria dell’input puo rendere il procedimento note-volmente piu veloce e che se utilizziamo un ulteriore nastro possiamo avereun miglioramento quadratico nel tempo di computazione [31]. Per discute-re in termini di massima generalita, consideriamo il modello piu generale dimacchina astratta:

Definizione (Iteratore) 1. Dati due insiemi X e W , un iteratore


φ : X W

e una quintupla (input, S, σ, T, output), dove:

1. S e l’insieme (non vuoto) degli stati di φ;

2. input : X → W e la funzione che “gestisce” l’input;

3. σ : S → S e la funzione di transizione di φ;

4. T ⊆ S e l’insieme degli stati di terminazione di φ e per ogni s ∈ T :σ(s) = s;

5. output : T → W e la funzione che “gestisce” l’output.

Si tratta sostanzialmente di un sistema di transizione in cui esplicitiamola gestione dell’input/output.

Una computazione di φ per un dato x ∈ X e costituita dalla sequenza distati {sn(x)}n∈N definita nel seguente modo:

s0(x) = input(x), sn+1(x) =

{sn(x) se sn(x) ∈ T,σ(sn(x)) altrimenti

La lunghezza di una computazione per l’input x dato (se finita) e:

l(x) = (il piu piccolo n tale che sn(x) ∈ T ) + 1,

e la funzione parziale φ : X ⇀ W calcolata da φ e:

φ(x) = output(sl(x)(x)).

E facile notare che una Macchina di Turing e un caso particolare di itera-tore. Ora, se le macchine forniscono un modello adeguato per gli algoritmi:quale macchina modella il Mergesort? Ed in generale un qualsiasi algoritmoricorsivo? Per tradurre la ricorsione nel formalismo delle macchine ci sononumerose tecniche che sono state sviluppate per l’implementazione dei com-pilatori, per i quali la traduzione dell’astrazione fornita dalla ricorsione inistruzioni macchina e uno dei compiti fondamentali; la tecnica piu comunecoinvolge l’uso dello stack per tener traccia del livello di chiamata ricorsiva acui ci si trova ad ogni passo. Adottando questa impostazione si riscontranodue problemi principali:


Gestione della ricorsione

Il primo riguarda il fatto che in tutte queste tecniche, l’oggetto che si ottiene,chiamiamolo φA (l’iteratore corrispondente alla procedura A), e molto diversoda A stesso e nella formalizzazione delle dimostrazioni delle proprieta basedi A gran parte dei dettagli riguardano proprio la traduzione della ricorsionepiuttosto che le caratteristiche di A. Il nocciolo del problema non e tantoil livello di tecnicismo che esse richiedono, quanto il fatto che si perdono divista le caratteristiche distintive di A a scapito dei dettagli “implementativi”.

Non unicita della compilazione

Ammesso comunque che si possa accettare questo fattore negativo e perseve-rare nel considerare un algoritmo come un iteratore associato ad un sistemadi equazioni ricorsive, sorge un secondo problema, piu serio; ovvero, l’associa-zione cercata corrisponde in sostanza ad una compilazione: il punto e che ilprocedimento di compilazione non e unico ma varia a seconda del linguaggioe della macchina astratta che si adottano! Qualsiasi scelta operiamo, risultaarbitraria e quel che e peggio, una formalizzazione di algoritmo adeguata do-vrebbe permettere di dedurre le proprieta base di un algoritmo direttamente,senza fare riferimento ad alcuna implementazione particolare (proprio perchesi suppone che qualsiasi implementazione le debba soddisfare).

Nella sezione seguente vedremo come possiamo risovere questi problemise accettiamo un’altra impostazione.

3.2.3 Teoria delle equazioni ricorsive

Per dimostrare la validita della scelta di una definizione di algoritmo tramitela teoria degli insiemi, presentiamo una possibile formalizzazione delle pro-prieta del Mergesort, enunciate in sezione 3.2.1, che si basa sulla teoria delleequazioni ricorsive. Di seguito enunciamo il risultato principale di tale teoriache sfrutteremo per i nostri intenti.

Una catena di un insieme parzialmente ordinato (D, ≤ ) e un suo sot-toinsieme sul quale l’ordine ≤ risulta totale. Ricordiamo che un insiemeparzialmente ordinato si dice completo, abbreviato cpo, se ogni catena C di(D, ≤ ) ha un estremo superiore, indicato con sup A.Si dimostra che il prodotto cartesiano di cpo e a sua volta un cpo come lo elo spazio (X → Y ) delle funzioni tra un insieme qualsiasi ed un cpo.


Una funzione f : D → E tra due insiemi parzialmente ordinati e monotonase ∀d, d′ ∈ D vale:

d ≤D d′ =⇒ f(d) ≤E f(d′).

Il risultato principale e costituito dalla seguente:

Proposizione 1. Sia π : X×D → D una funzione monotona, dove X×D eun prodotto di insiemi parzialmente ordinati, se D e un cpo, allora per ognix ∈ X e per ogni d ∈ D, l’equazione

d = π(x, d)

ammette minimo punto fisso, esiste cioe una soluzione dx che gode delleseguenti proprieta:

dx = π(x, dx), (∀e ∈ D)[e ≤ π(x, e)⇒ dx ≤ e].

Inoltre la funzione x 7→ dx e monotona da X in D.

Naturalmente il risultato vale anche per sistemi di equazioni ricorsive deltipo:

dx1 = π1(x, dx1, . . . , dxn)...

dxn = πn(x, dx1, . . . , dxn)

dove πi : X × D → Di, con D = D1 × · · · × Dn, prodotto di n cpo. LaProposizione 1 ci garantisce che e sempre possibile trovare simultaneamentei minimi punti fissi per tutte le n equazioni.Possiamo indicare con d = π(x,d) il sistema di cui sopra.

Uno dei cpo piu semplici e sufficiente per i nostri scopi e quello formatodalle funzioni parziali tra un insieme qualsiasi ed un cpo, che indicheremo con(X ⇀ Y ); ricordiamo che (X ⇀ Y ) = (X → Y ∪{⊥}) dove con ⊥ denotiamoil sup ∅4 che chiameremo anche bottom perche chiude dal basso l’insieme chestiamo considerando. In sostanza e come se aggiungessimo un elemento piupiccolo di ogni altro, nel nostro caso, dello spazio di funzioni, ⊥ rappresentala funzione “ovunque indefinita”; su questo spazio l’ordinamento parziale checonsideriamo e quello dato dall’ordinamento del grafo delle funzioni ovvero:

f ≤ g ⇐⇒ (∀x ∈ X)[f(x) = y ⇒ g(x) = y].

4Che deve esistere dato che l’insieme vuoto ∅ e banalmente una catena.


Per semplificare la comprensione nel seguito adottiamo le seguenti abbrevia-zioni:– S per (L∗ ⇀ L∗)–M per (L∗ × L∗ ⇀ L∗)– O per (L× L ⇀ {true, false})

Tornando al nostro esempio guida, vediamo come applicare la Proposi-zione 1 al nostro caso in modo da ottenere i risultati desiderati. Le funzionisort e merge sono elementi rispettivamente dei cpo S edM; abbiamo inoltrebisogno di un terzo cpo che contenga la relazione di ordine lessicografico suL, ≤ ∈ O, vista come funzione caratteristica:

χ(s, t) =

{true se s ≤ t,false se t < s

(3.4)

Per risolvere il nostro problema lo dobbiamo generalizzare alla ricerca didue generiche funzioni parziali, appartenenti ad S ed aM, che dipendono dauna relazione d’ordine parziale c ∈ O: possiamo considerare le due funzionisortc e mergec come le funzioni individuate dalle soluzioni (minime) deisistemi di equazioni:

sortc(u) =

{u se |u| ≤ 1,mergec(sortc(h1(u)), sortc(h2(u))) altrimenti

(3.5)

e rispettivamente

mergec(u, v) =

u se v = ∅,v altrimenti, se u = ∅,〈u0〉 ∗mergec(tail(u), v) altrimenti, se c(u0, v0) = true,〈v0〉 ∗mergec(u, tail(v)) altrimenti, se c(u0, v0) = false

(3.6).La Proposizione 1 ci garantisce che queste soluzioni esistono sempre.Se c coincide con ≤, l’ordine parziale su L, allora merge≤ e sort≤ sonoesattamente le funzioni che stiamo cercando. Alla luce di quanto detto,facciamo vedere dei risultati analoghi ai Lemmi 2 e 4 della sezione 3.2.1.

Teorema 2. Siano sortc e mergec due funzioni che dipendono monotonica-mente da c : L×L ⇀ {true, false} che soddisfano le equazioni (3.5) e (3.6).Risulta:(a) Se mergec(u, v) = z ∈ L, allora esiste una funzione parziale c′ ≤ c defini-ta su al piu |u|+ |v| − 1 coppie e tale che mergec′(u, v) = z.(b) Se |u| = 2n e sortc(u) = z ∈ L, allora esiste una funzione parziale c′ ≤ cdefinita su al piu n · 2n coppie e tale che sortc′(u) = z.


Notiamo che in questa formalizzazione dei Lemmi 2 e 4 non utilizziamopiu i termini ambigui algoritmo e utilizzo di confronti! Ammettendo cheil meccanismo che ci permette di estrarre un procedimento di calcolo dalleequazioni (3.2) e (3.3) possa essere esteso anche alle equazioni corrispondenti(3.5) e (3.6), indicato con φ tale procedimento, per ogni c fissato otteniamoun diverso procedimento φc in cui l’espressione “controlla se s ≤ t” vie-ne sostituita dall’espressione “calcola c(s, t)”. φc calcola sortc che dipendemonotonicamente da c ≤ χ≤, allora per il Teorema 2 il dominio di c ha car-dinalita finita limitata, per tutti gli altri valori φc diverge.Abbiamo mostrato una strada per tradurre in termini formali espressioniche riguardano utilizzo di confronti, ci rimane da mostrare la traduzione deltermine algoritmo.

3.2.4 Funzionali e ricorsori

Vorremmo quindi poter “estrarre” da un sistema di equazioni della forma di(3.2) e (3.3) un oggetto che individui un procedimento di calcolo. Cerchiamol’insieme di istruzioni che ci fornisca un oggetto la cui semantica sia quel-la corrispondente alla interpretazione procedurale di (3.2) e (3.3), enunciatanella sezione 3.2.1, a partire dalle seguenti equazioni:

f(u, p, q) =

{u se |u| ≤ 1,q(p(h1(u)), p(h2(u))) altrimenti

(3.7)

g(v, w, p, q) =

v se w = ∅,w altrimenti, se v = ∅,〈v0〉 ∗ q(tail(u), v) altrimenti, se v0 ≤ w0,〈w0〉 ∗ q(u, tail(v)) altrimenti

(3.8)

Notiamo che f e g sono funzioni che prendono come parametri altrefunzioni, nell’introduzione avevamo gia incontrato entita di questo genere eavevamo detto che si chiamano funzionali, di seguito ne diamo la definizione.

Definizione (Funzionale) 2. Un funzionale su una famiglia di insiemi Me una funzione parziale monotona:

h : X1 × · · · ×Xn ⇀ W ,

dove W ∈ M oppure W = {true, false}; ciascun Xi e o un insieme di Moppure uno spazio di funzioni parziali Xi = (U ⇀ V ), con U = U1×· · ·×Um

prodotto di insiemi diM e V ∈M oppure V = {true, false}.


Un esempio classico di funzionale e dato dall’applicazione parziale:

apm(x1, . . . , xm, f) = f(x1, . . . , xm).

Nella maggior parte dei casi lavorare coi funzionali e sufficiente, per la tratta-zione formale si preferisce pero un approccio piu generale: lavoreremo quindicon entita matematiche che generalizzano i funzionali (che li “contengono”come casi particolari).Prima di procedere abbiamo bisogno di introdurre la nozione di universo;qui la esponiamo solamente in modo informale, per la trattazione precisa sirimanda alla sezione 3.3.Un universo many-sorted e una famiglia di insiemi base, indicizzata da uninsieme di tipi base (contenente bool)

U = {U(i) | i ∈ B}

Uno spazio di individui U e il prodotto di insiemi base e tra gli spazi diprodotti ammettiamo anche il prodotto “nullo” (cioe di alcun fattore) e loindichiamo con I. Di seguito indicheremo con P (U, V ) lo spazio delle funzioniparziali da U in V , (U ⇀ V ).Ora possiamo dare la definizione di:

Definizione (Ricorsore) 3. Un ricorsore su un universo U e una tupla difunzionali:

f = [f0, f1, . . . , fn] : X ↪→ W ,

tale che fissando opportunamente gli spazi di individui U0 = I, W0 = W , U1,W1,. . . , Un, Wn, risulti:

fi : Ui × P (U1, W1)× · · · × P (Un, Wn)×X ⇀ Wi ,

per i = 0, 1, . . . , n.

Nel caso in cui abbiamo un solo funzionale f e facile verificare che il ri-corsore [f ] ed il funzionale f coincidono.

Nella Discussione in sezione 3.2.1 avevamo parlato di due livelli di inter-pretazione delle equazioni ricorsive: il livello in cui consideriamo solamente lefunzioni cosı definite, livello estensionale, ed il livello in cui ci interessa ancheil procedimento con cui esse vengono calcolate, livello intensionale. Antici-piamo qualche cosa sulla discussione riguardo il primo, il livello estensionale.La denotazione del ricorsore f e il funzionale:

f : X ⇀ W ,


cosı definito:

f(x) ' f0(p1,x, . . . , pn,x, x),

dove, per ogni x, p1,x, . . . , pn,x sono punti fissi delle equazioni:

pi(ui) ' fi(ui, p1, . . . , pn, x) (1 ≤ i ≤ n).

Notazione Introduciamo una notazione per i ricorsori che spesso risultapiu intuitiva. A partire da un ricorsore dato f , fissando un x ∈ X otteniamoun ricorsore “senza parametri”:

f(x) = [f0,x, f1,x, . . . , fn,x] : I ↪→ W ,

dove

fi,x(ui, p1, . . . , pn) ' fi(ui, p1, . . . , pn, x).

E facile notare che per ogni x ∈ X:

f(x) ' f(x)(),

dove con () indichiamo l’unico elemento di I.Per specificare un ricorsore possiamo quindi utilizzare una “espressione” checi descriva l’associazione x 7→ f(x) della forma:

f(x) = f0(~p, x) where [pi(ui) = fi(ui, ~p, x) | 1 ≤ i ≤ n],

dove ~p = p1, . . . , pn.

Esempi

1. Ad ogni iteratore φ = (input, S, σ, T, output) e associato il ricorsore:

rφ(x) =df p(input(x)) where[p(s) = if s ∈ T then output(s) else p(σ(s))],

che ha come dominio l’insieme delle funzioni parziali (S ⇀ W ).Risulta: rφ(x) = φ(x), che vuol dire che essi calcolano la stessa funzio-ne.


2. Nell’introduzione, sez. 1.2.2, avevamo visto il seguente ricorsore chemodella l’algoritmo per calcolare il quadrato di un numero naturale:

sq(x) = times(x, x) where[times(u, v) = if zero(v) then 0 else plus(times(u, pred(v)), u)].

3. Per quanto riguarda il Mergesort, il sistema di funzionali formato dalleequazioni (3.7), (3.8) puo essere riscritto sotto forma di ricorsore nelseguente modo:

mergesort(u) = p(u) where [p(u) = f(u, p, q), q(v, w) = g(v, w, p, q)],

dove f e g sono, per l’appunto, definite da (dai punti fissi delle equa-zioni) (3.7) e (3.8).

Abbiamo introdotto la nozione piu generale di ricorsore, e importantespecificare quando due ricorsori risultano equivalenti:

Definizione (Equivalenza tra ricorsori) 4. Due ricorsori

f = [f0, . . . , fn], g = [g0, . . . , gm] : X ↪→ W

si dicono fortemente equivalenti se hanno lo stesso numero di componenti, i.e.n = m, ed esiste una permutazione σ degli indici {0, 1, . . . , n} con inversa ρe σ(0) = 0, tale che per ogni i, 0 ≤ i ≤ n, e per tutti gli ui, p1, . . . , pn, x vale:

fi(ui, p1, . . . , pn, x) ' gρ(i)(ui, pσ(1), . . . , pσ(n), x).

Sostanzialmente stiamo dicendo che scambiando in modo coerente l’ordinedei funzionali che compongono un ricorsore ne otteniamo uno equivalente, adesmpio il seguente ricorsore e equivalente a quello definito nell’Esempio 3:

mergesort′(u) = p(u) where [q(v, w) = g(v, w, p, q), p(u) = f(u, p, q)].

Equivalenza tra ricorsori ed equivalenza tra algoritmi Quella ap-pena introdotta e una relazione di equivalenza molto fine: in che misurasi presta a “modellare” la relazione di equivalenza tra algoritmi? Prima ditutto, e facile notare che ricorsori equivalenti hanno la stessa denotazione.Consideriamo pero il ricorsore cosı definito:

α(x) = β(u, v) where [u = η(x), v = η(x)],


dove η e un funzionale, al limite un ricorsore, dato.Notando che η(x) va calcolata due volte, e naturale riscrivere il ricorsoreprecedente nella forma:

α′(x) = β(u, u) where [u = η(x)],

in cui tale valore viene calcolato una volta sola5. Ora, secondo la definizionedata, i due ricorsori α e α′ non sono equivalenti, il che e abbastanza contro-intuitivo. In realta si potrebbe argomentare che non e vero che essi dianoluogo allo stesso algoritmo ma che α′ sia una versione ottimizzata di α. Adogni modo e chiaro che e desiderabile approfondire lo studio delle relazionidi equivalenza tra ricorsori che risultino piu “grossolane” di quella data eche tengano conto delle piu comuni tecniche di ottimizzazione, allo stessomodo in cui la relazione da noi definita permette di riordinare i funzionaliche compongono i ricorsori6.

Prima di proseguire, facciamo il punto della situazione per non perderedi vista i nostri obiettivi: siamo partiti dal modello di calcolo di macchinaastratta piu generale, l’iteratore, per cercare di modellare l’algoritmo Merge-sort e abbiamo visto che questo porta a dei notevoli problemi; a questo puntoci siamo chiesti se le equazioni che lo definiscono non contengano esse stessetutte le informazioni che identificano questo algoritmo mediante un’ulterioreinterpretazione. Abbiamo dato il nome di intensionale a questa intepreta-zione per distinguerla da quella classica, estensionale. Per esprimere sistemidi equazioni ricorsive abbiamo quindi introdotto la nozione di ricorsore. Sinqui abbiamo tacitamente appoggiato la tesi che tale nozione puo essere uti-lizzata per modellare il concetto di algoritmo. Nel seguito ci occuperemo delproblema, gia accennato, di che cosa sia l’implementazione di un algoritmoe tratteremo in maniera piu approfondita alcuni aspetti importanti della tesi.

3.2.5 Implementazioni

Tra gli esempi di ricorsori dati nella sezione precedente, abbiamo visto checiascun iteratore φ puo essere visto come un ricorsore (degenere) rφ. Ora,avanziamo la proposta di considerare le implementazioni come iteratori; taleproposta risulta abbastanza naturale se consideriamo che un’implementa-zione, in sostanza, e una procedura eseguibile da una macchina (astratta o

5Naturalmente queste considerazioni sono fondate se assumiamo che il calcolo di η nondia luogo ad effetti collaterali.

6Uno studio di questo tipo potrebbe ispirarsi alle tecniche adottate dai compilatori perottimizzare certe espressioni.


reale). Ma in che modo funziona l’associazione tra un algoritmo/ricorsoreed una sua implementazione/iteratore? A livello intuitivo, introdurremo unarelazione, ≤r, di riducibilita tra ricorsori; α ≤r β ci dice che le computazio-ni del ricorsore α sono simulabili a partire da quelle di β. A questo puntodiremo che l’iteratore φ “implementa” α se α ≤r rφ. Prima di procederealla formalizzazione di quanto detto, per rendere la trattazione di piu facilelettura introduciamo alcune abbreviazioni che riguardano i ricorsori.Indichiamo con Dα il prodotto P (U1, W1) × · · · × P (Un, Wn); la funzione ditransizione associata ad un ricorsore α e:

τα(x,d) = (f1(x,d), . . . , fn(x,d)),

dove d indica un elemento di Dα.Chiamando inoltre la funzione α0 come valueα, un ricorsore α puo esserevisto come la terna (Dα, τα, valueα).

Definizione (Riduzione tra ricorsori) 5. Dati due ricorsori

α1 = (D1, τ1, value1) : X1 ↪→ W ,α2 = (D2, τ2, value2) : X2 ↪→ W ,

diciamo che α1 e riducibile ad α2, denotato con α1 ≤r α2, se esistono duefunzioni monotone:

ρ : X1 → X2, π : X1 ×D1 → D2,

tali che:

1. Per ogni x ∈ X1 e d ∈ D1, τ2(ρ(x), π(x, d)) ≤ π(x, τ1(x, d));

2. per ogni x ∈ X1 e d ∈ D1, value2(ρ(x), π(x, d)) = value1(x, d);

3. per ogni x ∈ X1, α1(x) = α2(ρ(x)).

Per fare un esempio, possiamo immaginare che X2 sia una espansione diX1, contenente “strutture dati” aggiuntive (pile, code, ecc. . . ). Che relazionec’e tra le computazioni dei due ricorsori? Possiamo pensare che ogni d ∈D1 rappresenti una quantita d’informazione sul valore α1(x) che secondo laclausola 3 coincide con α2(ρ(x)). Se chiamiamo v questo valore e consideratoche per ogni x, π(x, d) contiene l’informazione corrispondente riguardo alvalore v, le clausole 1 e 2 garantiscono che ciascun passo di computazionedi α2 non incrementa la quantita d’informazione sul valore v piu di quantofaccia il corrispondente passo di α1

7.

7Questa proprieta ci assicura che siamo in presenza di simulazione.


3.2.6 Algoritmi

Ammettendo che sia possibile specificare un algoritmo tramite il ricorsoreche “descrive” il modo in cui la computazione viene effettuata, va notatoche tale descrizione fa sempre riferimento a delle “operazioni” (in sostanzadelle funzioni) base che consideriamo come primitive; nel caso dell’esempiodel Mergesort facevamo uso dell’operazione ∗ di concatenazione fra stringhee delle operazioni tail e head sempre definite su stringhe, mentre nell’esempiodell’algoritmo che calcola il quadrato di un numero, nella sua definizione,facevamo riferimento alle operazioni zero, plus e pred. Nella maggior partedelle applicazioni le “istruzioni base” saranno funzioni8 e, generalizzando,funzionali e ricorsori. In generale non e chiaro a priori quali operazioni sia“lecito” considerare come primitive e dal momento che, in questo studio, sivuole proporre una teoria generale, si e scelto di non dare alcuna operazione“per scontata”.Il punto e che a differenza del concetto di funzione calcolabile, concetto asso-luto secondo la Tesi di Church–Turing, il concetto di algoritmo e un concettointrinsecamente relativo, relativo alle operazioni base di cui fa uso; tale ca-ratteristica deriva dalla natura intensionale del concetto stesso.

Ecco quindi che per tener conto dell’insieme di istruzioni che un datoalgoritmo ha a disposizione , dobbiamo “immergere” il ricorsore corrispon-dente in una struttura contenente le “strutture dati” e le istruzioni su di essedefinite.

Definizione (Struttura) 6. Una struttura e una coppia M = (M,F) taleche:

1. ogni M ∈ M e un insieme ed almeno un M e non vuoto, questi sonogli insiemi base di M;

2. ogni α ∈ F e un ricorsore definito sugli insiemi base di M, per cui α eun funzionale suM.

Il classico esempio di struttura e rappresentato dalla struttura del primoordine per i naturali:

M = (N, 0, S, P, χ0),

dove 0 e una costante, S(n) e P (n) calcolano rispettivamente il successoreed il predecessore di n e χ0 : N → {true, false} e la funzione caratteristicadi {0}.

8Come gia sottolineato, per omogeneita di trattazione, le relazioni possono esserecodificate, attraverso le loro funzioni caratteristiche.


In generale i ricorsori appartenenti ad una struttura M rappresentano glialgoritmi che accettiamo come dati e costituiscono i mattoni base coi quali“costruire” gli algoritmi di M.

Definibilita formale e semantica degli algoritmi Abbiamo visto comeun algoritmo abbia senso solo se messo in relazione a delle operazioni basecodificate da una apposita struttura: non basta piu dire che un algoritmo eun ricorsore, dobbiamo anche specificare la struttura in cui esso e immerso.Vediamo ora come “aggiornare” la nostra tesi inglobando questo requisito.Ad ogni struttura M e associata in modo naturale una segnatura in cui le va-riabili spaziano sugli insiemi base di M e con le funzioni (parziali) e relazionisu di essi definite e simboli di costante per i ricorsori dati; a partire da questasegnatura e possibile definire vari linguaggi formali che codificano la nozionedi definibilita su M. Fra questi linguaggi il Formal Language of Recursion[34], abbreviato FLR, e uno dei piu semplici; i suoi termini sono costruititramite: applicazione parziale, definizione per casi, chiamate ai ricorsori datie, naturalmente, ricorsione.

La semantica algoritmica o semantica intensionale del linguaggio FLRe definita in [33] e verra trattata in maniera approfondita nella sezione 3.4.Come al solito ci interessa prima di tutto dare un’intuizione di cio che avviene.Ad ogni termine A di FLR, data una struttura M, viene associato un ricorsore,l’intensione di A in M, che indicheremo con:

α = intAM,

tale che il dominio di α e il prodotto dei domini dei ricorsori dati di M e deisuoi insiemi base, ed i funzionali che lo compongono sono definiti in “manieraesplicita ed immediata” utilizzando applicazioni, condizionali e chiamate afunzione9.A questo punto possiamo enunciare la:

Tesi: ogni algoritmo relativo ad un insieme di ricorsori dati F e(modellato da) l’intensione intA

M di un certo FLR-termine A sudi una struttura M che ha F come parte funzionale; viceversa ogniintA

M e un algoritmo rispetto ad F .

9Naturalmente bisogna chiarire che cosa significhi “maniera esplicita ed immediata”,per questo aspetto si rimanda alla sezione 3.4.


3.3 FLR - Sintassi

Nella Presentazione abbiamo voluto dare un’idea della strada seguita da Mo-schovakis per risolvere il problema della definizione formale di algoritmo;abbiamo concluso tale panoramica accennando al linguaggio formale adotta-to, FLR, ovvero Formal Language of Recursion, e abbiamo affermato che unalgoritmo puo esser visto come una particolare interpretazione di un certotermine di questo linguaggio. Per comprendere la fondatezza di quest’affer-mazione e necessaria una trattazione approfondita di FLR: prima di tuttovedremo la sua sintassi e poi ne presenteremo le due semantiche (quella de-notazionale e quella intensionale) cui abbiamo precedentemente accennato.In questa sezione facciamo riferimento alla presentazione del linguaggio FLRcontenuta in [34].

3.3.1 Tipi

Definizione (Insieme di tipi base) 7. Un insieme di tipi base e un qual-siasi insieme B contenente la stringa bool. A partire da B definiamo ricor-sivamente l’insieme di tipi T = T (B) secondo le seguenti clausole:t1. Se u1, . . . , un sono tipi base in B, allora la stringa (u1, . . . , un) 10 e untipo individuale in T .t2. Sia u un tipo individuale e sia w un tipo base, allora la stringa (u ⇀ w)e un tipo funzione parziale o fp in T .t3. Se x1, . . . , xn sono tipi base o tipi fp, allora la stringa (x1, . . . , xn) e untipo prodotto in T .t4. Sia x un tipo prodotto e sia w un tipo base, allora la stringa (x ⇀ w) eun tipo funzione in T .

Ammettiamo anche il caso n = 0 e indichiamo tale tipo individuale con ( ).

3.3.2 Oggetti tipati

Chiaramente i nomi che abbiamo scelto per i nostri tipi rispecchiano l’usoche ne faremo. Di seguito diamo la definizione di universo puro, l’aggettivopuro si riferisce al fatto che tale genere di struttura e quello utilizzato permodellare algoritmi che non dipendono da uno stato e che non produconoeffetti collaterali11.

10In questo contesto usiamo la notazione (x1, . . . , xn) per la stringa x1x2 · · ·xn.11Il classico esempio di programmi di questo genere e dato dai programmi dei linguaggi

funzionali “puri” come il Pure Lisp.

3.3. FLR - SINTASSI 71

Definizione (Universo puro) 8. Un universo puro definito a partire daun insieme di tipi base B e una famiglia di insiemi U , indicizzata da B:U = {U(i) | i ∈ B}, tale che U(bool) = {true, false}. Gli oggetti base diU sono elementi degli insiemi base di U e gli altri oggetti (tipati) di U sonodefiniti ricorsivamente dalle seguenti clausole, corrispondenti alle t1–t4:po1. Un individuo di tipo u = (u1, . . . , un) e un qualsiasi elemento delprodotto cartesiano U = U(u1)× · · · × U(un).po2. Un oggetto di tipo fp (u ⇀ w) e una qualsiasi funzione parziale nellospazio P (U,W ) = {p : U ⇀ W}, dove U e di tipo individuale u e W e ditipo base w.po3. Un punto di tipo prodotto x = (x1, . . . , xn) e un oggetto nello spazioprodotto X = X1 × · · · ×Xn, dove ogni Xi e l’insieme base o lo spazio fp ditipo xi.po4. Un oggetto di tipo funzione x ⇀ w e una qualsiasi funzione (funzionale)parziale f : X ⇀ W , definita dallo spazio prodotto di tipo x nell’insieme basedi tipo w, monotono rispetto all’ordinamento canonico su X:

[f(x) ' w & x ≤ y]⇒ f(y) ' w.

3.3.3 Sintassi

Definizione (Segnatura) 9. Una segnatura e una tripla (B, S, d), dove Be un insieme di tipi base, S e un insieme qualsiasi di costanti di funzioni e de una funzione che mappa ogni f ∈ S su di un tipo d(f) ∈ B.

A partire da una segnatura fissata τ il linguaggio formale ad essa associatoFLR(τ) e definito nel seguente modo:–Variabili. FLR e “equipaggiato” con una infinita numerabile di variabilibase di tipo i, per ogni tipo base i in B, e di varibili fp di tipo u ⇀ w,per ogni tipo fp u ⇀ w in B. Utilizzeremo il termine variabile individualeper indicare una generica stringa u ≡ u1, . . . , un formata da una sequenza divariabili base separate da virgole; u ha tipo (u1, . . . , un), dove ciascun ui e iltipo di ui. La stringa vuota ∅ ha tipo ( ).–Costanti. Le costanti di funzione che appartengono alla segnatura τ sonoin FLR, a ciascuna di esse corrisponde un tipo funzione individuato da τ .Inoltre appartengono ad FLR anche le seguenti costanti:

• Vero e falso. true e false sono costanti di tipo (( ) ⇀ bool).

• Condizionali. Per ogni tipo base w, c’e una costante di funzione condw

di tipo ((bool, (( ) ⇀ w), (( ) ⇀ w)) ⇀ w).


–Espressioni. In FLR ci sono due tipi di espressioni: termini, di tipo base,ed fp-termini, di tipo fp. Ogni espressione contiene una lista di variabili cheoccorrono libere in essa. Trattiamo i vari casi con le seguenti clausole ricor-sive.T1. Ogni variabile base o fp e, rispettivamente, un termine oppure un fp-termine; ciascuna ha il proprio tipo ed occorre libera in se stessa.T2. Se ogni ti e un termine di tipo ti, con 1 ≤ i ≤ n, e p e una variabile fp ditipo ((t1, . . . , tn) ⇀ w), allora la stringa p(t1, . . . , tn) e un termine di tipo w.Le occorrenze libere di variabili in questo termine sono quelle in t1, . . . , tn acui si aggiunge la nuova occorrenza di p. Nel caso in cui n = 0, se p ha tipo(( ) ⇀ w) questa clausola introduce il termine p( ) di tipo w.T3. Sia t un termine di tipo w e u ≡ u1, . . . , um una variabile individualedi tipo u, allora il λ–termine λ(u)t e un fp-termine di tipo (u ⇀ w). Leoccorrenze libere in questo termine sono quelle di t diverse da u1, . . . , um.T4. Sia f una costante di funzione con tipo ((t1, . . . , tn) ⇀ w), in cui ogni tie un’espressione tipata a ti, allora la stringa f[t1, . . . , tn] e un termine di tipow. Le occorrenze libere in questo termine sono quelle in t1, . . . , tn. Se n = 0,scriveremo f al posto di f[ ]. Per le costanti che abbiamo richiesto che sianosempre presenti utilizzeremo le seguenti abbreviazioni:true ≡ true[ ], false ≡ false[ ],if s then t1 else t2 ≡ condw[s, λ( )t1, λ( )t2].

Diciamo che una espressione e esplicita se puo essere “costruita” utiliz-zando solamente le regole T1–T4.

L’ultima clausola introduce termini ricorsivi.T5. Se u1, . . . , un sono variabili individuali di tipo rispettivamente u1, . . . , un,se p1, . . . , pn sono variabli fp distinte di tipo rispettivamente

(u1 ⇀ w1), . . . , (un ⇀ wn)

e se t0, t1, . . . , tn sono termini con tipo rispettivamente w, w1, . . . , wn, allora

t ≡ rec(u1, p1, . . . , un, pn)[t0, t1, . . . , tn]

e un termine di tipo w. I termini t0, t1, . . . , tn sono le parti del terminericorsivo t e t0 prende il nome di parte di testa o output. Un altro modo discrivere lo stesso termine e quello piu intuitivo che abbiamo adottato nellaPresentazione:

rec(u1, p1, . . . , un, pn)[t0, t1, . . . , tn] ≡ t0 where [p1(u1) ' t1, . . . , pn(un) ' tn]


ma si e scelto di definirlo in questa forma perche nelle dimostrazioni perinduzione sulla struttura dei termini risulta piu semplice lavorare con talerappresentazione.

Nota (sulle occorrenze libere) Assumiamo che tutte le occorrenze divariabili presenti in un’espressione che non risultano libere secondo le regolespecificate dalle precedenti clausole, siano legate.

Sostituzioni Sia t(v) un’espressione, v una variabile base oppure unacostante di funzione con tipo base w e sia s una variabile base oppure untermine con tipo w, denotiamo l’espressione che si ottiene rimpiazzando ognioccorrenza libera di v in t(v) con s con:

t(s) ≡ subst(t(v), v/s).

Estendiamo la suddetta notazione anche al caso di sostituzioni simultanee:

t(s1, . . . , sn) ≡ subst(t(v1, . . . , vn), v1/s1, . . . , vn/sn).

Sia s(u) ≡ s(u1, . . . , un) un termine con tipo w, in cui ogni variabile base ui

ha tipo ui e sia r una costante di funzione o una variabile fp con tipo (u ⇀ w),dove u ≡ (u1, . . . , un), allora definiamo la λ-sostituzione di λ(u)s(u) al postodi r nell’espressione t(r):

t(λ(u)s(u)) ≡ subst(t(r), r/λ(u)s(u)),

per induzione su t(r). Gli unici casi non ovvi sono T1, quando r ≡ p, e T4,quando r ≡ f; in questi casi poniamo:

subst(p(t1, . . . , tn), p/λ(u)s(u)) ≡s(subst(t1, p/λ(u)s(u)), . . . , subst(tn, p/λ(u)s(u))),

procediamo allo stesso modo quando r ≡ f.Supponiamo ora che sia s(x) ≡ s(x1, . . . , xn), dove x1, . . . , xn sono variabilibase o fp e sia t(r) un’espressione in cui r e una costante di funzione tale cher(x1, . . . , xn) e un termine, allora definiamo:

t(λ(x1, . . . , xn)s(x)) ≡ subst(t(r), r/λ(x1, . . . , xn)s(x))

rimpiazzando ogni r(t1, . . . , tn) in t(r) con l’espressione

s(subst(t1, λ(x)s(x)), . . . , subst(tn, λ(x)s(x))).

Nel resto della trattazione assumeremo che le sostituzioni avvengano in mo-do “pulito”, nel senso che non avviene cattura di variabili. Scrivendo p/qintenderemo p/λ(u)q(u).


3.3.4 Congruenza e termini speciali

Introduciamo ora una relazione di congruenza fra termini che identifica i ter-mini che differiscono per l’ordine delle parti, esclusa la parte di testa. Possia-mo considerare termini congruenti come (sintatticamente) “indistinguibili”.

Definizione (Congruenza) 10. La relazione di congruenza e la piu piccolarelazione di equivalenza ≡c che soddisfa le seguenti condizioni:C1. Per ogni variabile fp p, p ≡c λ(u)p(u).C2. [t1 ≡c t1

′, . . . , tn ≡c tn′]⇒ p(t1, . . . , tn) ≡c p(t1

′, . . . , tn′).

C3. Se z1, . . . , zm sono variabili base fresh12, allora

subst(t, u1/z1, . . . , um/zm) ≡c subst(t′, v1/z1, . . . , vm/zm)⇒ λ(u1, . . . , um)t ≡c λ(v1, . . . , vm)t′.

C4. [t1 ≡c t1′, . . . , tn ≡c tn

′]⇒ f[t1, . . . , tn] ≡c f[t1′, . . . , tn

′].C5a. rec( )[t] ≡c t.C5b. rec(u1, p1, . . . , un, pn)[t0, . . . , tn] ≡c rec(v1, q1, . . . , vn, qn)[t0

′, . . . , tn′],

se esiste una permutazione σ degli indici {0, 1, . . . , n}, con σ(0) = 0 e inversaρ, tale che risulta:(a) Per ogni i, 1 ≤ i ≤ n, le variabili fp pσ(i) e qi hanno lo stesso tipo13.(b) Se r1, . . . , rn e una sequenza di variabili fp fresh e z1, . . . , zn e una sequenzadi variabili base fresh tali che le sostituzioni di seguito hanno senso, alloraabbiamo:

subst(tρ(i)′, vρ(i)/zρ(i), q1/r1, . . . , qn/rn) ≡c

subst(ti, ui/zρ(i), pσ(1)/r1, . . . , pσ(n)/rn).

Facciamo un esempio:

rec(u1, p1, u2, p2, u3, p3)[t0, t1, t2, t3] ≡c rec(u2, p2, u3, p3, u1, p1)[t0, t2, t3, t1],

per σ(1) = 2, σ(2) = 3, σ(3) = 1.

La seguente definizione individua la sottoclasse dei termini che interpre-tati daranno luogo ad “algoritmi”:

Definizione (Termini speciali) 11. Diciamo che un termine t e specialese e della forma p(t1, . . . , tn), f[t1, . . . , tn] oppure

rec(u1, p1, . . . , un, pn)[s0, s1, . . . , sn]

dove tutti i s0, s1, . . . , sn sono termini speciali.

12Che non occorrono ne in t ne in t′.13Non c’e bisogno di specificare che anche uσ(i) e vi hanno lo stesso tipo grazie alle

restrizioni sui tipi della clausola T4.


Esempio. Prendiamo il termine:

x · y ≡ rec(i, times, j, plus)[times(y),if zero[i] then 0 else plus(times(pred[i]))if zero[j] then x else succ[plus(pred[j])]],

in cui consideriamo come date le funzioni succ, pred e zero (e naturalmen-te lo 0).L’unico elemento che rende il termine non speciale e l’occorrenza della varia-bile libera x; possiamo trasformare il termine in questione in speciale rim-piazzando tale occorrenza con il seguente termine, a sua volta speciale, chedefinisce l’identita:

id[x] ≡ rec(i, p)[p(x), if zero[i] then 0 else succ[p(pred[i])]].

Concludiamo questa sezione con un ultimo:

Fatto. Se s ≡c t ed s e speciale allora lo e anche t.

3.3.5 FLR - Riduzione

In questa sezione affrontiamo un procedimento, la riduzione per l’appunto, dimodifica sintattica dei termini di FLR; ogni termine puo essere trasformato,secondo queste regole, in un altro non ulteriormente riducibile. Introdurremoil concetto di equivalenza intensionale e di forma normale ed il risultatoprincipale che presenteremo e l’unicita di tale forma normale. Le regole dimanipolazione, puramente sintattiche, di questo calcolo individuano quindi letrasformazioni base delle definizioni ricorsive che “preservano gli algoritmi”;in quest’ottica la forma normale di un termine t, ne identifica una definizione“diretta e immediata” (in relazione alle funzioni proprie della struttura in cuiinterpretiamo t) 14. L’idea di fondo e che se s e (intensionalmente) equivalentea t, allora essi definiscono lo stesso algoritmo ma la dimostrazione di questaaffermazione verra affrontata nella sezione relativa alla semantica di FLR.

14E dunque possibile vedere la riduzione come un procedimento analogo a quello dellacompilazione di programmi, in cui le funzioni ad alto livello devono essere trasformate insequenze di istruzioni macchina.


Il calcolo della riduzione

Secondo quanto detto il significato di un termine t′ varia a seconda dellaposizione che occupa nel termine t che lo contiene: quello che conta e qualisiano le variabili fp libere nello campo d’azione del quantificatore rec in t.Per formalizzare questa idea introduciamo alcuni concetti base:

Definizione (Contesto) 12. Un contesto e un qualsiasi insieme E di varia-bili; il contesto globale e l’insieme contenente tutte le variabili.

Per specificare l’algoritmo definito dal seguente termine:

rec(u1, p1, . . . , un, pn)[t0, . . . , tn],

nel contesto vuoto, abbiamo bisogno dell’algoritmo definito da ciascun ti nelcontesto Ei = {ui, p1, . . . , pn}.

Definizione (Espressione immediata) 13. Una espressione si dice im-mediata nel contesto E se e congruente ad una variabile base, p(v1, . . . , vn)con p, v1, . . . , vn ∈ E oppure λ(u1, . . . , um)p(v1, . . . , vm) con p, v1, . . . , vn ∈E ∪ {u1, . . . , um}.

L’idea e che quando calcoliamo una funzione f in un contesto E, in modoconcorrente calcoliamo anche le funzioni “nominate” da variabili fp in ma-niera mutuamente ricorsiva, le variabili base in E rappresentano le variabililocali della ricorsione.

Definizione (Riduzione ed equivalenza) 14. Le regole di riduzione →E

e di equivalenza ∼E, relative al contesto E, sono specificate nella tabellaseguente. In R1–R5 r, r1, . . . , rm sono variabili fresh; in R1 ed R2 suppo-niamo che t non sia immediato in E ed allo stesso modo in R3 supponiamoλ(u)t non immediato in E; per maggior chiarezza, in R5 abbiamo adottatola notazione algebrica r(u, ·) al posto della piu frequente λ(v)r(u, v).

Le regole R1–R3 riducono la computazione esplicita a ricorsione (ba-nale). R4 ed R5 riducono l’annidamento del quantificatore rec nei termi-ni; risulta piu semplice capire come agiscono su di un paio di esempi conn = m = 1:

• rec(u, p)[rec(v, q)[s0(q), s1(q)], t1]→E

rec(v, r, u, p)[s0(r), s1(r), t1];

• rec(u, p)[t0, rec(v, q)[s0(q), s1(q)]]→E

rec(u, p, u, v, r)[t0, s0(r(u, ·)), s1(r(u, ·))].


R6 rende la relazione →E piu grossolana rispetto a ≡c. R7 rende →E

transitiva. R8 permette la riduzione di termini ricorsivi non banali a partiredalle riduzioni delle loro parti in un contesto allargato. R6 ed R9–11 defi-niscono ∼E come la piu piccola relazione di equivalenza che e piu grossolanadi →E.

Regole di Riduzione ed Equivalenza

R1 p(a, t, b)→E rec(r)[p(a, r( ), b), t].R2 f[a, t, b]→E rec(r)[f[a, r( ), b], t].R3 f[a, λ(u)t, b]→E rec(u, r)[f[a, r, b], t].R4 rec(u1, . . . , pn)[rec(v1, . . . , qm)[s0(q1, . . . , qm), . . . , sm(q1, . . . , qm)], t1, . . . , tn]

→E rec(v1, r1, v2, r2, . . . , vm, rm, u1, p1, . . . , pn)[s0(r1, . . . , rm), . . . , sm(r1, . . . , rm), t1, t2, . . . , tn].

R5 rec(u1, . . . , pn)[t0, rec(v1, . . . , qm)[s0(q1, . . . , qm), . . . , sm(q1, . . . , qm)], t2, . . . , tn]→E rec(u1, p1, u1, v1, r1, u1, v2, r2, . . . , u1, vm, rm, u2, p2, . . . , pn)

[t0, s0(r1(u1, ·), . . . , rm(u1, ·)), . . . , sm(r1(u1, ·), . . . , rm(u1, ·)), t2, . . . , tn].R6 s1 ≡c s2 ⇒ s1 →E s2.R7 s1 →E s2 & s2 →E s3 ⇒ s1 →E s3.R8 Se J(i) = E ∪ {ui, p1, . . . , pn}, allora

s0 →J(0) t0, . . . , sn →J(n) tn ⇒rec(u1, . . . , pn)[s0, . . . , sn]→E rec(u1, . . . , pn)[t0, . . . , tn].

R9 s1 →E s2 ⇒ s1 ∼E s2.R10 s1 ∼E s2 ⇒ s2 ∼E s1.R11 s1 ∼E s2 & s2 ∼E s3 ⇒ s1 ∼E s3.

Di seguito enunceremo il risultato principale della sezione riguardante lasintassi di FLR: prima di tutto presenteremo il concetto di forma normale,mostreremo che ogni termine t puo essere ridotto ad un termine in formanormale t∗ non ulteriormente riducibile e vedremo che t∗ e unico (a menodi congruenza ≡c). Prima di procedere abbiamo pero bisogno di introdurrealcune definizioni base.

Definizione (Termine irriducibile) 15. Diciamo che un termine s e irri-ducibile nel contesto E, o semplicemente irriducibile quando E e il contestoglobale, se per ogni t risulta:

s→E t⇒ s ≡c t.


Definizione (Espressione semplificata) 16. Una espressione si dice sem-plificata se il quantificatore vuoto rec( ) non compare in t oppure se

t ≡ rec( )s

e rec( ) non compare in s.

Per semplificare la leggibilita della seguente definizione introduciamo laseguente notazione:scriveremo i 7→ n per abbreviare i = 1, . . . , n, escriveremo i 7−→ n per abbreviare i = 0, . . . , n.

Definizione (Combinazione di ricorsori) 17. Sia t un termine doppia-mente ricorsivo 15:

t ≡ rec(ui, pi : i 7→ n)[ti(p1, . . . , pn) : i 7−→ n],

e per i 7−→ n:

ti(p1, . . . , pn) ≡ rec(vij, qij : j 7→ m(i))[tij(qi1, . . . , qim(i), p1, . . . , pn) : j 7−→ m(i)].

La combinazione ricorsiva di t e il termine ricorsivo:

rc(t) ≡ rc t ≡ rec(ui, vij, rij : i 7−→ n, j 7−→ m(i), (i, j) 6= (0, 0))[tij(ri1(ui, ·), . . . , rim(i)(ui, ·), r10, . . . , rn0) : i 7−→ n, j 7−→ m(i)],

dove ciascuna rij e una variabile fp fresh e:

rij(ui, ·) ≡ λ(vij)rij(ui, vij).

Definizione (Forma normale) 18. Per ogni termine t ed ogni contestoE, il termine ricorsivo semplificato nf(t, E), la forma normale di t in E, edefinito per ricorsione su t. La forma normale (assoluta) di t e la formanormale di t nel contesto vuoto:

nf(t) ≡ nf(t, ∅),

e la forma normale globale di t e la forma normale di t nel contesto globale:

fnf(t) ≡ nf(t, {tutte le variabili}).15Con grado di annidamento del quantificatore rec pari a 2, un esempio e dato dal

termine di sinistra della regola R4.


NF1. Per una variabile base v: nf(v, E) ≡ rec( )[v] ≡ rec( )v.NF2. Come esempio di questo caso prendiamo t ≡ p(w, t∗), dove w eimmediato in E e t∗ non lo e; supponiamo di aver calcolato:

nf(t∗, E) ≡ rec(u1, p1, . . . , un, pn)[t0, . . . , tn],

allora poniamo:

nf(t, E) ≡ rec(r, u1, p1, . . . , un, pn)[p(w, r( )), t0, . . . , tn].

In generale, quando t ≡ p(t1, . . . , tn), vogliamo ridurre i ti che non sonoimmediati in E e lasciare quelli immmediati come argomenti. Osserviamoche se t1, . . . , tn sono tutti immediati in E, risulta:

nf(p(t1, . . . , tn), E) ≡ rec( )p(t1, . . . , tn) ≡c p(t1, . . . , tn).

NF3. Il caso corrispondente ai λ-termini non e presente perche in questocalcolo di riduzione non riduciamo mai λ-termini a se stanti ma li riduciamosolamente quando sono passati come parametro all’interno di un altro termi-ne, secondo il modo che viene specificato nella clausola seguente.NF4. Come esempio prendiamo il caso in cui

t ≡ f[w, s, λ(u1, . . . , uk)t∗],

dove w e immediato in E, mentre s e λ(u1, . . . , uk)t∗ non sono immediati inE (w puo essere un termine oppure un λ-termine). Supponiamo che sia:

nf(s, E) ≡ rec(v1, q1, . . . , vn, qn)[s0, . . . , sm],

nf(t∗, E ∪ {u1, . . . , uk}) ≡ rec(z1, p1, . . . , zn, pn)[t0(p1, . . . , pn), . . . , tn(p1, . . . , pn)],

e poniamo:

nf(t, E) ≡ rec(rs, v1, . . . , qm, rt, u, z1, r1, u, z2, . . . , u, zn, rn)[f[w, rs(), rt], s0, . . . , sm, t0

′, . . . , tn′],

dove u ≡ u1, . . . , uk e per 1 ≤ i ≤ n, ti′ ≡ ti(r1(u, ·), . . . , rn(u, ·)). In generale,

quando t ≡ f[t1, . . . , tn], si riducono le espressioni t1, . . . , tn in E che non sonoimmediate (come s e λ(u)t∗ nell’esempio) e poi otteniamo la forma normale“passando” ad f le espressioni immediate ed i risultati della riduzione dellet1, . . . , tn. Se tutte le ti sono immediate in E, otteniamo:

nf(f[t1, . . . , tn], E) ≡ rec( )f[t1, . . . , tn] ≡c f[t1, . . . , tn].


NF5. Sia

t ≡ rec(u1, p1, . . . , un, pn)[t0, . . . , tn],

e poniamo:

ti∗ ≡ nf(ti, E ∪ {ui, p1 . . . , pn}),

t∗ ≡ rec(u1, p1, . . . , un, pn)[t0∗, . . . , tn∗],

per i = 0, . . . , n. Ora t∗ e un termine doppiamente ricorsivo e possiamo porre:

nf(t, E) = rc t∗.

Ogni parte ti di t e ridotta nel contesto allargato E ∪ {ui, p1, . . . , pn}.

Di seguito riportiamo tre risultati, di cui non diamo la dimostrazioneper non appesantire la trattazione, che riguardano le principali proprietasintattiche della forma normale di un termine.

Teorema 3. Per ogni termine t ed ogni contesto E, nf(t, E) e un terminericorsivo semplificato ed irriducibile in E e:

t→E nf(t, E).

Nella definizione di forma normale di un termine e presente una strategiadi riduzione, l’ordine in cui applicare le regole per ottenere un termine irri-ducibile. Il seguente risultato mostra che la strategia di riduzione adottatanon importa.

Teorema 4. Per ogni contesto E e tutti i termini s e t, risulta:

s→E t⇒ nf(s, E) ≡c nf(t, E),

per cui:

s ∼E t⇔ nf(s, E) ≡c nf(t, E)⇔ per un certo w, s→E w & s→E w.

Ed infine il risultato principale di questa sezione:

Teorema 5. Per ogni termine t ed ogni contesto E, nf(t, E) e l’unico (ameno di congruenza) termine t∗ che e irriducibile in E e tale che t→E t∗.

3.4. FLR - SEMANTICA 81

3.4 FLR - Semantica

Come anticipato nella sezione 3.2.6 sulla definibilita formale degli algoritmi,secondo la Tesi avanzata da Moschovakis, ogni algoritmo e una particolareinterpretazione di un termine t del linguaggio FLR: l’intensione di t (un ri-corsore) che calcola la denotazione di t (una funzione). In questa sezionetratteremo dunque due semantiche su termini del linguaggio FLR: la seman-tica denotazionale e la semantica intensionale. Concluderemo presentandodue risultati che rappresentano un argomento valido a favore del lavoro svi-luppato da Moschovakis. Il primo, che costituisce il risultato principale dellasezione presente, dimostra la correttezza del calcolo della riduzione di FLRmentre il secondo rappresenta una variante intensionale del Primo teoremadi Ricorsione di Kleene.

3.4.1 Semantica denotazionale su strutture funzionali

Di seguito presentiamo il livello denotazionale: l’interpretazione denotazio-nale di un termine in FLR (la sua denotazione) e una funzione (un funzio-nale). Prima di dare la definizione di denotazione abbiamo pero bisogno diintrodurre alcuni concetti base.

Definizione (Struttura funzionale) 19. Una struttura funzionale con se-gnatura τ = (B, S, d) e una coppia A = (U ,F), dove U e un universo purosu B e dove F = {F(f) | f ∈ S} e una famiglia di funzionali monotoni su U ,tali che F(f) ha tipo d(f).

Definizione (Assegnamento) 20. Un assegnamento su di una strutturafunzionale A e una qualsiasi funzione parziale π definita su tutte le variablifp e su “alcune” variabili base di FLR 16 e che associa ad ogni variabile x unoggetto (base o fp) in A con lo stesso tipo di x.Possiamo individuare un ordine parziale sugli assegnamenti cosı definito:

π ≤ ρ ⇐⇒ (∀x)[π(x) ↓ ⇒ [ρ(x) ↓ & π(x) ≤ ρ(x)]].

Definiamo ora una funzione parziale

val : Espressioni × Assegnamenti ⇀ Oggetti diA,

tale che valgono le seguenti proprieta:

16Con “alcune” intendiamo che non e richiesto che sia una associazione totale, definitasu tutte le variabili base.


1. val(t, π) e definita su tutte le espressioni fp t e se val(t, π) ' w, allorail tipo di w e il medesimo dell’espressione t;

2. val e monotona, nel senso che, per ogni termine t abbiamo:

[val(t, π) ' w & π ≤ ρ]⇒ val(t, ρ) ' w,

e per ogni espressione fp t abbiamo:

π ≤ ρ⇒ val(t, π) ≤ val(t, ρ);

3. val(t, π) dipende solamente dai valori che π assume sulle variabili cheoccorrono libere in t.

Di seguito diamo le definizione di val secondo clausole ricorsive corrispondentiai casi T1–T5:V1. val(x, π) ' π(x).V2. val(p(t1, . . . , tn), π) ' π(p)(val(t1, π), . . . , val(tn, π)).V3. val(λ(u)t, π) ' λ(u)val(t, π[u/u]), dove π[u/u] indica l’assegnamentoche assume lo stesso valore su tutte le variabili eccetto le variabili base chesi trovano nella lista u, sulle quali agisce secondo la sostituzione u← u.V4. val(f[t1, . . . , tn], π) ' F(f)[val(t1, π), . . . , val(tn, π)].V5. Se t ≡ rec(u1,p1, . . . ,un,pn)[t0, t1, . . . , tn], sia per i = 0, . . . , n:

hi[ui, p1, . . . , pn] ' val(ti, π[ui/ui,p1/p1, . . . ,pn/pn]),

dove l’assegnamento π[ui/ui,p1/p1, . . . ,pn/pn] e ottenuto a partire da π mo-dificando solamente i valori in corrispondenza delle variabili ui,p1, . . . ,pn,cambiandoli in ui, p1, . . . , pn

17. Il punto 2. ci dice che ciascun hi e un funzio-nale monotono, applicando ora i risultati di teoria delle equazioni ricorsiveenunciati nella sezione 3.2.3 otteniamo che il sistema di equazioni:

h0[u0, p1, . . . , pn] ' p0(u0)h1[u1, p1, . . . , pn] ' p1(u1)

...hn[un, p1, . . . , pn] ' pn(un)

ammette simultaneamente soluzioni minime, p0, p1, . . . , pn.Inoltre se poniamo:

17u0 e la variabile individuale vuota.


val(t, π) ' p0( )' val(t0, π[p1/p1, . . . ,pn/pn]),

val(t, π) e monotona rispetto a π.

Ora siamo pronti per dare la definizione centrale di questa sezione:

Definizione (Denotazione) 21. Sia x = x1, . . . ,xn una sequenza di varia-bili base o fp contenente tutte le variabili libere che occorrono in un terminet. La denotazione di t, nella struttura funzionale A, relativamente ad x, e ilfunzionale:

den(x, t) : X ⇀ W, den(x, t)(x) ' val(t, πx),

dove X e lo spazio prodotto che ha come tipo quello della sequenza x, W el’insieme base che ha come tipo quello del termine t e per ogni x = x1, . . . , xn,πx e un assegnamento qualsiasi che associa xi ad xi per ogni i, 0 ≤ i ≤ n.

Esempio. Data la struttura funzionale N = {N, 0, succ, pred, zero}, ri-prendiamo il termine:

x · y ≡ rec(i, times, j, plus)[times(y),if zero[i] then 0 else plus(times(pred[i]))if zero[j] then x else succ[plus(pred[j])]],

La denotazione del termine x · y relativamente alle variabili x, y e lafunzione che ad ogni x, y assegna il valore del minimo punto fisso del sistemadi equazioni:

p0( ) ' times(y),times(i) ' if i = 0 then 0 else plus(times(i− 1)),plus(j) ' if j = 0 then x else plus(j − 1) + 1

che e esattamente la funzione prodotto applicata a x ed y.

Definizione (Equivalenza denotazionale) 22. Diciamo che due terminisono denotazionalmente equivalenti se assumono lo stesso valore per ogniassegnamento e su ogni struttura, cioe:

s ∼den t ⇐⇒ (∀A,∀π in A)val(s, π) ' val(t, π).


Per concludere, presentiamo due risultati che mostrano delle proprietabase di val rispetto alla congruenza ≡c ed alla riduzione ∼E: il primo mettein luce l’indistinguibilita sostanziale dei termini congruenti mentre il secondoevidenzia che tutte le regole di riduzione preservano i valori.

Proprieta 1. Se t ≡c s, allora su ogni struttura funzionale A e per ogniassegnamento π in A, risulta:

val(t, π) ' val(s, π).

Proprieta 2. Per ogni struttura funzionale A, per ogni assegnamento π inA e per ogni contesto E, risulta:

s ∼E t⇒ val(s, π) ' val(t, π).

3.4.2 Semantica intensioniale

In questa sezione vedremo che l’intensione di un termine t e il ricorsore ad essoassociato che ne calcola la denotazione. Ricordiamo che avevamo utilizzatola notazione:

f = [f0, f1, . . . , fn] : X ↪→ W

per indicare un ricorsore, e

f : X ⇀ W ,

per la denotazione del ricorsore f .

Per evitare di perdere il filo del discorso enunciamo immediatamente ilrisultato principale:

Risultato principale. Fissata una struttura di ricorsore A:

(a) C’e un unico modo di associare ad ogni termine t, ogni contesto E edogni lista di variabili ~x ≡ x1, . . . , xk che contiene tutte le variabili libere in t,un ricorsore:

int(~x, E)t : X ↪→ W ,

dove X e lo spazio con lo stesso tipo della lista ~x e W e l’insieme base contipo il valore di t, tale che siano verificate le seguenti condizioni:


1. int(x1, . . . , xk, E)xi = [λ(x1, . . . , xk)xi].

2. Se t1, . . . , tn sono immediati in E, allora:

int(~x, E)p(t1, . . . , tn) = [den(~x, p(t1, . . . , tn))].

3. Se t1, . . . , tn sono immediati in E ed f e intepretato in A come ilricorsore f, allora:

int(~x, E)f[t1, . . . , tn](x) = f(den(~x, t1)(x), . . . , den(~x, tn)(x)).

4. Se t non e immediato in E e a, b sono sequenze di termini, allora:

int(~x, E)p(a, t, b) = rec(r)[int(r,~x, E ∪ {r})p(a, r( ), b), int(r,~x, E)t].

5. Se t non e immediato in E e a, b sono sequenze di termini o di λ-termini, allora:

int(~x, E)f[a, t, b] = rec(r)[int(r,~x, E ∪ {r})f[a, r( ), b], int(r,~x, E)t].

6. Se λ(u)t non e immediato in E e a, b sono sequenze di termini o diλ-termini, allora:

int(~x, E)f[a, λ(u)t, b] = rec(u, r)[int(r,~x, E ∪ {r})f[a, r, b], int(u, r,~x, E)t].

(b) Sia ~p ≡ p1, . . . , pn, se per i = 0, . . . , n, vale:

fi = int(ui, ~p,~x, E ∪ {ui, ~p})ti,allora:

int(~x, E)rec(u1, p1, . . . , un, pn)[t0, t1, . . . , tn] = rc[f0, f1, . . . , fn],

dove rc e l’ovvia versione semantica del costrutto rc.

(c) L’intensione di un termine ne calcola la denotazione, cioe per ognicontesto E, risulta:

int(~x, E)t(x) = den(~x, t)(x).

(d) Il calcolo della riduzione di FLR e corretto rispetto alle intensioni:

s ∼E t ⇒ int(~x, E)s ' int(~x, E)t.

L’idea della dimostrazione e di utilizzare un escamotage: definiamo l’in-tensione di un termine a partire dalla sua forma normale in modo da ottenerel’unicita attraverso il risultato principale della sezione sulla sintassi di FLR,l’unicita della forma normale.


Intensioni

Se in una struttura funzionale riduciamo il termine t nella sua forma normale:

nf(t, E) ≡ rec(u1, p1, . . . , un, pn)[t0, t1, . . . , tn],

allora dovremmo porre:

int(~x, E)t = [den(~p,~x, t0), den(u1, ~p,~x, t1), . . . , den(un, ~p,~x, tn)].

Per parlare dell’intensione di un termine abbiamo prima bisogno di intro-durre una generalizzazione della Definizione 20 di struttura funzionale:

Definizione (Struttura di ricorsore) 23. Una struttura di ricorsore contipo τ = (B, S, d) e una coppia

A = (U ,F),

dove U e un universo puro su B ed F = {F(f) | f ∈ S} e una famiglia diricorsori, tale che per ogni f ∈ S la denotazione F(f) ha tipo d(f).

In generale seguiremo il seguente approccio: prima di tutto ad ogni strut-tura di ricorsore A associamo una struttura funzionale A◦, poi definiamoun meccanismo di traduzione del linguaggio di A in quello di A◦ ed infinecalcoliamo le intensioni in quest’ultimo.

Definizione (Espansione funzionale) 24. Ad ogni struttura di ricorsoreA e possibile associare la sua espansione funzionale A◦, rimpiazzando ogniricorsore f = [f0, f1, . . . , fn] in A con i funzionali f0, f1, . . . , fn. La segnatura(B, S, d)◦ di A◦ e una espansione della segnatura di A; il simbolo f, che erail nome di f in A, viene ad essere il nome di f0 ed introduciamo i simbolif1, . . . , fn per le parti di f.

Definizione (Traduzione) 25. Data una struttura fissata A, con segnaturaτ , ad ogni termine o λ-termine t ∈ FLR(τ) ed ogni contesto E, e associatala traduzione tr(t, E), un’espressione in FLR(τ ◦) con lo stesso tipo di t.tr(t, E) e definita per ricorsione su t:

1. Se t e una variabile, allora tr(t, E) ≡ t.

2. tr(p(t1, . . . , tn), E) ≡ p(tr(t1, E), . . . , tr(tn, E)).

3. tr(λ(u)t, E) ≡ λ(u)tr(t, E ∪ {u}).

4. Per questo caso iniziamo con un esempio, supponiamo che sia:


t ≡ f[w, s, λ(u)t∗],

dove w e immediato in E ed s e λ(u)t∗ invece no. Supponiamo che fabbia n + 1 parti in A di modo che abbiamo i simboli f, f1, . . . , fn inFLR(τ ◦). Poniamo:

tr(f[w, s, λ(u)t∗], E) ≡ rec(v1, q1, . . . , vn, qn, r, u, p)[f[~q, w, r( ), p], f1[v1, ~q, w, r( ), p], . . . , fn[vn, ~q, w, r( ), p],tr(s, E), tr(t∗, E ∪ {u})],

dove r, p e le vi e qi sono variabili fresh. Nel caso generale traduciamoallo stesso modo gli argomenti di f che non sono immediati in E elasciamo gli altri immutati.

5. Sia

t ≡ rec(u1, p1, . . . , un, pn)[t0, . . . , tn],

allora calcoliamo per ogni i la traduzione:

ti∗ ≡ tr(ti, E ∪ {ui, p1, . . . , pn}),

e poniamo:

tr(t, E) ≡ rec(u1, p1, . . . , un, pn)[t0∗, . . . , tn

∗].

La proprieta piu interessante che riguarda quest’operazione di traduzionee che preserva la relazione di equivalenza (intensionale), Definizione 23.

Fatto 1. Nelle ipotesi della definizione precedente, abbiamo:

s ∼E t ⇒ tr(s, E) ∼E tr(t, E),

inoltre se A e una struttura funzionale, allora per ogni t ed ogni contesto E,risulta:

t ∼E tr(t, E).

Ora siamo pronti per dare la seguente definizione:


Definizione (Intensione) 26. Fissiamo una struttura A, sia A◦ la suaespansione funzionale, supponiamo che ~x sia una lista di variabili che contienetutte le variabili libere di un qualche termine t e sia E un contesto. Se

nf(tr(t, E), E) ≡ rec(u1, p1, . . . , un, pn)[t0, . . . , tn]

e la forma normale (rispetto ad E) della traduzione di t, allora poniamo:

int(~x,E)t = [den(~x, t0), den(~x, t1), . . . , den(~x, tn)].

Nel caso in cui A sia una struttura funzionale, applicando il Fatto 1otteniamo:

Fatto 2. Se nf(t, E) ≡ rec(u1, p1, . . . , un, pn)[t0, t1, . . . , tn], allora

int(~x,E)t = [den(~x, t0), den(~x, t1), . . . , den(~x, tn)].

Algoritmi

Diamo ora la definizione di algoritmo dovuta a Moschovakis, lasceremo la di-scussione sulla sua ragionevolezza per il prossimo capitolo in cui metteremoa confronto i due lavori: quello di Gurevich e quello di Moschovakis. Con-cluderemo il capitolo enunciando un risultato che ne avvalla la plausibilita.

Definizione (Algoritmo) 27. Un algoritmo su di una struttura di ricorsoreA e un qualsiasi ricorsore

f = [f0, f1, . . . , fn] : X ↪→ W

sull’universo di A, tale che per una certa lista di variabili ~x con tipo quellodi X e per un certo termine speciale t(~x) le cui variabili libere sono tuttecontenute in ~x, vale

f = int(~x, ∅)t(~x).

Inoltre, le denotazioni degli algoritmi associati ad una struttura A prendonoil nome di funzionali ricorsivi di A.

Ricordando che il punto (c) del Teorema principale ci dice che:

int(~x, E)t(x) = den(~x, t)(x)


otteniamo il seguente:

Fatto 3. I funzionali ricorsivi di una struttura A sono esattamente le deno-tazioni dei termini speciali su A, da cui segue che A e la struttura funzionalead essa associata A hanno gli stessi funzionali ricorsivi.

Il seguente teorema rappresenta un risultato che, come vedremo, puoessere messo in relazione al primo teorema di ricorsione di Kleene, per questomotivo prende il nome di:

Teorema intensionale di ricorsione. Sia f un algoritmo di una strutturadi ricorsore A, allora l’espansione (A, f) ha gli stessi algoritmi di A.Piu precisamente, se t(~x) e un termine ∅–irriducibile e:

f = int(~x, ∅)t(~x),

e se s(f) e un termine del linguaggio dell’espansione (A, f), irriducibile inun qualche contesto E, allora per ogni lista ~y di variabili che contiene tuttele variabili libere di s(f), vale:

int(~y, E)s(f) = int(~y, E)s(λ(~x)t(~x)).

In buona sostanza tale teorema afferma che la classe degli algoritmi as-segnati ad una certa struttura fissata A non e espandibile via definizioniimplicite od esplicite (a partire dagli elementi di A o da essi derivati tramitele regole del FLR). Per meglio comprendere il teorema precedente ed il suolegame con il primo teorema di ricorsione di Kleene e utile confrontarlo conla sua variante estensionale, che deriva da esso notando che se due strut-ture hanno gli stessi algoritmi allora necessariamente hanno anche gli stessifunzionali ricorsivi:

Teorema estensionale di ricorsione. Se f e un funzionale ricorsivo di unastruttura A, allora l’espansione (A, f) ha esattamente gli stessi funzionaliricorsivi di A.

Se consideriamo come struttura quella dell’aritmetica N, questo teoremarappresenta una versione del primo teorema di ricorsione di Kleene, teoremaXXVI in [28]. Kleene considerava questo teorema come un elemento forte afavore della Tesi di Church poiche esso ci dice che non si puo “sfuggire” allaclasse delle funzioni parziali ricorsive via definizioni implicite. Allo stessomodo Moschovakis considera il suo Teorema intensionale di ricorsione comeun forte argomento a favore della (sua) congettura che gli algoritmi sianomodellabili tramite i ricorsori.

Capitolo 4

Confronto e conclusioni

Il presente capitolo, conclusivo, si suddivide in due parti: nella prima presen-tiamo il “botta e risposta” tra Gurevich e Moschovakis mentre nella secondaesponiamo le nostre osservazioni in merito ai lavori dei due studiosi. Lapresentazione della nostra critica alle Abstract State Machines, presentata aGurevich e Borger e la loro risposta apparetngono a questa seconda parte,sezione 4.2.4.

4.1 Moschovakis vs. Gurevich

Abbiamo gia notato che sia Moschovakis che Gurevich iniziano ad interessar-si del problema contemporaneamente, intorno alla meta degli anni ottanta;abbiamo anche accennato al fatto di come i loro approcci rispecchino dueimpostazioni che hanno caratterizzato la ricerca sulla trattazione formale deilinguaggi di programmazione: la semantica operazionale e quella denotazio-nale. Queste due semantiche sono intimamente legate ai primi paradigmi diprogrammazione: il paradigma imperativo e quello funzionale. La semanticaoperazionale e stata la prima in ordine temporale dato che rappresenta ilcorrispettivo piu naturale di un linguaggio di programmazione imperativo edella visione di Von Neumann del calcolatore (come macchina a stati): secon-do quest’impostazione i programmi vengono identificati con procedimenti ditrasformazione dello stato globale di una certa macchina (inizialmente fisicapoi virtuale). Si potrebbe affermare, ed in certa misura corrisponde al vero,che la semantica denotazionale si e sviluppata in contrapposizione alla pri-ma e come risposta alle problematiche che la prima poneva, prima fra tuttela gestione poco “pulita” e talvolta “pericolosa” 1 degli effetti collaterali dicerte istruzioni, sullo stato globale. Secondo quest’impostazione, sviluppata

1Si veda lo storico articolo [15] di Edsger Dijkstra.

91

92 CAPITOLO 4. CONFRONTO E CONCLUSIONI

da Dana Scott in [40], i programmi sono identificati con punti fissi di par-ticolari spazi di funzioni. Era dunque normale che nascesse una discussionetra i due studiosi riguardo al problema “riscoperto” della formalizzazione delconcetto di algoritmo; purtroppo tale dialettica, svoltasi negli articoli [36] e[4] rispettivamente di Moschovakis e di Gurevich, e stata viziata da numeroseincomprensioni da entrambe le parti, di modo che non se ne e potuto trarreil massimo beneficio per una migliore comprensione del problema in se.Di seguito presenteremo la critica portata da Moschovakis all’approccio diGurevich e la risposta di quest’ultimo.

4.1.1 Moschovakis critica Gurevich

Nell’articolo [36] Moschovakis “attacca” l’impostazione adottata da Gurevi-ch sostenendo, sostanzialmente, che l’approccio operazionale da lui seguitoe inadeguato poiche costringe a pensare a livello “troppo basso”, al livellodelle macchine per intenderci. Egli e disposto a riconoscere l’importanzadelle macchine ed in effetti nella sua teoria utilizza le stesse macchine (se-quenziali), gli iteratori, per modellare le implementazioni degli algoritmi; pergli algoritmi in se sostiene pero che c’e bisogno di una nozione piu astratta:quella di ricorsore.La sua e in effetti la critica mossa piu di frequente alla semantica operazio-nale dei linguaggi di programmazione e cioe che essa impone un livello diastrazione troppo basso. Come esempio Moschovakis porta quello degli algo-ritmi ricorsivi, egli pone la seguente domanda: se gli algoritmi sono macchinequal’e la macchina corrispondente al Mergesort? Nella sezione 3.2.2 abbiamoesposto i problemi cui si va incontro accettando di identificare gli algoritmicon macchine; ricordiamo qui che essi ammontano a due problemi essenziali:

Non naturalezza Il primo riguarda il fatto che la ricorsione e un’astrazio-ne che nelle macchine dev’essere emulata/implementata in qualche modo; cisono diverse tecniche ma il problema di base e che qualsiasi tecnica adottiamotra di esse, la macchina corrispondente, che otteniamo, risulta molto “distan-te” dall’algoritmo A di partenza e le caratteristiche intrinseche di A vengono“offuscate” dai tecnicismi propri dell’emulazione scelta. Come esempio pos-siamo pensare di dover analizzare le proprieta base del Mergesort (come ilcalcolo del numero minimo di confronti) a partire dal programma corrispon-dente, eseguibile su un calcolatore, che fa uso dello stack per la gestione dellaricorsione: e chiaro che il fatto di ragionare a questo livello non farebbe altroche complicare inutilmente le cose!

4.1. MOSCHOVAKIS VS. GUREVICH 93

Non unicita E naturale vedere il procedimento che associa ad ogni algo-ritmo ricorsivo una macchina come un processo di compilazione. Il problemaprincipale e dato dalla non unicita di tale processo; non e chiaro in base aquali criteri se ne possa scegliere, fra i tanti possibili, uno canonico: qualelinguaggio e quale macchina astratta e meglio scegliere?

4.1.2 La risposta di Gurevich

A queste obiezioni Gurevich risponde nell’articolo [4] in cui viene mostratauna Abstract State Machine che modella il Mergesort.Il punto cruciale sta nel fatto che Moschovakis come concetto piu astrattodi macchina considera l’iteratore che corrisponde ad una macchina la cuiesecuzione e inerentemente sequenziale e giustamente giunge alla conclusioneche non e possibile modellare tutti gli algoritmi tramite tale nozione; ineffetti la nozione di iteratore e praticamente identica al postulato di Temposequenziale proposto da Gurevich nella sua caratterizzazione ma esistonoanche ASM piu astratte che non rispettano tale postulato, ad esempio le ASMdistribuite. Gurevich nota che la critica di Moschovakis potrebbe quindi volerdire che non tutti gli algoritmi hanno una computazione sequenziale. Secondole parole stesse di Gurevich, il problema della gestione della ricorsione tramitele ASM rappresenta uno dei principali ostacoli all’accettazione della sua tesie per “sedare” ogni dubbio presenta un modello operazionale del Mergesort(tramite le ASM distribuite) che riportiamo di seguito.

Modello ASM del Mergesort

La modellazione del Mergesort in realta passa attraverso la definizione diuna particolare estensione del modello base delle Abstract State Machines:le ASM ricorsive; tale estensione e presentata in [24], articolo in cui dapprimasi estende la sintassi base delle ASM con il costrutto rec, se ne da’ la se-mantica ed infine si mostra un procedimento per trasformare/compilare unaASM ricorsiva in una ASM distribuita. Per non appesantire ulteriormente lapresente trattazione e dal momento che la comprensione del funzionamentodella ASM in questione e piuttosto intuitiva si e scelto di non fornire unapresentazione formale delle ASM ricorsive ma di procedere bensı presentan-do il programma ASM che modella il Mergesort e di spiegarne via via i puntisalienti.

Il programma Leggendo il programma in Figura 4.1 e facile notare che ilfunzionamento e piuttosto intuitivo, bisogna comunque fornire alcune spie-


if Mode = Initial then

Output := Sort(Input), Mode := Final

rec Sort(u)if Mode = Initial then

if |u| ≤ 1 then

Result := u, Mode := Final

else

v := Sort(h1(u))w := Sort(h2(u))Mode := Halfway

elseif Mode = Halfway then

Result := Merge(v, w), Mode := Final

rec Merge(v, w)

if Mode = Initial then

if v = ∅ then Result := welseif w = ∅ then Result := velseif v0 ≤ w0 then Result := 〈v0〉 ∗ Merge(tail(v),w)

else Result := 〈w0〉 ∗ Merge(v,tail(w))

Mode := Final

Figura 4.1: Programma ASM del Mergesort


gazioni. Come anticipato ci serviamo delle ASM distribuite: l’idea e che ognichiamata ricorsiva corrisponde all’invocazione di un agente supplementare ilcui compito e quello di eseguire il programma corrispondente ad una chia-mata rec. L’agente chiamante prende il nome di “signore” mentre l’agentechiamato prende il nome di “vassallo”, quest’ultimo una volta completatala computazione restituira il valore al suo signore. La traduzione da ASMricorsive ad ASM distribuite essenzialmente consiste nell’esplicitare la crea-zione dei vassalli ed il passaggio dei parametri e del risultato. Come si puovedere il programma e composto essenzialmente da tre parti: il controlloiniziale, che corrisponde al main, piu i due sottoprogrammi che iniziano conil costrutto rec. I due sottoprogrammi individuano quindi due tipi diversidi vassallo, ciascuno di essi restituira al suo signore il valore calcolato nellavariabile Result. Per comprendere il funzionamento globale e importantenotare che i due sottoprogrammi assumono il comportamento proprio deiprogrammi ASM e cioe una volta attivati, essi entrano in un ciclo che iteracontinuamente fino a che la variabile Mode assume il valore Final.

Convenzioni Chiaramente se la variabile Result fosse globale il suo va-lore potrebbe essere sovrascritto in maniera incoerente, in effetti in [24] sie stabilita la convenzione che ogni variabile “condivisa”, che occorre in unblocco rec, abbia un ulteriore parametro implicito che la rende in realta lo-cale: scrivendo Result intendiamo dunque Result′(a), in cui ciascun agenteinterpreta a con la variabile Self che identifica l’agente stesso 2. A questaconvenzione aggiungiamo anche l’assunto che all’inizio della computazione lavariabile Mode di tutti gli agenti vale Initial e la loro esecuzione terminaquando essa assume il valore Final.

Numero di confronti Vogliamo determinare il numero di confronti che ilprogramma ASM in Figura 4.1 effettua per ordinare una stringa u di lun-ghezza n = 2m (per semplicita adottiamo le stessa assunzione fatta da Mo-schovakis che n sia una potenza di 2). Analizziamo il flusso di informazionedel programma: inizialmente il programma principale (l’agente–main) creaun agente–sort cui passa come parametro la stringa u, alla fine questo agenterestituisce la stringa ordinata e la computazione termina. Tale agente, tro-vandosi in modalita Initial, crea due vassalli, due agenti–sort, ciascuno echiamato ad ordinare una sottostringa di lunghezza la meta di quella iniziale,dunque 2m−1. In generale, iniziando a contare da 0, al passo k avremo 2k

agenti–sort attivi, ciascuno col compito di ordinare una sottostringa di lun-ghezza 2m−k. La creazione di vassalli–sort termina quando le sottostringhe

2Naturalmente lo stesso vale anche per la variabile Mode.


hanno raggiunto lunghezza 1 (banalmente ordinate); a questo punto ciascunagente–sort (tranne quelli dell’ultimo livello) chiama un agente–merge perordinare le due sottostringhe corrispondenti. Notando che il numero di con-fronti non supera il numero di agenti–merge, dal momento che ciascuno diessi effettua un confronto se entrambe le stringhe sono non vuote, per otte-nere il limite superiore cercato ci basta calcolare il numero di agenti–mergeattivati nel corso della computazione. Ogni agente–sort invoca esattamenteun solo agente–merge, che ad ogni passo (non banale) effettua un controllo,aggiunge l’elemento minore in testa ed attiva un altro agente–merge. Al li-vello k < m ogni agente–merge deve eseguire la fusione di due sequenze dilunghezza 2m−k−1, per cui il numero di agenti–merge che discendono da unagente–sort a livello k e al massimo pari a 2m−k, ognuno (tranne l’ultimo) ef-fettua un confronto. Un agente–sort a livello k genera dunque meno di 2m−k

confronti; contando tutti i 2k agenti–sort, otteniamo meno di 2m confronti edal momento che dobbiamo considerare m livelli il numero massimo di con-fronti effettuato durante una computazione e pari a 2m ·m. Considerato che|u| = n = 2m, il numero di confronti effettuati ammonta a n · log n, che equello che ci si aspettava.

Gestione della memoria ed implementazioni E da notare che questaimplementazione non fa uso di uno stack, la gestione della memoria e dun-que locale invece che globale. Questo aspetto e importante perche la gestionetramite stack va bene se le chiamate avvengono in modo sequenziale ma pergestire casi piu generali in cui l’ordine delle chiamate e lasciato libero no. Dalmomento che fa uso, in ultima analisi, di ASM distribuite, l’implementazio-ne presentata ammette vari tipi di esecuzione: quella in cui viene ordinataprima la sottostringa destra e poi quella sinistra, oppure quella che agisce inordine contrario, oppure quella in cui le due procedure di ordinamento si al-ternano, oppure ancora quella, nel caso piu generale possibile, in cui le mossedi un agente–sort si alternano a quelle di un agente–merge 3. Cosı facendootteniamo quindi una macchina che modella il Mergesort e “contiene” tuttele diverse implementazioni citate da Moschovakis in [36], quando argomentache un modello operazionale non va bene perche dovrebbe adottare una diqueste strategie e risulterebbe quindi, in ogni caso, arbitrario.

Osservazione Precedentemente abbiamo mostrato la ASM con la qualeGurevich risponde alla critica di Moschovakis e abbiamo detto che si tratta

3In questo caso chiaramente i due agenti in questione devono appartenere a linee diesecuzione differenti: l’agente–merge concorrente non puo appartenere all’insieme degliagenti attivati dall’agente–sort o dai suoi vassalli!


di una ASM (implicitamente) distribuita. A prima vista il programma ASMpresentato sembra convincente ma se ci fermiamo un momento a rifletterenotiamo che adottare il paradigma distribuito per spiegare la ricorsione e unpo’ come “sparare ad una mosca con un cannone”! E stato espresso in modoun po’ scherzoso ma il problema e serio dal momento che lo sforzo delle ASMmira a renderci in grado di modellare qualsiasi algoritmo al suo naturale li-vello di astrazione; vedere la ricorsione come la computazione effettuata dauna serie di agenti tra loro indipendenti non e il modo piu naturale per mo-dellare questa particolare modalita di calcolo. In genere quello che ciascunodi noi “vede” quando pensa al processo di calcolo ricorsivo e un solo agenteche si muove effettuando una visita in profondita dell’albero di ricorsionecorrispondente. Questo aspetto e stato notato e trattato da Borger e Bolo-gnesi che in [18] hanno sviluppato una estensione delle ASM sequenziali (unagente solo) che si basa sul passaggio del risultato ad ogni passo di ricorsioneed il cui procedimento di calcolo coincide con l’idea intuitiva di ricorsione.Questa versione di ASM ricorsive e sicuramente piu convincente di quelloprecedentemente presentato ma la sua trattazione approfondita richiedereb-be un capitolo a parte dato che si basa su di una diversa definizione base diASM 4.

4.1.3 Gurevich critica Moschovakis

La risposta di Gurevich e ad ogni modo forte, anche in vece dei successiottenuti dalla comunita dei ricercatori delle ASM che presenteremo nellasezione seguente, ed in effetti non ci sono state ulteriori critiche (per lo menoufficiali) alla validita del formalismo delle ASM. A sua volta Gurevich critical’approccio adottato da Moschovakis da due punti di vista:

Interpretazione delle equazioni ricorsive Nella parte finale di [4] eglisostiene che le equazioni ricorsive con cui Moschovakis definisce il Mergesortindividuano delle funzioni e non contengono alcun algoritmo:

Le equazioni (1) e (2) forniscono una specifica non un algoritmo.Come dicevi, esse definiscono le funzioni sort e merge. Ma ameno di fornire o di assumere informazioni ulteriori, potremmo“implementare” questa definizione di ordinamento utilizzando ilQuicksort e verificando poi che il risultato soddisfa la (1).

4Si tratta della cosiddetta Turbo–ASM sviluppata da Borger ed altri, che ai costrut-ti base aggiunge quello per la sequenzializzazione e quello per l’iterazione, per la suaspiegazione e tutti i dettagli si veda [17].


Certamente, nella semantica denotazionale un’equazione ricorsiva e pensatacome una definizione implicita di una funzione che e il minimo punto fissorispetto ad un certo funzionale ma abbiamo visto che Moschovakis sviluppaun’ulteriore semantica, ch’egli chiama intensionale, dei sistemi di equazioniricorsive che associa ad ogni sistema un insieme di funzionali che costituisconoun ricorsore. Questa critica e dunque frutto di un fraintendimento da partedi Gurevich.

Arbitrarieta del modello In [8] Gurevich esprime il proprio scetticismoriguardo alla scelta dei ricorsori, come nozione che funga da modello per glialgoritmi. Il modello proposto da Moschovakis non sembra scalabile rispet-to, ad esempio, ad algoritmi che interagiscono con un “ambiente esterno”.Inoltre, secondo le parole stesse di Gurevich:

Non siamo a conoscenza di alcun modo per derivare da principibase la tesi che gli algoritmi sono ricorsori.

Essenzialmente questa e una critica che riguarda il (possibile) primato diuna caratterizzazione assiomatica su di una basata sulla teoria degli insiemi:torneremo su questo aspetto nella sezione 4.2.2.

4.2 Confronto e conclusioni

Nella sezione precedente abbiamo presentato la dialettica sviluppatasi traMoschovakis e Gurevich, nella sezione presente esporremo le nostre osserva-zioni in merito alle due caratterizzazioni proposte.

4.2.1 Implementazioni

Bisogna dire innanzitutto che Moschovakis da’ un’importanza maggiore alconcetto di implementazione in una nuova trattazione dei fondamenti del-l’informatica. La motivazione di tale primato e naturale se consideriamoche, come dice egli stesso in [35]:

Il ruolo corretto di una “definizione in teoria degli insiemi” di unanozione matematica C e non quello di dirci in ultima analisi, intermini metafisici che cosa sono esattamente i C–oggetti, bensıquello di identificare e di delineare le loro proprieta matematichefondamentali.

Nella sezione 3.2.5 del secondo capitolo abbiamo visto che le implementazio-ni sono iteratori e che ad ogni iteratore corrisponde un ricorsore. Il fatto

4.2. CONFRONTO E CONCLUSIONI 99

essenziale e che algoritmi ed implementazioni sono modellati da nozioni so-stanzialmente diverse: c’e un confine netto tra le due entita.

Nello sviluppo delle ASM, la trattazione del concetto di implementazionee stata svolta nell’area di studio delle applicazioni riguardanti l’Ingegneriadel Software 5. In questo ambito il confine tra il concetto di algoritmo equello di implementazione e invece “sfumato”: date due ASMM edM′, seM′ e un raffinamento di M 6, M puo essere vista come una specifica perM′; invertendo il ragionamento M′ puo essere considerata come un’imple-mentazione diM. Il concetto di implementazione e quindi relativo poiche euna questione di “ruolo”: la stessa ASM puo essere vista a seconda dei casicome specifica o come implementazione. A differenza della strada seguita daMoschovakis, c’e quindi uniformita di concetto tra algoritmi ed implementa-zioni. Gurevich stesso non si e occupato in modo esplicito del problema delconcetto di implementazione, forse anche perche lo riteneva meno importanteuna volta stabilitane la relativita.

Ad ogni modo, a nostro parere un’analisi piu approfondita del rappor-to tra un algoritmo e le sue implementazioni deve senz’altro far parte diuno studio che si ponga come obiettivo quello di investigare i fondamentidell’informatica.

4.2.2 Assiomatica vs. Teoria degli insiemi

Come gia accennato nell’introduzione e poi nella sezione 4.1.3 le due for-malizzazioni proposte appartengono a due generi diversi: quella sviluppatada Gurevich e una definizione di tipo assiomatico mentre quella sviluppa-ta da Moschovakis e una definizione di teoria degli insiemi. Sviluppandoun’assiomatizzazione A di un concetto C si cerca di catturarne le caratte-ristiche principali (tramite dei postulati) e si definisce poi il concetto comequell’oggetto che soddisfa gli assiomi di A. Adottando invece la teoria degliinsiemi si cerca un oggetto (gia esistente) appartenente a tale teoria che possaessere usato come modello di C, nel senso che le sue caratteristiche devonocombaciare quanto piu possibile con quelle di C. La differenza principaleconsta nella granularita: la prima ha una granularita piu fine, in quanto lasua validita si suddivide nella validita dei singoli assiomi che possono essereoggetto di discussione (e di modifica eventualmente); la seconda, invece, epiu monolitica come proposta, o la si accetta in toto oppure niente. Questo

5Una buona trattazione si trova nel libro [17] di Borger e Stark.6Per una definizione formale di raffinamento si veda il gia citato libro [17].


e anche il motivo per cui una definizione assiomatica e piu facilmente sca-labile: si possono mantenere certi assiomi e modificarne altri, mantenendocomunque uniformita d’impostazione. Cosı e stato fatto, ad esempio, perla caratterizzazione degli algoritmi paralleli in cui si sono mantenuti i pri-mi due postulati del caso sequenziale (stati astratti e tempo sequenziale) esi sono introdotti nuovi assiomi al posto di quello di esplorazione limitata.L’impostazione assiomatica risulta in certa misura piu convincente poiche daessa derivano dei teoremi di caratterizzazione, come il teorema presentato insezione 2.3.2, che mostrano la solidita della scelta degli assiomi.

4.2.3 Critica a Moschovakis

In filosofia si usa il termine rasoio di Occam per indicare il principio secondoil quale tra due teorie che spiegano un fenomeno dato, bisogna scegliere quellapiu semplice, nel senso di quella che necessita del minor numero assunzioni.Tale principio e alla base di tutte le scienze naturali e ha guidato lo sviluppodi tutte le teorie scientifiche. La critica principale al lavoro di Moschovakise proprio questa: la tesi che gli algoritmi siano modellabili tramite ricorsorinecessita di ben piu assunzioni rispetto agli “scarni” tre postulati avanzatida Gurevich!Inoltre in paragone a quello delle ASM il formalismo dei ricorsori risultacomplesso: basandosi sulla teoria dei punti fissi e della ricorsione astratta,essa richiede conoscenze con cui molti laureati in informatica non hannodimistichezza. Si puo obiettare che gli intenti erano diversi in partenza eche lo sforzo di Gurevich e stato fin dall’inizio guidato da considerazionidi applicabilita pratica. In ogni caso la teoria che ne e risultata e di piufacile comprensione e se si pensa di voler proporre alle nuove generazioni diinformatici un modo formale di considerare gli algoritmi, la scelta ricadrebbepiu facilmente sulle Abstract State Machines.Senza dubbio il principio della semplicita deve servirci da guida anche inquesto caso.

4.2.4 Critica a Gurevich

ASM e vincoli sulla Calcolabillita ed Implementabilita

Abbiamo notato piu volte nel corso della nostra trattazione che nell’impo-stazione delle Abstract State Machines e compito del “programmatore” as-sicurarsi che la computazione sia “realizzabile”. Questo aspetto si riconducea due proprieta:


1. Gli stati della ASM devono essere implementabili.

2. Le funzioni della ASM devono essere perlomeno7 calcolabili nel sensodi Church–Turing.

E piu che normale chiedersi se questo sia ragionevole. La liberta ottenutanon imponendo questi vincoli (apparentemente necessari) e quella che ci per-mette di liberarci dalle limitazioni degli approcci operazionali classici; se ilmodello ASM stesso dovesse assicurare la realizzabilita di una computazione,esso dovrebbe di volta in volta scendere al livello di dettaglio sufficiente im-ponendo al programmatore una “visione” implementativa di cio che si vuolemodellare. Nell’impostazione adottata da Gurevich, invece, la descrizione adalto livello non e minimamente limitata e cio permette cosı di guadagnareil massimo grado di astrazione/generalita possibile. Concludiamo citandol’analisi del modello ASM fatta da Reisig [37]:

Questa e l’idea fondamentale delle ASM, come introdotte in [21]:solamente la rappresentazione simbolica della funzione di transi-zione deve essere finita, mentre questa restrizione non si applicaalla rappresentazione sottostante degli stati. Questo approccio ineffetti trascende i modelli di computazione standard.

Considerazioni epistemologiche

In [21] Gurevich riporta da dove trae origine la ricerca che lo ha portato alladefinizione delle Abstract State Machines:

Cercavo un modello operazionale 8 (con un particolare linguag-gio di programmazione) tale che ogni 9 algoritmo sequenziale,per quanto astratto, potesse essere simulato passo–passo da unamacchina di quel modello. Possiamo chiamare un tale modellouniversale rispetto agli algoritmi sequenziali. Il modello di Tu-ring e universale rispetto alle funzioni calcolabili ma non rispettoagli algoritmi. In essenza, la ASM–Thesis e che il modello ASMsequenziale e universale rispetto agli algoritmi.

7Perlomeno nel senso che altrimenti si rischia di entrare nell’ambito della non–calcolabilita; naturalmente sono “ammesse” anche classi piu ristrette di funzioni comead esempio quella delle funzioni calcolabili in tempo polinomiale.

8Nel testo originale c’e machine model.9Corsivo dell’autore.


Di seguito riportiamo gli enunciati delle tesi che giocano un ruolo principalenel discorso che stiamo trattando:

Tesi di Turing: per ogni funzione calcolabile in modo effettivo esisteun’opportuna MdT che la calcola.

Tesi implicita di Turing: ogni procedimento di calcolo effettivo puoessere simulato da un’opportuna MdT.

ASM–Thesis: per ogni algoritmo esiste un’opportuna ASM in grado disimularlo passo–passo (fissato un certo livello di astrazione).

Dato che la ASM–Thesis risulta essere un affinamento della Tesi impli-cita di Turing, per cercare di comprenderne appieno il significato l’abbiamoanalizzata in relazione al lavoro svolto da Turing. Dal momento che ognifunzione calcolata da una MdT e evidentemente calcolabile in modo effetti-vo, accettando la sua Tesi otteniamo una catterizzazione della calcolabilita,nel senso che essa ci dice che cosa effettivamente sono le funzioni calcolabili.Uno degli aspetti che rendono tale caratterizzazione convincente e che si basasu di un legame “biunivoco” tra la classe delle funzioni calcolabili da MdT(FMdT ) e la classe delle funzioni calcolabili in modo effettivo (Feff ):

(1) Feff → FMdT

(2) FMdT → Feff

E importante sottolineare che la Tesi di Turing stabilisce il legame in unsenso solo e cioe (1), mentre la validita del legame in senso contrario, (2),e stata lasciata implicita poiche evidente10. Seguendo questo percorso si equindi giunti ad una formalizzazione del concetto di funzione calcolabile uni-versalmente accettata.Vogliamo ora vedere che cosa succede se proviamo ad applicare lo stesso sche-ma per indagare l’identita del concetto di algoritmo. A questo punto, primadi proseguire e importante sottolineare che la nostra analisi si restringe alconcetto di algoritmo nel senso classico, intuitivo del termine, come sequen-za (finita) di istruzioni la cui esecuzione risolve, in modo deterministico, unproblema dato.Per formalizzare il concetto di algoritmo bisogna qundi trovare un legame

10Bisogna anche notare che ai fini dei suoi intenti, dimostrare l’indecidibilita dell’En-tscheidungsproblem di Hilbert, Turing aveva bisogno solamente di (1): egli dimostra chenon esiste alcuna MdT in grado di calcolare tale funzione, da cui ne consegue che essa nonpuo appartenere ad Feff .


tra la classe degli algoritmi e quella delle ASM allo stesso modo di come estato fatto per la formalizzazione del concetto di funzione calcolabile in modoeffettivo:

(1) Alg→ ASM(2) ASM→ Alg

(1) corrisponde proprio alla ASM–Thesis che accettiamo come valida (in baseall’analisi che abbiamo precedentemente esposto); la (2) invece dice che adogni ASM corrisponde un algoritmo. Se ci fermiamo a riflettere su questosecondo punto (che a prima vista sembrerebbe la parte piu semplice) notiamoche la (2) non e verificata. E infatti possibile definire delle ASM che, al gradomassimo di astrazione, sono essenzialmente delle specifiche di un algoritmoed in quanto tali non riconoscibili come algoritmi (nel senso intuitivo deltermine). Ad esempio, la seguente:

begin d := gcd(a,b) end

e a tutti gli effetti una ASM ma ben poche persone ammetterebbero che essarappresenti un algoritmo dato che non ci dice nulla su come venga calcolatoil valore gcd(a,b), quale che sia l’interpretazione del nome di funzione gcd.Tale caratteristica non e certo una dimenticanza da parte degli sviluppatoridelle ASM ma, come abbiamo messo in luce piu volte nel corso della nostratrattazione, si tratta di una ben precisa scelta programmatica: cosı facendosono ammesse anche delle descrizioni ad alto livello, delle specifiche appun-to, di sistemi di cui inizialmente ignoriamo e vogliamo ignorare 11 i dettagliimplementativi; l’idea di base e che il comportamento globale del sistema faastrazione da questi ultimi e puo essere studiato a prescindere da essi.Possiamo concludere che cio che e stato formalizzato, a partire dalla ASM–Thesis, non e tanto il concetto di algoritmo bensı quello (piu generale) disistema di calcolo algoritmico: un sistema di calcolo cioe che esibisce uncomportamento algoritmico12. Notiamo innanzitutto che il concetto di algo-ritmo rappresenta un caso particolare di quest’ultimo poiche un sistema dicalcolo algoritmico S puo anche essere una specifica mentre il primo, doven-do esplicitare come vada eseguito il procedimento di calcolo, puo essere vistocome una implementazione di S; se il comportamento di S e di tipo algorit-mico a maggior ragione lo sara anche quello delle sue implementazioni. Se

11Perche non significativi a questo livello.12Il tipo di comportamento caratterizzato tramite i tre postulati individuati da Gurevich;

sostanzialmente significa che ogni stato e ottenuto dal precedente per applicazione dellafunzione di transizione e che quest’ultima puo essere “descritta” per mezzo di un numerofinito di aggiornamenti.


nell’enuncire la ASM–Thesis consideriamo il concetto di sistema di calcoloalgoritmico al posto di quello di algoritmo la validita della (2) risulta abba-stanza evidente. In effetti in numerosi articoli sulle ASM si accenna al fattoche il termine algoritmo, nella formulazione della ASM–Thesis e da intender-si in senso “ampio”, in cui rientrano: macchine fisiche, virtuali, linguaggi diprogrammazione, protocolli di rete, ecc...Questa accezione viene esplicitata in [22]:

La nozione di Abstract State Machine (ASM) formalizza la no-stra nozione di sistema di calcolo dato ad un livello di astrazionefissato.

La ASM–Thesis puo quindi essere riformulata in modo da escludere possibiliambiguita:

ASM–Thesis: per ogni sistema di calcolo algoritmico esiste un’opportu-na ASM in grado di simularlo passo–passo (fissato un certo livello di astra-zione).

Per tornare all’esempio precedente, tale ASM difficilmente potra essereconsiderata come un algoritmo ma e chiaro che il comportamento che essa“segue” e di tipo algoritmico: da uno stato iniziale in cui a, b e d “valgono”undef si passa ad uno stato (il successore rispetto alla transizione specificata)in cui l’ambiente ha “caricato” in a e b i rispettivi valori ed infine si giun-ge allo stato (di terminazione) in cui d contiene il risultato dell’applicazionedella funzione corrispondente al nome gcd ai parametri a e b 13.

Abbiamo visto che la presunta formalizzazione del concetto di algoritmo(come conseguenza della ASM–Thesis) “cade” perche viene violata la pro-prieta (2). Essenzialmente essa non e verificata perche il modello ASM etroppo permissivo: esso ci permette di definire dei programmi ASM che cor-rispondono a specifiche, non accettabili come algoritmi (in senso intuitivo,classico). A questo punto ci siamo chiesti se non fosse possibile restringere ilmodello ASM, vincolando l’eccessivo grado di “liberta”, in modo da ottenerela formalizzazione cercata.

Una argomentazione speculativa (ma non troppo) Torniamo per unmomento a considerare la possibile formalizzazione del concetto di algoritmo

13A questo livello non sappiamo quale sia l’interpretazione del nome gcd, a prioripotrebbe essere una qualsivoglia funzione come f(x, y) := x + y.


nel senso stretto (intuitivo) del termine. In questa nota vogliamo argomenta-re il motivo per cui, a nostro parere, non e possibile affinare il modello delleASM in modo da escludere “algoritmi troppo astratti” (cio che abbiamo chia-mato specifiche). Per formalizzare il concetto di algoritmo sarebbe necessarioporre dei vincoli sul modello delle ASM il che equivale a tracciare una lineadi demarcazione che separi le ASM “buone” (che tutti accetterebbero co-me algoritmi) da quelle “cattive” (quelle troppo generiche: le specifiche). Apartire dal gia citato procedimento di raffinamento delle ASM, ad ogni algo-ritmo A corrisponde una gerarchia H di sue ASM–caratterizzazioni: al livellopiu alto abbiamo una specifica e da quest’ultima, esplicitando (tramite dellesotto–ASM) la definizione delle funzioni coinvolte, andiamo via via verso unasua implementazione; ammesso che tutte le funzioni coinvolte siano calcola-bili, al livello piu basso troveremo la Macchina di Turing corrispondente adA. Nella figura seguente viene illustrata la gerarchia H di ASM e la linea didemarcazione cercata che dovrebbe separare le specifiche dagli algoritmi verie propri.

(specifica - modello ground) Ar1 (raffinamento) ↓

A1

r2 ↓A2...

Ai

SPECIFICHE−−−−−−−−− −−−−−

ri+1 ↓− −−−−−−−− −−−−−

ALGORITMIAi+1

...An

rn+1 ↓(implementazione - MdT) An+1

E’ chiaro che a noi basta giungere ad un livello di dettaglio che ci illustrile idee fondamentali sul funzionamento dell’algoritmo (in pratica lo pseudo-codice dell’algoritmo in questione), ora il punto e: come fare a distinguere,


nella gerarchia H, il livello a partire dal quale siamo abbastanza nello “specifi-co” da poter dichiarare che la ASM definita e, a tutti gli effetti, un algoritmo?Il primo problema e che cio richiederebbe di possedere gia una formalizza-zione del concetto di algoritmo mentre questo e proprio quello che si stacercando di fornire. A questo pero si puo ovviare considerando un approc-cio empirico nel senso che si potrebbe considerare la formalizzazione trovatacome un’ipotesi di lavoro da considerare valida fino al momento di eventualicontroesempi, in continua verifica.Il vero problema e che, pur ammettendo che fosse possibile individuare talelinea, essa specificherebbe una volta per tutte un certo livello di astrazione: ilche andrebbe contro l’intera impostazione delle ASM poiche verrebbe menola liberta, da cui deriva il grande potere di questo modello, di fissare voltaper volta, a seconda delle esigenze, il livello di astrazione che si vuole consi-derare.Naturalmente questa non e altro che una argomentazione informale (tutta-via fondata) a favore dell’ipotesi che non sia possibile “restringere” il modellodelle ASM in modo tale che siano “ammessi” solo algoritmi (nel senso strettodel termine) perche c’e una limitazione intrinseca al modello stesso.

Fondatezza dell’osservazione Il problema di verificare se fosse possibileutilizzare il modello ASM per formalizzare il concetto di algoritmo in sensostretto, cosa che abbiamo argomentato non essere possibile, sorprendente-mente non e stato analizzato in letteratura!Avanziamo l’ipotesi che la ragione per cui tale problema sia stato trascuratosia riconducibile a due motivazioni:

1. Nessuno ha sentito il bisogno di sottolinearlo perche alla comunita ASMera chiaro che le cose stavano cosı e l’interesse verso le considerazioniepistemologiche e stato presto abbandonato a favore di quello verso il ri-goglioso campo di ricerca delle estensioni del modello base (sequenziale)e delle applicazioni del modello a diversi domini.

2. La tacita opinione degli studiosi che cio che si e ottenuto e cioe la forma-lizzazione del (piu generale) concetto di sistema di calcolo algoritmicofosse piu importante, dal punto di vista fondazionale, per l’informatica.In effetti le entita con cui si lavora in informatica sono piu spesso ricon-ducibili a sistemi che esibiscono un comportamento algoritmico che nonad algoritmi in senso classico: come gia accennato il formalismo delleASM e stato sfruttato con successo per modellare vari tipi di macchine(fisiche e virtuali), compilatori, protocolli di rete, ecc. . .


Non avendo trovato in letteratura alcun riferimento a questa problematica,in cerca di un parere critico sulla fondatezza dell’osservazione precedente,abbiamo contattato i professori Gurevich e Borger presentando loro l’argo-mentazione informale esposta in precedenza.

Dalle risposte ricevute, [23] e [10], e emerso che il problema base riguardoalla nostra critica e che non e chiaro che cosa intendiamo quando parliamodi algoritmo in senso classico, intuitivo del termine o di algoritmo nel sensostretto del termine. Si tratta di espressioni troppo generiche che lasciano“sfumati” molti aspetti non secondari. Intendiamo limitarci agli algoritmisequenziali (con un solo agente di calcolo) oppure quello che ci preme e chele informazioni fornite siano sufficientemente dettagliate per descrivere il pro-cedimento di calcolo (e a questo punto ammettiamo anche algoritmi parallalie distribuiti)? Aggiungiamo poi anche la possibilita di algoritmi ad esecu-zione infinita (che non terminano)14? O ci interessano forse i procedimentidi calcolo effettuati dalle Macchine di Turing? In questo caso bisogna con-siderare che questi non catturano, perlomeno non e chiaro come inglobarenell’analisi di Turing, gli algoritmi in senso classico come ad esempio le clas-siche costruzioni con riga e compasso poiche si sfugge al discreto15.Queste sono caratteristiche fra loro ortogonali che e importante definire inmaniera chiara prima di affrontare uno studio come quello che ci siamo pro-posti. Ammesso che la nostra argomentazione e, per certi versi, ambiguaci preme sottolineare che l’aspetto che ci sembra piu significativo e a cuiabbiamo pensato fin dall’inizio e quello del sufficiente grado di dettaglio del-l’informazione sul procedimento di calcolo.Siamo interessati nell’approfondire questa tematica e ci proponiamo di farloin futuro ma al momento della stesura della presente tesi di laurea ancoranon e stato possibile sviluppare lo studio in questa direzione.

Osservazione Concludiamo la presente sezione con una osservazione do-vuta a Borger, [10] e [18]: nel modello ASM sviluppato da Gurevich c’e unaspetto in un certo senso contradditorio. Da una parte si vuole un modelloin grado di simulare passo–passo un qualsiasi sistema di calcolo algoritmi-co, nel modo piu naturale possibile; questo significa che, fissato un livello di

14Richiamiamo l’esempio gia dato dell’algoritmo che applicando il Crivello di Eratosteneper valori crescenti stampa via via la sequenza dei numeri primi.

15Come rappresentare tramite una stringa finita un punto nel piano euclideo nel casoin cui si tratti di un numero (irrazionale) con una espansione infinita di decimali? Questocaso particolare e gestibile [27] ma il caso generale non e chiaro in che misura lo sia: sitratta di studiare la potenza della rappresentabilita tramite stringhe.


astrazione L, per catturare le entita coinvolte (strutture dati e operazioni sudi esse) non abbiamo bisogno di codificarle a partire da strutture primitivepiu semplici perche siamo liberi di “regolare” il livello di astrazione dellanostra macchina in modo che coincida con L. Dall’altra parte, per ottenereil teorema di caratterizzazione degli algoritmi a partire dalla ASM–Thesis,abbiamo bisogno di individuare possibilmente pochi16 assiomi; questi ultimi,per poter catturare l’intera gamma di sistemi di calcolo algoritmici, devonoesporre il massimo grado di generalita. In questo senso il modello ASM puoessere definito minimalistico: c’e il minimo necessario. Questo pero porta alfatto che quando ci si trova a voler modellare un sistema reale S, il modelloASM classico risulta troppo “scarno” perche gli strumenti che esso ci mettea disposizione sono troppo generali; siamo dunque costretti ad un lavoro didecodifica per passare dalla massima generalita allo specifico del sistema S.Riassumendo: da un lato si vorrebbe eliminare del tutto la codifica, che rendela simulazione non naturale; dall’altro, mirando al massimo potere espressi-vo, essa viene sostituita dalla decodifica, ugualmente innaturale!

4.2.5 Conclusioni

Abbiamo esaminato due formalismi, in cui esprimere algoritmi, che a dif-ferenza degli usuali linguaggi di programmazione si prefiggono di catturarela parte concettuale di ciascun algoritmo, non legata a particolari dettagliimplementativi: le Abstract State Machines lo fanno rendendo dinamica lascelta del livello di astrazione mentre i Ricorsori sfruttano le equazioni ricorsi-ve che sono alla base dell’algoritmo dato. Se ci limitiamo al caso sequenzialeentrambi sembrano riuscire nell’intento di fornire uno formalismo comple-to, nel senso che ogni algoritmo e in essi esprimibile . Se pero mettiamo aconfronto i risultati ottenuti con la formalizzazione delle funzioni calcolabiliottenuta da Turing ed altri, ci accorgiamo che e stato fatto molto ma non ab-bastanza. Per le ragioni esposte in precedenza, risulta che nessuna delle duesoluzioni proposte e pienamente soddisfacente se consideriamo il problemada cui eravamo partiti: formalizzare il concetto di algoritmo. Tale difficoltae chiara se si pensa al fatto che l’aspetto intensionale e naturalmente a gra-nularita piu fine rispetto a quello estensionale cui si limita lo studio dellefunzioni calcolabili in modo effettivo. Potrebbe anche darsi che un tipo diformalizzazione equivalente alla Tesi di Church–Turing per gli algoritmi nonsia possibile poiche a differenza di quello di funzione calcolabile, il concettodi algoritmo e, intrinsecamente ed indissolubilmente, relativo ad un insieme

16Come abbiamo visto, nel caso sequenziale sono solo tre!


di operazioni/funzioni, considerate primitive, di cui fa uso l’algoritmo in que-stione, come emerge in maniera chiara dai due lavori presi qui in esame. Aquesto proposito citiamo le parole di Godel [19]:

Tarski ha sottolineato nella sua conferenza (e credo giustamente)la grande importanza del concetto di ricorsione generalizzata (oTuring–calcolabilita). Mi sembra che tale importanza sia in granparte dovuta al fatto che con questo concetto si e riusciti perla prima volta a dare una definizione assoluta di una interessan-te nozione epistemologica, e cioe che non dipende dal formalismoscelto. In tutti gli altri casi, trattati in precedenza, coma la dimo-strabilita oppure la definibilta, si e riusciti a darne una definizionesoltanto relativamente al linguaggio dato e per ogni linguaggio,preso individualmente, e chiaro che quella ottenuta differisce daquella cercata. Per il concetto di calcolabilita, tuttavia, anche sesi tratta meramente di un certo tipo particolare di dimostrabilitao decidibilita, la situazione e diversa. Per una sorta di miracolonon e necessario fare distinzione tra gli ordini ed il processo didiagonalizzazione non ci porta fuori dalla nozione definita.

Il concetto di algoritmo non puo, per sua natura, essere un concetto assolutoe questo unito alla natura intensionale potrebbe renderlo non formalizzabilenei termini richiesti. Il caso delle funzioni calcolabili potrebbe rappresentareun caso particolarmente, al limite troppo, “fortunato”.Alcune tra queste ultime considerazioni potranno apparire come gia note ecome tali si potrebbe essere portati a pensare che si sia “reinventata la ruota”ma ribadiamo che e solo dopo un attento studio ed un tentativo come quellointrapreso da Gurevich e Moschovakis che possiamo affermare con certezzala validita di esse.

Bibliografia

[1] ASM–Gofer. http://www.tydo.de/AsmGofer/index.html.

[2] ASM Michigan Webpage. http://www.eecs.umich.edu/gasm/.

[3] Microsoft’s AsmL Webpage. http://research.microsoft.com/fse/asml/.

[4] A. Blass and Y. Gurevich. “Algorithms vs. Machines”. Bulletin ofEATCS, 77:96–118, June 2002.

[5] Andreas Blass and Yuri Gurevich. “Ordinary interactive small-stepalgorithms, II”. ACM Trans. Comput. Logic. to appear.

[6] Andreas Blass and Yuri Gurevich. “Ordinary interactive small-stepalgorithms, III”. ACM Trans. Comput. Logic. to appear.

[7] Andreas Blass and Yuri Gurevich. “Abstract state machines captureparallel algorithms”. ACM Trans. Comput. Logic, 4(4):578–651, 2003.

[8] Andreas Blass and Yuri Gurevich. “Algorithms: A Quest for Absolu-te Definitions”. Bulletin of the European Association for TheoreticalComputer Science, (81):195–225, October 2003.

[9] Andreas Blass and Yuri Gurevich. “Ordinary interactive small-stepalgorithms, I”. ACM Trans. Comput. Logic, 7(2):363–419, 2006.

[10] E. Borger. Comunicazione personale. Maggio 2007.

[11] Egon Borger. “High Level System Design and Analysis using AbstractState Machines”. In D. Hutter et al., editor, Current Trends in AppliedFormal Methods, volume 1464 of LNCS, pages 1–43, 1999.

[12] Egon Borger. “The Origin of the ASM Method for High Level SystemDesign and Analysis”. Journal of Universal Computer Science, 8(1):2–74, 2002.

111

112 BIBLIOGRAFIA

[13] Alonzo Church. “A note on the Entscheidungsproblem”. Journal ofSymbolic Logic, 1:40–41, 1936.

[14] Alonzo Church. “An unsolvable problem of elementary number theory”.American Journal of Mathematics, 58:345–363, 1936.

[15] Edsger W. Dijkstra. “Go to statement considered harmful”.Communications of the ACM, 11(3):147–148, 1968.

[16] Donald E. Knuth. The Art of Computer Programming, volume 1.Reading, MA, 1968. “Fundamental Algorithms”.

[17] Egon Borger e Robert Stark. Abstract State Machines. Springer, 2003.

[18] E. Borger e T. Bolognesi. “Remarks on turbo ASMs for computingfunctional equations and recursion schemes”. In A. Gargantini e E. Ric-cobene E. Borger, editor, Abstract State Machines 2003 – Advances inTheory and Applications, volume 2589 of Lecture Notes in ComputerScience, pages 218–228. Springer Verlag, 2003.

[19] Kurt Godel. Article 1946. In Collected Works, volume II. OxfordUniversity Press, 1990.

[20] Dima Grigoriev. “Kolmogorov algorithms are stronger than Turingmachines”. Journal of Soviet Mathematics, 14(5):1445–1450, 1980.

[21] Y. Gurevich. “Sequential Abstract State Machines Capture SequentialAlgorithms”. ACM Transactions on Computational Logic, 1(1):77–111,July 2000.

[22] Y. Gurevich. “Logician in the land of OS: Abstract State Machines atMicrosoft”. In Proceedings of the Sixteenth Annual IEEE Symposiumon Logic in Computer Science, pages 129–136. IEEE Computer Society,2001.

[23] Y. Gurevich. Comunicazione personale. Maggio 2007.

[24] Y. Gurevich and M. Spielmann. “Recursive Abstract State Machines”.Journal of Universal Computer Science, 3(4):233–246, 1997.

[25] Yuri Gurevich. “A new thesis”. American Mathematical SocietyAbstracts, page 317, August 1985.

[26] Yuri Gurevich and Tatiana Yavorskaya. “On Bounded Explorationand Bounded Nondeterminism”. Technical report, Microsoft Research,January 2006.

BIBLIOGRAFIA 113

[27] Dono Kijne. Plane Construction Field Theory. Van Gorcum, Assen,1956.

[28] S. C. Kleene. Introduction to metamathematics. van Nostrand, 1952.Princeton.

[29] Andrei N. Kolmogorov and Vladimir A. Uspensky. “On the definitionof algorithm”. Uspekhi Mat. Nauk, 13(4):3–28, 1958.

[30] M. Shub L. Blum and S. Smale. “On a theory of computation andcomplexity over the real numbers: NP-completeness, recursive functionsand universal machines”. Bulletin of American Mathematical Society,21:1–46, 1989.

[31] Wolfgang Maass. “Combinatorial Lower Bound Arguments for Deter-ministic and Nondeterministic Turing Machines”. Transactions of theAmerican Mathematical Society, 292(2):675–693, 1985.

[32] Y. N. Moschovakis. “Abstract recursion as a foundation of the theoryof algorithms”. In M. M. Richter et al., editor, Computation and ProofTheory, volume 1104. Lecture Notes in Mathematics, Springer Verlag,Berlin, 1984.

[33] Y. N. Moschovakis. “A mathematical modeling of pure, recursive al-gorithms”. In Logic at Botik’89 Symposium on logical foundations ofcomputer science, pages 208–229. Springer-Verlag New York, Inc., NewYork, NY, USA, 1989.

[34] Y. N. Moschovakis. “The Formal Language of Recursion”. Journal ofSymbolic Logic, 54(4):1216–1252, 1989.

[35] Y. N. Moschovakis. “On founding the theory of algorithms”. In H. G.Dales and G. Olivieri, editors, Truth in mathematics, pages 71–104.Clarendon Press, Oxford, 1998.

[36] Y. N. Moschovakis. “What Is an Algorithm?”. In Bjorn Engquist andWilfried Schmid (Eds.), Mathematics Unlimited – 2001 and Beyond,Springer. 2001.

[37] Wolfgang Reisig. “On Gurevich’s Theorem on Sequential Algorithms”.Acta Informatica, 39(5):273–305, 2003.

[38] Arnold Schonhage. “Universelle Turing Speicherung”. In J.Dorr andG. Hotz, editors, Automathentheorie und Formale Sprachen, pages 369–383. Bibliograf. Institut, Mannheim, 1970.

[39] Arnold Schonhage. “Storage modification machines”. SIAM Journal ofComputing, 9:490–508, 1980.

[40] D. S. Scott and C. Strachey. “Towards a mathematical semantics forcomputer languages”. In J. Fox, editor, Proceedings of the Symposiumon computers and automata, pages 19–46, New York, 1971. Polytechnicinstitute of Brooklin Press.

[41] A. Tarski. “The concept of truth in the language of deductive sciences”,pages 152–278. Logic, Semantics, Metamathematics: Papers from 1923to 1938. Clarendon Press, Oxford, 1933.

[42] A. M. Turing. “On computable numbers, with an application to the En-tscheidungsproblem.”. Proceedings of the London Mathematical Society,42(2):230–265, 1936-1937.

Ringraziamenti

Il completamento del mio percorso di studi si puo dire che sia il risultato diuno sforzo comune.Devo infatti ricordare che sono stato appoggiato, nel corso degli anni, damoltissime persone che mi sono state vicine: esse mi hanno dato un supportosenza il quale difficilmente sarei potuto arrivare a quello che per me rappre-senta un traguardo significativo.

Oltre a mio padre, ringrazio:

• la mia famiglia: mia sorella Alina (e Marco), mio fratello Andrei e lemie due zie Nana e Rodi;

• i miei amici d’infanzia e non, che ancora non si sono stufati della miacompagnia: Michele, Giacomo, Paolo, Stefano, Fazio e Chiara, Vas-so, Francesca, Franceschina, Elena, Uberto, Cecilia, Alessandro, Fra eMari, Faggio e Sem;

• Paola, la ragazza con la quale sto molto bene e che ha sopportatopazientemente tutto lo stress degli ultimi mesi;

• Giuliano, amico e avventuriero, con il quale discutendo ho potutovedere in maniera piu critica i miei ragionamenti (sulla tesi e non solo);

• altri amici sparsi in giro per il mondo che non per questo sono menovicini: Mario e Lucia, Mihnea e Theia, Angi e Victor, Narcisa, Norbert,Sorana, Steve e Beverly;

• la signora Antonia senza la quale la nostra casa sarebbe invivibile;

• Mariolina e Seva che mi hanno sempre dimostrato grande simpatia;

• Pierre che nell’ultimo periodo pre–tesi e stato un coinquilino modelloe ha fatto di tutto per aiutarmi a non perder tempo;

• i compagni di studi che hanno reso piu leggeri certi periodi particolariall’universita e non solo: Matteo, Luana, Antonio, Andrea, Valerio,Kosta;

Molte di queste persone mi hanno seguito nei miei (numerosi) tentenna-menti senza mai stancarsi e cercando sempre di incoraggiarmi a percorrerela strada che ho scelto di volta in volta. Vorrei essere riuscito a comunicare

a tutti la profonda gratitudine che provo: ciascuno di essi mi ha dato e con-tinua a darmi qualcosa di assolutamente originale!Con queste persone sono cresciuto e nessuno verra dimenticato anche se lecircostanze della vita dovessero allontanarci fisicamente.

Infine devo ringraziare i professori Gurevich e Borger che hanno rispostocon prontezza ed entusiasmo alle mie domande.

La formalizzazione del concetto di algoritmo: rassegna e...

Documents

Transcript of La formalizzazione del concetto di algoritmo: rassegna e...