Applications quotidiennes de la théorie des types

10

Je veux comprendre la théorie des types mais je dois d'abord savoir comment l'appliquer. Pourrait-il y avoir des applications plus évidentes de la théorie des types en dehors des systèmes de types en programmation? Pourrait-il y avoir d'autres applications, disons dans le profilage de personnalité et autres?

Tamad Lang
la source
2
Pourquoi quelque chose doit-il avoir des applications en dehors de ce pour quoi il a été inventé?
Raphael
3
Fondements des mathématiques? Les gens ont également utilisé la théorie des types pour formaliser des choses comme la théorie des domaines synthétiques, la topologie, etc. Il y a aussi le travail de Chris Martens sur l'utilisation d'outils de théorie des types pour modéliser la narration narrative. Lien de thèse
Daniel Gratzer
1
Pourriez-vous clarifier les comptes comme application?
Jake
4
Je ne suis pas convaincu par votre prémisse. Supposons que quelqu'un dise: "Je veux comprendre l'ingénierie automobile mais je dois d'abord savoir à quoi je peux utiliser une voiture. Pourrait-il y avoir des applications plus évidentes des voitures en dehors du transport?" Ils obtiennent des réponses disant que certaines personnes dorment dans leurs voitures, et Ansel Adams a utilisé la sienne comme plate-forme pour prendre des photos . Eh bien, c'est super, mais cela n'aide personne à comprendre l'ingénierie et conduira probablement notre étudiant hypothétique à concevoir des voitures avec des sièges super inclinables et une suspension très rigide.
David Richerby
3
Le fait est qu'une grande partie de l'informatique théorique (y compris les choses sur lesquelles je travaille) est pratiquement inutile, bien que mathématiquement belle. Malheureusement, vous devez choisir votre camp.
Yuval Filmus

Réponses:

10

Vous pouvez être intéressé par les travaux sur Ceptre , un résultat de la recherche doctorale de Chris Martens , qui utilise la théorie des types pour la narration interactive. Voici le résumé de la thèse :

La narration interactive associe des idées informatiques profondes à la riche histoire de l'histoire et du jeu de l'humanité, fournissant un contexte important pour les outils et les langages à construire. Dans le même temps, les langages de spécification formels offrent une palette de techniques de représentation et d'inférence généralement réservées à l'analyse des langages de programmation et des systèmes déductifs complexes. Cette thèse relie les problèmes du domaine de la narration interactive aux solutions de spécification formelle.

Plus précisément, nous examinons le récit d'un point de vue structurel et observons que les chemins narratifs alternatifs jouent un rôle complémentaire aux chronologies d'interaction simultanée. La logique linéaire fournit les outils de représentation nécessaires pour étudier cette structure, et en étendant la correspondance aux preuves et à la construction de preuves, nous trouvons une suite de possibilités de calcul. Nous présentons trois efforts pour réaliser ces possibilités: (1) l'utilisation de la programmation logique linéaire pour générer des récits; (2) un nouveau langage de programmation pour créer des récits interactifs, des jeux et des simulations; et (3) des techniques pour énoncer et prouver les propriétés du programme au niveau de la conception.

Nous constatons que la programmation logique linéaire, enrichie d'une extension minimale de sa sémantique logique, permet une large gamme d'idiomes de programmation et d'encodages de domaine. Pour preuve, nous donnons cinq études de cas, y compris la simulation sociale, les jeux d'aventure basés sur le combat et les jeux de société. Pour soutenir le raisonnement sur l'exactitude de la conception, nous présentons des techniques pour énoncer et prouver les invariants de programme, ainsi qu'une preuve de décidabilité pour vérifier automatiquement ces invariants pour un grand fragment du langage.

Ces résultats montrent que la logique linéaire est un langage de représentation fructueux pour servir de base à la modélisation et à l'exécution de mondes interactifs, et ils invitent à de futures recherches sur l'utilisation de méthodologies de preuve-théorique pour les systèmes créatifs.

gasche
la source
1
Cela ressemble à une utilisation de la logique linéaire, plutôt qu'à une théorie des types en soi .
David Richerby
6
La logique linéaire est un sujet fondamental de la théorie des types. Ce travail fait partie de la théorie des types en tant que discipline (certaines personnes décrivent leur travail comme "théorie de la preuve" quand il est également pertinent pour la théorie des types, bien que les noms ne soient pas équivalents car certains autres travaux de la "théorie de la preuve" seraient considérés comme plus spécifique à la théorie de la preuve qu’au centre de la théorie des types).
gasche
9

Il y a eu des utilisations intéressantes de la théorie des types en linguistique. Voir par exemple les ouvrages linguistiques de Chung-chieh Shan ou Christian Rétoré .

Ci-dessous est la description du livre de Rétoré sur les grammaires catégorielles:

Ce livre est une introduction contemporaine et complète aux grammaires catégorielles dans la tradition logique initiée par les travaux de Lambek. Il guide les étudiants et les chercheurs à travers les résultats fondamentaux dans le domaine, fournissant des preuves modernes de nombreux théorèmes classiques, ainsi que des avancées récentes originales. De nombreux exemples et exercices illustrent les motivations et les applications de ces résultats d'un point de vue linguistique, informatique et logique. Le calcul de Lambek et ses variantes, ainsi que les grammaires correspondantes, sont au cœur de ces notes de cours. Un chapitre est consacré à une caractéristique clé de ces grammaires catégorielles: leur interface syntaxique-sémantique très élégante. De plus, nous adaptons des réseaux de preuve de logique linéaire à ces calculs car ils fournissent des algorithmes d'analyse efficaces comme illustré dans l'analyseur Graal.

La citation suivante est dans l'introduction des effets secondaires linguistiques de Shan chapitre du livre sur les :

Cet article relie les cas de non-compositionnalité apparente dans les langues naturelles à ceux des langages de programmation. Il a la forme d'un sablier: je commence au §1 par une approche de l'interface syntaxique-sémantique qui nous aide à construire des théories sémantiques compositionnelles. Cette approche consiste à établir une analogie entre les effets secondaires de calcul dans les langages de programmation et ce que j'appelle par analogie les effets secondaires linguistiques dans les langages naturels.

Cette connexion peut bénéficier aux informaticiens ainsi qu'aux linguistes, mais je me concentre ici sur cette dernière direction du transfert de technologie. Les continuations ont été utiles pour traiter les effets secondaires de calcul. Au §2, j'introduis un nouveau métalangage pour les continuations en sémantique.

Le métalangage que j'introduis est utile pour analyser à la fois les langages de programmation et les langages naturels. Pour l'intuition, je passe en revue la première utilisation au §3, puis souligne les vertus de ce traitement au §4.

Passant au langage naturel au §5, je décris en détail comment cette perspective a aidé Chris Barker et moi à étudier la liaison et le croisement, ainsi que les questions de la WH et la supériorité. J'ai également utilisé des continuations pour étudier la quantification et la portée indéfinie, en particulier en chinois mandarin, mais il n'y a que de la place ici pour esquisser ces développements ultérieurs, au §6.

gasche
la source
9

En raison de la correspondance Curry-Howard , les types peuvent être interprétés comme des propositions et les propositions comme des types.

En conséquence, la théorie des types est applicable à littéralement n'importe quel domaine qui utilise la logique formelle pour ses preuves. Cela peut être une vérification de circuit, une analyse réelle, une logique symbolique, une géométrie, etc.

Par exemple, certains outils automatisés de vérification des preuves fonctionnent selon ce principe: ils vérifient la validité de la preuve en vérifiant le type d'un terme particulier dans un système de type. Le vérificateur d'épreuves LF est basé sur cette approche, tout comme HOL Light . À titre d'exemple d'application, le code de vérification de preuve a utilisé LF pour vérifier les preuves de sécurité de la mémoire du code non approuvé. L'avantage d'utiliser ce type de vérificateur est que la mise en œuvre peut être très simple, et nous pouvons ainsi obtenir une assurance élevée que la mise en œuvre est correcte. Voir, par exemple, le document suivant:

Vérificateurs de preuve fondamentaux avec de petits témoins . Dinghao Wu, Andrew W. Appel, Aaron Stump. PPDP 2003.

jmite
la source
Cela pourrait aider: math.ucr.edu/home/baez/rosetta.pdf
Pseudonyme
Je ne pense pas que cela réponde à la question. Qu'en est-il des applications réelles?
Yuval Filmus
@YuvalFilmus Définir "réel"?
David Richerby
1
Savez-vous si quelqu'un a utilisé la théorie des types pour prouver quelque chose de nouveau sur la vérification des circuits, l'analyse réelle, la logique symbolique ou la géométrie? Ou parlons-nous seulement de cas où quelqu'un utilise 20 pages de théorie des types pour prouver quelque chose qui prend trois lignes dans un manuel élémentaire?
David Richerby
@David Qu'est-ce que cette réponse est qu'en principe, vous pouvez utiliser la théorie des types pour prouver des choses. De plus, en principe, nous pouvons utiliser des automates cellulaires pour prouver des choses, puisque la règle 110 est Turing-complete. Je pense que la première déclaration est aussi dénuée de sens que la seconde.
Yuval Filmus
7

Un article intéressant qui explique les applications des types dépendants, est The Power of Pi , qui montre comment Agda peut être utilisé pour résoudre des problèmes intéressants.

Un autre bon exemple est l'utilisation de types dépendants pour contrôler les ressources. Un bon exemple est l'API de gestion de fichiers d' Effets of Idris . Par exemple, la fonction de lecture d'une ligne dans un fichier a le type suivant

readLine  : { [FILE_IO (OpenFile Read)] } Eff String

qui spécifie que cette fonction n'est applicable que si un fichier est ouvert. La liste entre accolades indique les effets disponibles. Dans ce cas, nous avons que cette fonction nécessite d'avoir un fichier ouvert en lecture.

Vous trouverez plus d'informations sur la bibliothèque d'effets ici .

Une autre application est l'utilisation de types dépendants pour la concurrence, comme indiqué dans l' article suivant par le créateur d'Idris.

Rodrigo Ribeiro
la source
1
Plus d'exemples ajoutés.
Rodrigo Ribeiro
3

comme mentionné dans la réponse de jmite, la théorie de logique / type d'ordre supérieur dans la vérification des circuits / matériel / électronique existe depuis des décennies et est maintenant si routinière qu'elle n'est même plus remarquée / considérée comme une "application" après un effort de transfert apparemment majeur dans les années 90, bien que son domaine de recherche soit toujours actif. il y a aussi beaucoup d'application de Coq et de sa logique de type, en particulier pour la vérification de circuits / matériel / électronique, de la logique de porte de bas niveau à des structures / sous-systèmes de niveau / ordre beaucoup plus élevés. voici quelques références clés

vzn
la source
1
Pour être juste, cependant, la plupart des vérifications matérielles à l'échelle industrielle ont été effectuées à l'aide de la vérification des modèles, une technologie de vérification qui n'est généralement pas liée à la théorie des types (bien que des ponts aient été récemment dessinés). La théorie des types a été utilisée pour créer des langages de description du matériel (pas très éloignés des langages de programmation), et la plupart des langages que vous donnez sont dans cette catégorie, et certains des assistants de vérification conçus pour la vérification du matériel (notamment le HOL d'origine, mais pas le PVS le plus utilisé) sont des transpositions de Curry-Howard de la théorie des types.
gasche
si vous avez une expérience approfondie de la vérification du matériel, il serait intéressant d'entendre plus de détails dans Computer Science Chat, mais il n'est pas facile de tracer / suspecter des lignes / généralisations étroites / distinctes dans ce domaine, par exemple entre la vérification des modèles et la théorie des types. Cela peut prendre une analyse historique très subtile pour découvrir / reconstituer de manière complète les connexions entre deux domaines différents avec des objectifs différents et est parfois même en dehors des capacités des experts dans l'un ou l'autre domaine individuellement ... les références globales montrent des connexions solides qui pourraient être analysées plus en détail. ..
vzn