Curry-Howard, void e controllo del tipo in Haskell

Question

Sto cercando di capire un esempio di dimostrazione di teoremi tramite il controllo del tipo in Haskell fornito qui . L'esempio è il seguente.

Usando l'isomorfismo di Curry-Howard, costruisci un abitante del tipo e dimostralo $N= (A\vee (B\rightarrow A))\& (C\&(C\rightarrow B))\rightarrow ((\neg B\& A)\vee ((A\rightarrow B)\&(B\rightarrow A)))$ tiene.

L'autore fornisce un codice seguente.

data Void
nnot :: Void -> a
nnot = undefined
proposition :: (Either a (b -> a), (c, c -> b)) -> Either (Void -> b, a) (b -> a)
proposition (Left x, (y, f)) = Left (nnot, x)
proposition (Right g, (y,f)) = Left (nnot, (g (f y)))

L'implicazione $(A\vee (B\rightarrow A))\& (C\&(C\rightarrow B))\rightarrow (\neg B \& A)$non regge. Ma il termine costruito è affermato per dimostrarlo e il controllore di tipo ne è soddisfatto. Perché?

Sento che la trascrizione delle formule iniziali al tipo di propositionnon è corretta, poiché bè rappresentata la negazione di Void -> bche è l'assurdità (ed è definita come nnot). Cioè dal punto di vista logico, la coppia (Void -> b, a)corrisponde al termine$\bot \& A$. Ma questo non fornisce una risposta sul motivo per cui il controllo del tipo verifica il codice sopra. Pertanto, apprezzerò molto qualsiasi suggerimento sulle seguenti due domande.

1. Perché il compilatore Haskell approva il tipo di proposition?
2. Se questo è il caso in cui Curry-Howard non è a posto, come posso effettivamente utilizzare il controllo del tipo per provare le formule con negazione tramite Curry-Howard?

Non so né questa domanda sia più appropriata su cs o stackoverflow, quindi scusa se è fuori tema.

EDIT: data la seguente proposta corretta:

proposition :: (Either a (b -> a), (c, c -> b)) -> Either (b -> Void, a) (b -> a)

Ho scritto la seguente "prova" per questo e il controllo del tipo è stato soddisfatto. Non so se posso credere che la proposizione possa essere conteggiata come dimostrata dopo il controllo del tipo.

proposition (Left x, (y, f)) = Right ((\z1 z2 -> z1) x)
proposition (Right g, (y,f)) = Right ((\z1 z2 -> z1) (g (f y))) 

E ancora non ho idea se sia possibile provare qualsiasi negazione con la procedura di controllo del tipo.

Edit2: pensavo di aver capito un po 'l'argomento, ma poi ho provato quanto segue:

prop1 :: ((Either a b), c) -> b
prop1 (Right x, y) = x

Questo codice va bene per Haskell (ad esempio, lì ). Ma sembra essere mal digitato dal punto di vista della logica: il tipo corrispondente lo è$(A\vee B)\& C\rightarrow B$. È ovvio che il caso fornito prop1(Right x, y) = xha il tipo giusto (heh), ma non ho definito il caso per prop1(Left x, y), quindi la proposizione non è dimostrata per questo caso. Quindi, posso avere problemi anche con la disgiunzione.

Answer 1

Troverei un tutorial diverso perché l'autore di quello è fondamentalmente confuso. Lo affermano erroneamente$\neg a$ e $\bot\to a$ sono equivalenti ($a\to\bot$ sarebbe corretto), e anche erroneamente affermare che non è possibile scrivere una funzione di tipo $\texttt{Void}\to a$.

$\texttt{Void}\to a$è vacuamente vero. In linea di principio una funzione di quel tipo non dovrebbe richiedere alcuna definizione perché il numero di casi per i quali è necessario definirla è zero. GHC non lo accetta, ma (con -XEmptyCase) lo accetta

f :: Void -> a
f x = case x of {}

che è una definizione perfettamente valida e logicamente valida.

Perché il compilatore Haskell approva il tipo di proposta?

La proposizione scritta nel codice Haskell è effettivamente vera. La prova non è tuttavia valida poiché utilizza$\texttt{undefined}$.

Se hai sostituito il lato destro con $(b\to\texttt{Void},a)$ allora sarebbe falso, ma potresti ancora "provarlo" usando $\texttt{undefined}$; infatti potresti semplicemente scrivere$\texttt{proposition} = \texttt{undefined}$e il controllo del tipo lo accetterebbe. Accetterebbe anche$\texttt{proposition} = \texttt{proposition}$. Se vuoi usare Haskell come un sandbox di Curry-Howard devi fare attenzione che il tuo codice non generi un'eccezione o non riesca a terminare, perché il compilatore non rileverà quegli errori.

---

Risposta da modificare: la tua bozza è corretta ma può essere semplificata. Nel primo caso, non è necessario creare una funzione e applicarla immediatamente a uno dei suoi argomenti. Invece di (\z1 z2 -> z1) xpuoi scrivere \z2 -> x, o \_ -> xpoiché l'argomento / premessa non viene utilizzato. Nel secondo caso, non è necessario dimostrare b -> apoiché lo hai già fatto g :: b -> a. La dimostrazione semplificata è

proposition (Left x, _) = Right (\_ -> x)
proposition (Right g, _) = Right g

Oltre alle insidie ​​menzionate da Dan Doel in un commento, i casi mancanti sono un'altra cosa a cui prestare attenzione. GHC per impostazione predefinita non li avvisa nemmeno. Con -Werror=incomplete-patternsesso rifiuterà di accettare programmi con casi mancanti.

Puoi provare le negazioni. Devi restituire un valore di tipo$\texttt{Void}$, che non puoi creare da solo ma puoi ottenere altrove. Ad esempio, ecco una prova di$((P\Rightarrow Q) \mathbin{\&} \neg Q)\Rightarrow \neg P$:

f :: (a -> b, b -> Void) -> (a -> Void)
f (x, y) = \z -> y (x z)

Potresti ragionevolmente chiederti da dove il tuo chiamante ha ottenuto il valore di tipo $\texttt{Void}$, ma questo è il problema del chiamante, non il tuo. Derivare una contraddizione in una sottoprova non significa che la logica sia incoerente, significa solo che hai dimostrato che non raggiungerai mai questo punto nel mondo reale.