Post on 08-Nov-2020
Introduzione alla
calcolabilitàGabriella Trucco
E-Mail: gabriella.trucco@unimi.it
Libro di riferimento: Sipser, Introduction to the theory of computation
Controlli automatici di
correttezza dei programmi
Obiettivo chiave dei LdP: fornire costrutti che riducano la probabilità di lasciare errori nei programmi
... ovvero: il programma implementa effettivamente l'algoritmo per cui è progettato
Perché non costruire verificatori automatici della correttezza dei programmi, e poi utilizzare il linguaggio che preferiamo?
Ci sono risultati teorici che dimostrano che non è possibile costruire verificatori perfetti.
Verificatore della terminazione
di programmi C
Supponiamo di avere un programma term (alla
lavagna ...)
In ogni caso, term si comporta diversamente dalle
specifiche
Infatti, term non può essere realizzato!
Linguaggi di programmazione
general purpose
Abbiamo dimostrato che non esiste nessun programma C che verifichi la terminazione di un programma (system, exit ...)
Dato un linguaggio di programmazione ed un problema calcolabile, posso sempre scrivere un programma in quel linguaggio che risolva il problema?
Linguaggi di programmazione con questa caratteristica vengono definiti general purpose
es. C, C++, Java, LISP, ML, Prolog ... ma NON SQL
Per caratterizzare i linguaggi general purpose abbiamo bisogno di formalità e generalità
Modelli di calcolo astratti
Come dimostrare qualcosa che valga
indipendentemente dal linguaggio utilizzato?
Con modelli di calcolo astratti
es. macchina di Turing
Modelli di calcolo astratti
Diversi modelli di computazione, tra cui:
Automi a stati finiti
Automi a pila
Esistono problemi che per essere risolti richiedono
capacità che vadano oltre le possibilità di questi
modelli
Automi non general-purpose
Macchina di Turing Macchina di Turing: modello per calcolatore general
purpose
Simile ad automa a stati finiti, ma con memoria illimitata
Certi problemi non possono essere risolti nemmeno con questo modello problemi che vanno oltre il limite della calcolabilità
Nastro infinito usato come memoria illimitata
Testina legge e scrive simboli e si muove lungo il nastro
Inizialmente sul nastro solo stringa in ingresso
Computazione continua finché viene prodotto un output accept/reject
Se non si raggiunge uno stato di accept o reject, la computazione prosegue all’infinito
Esempio
M1 per verificare l’appartenenza di una stringa al
linguaggio
Verificare che le due stringhe siano identiche e
separate da #
Stringhe molto lunghe impossibile ricordarle a
memoria ci spostiamo avanti e indietro lungo il nastro
per verificare la corrispondenza, fissando dei marcatori
per ricordarci quali simboli sono già stati confrontati e
corrispondono
Esempio
Definizione formale
MdT: computazione
M riceve la stringa in ingresso scritta nella parte iniziale sinistra del nastro
Il resto del nastro è vuoto
L’alfabeto della stringa in ingresso non contiene il simbolo blank! quando la testina legge tale simbolo, significa che la stringa in ingresso è finita
Computazione procede in accordo alla funzione di transizione
Terminazione se si raggiunge stato accept o reject, altrimenti loop infinito
Configurazione
Durante la computazione, modifiche a
1. stato corrente
2. contenuto del nastro
3. posizione testina
Configurazione: impostazione di 1, 2, 3
Rappresentazione di una configurazione:
1011q701111
La config. C1 produce la config. C2 se si passa da C1 a C2 in un solo passo
Configurazione di M su ingresso w
partenza
accettazione
rifiuto
M accetta l’ingresso w se esiste una sequenza di config. C1, ..., Ck t.c.
C1: configurazione di partenza di M su w
Ogni Ci produce Ci+1
Ck: configurazione di accettazione
Computazione
a,b,c in G; u,v in G*; qi, qj
If d(qi,b)=(qj,c,L): uaqibv uqjacv
If d(qi,b)=(qj,c,R): uaqibv uacqjv
Linguaggio Turing-riconoscibile
Linguaggio di M (o linguaggio riconosciuto da M):
collezione di stringhe accettate da M
Un linguaggio è Turing-riconoscibile se esiste una
macchina di Turing che lo riconosce
Decidibilità
M può non accettare un ingresso
Terminando in uno stato di rifiuto
Andando in loop
Difficile distinguere loop da lungo tempo di calcolo utile macchina di Turing che termina con qualsiasi input: decisore
Decisore che riconosce un linguaggio decide il linguaggio
Linguaggio Turing-decidibile se esiste una macchina di Turing che lo decide
Varianti
Robustezza: la MdT e le sue varianti sono tutte
equivalenti in potenza, ovvero riconoscono gli
stessi libguaggi (macchine equivalenti)
MdT multinastro
MdT non-deterministica
Nuova definizione di funzione di transizione
MdT multinastro
Ogni nastro ha la propria testina
Ingresso su nastro 1
Altri nastri inizialmente vuoti
Funzione di transizione:
MdT multinastro
Teorema: ogni MdT multinastro ha una
equivalente MdT a nastro singolo
Cenni di dimostrazione
MdT non-deterministica
In ogni punto della computazione, la
macchina può procedere in più modi, in
accordo alle diverse possibilità
Funzione di transizione:
Theorem: ogni MdT non-deterministica ha una
equivalente MdT deterministica
Definizione di algoritmo
Algorithm: set of simple instructions to carry out
some task
Commonplace called procedure or receipt
Mathematics contains description of algorithms to
solve different kind of problems
For example finding prime numbers, or calculate
greatest common divisors….)
Even though algorithms have had a long history in
mathematics, their formalization was not defined
until 20th century
Hilbert’s problem
1900: mathematician David Hilbert identified 23 hard problems and posed them as a challange for the coming century
10th problem concerned algorithms
10th problem: Define an algorithm that takes a polynomial as input and verifies if it has integral root.
Example: 6x3yz2 + 3xy2 -x3 -10 polynomial of 4 terms, variables x, y e z.
Root: x = 5, y = 3, and z = 0.
Integral root, since all assignment to variables are integral values
There exist polynomial with non-integral roots
10th Hilbert’s problem
Today we know such algorithm does not exist algorithmically unsolvable problem
We need a precise definition of algorithm to demonstrate that an algorithm doesn’t exist
The definition came in 1936 by Alonzo Church and Alan Turing
Church used the notational system called l-calculus
Turing used a model of computational machine (the Turing machine)
The two definitions were shown to be equivalent
Equivalence between
computational models
Very different computational models
Common element: formal definition of algorithm they give a precise formulation of function computable by an algorithm
The formal definition of algorithm strictly depends on the adopted computational model
Main result: every function computable with a certain formal computational model is computable also with others equivalent models, if it is properly encoded according to different formalisms
Church-Turing thesis
Equivalence between computational models real computability
Since the most wide concept of computability is the Turing’s one (or of the Turing equivalent models), it’s clear that each computable function is Turing computable
Church-Turing thesis: a function, computable with any reasonable computational model, is computable using a TM
A function is computable if it is computable with a TM
Not-demonstrable thesis
We can’t exclude that one day somebody will discover a new computational model that allows to compute a function at the moment not computable
Today we can demonstrate that what is computable with models apparently more powerful than a TM, can be calculated with a TM
10th Hilbert’s problem
D = {p | p is a polynomial with integral roots}
The problem asks whether the set D is decidible
Negative answer
Let us demonstrate that D is Turing-recognizable
Consider a simpler problemD1: consider polynomials with a single variable
M1 that recognizes D1:
Analogously we can find M for D
10th Hilbert’s problem
M1 and M recognizers, not deciders
It is possible to convert M1 to be decider for D1: it is possible to
compute the bounds within which the roots of a single variable must
lie, and restrict the search to these bounds
Impossible in the case of multivariables
There is no TM that is decider for D there is no algorithm for D