Curry Howard corrispondenza e tesi di chiesa della chiesa

Question

La corrispondenza Curry-Howard afferma l'equivalenza tra logica/detrazione e tipi/programmi.

La tesi della Chiesa-Turing afferma l'equivalenza di alcuni modelli di calcolo. In particolare, tutte le funzioni calcolabili possono essere scritte sia su una macchina Turing che nel calcolo Lambda.

Tuttavia, non tutte le logiche sono equivalenti. Logica del 2 ° ordine può quantificare i set mentre 1 ° ordine Non posso.

Qualcuno può spiegare la dissonanza? Alcune funzioni calcolabili possono essere espresse a un "livello superiore" ma non a un "livello più semplice"?

UNA PRECISAZIONE

Se definisco un modello per il calcolo, dire la logica del 2 ° ordine mentre la macchina Turing è un modello per la logica del 1 ° ordine, ciò significa che il mio linguaggio ipotetico può calcolare le funzioni "non pubblicabili"? Mi sembra così perché la logica del 2 ° ordine è più potente della logica del 1 ° ordine. Questo è chiaramente senza senso perché Haskell si basa su un sapore di 2 ordini logica (sistema F con estensioni) ma non è più potente di dire C: qualsiasi programma realizzabile in Haskell è realizzabile in C. La mappatura (o equivalenza) tra logica e Il calcolo non sembra preservare la nozione di forza: la logica del 2 ° ordine è più forte della logica del 1 ° ordine, ma i linguaggi di programmazione sulla logica del 2 ° e del 1 ° ordine hanno la stessa forza. Ha senso?

L'unica conclusione a cui posso venire è che la relazione tra logica e tipi non è una mappatura semplice. La macchina Turing non si basa su alcuna logica specifica e che qualsiasi sistema logico/deduttivo possa essere mappato sulla macchina Turing. Puoi confermare?

Parole di chiusura

Penso che il mio errore non stia realizzando che esiste una grande divisione tra il "programma" colloquiale e i programmi nel contesto dei tipi.

Haskell che si basa su un sistema di tipo più forte e più espressivo fornisce effettivamente programmi più forti ed espressivi. Questi programmi sono più forti nel senso che più possono essere garantiti su di loro (nello stesso senso di "tipo sicuro"). Ciò non significa che Haskell possa "calcolare" di più; È ancora semplicemente completo completo.