Post, sistema di
Post, sistema di
Post, sistema di in logica, uno dei modelli sviluppati per proporre una definizione matematica del concetto intuitivo di → funzione calcolabile; altri modelli, tutti tra loro equivalenti, sono la macchina di → Turing, le → funzioni ricorsive e il → lambda-calcolo. Nel sistema di Post il calcolo di una funzione matematica è simulato dalla manipolazione di una stringa di simboli attraverso un insieme di regole stabilite in modo assiomatico. Formalmente un sistema di Post è costituito da:
• un insieme S di simboli, detto alfabeto;
• un insieme X di variabili;
• una relazione binaria finita e non vuota ρ che associa a una stringa u, detta antecedente, una stringa ν, detta conseguente.
In simboli u ρ ν, qualora siano verificate le seguenti ipotesi: 1) u deve essere costruita alternando stringhe costruite con l’alfabeto S a variabili di X; 2) se ν contiene una variabile di X, anche u contiene la stessa variabile. La relazione binaria ρ definisce le regole di riscrittura (o regole di produzione) che permettono il passaggio da una stringa all’altra. A titolo di esempio si consideri un sistema di Post costituito da S = {a, b, c}, X = {x, y} e dalle seguenti regole: axbyc ρ abyc; axbb ρ ba; bxa ρ axxc. Si noti che, in ogni regola, l’antecedente è costituito da stringhe di S alternate a variabili e contiene almeno una variabile mentre il conseguente non contiene variabili diverse da quelle dell’antecedente. Non sono per esempio ammissibili regole di produzione come: abc ρ bc; axbb ρ bxayc. Non è possibile, quindi, utilizzare come antecedente una stringa non contenente variabili oppure introdurre nuove variabili nel conseguente. Se come unica regola di produzione si accetta la regola s1x ρ xs2 (dove s1 e s2 sono due parole formate con i simboli di S mentre x è una variabile di X) allora il sistema di Post è detto sistema normale di Post.
Un sistema di Post può essere considerato come una grammatica generatrice di un linguaggio formale; da ciò deriva anche la nozione di funzione calcolabile in un sistema di Post. Tale nozione è equivalente alla calcolabilità secondo il modello della macchina di Turing; ciò rientra nell’ambito della tesi di → Church secondo cui i modelli di calcolo formali rappresentano tutte e sole le funzioni calcolabili.