Curry-Howard, annulation et vérification de type dans Haskell

Question

J'essaie de comprendre un exemple de démonstration de théorème via la vérification de type dans Haskell donné ici . L'exemple est le suivant.

En utilisant l'isomorphisme de Curry-Howard, construisez un habitant du type et prouvez que $N= (A\vee (B\rightarrow A))\& (C\&(C\rightarrow B))\rightarrow ((\neg B\& A)\vee ((A\rightarrow B)\&(B\rightarrow A)))$ tient.

L'auteur fournit un code suivant.

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'implication $(A\vee (B\rightarrow A))\& (C\&(C\rightarrow B))\rightarrow (\neg B \& A)$ne tient pas. Mais le terme construit est censé le prouver, et le vérificateur de type en est satisfait. Pourquoi?

Je sens que la transcription des formules initiales au type de propositionest incorrecte, puisque la négation de best représentée avec Void -> blaquelle est l'absurdité (et elle est définie comme nnot). C'est-à-dire du point de vue logique, la paire (Void -> b, a)correspond au terme$\bot \& A$. Mais cela ne donne pas une réponse pour laquelle le vérificateur de type vérifie le code ci-dessus. Par conséquent, j'apprécierai grandement toute suggestion sur les deux questions suivantes.

1. Pourquoi le compilateur Haskell approuve-t-il le type de proposition?
2. Si tel est le cas lorsque Curry-Howard n'est pas en place, comment puis-je utiliser le vérificateur de type pour prouver des formules avec négation via Curry-Howard?

Je ne sais pas non plus que cette question est plus appropriée sur cs ou stackoverflow, alors veuillez nous excuser si elle est hors sujet.

EDIT: Compte tenu de la proposition corrigée suivante:

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

J'ai écrit la "preuve" suivante pour cela, et le vérificateur de type était satisfait. Je ne sais pas si je peux croire que la proposition peut être considérée comme prouvée après la vérification de type.

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

Et je ne sais toujours pas s'il est possible de prouver une négation par la procédure de vérification de type.

Edit2: Je pensais avoir une certaine compréhension du sujet, mais j'ai ensuite essayé ce qui suit:

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

Ce code est OK pour Haskell (par exemple, là - bas ). Mais il semble mal typé du point de vue de la logique: le type correspondant est$(A\vee B)\& C\rightarrow B$. Il est évident que le cas donné dans prop1(Right x, y) = xa le bon type (heh), mais je n'ai pas défini le cas pour prop1(Left x, y), donc la proposition n'est pas prouvée pour ce cas. Par conséquent, je peux aussi avoir des problèmes avec la disjonction.

Answer 1

Je trouverais un tutoriel différent car l'auteur de celui-ci est fondamentalement confus. Ils prétendent à tort que$\neg a$ et $\bot\to a$ sont équivalents ($a\to\bot$ serait correct), et prétend également à tort que vous ne pouvez pas écrire une fonction de type $\texttt{Void}\to a$.

$\texttt{Void}\to a$est vide de sens. En principe, une fonction de ce type ne devrait nécessiter aucune définition car le nombre de cas pour lesquels vous devez la définir est zéro. GHC n'accepte pas cela, mais (avec -XEmptyCase) il accepte

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

qui est une définition parfaitement valide et logique.

Pourquoi le compilateur Haskell approuve-t-il le type de proposition?

La proposition telle qu'elle est écrite dans le code Haskell est en fait vraie. La preuve est invalide car elle utilise$\texttt{undefined}$.

Si vous avez remplacé le côté droit par $(b\to\texttt{Void},a)$ alors ce serait faux, mais vous pourriez toujours le "prouver" en utilisant $\texttt{undefined}$; en fait tu pourrais juste écrire$\texttt{proposition} = \texttt{undefined}$et le vérificateur de type accepterait cela. Il accepterait également$\texttt{proposition} = \texttt{proposition}$. Si vous souhaitez utiliser Haskell comme bac à sable Curry-Howard, vous devez veiller à ce que votre code ne lève pas d'exception ou ne se termine pas, car le compilateur ne détectera pas ces erreurs.

---

Réponse à modifier: votre preuve est correcte mais elle peut être simplifiée. Dans le premier cas, il n'est pas nécessaire de créer une fonction et de l'appliquer immédiatement à l'un de ses arguments. Au lieu de cela, (\z1 z2 -> z1) xvous pouvez écrire \z2 -> x, ou \_ -> xpuisque l'argument / prémisse n'est pas utilisé. Dans le second cas, vous n'avez pas besoin de le prouver b -> apuisque vous l'avez déjà g :: b -> a. La preuve simplifiée est

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

En plus des écueils mentionnés par Dan Doel dans un commentaire, les cas manquants sont une autre chose à surveiller. GHC par défaut ne les avertit même pas. Avec -Werror=incomplete-patternselle refusera d'accepter les programmes avec des cas manquants.

Vous pouvez prouver des négations. Vous devez renvoyer une valeur de type$\texttt{Void}$, que vous ne pouvez pas créer vous-même mais que vous pouvez obtenir d'ailleurs. Par exemple, voici une preuve de$((P\Rightarrow Q) \mathbin{\&} \neg Q)\Rightarrow \neg P$:

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

Vous pouvez raisonnablement vous demander d'où votre appelant a obtenu la valeur de type $\texttt{Void}$, mais c'est le problème de l'appelant, pas le vôtre. Dériver une contradiction dans une sous-épreuve ne signifie pas que la logique est incohérente, cela signifie simplement que vous avez montré que vous n'atteindrez jamais réellement ce point dans le monde réel.