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