Développements d'algorithmes dans le calcul des constructions - Université de Lorraine Accéder directement au contenu
Thèse Année : 1994

Développements d'algorithmes dans le calcul des constructions

Joseph Rouyer
  • Fonction : Auteur
  • PersonId : 756558
  • IdRef : 027113957

Résumé

Not available
Le calcul des constructions est d'abord un lambda-calcul type d'ordre supérieur avec polymorphisme et types dépendants. La forte normalisation de ce lambda-calcul a été prouvée par Thierry Coquand qui en a fait un langage logique d'ordre supérieur permettant de coder la logique naturelle intuitionniste. Il en a démontré la cohérence et en a réalisé les premières implantations. Ce calcul des constructions initial a été enrichi (à la suite des travaux de Christine Paulin-Mohring) par de nouvelles sortes puis par les types inductifs et un procédé d'extraction de programmes. C'est dans l'implantation v5.8 de cette dernière version que nous avons développé un algorithme d'unification au premier ordre (celui de Robinson), puis deux algorithmes de recherche de recouvrements connexes d'un graphe pondère, celui de Prim et celui de Kruskal. Ces algorithmes ont été entièrement synthétises. Il ne s'agit pas de simples preuves de programmes. Le revers de la médaille est que les programmes que l'on extrait de ces preuves contiennent des calculs provenant de la preuve de terminaison qui ne servent pas dans la construction du résultat. Pour l'algorithme d'unification nous montrons de deux manières comment, en réalisant un axiome d'induction non structurelle, on peut réduire au maximum les traces de la preuve de terminaison
Fichier non déposé

Dates et versions

tel-01751855 , version 1 (29-03-2018)

Identifiants

  • HAL Id : tel-01751855 , version 1

Accès intranet

Citer

Joseph Rouyer. Développements d'algorithmes dans le calcul des constructions. Ordinateur et société [cs.CY]. Institut National Polytechnique de Lorraine, 1994. Français. ⟨NNT : 1994INPL042N⟩. ⟨tel-01751855⟩
64 Consultations
0 Téléchargements

Partager

Gmail Facebook X LinkedIn More