Corrispondenza tra deduzioni e programmi: un cenno

Piu' volte durante il corso abbiamo accennato al fatto di come la Logica e la Programmazione abbiano molto in comune, ed anzi siano intrinsecamente fondate sugli stessi processi mentali. E questo non solo da un punto di vista di semplici similitudini informali, ma in modo estremamente preciso e profondo.
Il fatto che l'attivita' di programmazione e quella di dimostrazione siano quindi intrinsecamente la stessa cosa puo' aiutare l'informatico ad affrontare con uno spirito diverso lo studio della matematica e della logica in particolare. Infatti, dimostrando teoremi e descrivendo deduzioni logiche, egli non sta facendo altro che esercitare gli stessi meccanismi mentali che sono alla base della descrizione di processi computazionali, di algoritmi. Sta' cioe' esercitandosi a programmare.

Nel nostro corso non abbiamo il tempo (e le basi logiche e matematiche sufficienti) di mostrare con precisione ed in dettaglio quanto abbiamo appena affermato, ma possiamo senza troppa difficolta' giustificare con un certo grado di formalizzazione l'affermazione che esiste una corrispondenza precisa tra Programmi e Dimostrazioni logiche, oltre che tra computare (un'attivita' che, ricordiamo, possiamo assimilare a quella di trasformazione di informazione da una forma implicita ad una esplicita) e semplificare deduzioni.

Quello che segue e' un esempio che ci puo' dare un'idea di cosa possa essere nel concreto tale corrispondenza.

Prendiamo il sistema della deduzione naturale per la logica proposizionale, e di questo, per semplicita', consideriamo le sole regole per il connettivo implicazione, cioe' (→-I) e (→-E)

Vediamo ora come, presa una deduzione in questo sistema, si possa associare ad ogni sottodeduzione (e quindi alla deduzione completa) un termine del λ-calcolo.
Tale associazione verra'indicata nel modo seguente:

Questa notazione indica che il termine M e' associato ad una particolare deduzione della formula ben formata σ

L'associazione e' definita come segue:

• Ad ogni ipotesi associamo una variabile del λ-calcolo (la stessa variabile non puo' essere associata a ipotesi differenti, ma, volendo, si puo' associare a piu' ipotesi uguali)

• Ogni volta che si utilizza la regola (→-E), alla conclusione associamo l'applicazione dei termini associati alle due premesse della regola.
  La regola (→-E) e' come se diventasse
  
  

  M : σ → τ      N : σ
  ---------------------------
  (M N) : τ
  
  

• Ogni volta che si utilizza la regola (→-I), alla conclusione associamo l'astrazione funzionale del termine associato alla premessa della regola rispetto alla variabile corrispondente all'ipotesi (o alle ipotesi) che vengono scaricate.
  La regola (→-E) e' come se diventasse
  
  

  [x : σ]
  :
  :
  M : τ
  -------------
  λx.M : σ → τ
  
  

Un esempio ci permettera' meglio di comprendere quanto detto.

Prendiamo la seguente deduzione:

Associando all'ipotesi σ (che poi verra' scaricata) la variabile z, all'ipotesi σ → τ la variabile y ed all'ipotesi σ → (τ → γ) la variabile x, otteniamo la seguente associazione di λ-termini a tutte le sotodeduzioni ed alla deduzione completa:

λx.λy.λz.xz(yz) e' quindi il lambda termine associato alla nostra prova di
σ → (τ → γ)) → ((σ → τ) → (σ → γ) in deduzione naturale.

Nel modello computazionale del λ-calcolo le entita' computazionali, i "programmi", sono appunto λ-termini.
Questo pero' ovviamente non basta supportare l'affermazione che le prove logiche siano assimilabili a programmi: una prova non dovrebbe semplicemente somigliare ad un programma, dovrebbe anche, in un certo senso, comportarsi come un programma!
Ed e' proprio questo che cerchiamo di illustrare ora.

Supponiamo che in una deduzione sia presente un'applicazione della regola (→-I) immediatamente seguita da una (→-E)

Dove D e' una sottodeduzione con conclusione σ.

E' chiaro che introdurre una formula con una implicazione per eliminare quest'ultima subito dopo e' un inutile giro deduttivo. Avendo a disposizione la sottodeduzione D potremmo utilizzare questa al posto dell'ipotesi σ senza avere quindi la necessita' di scaricarla. La formula τ puo' cioe' venire piu' semplicamente derivata nel modo seguente.

A cosa corrisponde, dal punto di vista computazionale questa semplificazione della nostra dimostrazione di τ?
Vediamo qual e' il λ-termine corrispondente alla nostra deduzione

E' un beta-redex!
E nella versione semplificata della deduzione, la sottodeduzione D viene inserita al posto dell'ipotesi. Questo, dal punto di vista dei λ-termini corrispondenti alle varie sottodeduzioni, corrisponde a sostituire il λ-termine N corrispondente alla sottodeduzione di σ al posto della variabile x associata all'ipotesi σ. Cioe':

La semplificazione della nostra dimostrazione corrisponde, dal punto di vista del λ-calcolo, alla regola di β-riduzione!!

La nozione di computazione, che sappiamo essere un processo di trasformazione dell'informazione da una forma implicita ad una forma esplicita (cosa che nel λ-calcolo e' formalizzata dalla nozione di β-riduzione), corrisponde quindi, dal punto di vista logico alla semplificazione di ragionamenti deduttivi.

I programmi e le computazioni da una parte, e le dimostrazioni e le semplificazioni di dimostrazioni sono quindi intrinsecamente la stessa cosa.

Il nostro esempio con la deduzione naturale per l'implicazione e il λ-calcolo, possono ovviamente solo dare un'idea della cosrrispondenza intrinseca esistemte tra prove e programmi.
Questa corrispondenza si puo' ovviamente rendere ancora piu' chiara ed esplicita, ma per il nostro corso quanto detto puo' essere sufficiente, non avendo noi il tempo e le basi matematiche e logiche necessarie per approfondire l'argomento.

Esercizio: Fornire una dimostrazione di σ → (τ → γ) che utilizzi una ipotesi γ. Prendere il λ-termine corrispondente (dimostrazioni con ipotesi non scaricate corrispondono a λ-termini con variabili libere) ed applicarlo al λ-termine λx.λy.λz.xz(yz) che corrisponde alla dimostrazione che abbiamo visto prima di (σ → (τ → γ)) → ((σ → τ) → (σ → γ))
Ridurre il tutto a forma normale facendo vedere qual e' la dimostrazione di (σ → τ) → (σ → γ) che corrisponderebbe al termine ottenuto.

La corrispondenza tra deduzioni e programmi, che abbiamo appena descritto utilizzando il frammento implicativo della logica proposizionale in deduzione naturale ed il λ-calcolo, puo' essere resa evidente anche utilizzando il frammento implicativo del sistema P₀ (il sottosistema che utilizza solo gli assiomi AxK e AxS) e la Combinatory Logic (CL).
CL e' un semplicissimo modello computazionale in cui l'insieme di termini τ - definito nella sezione 2.2 di [SM] - formalizza il concetto di programma/dato. La nozione di computazione e' formalizzata dalle relazioni →_s e →_k che si ottengono sostituendo una freccia al posto del simbolo '=' negli assiomi (Axk) ed (Axs) del sistema formale in sezione 2.2 di [SM] (tale sistema e' per il modello computazionale CL quello che per il λ-calcolo e' il sistema formale per la β-conversione, =_β).
Mettendo in corrispondenza l'assioma (AxK) di P₀ con il termine k di τ, l'assioma (AxS) di P₀ con il termine s di τ e la regola MP di P₀ con l'operatore di applicazione di τ (quello che permette di costruire il termine (PQ) a partire dai termini P e Q), possiamo associare termini di τ a deduzioni nel frammento implicativo di P₀.
Per esempio, la deduzione descritta nella dimostrazione della Proposizione 3.1 di [SM] corrisponde al termine ((sk)k), che, non a caso, rappresenta un programma per il calcolo della funzione identita' (infatti, dato un termine P si puo' controllare che skkP →_s (kP)(kP) →_k P). Inoltre, cosi' come la β-riduzione corrisponde ad una semplificazione di derivazioni in deduzione naturale, cosi' le riduzioni →_s e →_k corrispondono a semplificazioni di derivazioni in P₀ (controllare tale affermazione come esercizio).