Una domanda sulla logica e sulla corrispondenza di Curry-Howard

Question

Potresti spiegarmi quale è la connessione di base tra i fondamenti della programmazione logica e il fenomeno della somiglianza sintattica tra i sistemi di tipi e la logica convenzionale?

Answer 1

La corrispondenza di Curry-Howard non riguarda la programmazione logica, ma la programmazione funzionale. La meccanica fondamentale di Prolog è giustificata nella teoria delle prove da John Robinson resolution technique, che mostra come è possibile verificare se le formule logiche espresse come clausole Horn siano satisfiable, ovvero se sia possibile trovare termini per sostituire le loro variabili logiche che li rendono vero.

Quindi la programmazione logica riguarda la specificazione dei programmi come formule logiche e il calcolo del programma è una qualche forma di inferenza di prova, nella risoluzione di Prolog, come ho detto. Al contrario, la corrispondenza di Curry-Howard mostra come le dimostrazioni in una speciale formula di logica, chiamate natural deduction, corrispondano a programmi nel calcolo lambda, con il tipo di programma corrispondente alla formula che la dimostrazione dimostra; il calcolo nel calcolo lambda corrisponde a un fenomeno importante nella teoria della prova chiamato normalizzazione, che trasforma le prove in nuove prove più dirette. Quindi la programmazione logica e la programmazione funzionale corrispondono a diversi livelli in queste logiche: i programmi logici corrispondono a formule di una logica, mentre i programmi funzionali corrispondono a prove di formule.

C'è un'altra differenza: le logiche utilizzate sono generalmente diverse. La logica di programmazione generalmente utilizza le logiche più semplici — come ho detto, il Prolog è basato sulle clausole di Horn, che sono una classe di formule altamente ristretta in cui le implicazioni non possono essere annidate, e non ci sono disgiunzioni, sebbene Prolog recuperi tutta la forza della logica classica usando il regola di taglio. Al contrario, i linguaggi di programmazione funzionale come Haskell fanno un uso pesante di programmi i cui tipi hanno implicazioni nidificate e sono decorati da tutti i tipi di forme di polimorfismo. Si basano anche sulla logica intuizionista, una classe di logiche che proibisce l'uso del principio del mezzo escluso, su cui si basa il meccanismo computazionale di Robinson.

Alcuni altri punti:

1. E 'possibile la programmazione logica di base su logiche più sofisticate di clausole di Horn; ad esempio, Lambda-prolog si basa sulla logica intuizionista, con un meccanismo di calcolo diverso dalla risoluzione.
2. Dale Miller ha chiamato il paradigma a prova di teoria dietro logica di programmazione la ricerca prova di come la programmazione metafora, in contrasto con le prove come programmi metafora che è un altro termine usato per la corrispondenza di Curry-Howard.

Answer 2

La programmazione logica è fondamentalmente basata sulla ricerca diretta di prove. La relazione strutturale tra i linguaggi tipizzati e la logica generalmente implica linguaggi funzionali, sebbene a volte imperativi e altre lingue - ma non i linguaggi di programmazione logica direttamente. Questa relazione collega le dimostrazioni ai programmi.

Così, la ricerca di prove di programmazione logica può essere utilizzata per trovare prove che vengono quindi interpretate come programmi funzionali. Questa sembra essere la relazione più diretta tra i due (come richiesto).

Costruire interi programmi in questo modo non è pratico, ma può essere utile per riempire i noiosi dettagli nei programmi, e ci sono alcuni esempi importanti di questo nella pratica. Un esempio di base di questo è il sottotipo strutturale, che corrisponde alla compilazione di alcuni passaggi di prova tramite una semplice prova di sicurezza.Un esempio molto più sofisticato è il sistema di classe tipo di Haskell, che comporta un particolare tipo di ricerca diretta all'obiettivo - nel caso estremo si tratta di una forma di programmazione logica completa di Turing in fase di compilazione.