computability theory era Re: [Soci SLIP] input/output error

[loredana]

On Tue, 2010-06-08 at 12:05 +0200, Lucio Crusca wrote:
> In data martedì 08 giugno 2010 11:10:55, loredana ha scritto:
> 
> > Ah, ribadisco, l'informatica e' una scienza esattissima
> 
> Parrebbe di no:
> 
> http://it.wikipedia.org/wiki/Scienza_esatta
> http://it.wikipedia.org/wiki/Qualità_del_software#Correttezza

Non parliamo della stessa cosa e diciamo la stessa cosa. Quando
Turing ha definito la teoria della computabilita' e' stato in
grado di dimostrare che non e' possibile scrivere un programma
in grado di accettare come input un QUALSIASI altro programma e
stabilire in modo automatico se quel programma si fermera' oppure
no (halt problem), o se quel programma fa quel che deve fare
(correttezza) e ha dimostrato  che le funzioni non computabili
sono numericamente (parliamo di infiniti di ordine diverso) molto piu'
numerose di quelle computabili. In soldoni, le funzioni computabili sono
numerabili, cioe' possono essere numerate usando i numeri naturali (1,2,
3 etc) che sono infiniti, ma molto "meno numerosi" dei numeri tutti. 
L'insieme delle funzioni computabili invece non e' numerabile.

Questo vale per TUTTI i sistemi di calcolo, all'epoca non ne esisteva
neppure uno, neanche il calcolatore (parliamo degli anni 30). E non ha
a che fare con la nostra abilita' o con i nostri strumenti. L'unica cosa
che si assume e' che l'algoritmo sia una ricetta in cui ogni singolo
passo e' finito (termina in un tempo finito) e il numero di passi e'
finito. Tutti i programmi rientrano in questa definizione. Nota che non
e' il tempo di esecuzione che deve essere finito, ma la descrizione del
processo (il codice, per intenderci). Un kernel e' un insieme finito 
di passi, per esempio.

> Era una scienza esatta forse al tempo di Turing 
Al piu' si puo' discutere se chiamare l'informatica scienza, come non lo
e' la matematica, una scienza, non lo e' neppure l'informatica, se con scienza
si intende scienza della natura (fisica, biologia etc). L'informatica e' una
branca della matematica.

> ed oggi solo per casi molto particolari 
> (sistemi a singolo utente real time come potrebbe essere la circuteria della 
> cabina di controllo di un aereo).
> 
> In un normale pc intervengono troppe condizioni imprevedibili perché sia 
> possibile scrivere un software in modo deterministico. 

Questo fa parte della teoria della computabilita' (vedi sopra). Tutti
noi lo sappiamo in pratica, la teoria lo prova in generale. Turing (e
altri con lui, lavorando sui sistemi formali, da Godel in poi) lo hanno
dimostrato prima che tutti gli oggetti a cui la loro teoria si applicava
(calcolatori e derivati) venissero inventati. 

> Possiamo dire che un 
> software, se eseguito su un sistema deterministico, a sua volta può essere 
> deterministico (ma è da dimostrare di volta in volta per ogni singolo 
> software). 

Esatto, questo e' quello che dimostra la teoria. Non dice affatto che
per uno specifico programma non sia possibile determinare se termina
oppure no, o se calcola la stessa funzione di un altro programma, o se
e' corretto oppure no. Dice che non e' possibile farlo in modo
automatico per TUTTI i programmi/funzioni/software possibili. 

> In ogni caso i nostri PC non sono sistemi deterministici, ovvero 
> dato un certo input non è possibile dire a priori quale sarà l'output. 

Questo invece non e' vero, mi pare. Se sappiamo esattamente qual e'
l'input, e sappiamo cosa il pc fa, allora il sistema e' completamente
deterministico, cioe' quello che nella teoria si chiama sistema formale:
a parita' di input, applicando una serie finita di passi non puo' che
produrre lo stesso output. Solo in presenza di una sorgente davvero
random potrebbe essere diversamente. Anche i generatori di numeri
casuali sono programmi deterministici. La sorgente random dovrebbe
essere fisica per esser random davvero (tipo il tempo di decadimento
delle singole particelle di uranio).

E' MOLTO interessante. Godel ha dimostrato, nel 1930, che non esistono
sistemi formali sufficientemente complessi che siano allo stesso tempo
completi (tutto cio' che 'e vero si puo' dimostrare all'interno del
sistema) e consistenti (il sistema non contiene contraddizioni). Ha
anche dimostrato che per OGNI sistema formale, ci sono verita' che sono
vere ma che non possono essere dimostrate all'INTERNO del sistema. Basta
e avanza per distruggere qualsiasi concetto assoluto di autorita'.

Loredana