Mise en œuvre de la théorie mathématique de l'arithmétique dans Haskell via Curry-Howard Correspondance

Question

Je dois demander pardon à l'avance si toute la question n'a pas beaucoup de sens, mais malheureusement, je n'ai pas une meilleure intuition pour le moment et cela semble être le meilleur point de départ que je puisse trouver.

Je lis le livre de Tarski "Introduction à la logique: et à la méthodologie des sciences déductives", je suis sur la partie VII Chapitre 43 "Termes primitifs de la théorie en construction; axiomes concernant les relations fondamentales entre les nombres". Il commence par présenter une théorie mathématique élémentaire de l'arithmétique des nombres réels.

Les termes primitifs sont:

• nombre réel (indiqué comme des variables comme x, y)
• est inférieur à (<)
• est supérieur à (>)
• somme (+)
• N ce qui signifie "l'ensemble de tous les nombres". Ainsi, une expression "x est un nombre" serait écrite comme x ∈ N
• n'est pas moins que (≮)
• n'est pas plus grand que (≯)

Parmi les axiomes de la théorie considérés, deux groupes peuvent être distingués. Les axiomes du premier groupe expriment les propriétés fondamentales des relations inférieures à celles et supérieures à celles, tandis que celles du second sont principalement concernées par l'addition. Pour le moment, nous considérerons le premier groupe uniquement; Il consiste, au total, de cinq déclarations:

• Axiome 1. pour tous les nombres x et y (Par exemple, pour les éléments arbitraires de l'ensemble N) Nous avons: x = y ou x < y ou x > y
• Axiome 2. Si x < y, alors y ≮ x
• Axiome 3. Si x > y, alors y ≯ x
• Axiome 4. Si x < y et y < z, alors x < z
• Axiome 5. Si x > y et y > z, alors x > z

Notre tâche suivante consiste en la dérivation d'un certain nombre de théorèmes des axiomes adoptés par nous:

• Théorème 1. Aucun nombre n'est plus petit que lui-même x ≮ x
• Théorème 2. Aucun nombre n'est supérieur à lui-même: x ≯ x

Maintenant, je dois m'arrêter et enfin expliquer mes intentions. J'ai entendu plusieurs fois sur une soi-disant «correspondance curry-howard-lambek», et cela avait du sens chaque fois que j'en ai lu des exemples. Je ne suis pas non plus à l'aise pour écrire manuellement le raisonnement pour prouver les théorèmes, j'aimerais que la machinerie passe par des étapes de raisonnement à vérifier par un ordinateur pour moi.

J'ai donc essayé d'encoder les termes, les axiomes et les théorèmes potentiellement (je suis resté bloqué plus tôt) dans Haskell, mais j'ai échoué à bien des égards. Je ne vous montrerai pas tous les exemples de ce que j'ai fait, mais voici l'approche la plus naïve des propositions d'encodage comme types et leurs preuves comme programmes:

data Nats
  = NatX
  | NatY
  | NatZ

x :: Nats
x = NatX

data OpGt =
  OpGt Nats
       Nats

data OpLt =
  OpLt Nats
       Nats

data OpEq =
  OpEq Nats
       Nats

data OpNotLt =
  OpNotLt Nats
          Nats

data OpNotGt =
  OpNotGt Nats
          Nats

data Ax1Res
  = Ax1ResLt OpLt
  | Ax1ResGt OpGt
  | Ax1ResEq OpEq

-- how to implement best?
ax1 :: Nats -> Nats -> Ax1Res
ax1 = undefined

-- this doesn't describe the x and y in the type
ax2 :: OpLt -> OpNotGt
ax2 = undefined

Ce morceau de code apporte plus de questions qu'il ne donne des réponses:

• Les axiomes devraient-ils être mis en œuvre ou conservés comme des fonctions non implémentées que nous supposons simplement exister?
• Comment limiter la mise en œuvre de mes fonctions pour ne s'appuyer que sur les théorèmes et les axiomes disponibles si je peux construire essentiellement un terme? Dois-je cacher les constructeurs?
• Les types doivent évidemment contenir des variables comme x et y, J'ai essayé cela dans d'autres approches mais cela devient encore plus poilu

Mes questions sont:

• Quelle serait une mise en œuvre appropriée de ces preuves dans Haskell?
• Quels matériaux dois-je lire afin de faire une implémentation appropriée moi-même et de mieux comprendre le sujet?

J'espère que l'imprécision et mon niveau d'ignorance dans la question ne vous permettra pas de y répondre. Merci!