Djinn est un vérificateur de théorèmes. Il semble que votre question soit : qu'est-ce que la preuve de théorème a à voir avec la programmation ?
La programmation fortement typée a une relation très étroite avec la logique. En particulier, les langages fonctionnels traditionnels de la tradition ML sont étroitement liés à la logique. Intuitionniste Logique propositionnelle .
Le slogan est "les programmes sont des preuves, la proposition qu'un programme prouve est son type".
En général, vous pouvez penser à
foo :: Foo
comme disant que foo est une preuve de la formule Foo . Par exemple, le type
a -> b
correspond aux fonctions de a a b donc si vous avez une preuve de a et une preuve de a -> b vous avez une preuve de b . Ainsi, la fonction correspond parfaitement à l'implication en logique. De même,
(a,b)
Correspond à la conjonction (logique et). Donc la tautologie logique a -> b -> a & b correspond au type Haskell a -> b -> (a,b) et a la preuve :
\a b -> (a,b)
c'est la "règle de l'introduction" Alors que, fst :: (a,b) -> a y snd :: (a,b) -> b correspondent aux 2 "règles d'élimination"
de la même manière, a OR b correspond au type Haskell Either a b .
Cette correspondance est parfois appelée "isomorphisme de Curry-Howard" ou " Correspondance Curry-Howard "après Haskell Curry y William Alvin Howard
Cette histoire est compliquée par la non-totalité en Haskell.
Djinn est "juste" un vérificateur de théorèmes.
Si vous souhaitez essayer d'écrire un clone, la première page de résultats de Google pour "Simple Theorem Prover" contient les éléments suivants este qui décrit l'écriture d'un vérificateur de théorèmes pour LK qui semble être écrit en SML.
Edit : à la question "comment la preuve par le théorème est-elle possible ?" La réponse est que dans un certain sens, ce n'est pas difficile. C'est juste un problème de recherche :
Considérons le problème reformulé comme suit : nous avons un ensemble de propositions que nous savons prouver S, et une proposition que nous voulons prouver P. Que faisons-nous ? Tout d'abord, nous demandons : avons-nous déjà une preuve de P dans S ? Si oui, nous pouvons l'utiliser, sinon nous pouvons correspondance de motifs sur P
case P of
(a -> b) -> add a to S, and prove b (-> introduction)
(a ^ b) -> prove a, then prove b (and introduction)
(a v b) -> try to prove a, if that doesn't work prove b (or introduction)
si aucune de ces solutions ne fonctionne
for each conjunction `a ^ b` in S, add a and b to S (and elimination)
for each disjunction `a v b` in S, try proving `(a -> P) ^ (b -> P)` (or elimination)
for each implication `a -> P` is S, try proving `a` (-> elimination)
Les vrais prouveurs de théorèmes ont un peu d'intelligence, mais l'idée est la même. Le domaine de recherche des "procédures de décision" examine la stratégie permettant de trouver des preuves pour certains types de formules dont le fonctionnement est garanti. D'autre part, la "tactique" examine comment ordonner de manière optimale la recherche de preuves.
Quant à : "Comment traduire les preuves en Haskell ?"
Chaque règle d'inférence d'un système formel correspond à une construction Haskell simple, donc si vous avez un arbre de règles d'inférence, vous pouvez construire un programme correspondant - Haskell est un langage de preuve après tout.
Introduction de l'implication :
\s -> ?
Ou introduction
Left
Right
Et introduction
\a b -> (a,b)
Et l'élimination
fst
snd
etc.
augustss dit dans sa réponse que la façon dont il a implémenté cela dans Djinn est un peu fastidieuse pour une réponse SO. Je parie cependant que vous pouvez trouver comment l'implémenter par vous-même.
