Quelle est la base théorique de la programmation impérative?

48

La programmation fonctionnelle a une base théorique en calcul lambda et en logique combinatoire . En tant que personne impliquée dans le calcul statistique, je trouve ces concepts très utiles pour la modélisation.

Existe-t-il une base mathématique équivalente pour la programmation impérative , ou s'agit-il simplement d'une application matérielle pratique en langage machine et du développement ultérieur de FORTRAN ?

Shane
la source

Réponses:

27

En général, lorsque les mathématiques sont utilisées pour étudier un X , il faut d’abord un modèle de X , puis développer une théorie, un ensemble de résultats concernant ce modèle. Je suppose que la théorie peut être considérée comme une « base théorique » pour X . Définissez maintenant X = calcul. Il existe de nombreux modèles de calcul, beaucoup impliquant "l'état". Chaque modèle a sa propre "théorie" et il est parfois possible de "traduire" entre les modèles. Je crois qu'il est difficile de dire quel modèle est le plus "basique" - ils sont simplement conçus avec des objectifs différents.

Les machines de Turing ont été conçues pour définir ce qui est calculable . Donc, ils font un bon modèle si vous vous souciez de savoir s'il existe un algorithme pour un certain problème. On abuse parfois de ce modèle pour étudier l' efficacité d'algorithmes ou la dureté des problèmes, sous prétexte qu'il est suffisant, du moins si vous vous souciez uniquement de polynôme / non-polynôme. Le modèle de RAM est plus proche d'un ordinateur réel et donc mieux si vous voulez une analyse précise d'un algorithme. Pour minimiser la dureté des problèmes, il vaut mieux ne pasUtilisez un modèle qui ressemble trop aux ordinateurs d'aujourd'hui, car vous souhaitez couvrir un large éventail d'ordinateurs possibles, tout en restant plus précis que les systèmes polynomiaux / non polynomiaux. Dans ce contexte, j'ai vu par exemple le modèle de sonde cellulaire utilisé.

Si vous vous souciez de l' exactitude , d'autres modèles sont encore utiles. Ici, vous avez la sémantique opérationnelle (qui serait l'analogue du lambda calcul pour les calculs étatiques), la sémantique axiomatique (développée en 1969 par Hoare sur la base des assertions inductives de Floyd de 1967, popularisées par Knuth dans The Art of Computer Programming , volume 1) et autres.

Pour résumer, je pense que vous recherchez des modèles de calcul. Il existe de nombreux modèles de ce type, développés avec des objectifs variés, et beaucoup ont un état, ils correspondent donc à une programmation impérative. Si vous voulez savoir si quelque chose peut être calculé, examinez les machines de Turing. Si vous vous souciez de l'efficacité, regardez les modèles de RAM. Si vous vous souciez de l'exactitude, regardez les modèles qui se terminent par une "sémantique", telle que la sémantique opérationnelle.

Enfin, permettez-moi de mentionner qu’il existe un grand livre en ligne uniquement sur Models of Computation de John Savage. C'est surtout une question d'efficacité. Pour la partie concernant l'exactitude, je vous recommande de commencer par les articles classiques de Floyd (1967) , Hoare (1969) , Dijkstra (1975) et Plotkin (1981) . Ils sont tous plutôt cool.

Radu GRIGore
la source
4
Je pense que la sémantique opérationnelle est bien ce que recherche l’affiche. Un peu plus d'infos sur wikipedia: en.wikipedia.org/wiki/Semantics_performants
sclv
22

Le modèle théorique le plus simple d'un programme impératif est la machine de Turing elle-même. Il comporte les deux composants essentiels d’un programme impératif: un état modifiable non borné et une machine à états qui le gère.

Vous pouvez également intégrer la programmation impérative à la programmation fonctionnelle en considérant les programmes comme des compositions d'opérations monadiques qui transmettent et renvoient des versions modifiées de l'état global, comme dans le langage de programmation Haskell.

Alexandre Passos
la source
2
Utiliser des monades pour obtenir des constructions de type impératif dans un langage purement fonctionnel (tel que Haskell) ne vous donne pas toute la puissance de la programmation impérative. En particulier, sans état véritablement mutable (comme dans de nombreux langages avec références), il existe encore de nombreuses structures de données dont la mise en oeuvre efficace dans un langage purement fonctionnel est inconnue.
Joshua Grochow
@ Josué: Pourquoi pensez-vous que les monades d'État n'expriment pas la sémantique des références? Je n'arrive pas à comprendre ce que l'objection pourrait être.
Charles Stewart
Une monade d'état est fondamentalement un sucre syntaxique pour avoir une collection de fonctions qui acceptent toutes un argument supplémentaire (état) et produisent une sortie supplémentaire (état suivant). Mais dans un langage purement fonctionnel, vous ne pouvez pas réellement modifier l'état pour obtenir l'état suivant, vous devez toujours copier et reconstruire. Je ne sais pas s'il existe des structures de données spécifiques pour lesquelles on sait qu'elles ne peuvent pas être mises en œuvre efficacement dans un langage purement fonctionnel, mais il existe certainement des preuves suggestives (par exemple, Pippenger. Pure vs impure Lisp. 1997).
Joshua Grochow
6
On peut parfaitement bien saisir la sémantique de la mutation avec les monades - voir, par exemple, la monade ST à Haskell. Nous parlons ici de sémantique, pas de mise en œuvre.
sclv
20

En bref, je dirais que la programmation impérative a évolué à partir du langage machine et de la pratique de la programmation. D'autre part, les monades fournissent un cadre sémantique approprié pour décrire la sémantique des fonctionnalités impératives du langage de programmation. Les notions de calcul et de monades de Moggi établissent les fondements formels. Phil Wadler a popularisé cette idée et a largement contribué à en faire le moyen essentiel d'intégrer des fonctionnalités impératives dans le langage de programmation Haskell. Des travaux récents de Plotkin et de Power Notions of Computation déterminent des monades en sens contraire, certaines notions de calcul (impératif), mais pas toutes, donnent une monade, ce qui signifie que les monades correspondent de manière essentielle aux notions de calcul impératives (et autres).

Dave Clarke
la source
8
Les monades peuvent être utilisées pour isoler la programmation impérative dans un monde purement fonctionnel, mais je ne vois pas l'intérêt de prétendre qu'elles constituent une base théorique pour une programmation impérative analogue à la relation entre le lambda calcul et de nombreux langages fonctionnels. Les monades ne modélisent pas le calcul autant qu'elles forment une abstraction sur des classes de calcul (par exemple, calcul pur vs calcul qui implique IO, ou calcul qui repose sur un paquet particulier d'état mutable).
blucz
1
Les monades sont un moyen d'écrire une sémantique dénotationnelle plus claire pour les langages efficaces, alors pourquoi pas?
nponeccop
15

Si vous recherchez un traitement mathématique rigoureux d'un langage de programmation impératif, le livre de Winskel "La sémantique formelle des langages de programmation" (1993) en est un exemple.

Dans le livre, il définit un langage de programmation impératif appelé IMP et en fournit une sémantique opérationnelle, dénotationnelle et axiomatique.

Yhirai
la source
14

J'arrive en retard à cette question, mais c'est une question fascinante. Alors, voici mes points de vue.

Lorsque j'étais étudiant, nous avions un excellent professeur de mathématiques qui nous donnait des conférences sur l'histoire et le développement des mathématiques. Selon lui, les mathématiques se sont développées par vagues "d'expansion" et de "consolidation". Au cours d'une phase d'expansion, de nouvelles idées jusqu'alors inconnues ont été examinées et étudiées. Ensuite, lors d’une phase de consolidation, les nouvelles théories ont été intégrées au corpus de connaissances existant. Cependant, au 20ème siècle, a-t-il dit, l'expansion et la consolidation se déroulent en parallèle.

La programmation impérative est actuellement une activité d'expansion pour les mathématiques. C'était auparavant "inconnu". (Cela peut ne pas être tout à fait vrai. Hoare nous dit qu'Euclid faisait quelque chose de programmation impérative dans sa géométrie. Mais les mathématiques s'y sont désintéressées, pour le meilleur ou pour le pire.) Les mathématiciens ne s'intéressent toujours pas à la programmation impérative. Tellement la perte pour eux. Mais je considère toute l’informatique comme une branche des mathématiques dans un sens abstrait. Nous l'étudions en développant les mathématiques.

Donc, je ne voudrais pas savoir s'il existe une base théorique a priori pour la programmation impérative. S'il n'y en a pas, allons le chercher. Ce que nous savons déjà nous dit que la programmation impérative est incroyablement profonde et belle. La programmation fonctionnelle est dérisoire en comparaison. Mais nous avons beaucoup de travail à faire pour faire connaître toute cette théorie aux gens.

Uday Reddy
la source
"La programmation fonctionnelle est médiocre en comparaison". Maintenant, si seulement je pouvais vous et Bob Harper entrer dans une arène de combat. Vous balanceriez un gros bloc de commandes et il essaierait de vous fermer la porte. (PS: très bonne réponse, je l'ai voté.)
Andrej Bauer
Eh bien, il m'évite en quelque sorte. Je ne sais pas si ça veut dire quoi que ce soit :-)
Uday Reddy
11

La programmation fonctionnelle a une base claire en mathématiques, car les langages de programmation fonctionnels ont évolué parallèlement aux mathématiques pertinentes et leurs concepteurs ont généralement tenu les mathématiques en haute estime. La relation forte et directe est une prophétie auto-réalisatrice.

La programmation impérative a une histoire beaucoup plus complexe qui est liée beaucoup plus étroitement aux problèmes d’entreprise et d’ingénierie et était historiquement beaucoup plus préoccupée par la performance des compilateurs et du code qu’ils génèrent que par le respect des formalismes mathématiques.

Beaucoup de gens ont tenté d'expliquer la programmation impérative en termes (traditionnellement) fonctionnels. C’est peut-être ce qui se rapproche le plus de ce que vous cherchez, mais ces tentatives sont toujours maladroites, fastidieuses, médico-légales. Je suis persuadé que je préférerais m'arracher les yeux au visage plutôt que de lire une preuve de progrès / préservation pour le CLR.

Habituellement, si vous arrivez à la fin d'un manuel pl correct (par exemple, Types et langages de programmation de Pierce), vous commencerez à voir une modélisation formelle des fonctionnalités du langage impératif. Cela peut être intéressant pour vous.

Blucz
la source
11

An Axiomatic Basis for Computer Programming par CAR HOARE

Dans cet article, nous essayons d'explorer les fondements logiques de la programmation informatique en utilisant des techniques qui ont d'abord été appliquées à l'étude de la géométrie et qui ont ensuite été étendues à d'autres branches des mathématiques. Cela implique l’élucidation d’ensembles d’axiomes et de règles d’inférence pouvant être utilisés pour prouver les propriétés des programmes informatiques. Des exemples de tels axiomes et règles sont donnés et une preuve formelle d'un théorème simple est affichée. Enfin, il est avancé que la poursuite de ces sujets peut apporter d’importants avantages, tant théoriques que pratiques.

http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.85.8553&rep=rep1&type=pdf

Vag
la source
8

Je souscris à ce qu'Alexandre a dit, à savoir que la machine de Turing fournissait la base théorique originale de la programmation impérative. Dans la mesure où l'organisation des langages de programmation impératifs reflète l'architecture de la machine, je pense que le travail de John Von Neumann serait également un élément clé de leurs fondements théoriques.

Kurt
la source
7

Existe-t-il une base mathématique équivalente pour la programmation impérative, ou s'agit-il simplement d'une application matérielle pratique en langage machine et du développement ultérieur de FORTRAN?

Si vous voulez dire "base" au sens historique, je pense qu'il n'y a pas de "base mathématique équivalente". Cependant, même si la programmation impérative est née de préoccupations pratiques, il existe plusieurs manières de caractériser de manière exhaustive le sens de la programmation impérative d'une manière que vous pourriez trouver "utile pour la modélisation", telle que la logique de Hoare .

jbapple
la source
vouliez-vous vraiment faire de ce wiki de communauté?
Suresh Venkat
Oui, je voulais faire de ce wiki une communauté.
jbapple
7

les articles qui mentionnent la logique de hoare et la logique de séparation sont les bons sur cette question. La logique Hoare vous permet d’énoncer les propriétés de la configuration de tas entière d’un programme, et la logique de séparation est le relatif le plus moderne qui vous permet d’utiliser une "conjonction de séparation" qui vous permet d’énoncer en tant que conditions préalables et postérieures à un segment de code les propriétés correspondantes. la partie du segment que le segment de programme manipulera lors de la quantification sur le reste du segment.

La réponse concernant les monades n'est pas strictement exacte, car haskell utilise un monad simplement parce que c'est une abstraction qui permet le codage des contraintes d'ordre et le suivi explicite de la propriété "pourrait utiliser IO".

Il convient de souligner à la fois que la logique de séparation / séparation peut être considérée comme une monade et qu'il existe un certain nombre de projets contemporains tels que le projet ynot de harvard qui explorent ces sujets.

la recherche en logique de séparation est un domaine actif et continu.

Carter Tazio Schonwald
la source
Il me semble une erreur de confondre le fait que Haskell utilise une notion de monades (et une classe de types Monad) avec l’approche plus générale, telle que proposée par exemple par Moggi, qui utilise des monades pour structurer un compte de la sémantique catégorique. L'adoption des monades comme outil de structuration de la programmation ne doit pas nous empêcher de recourir à la sémantique catégorique comme outil de structuration du raisonnement sur la programmation.
sclv
très bonne clarification, bien que je pense que beaucoup de gens ont utilisé des monades à la hache pour explorer la sémantique via les transformateurs de monades. En particulier, les sémantiques différentes pour les opérations qui proviennent de compositions différentes desdits transformateurs (par exemple pour l'état / mutabilité, les continuations, le non déterminisme, etc.)
Carter Tazio Schonwald
5

J'arrive à cette question encore plus tard, mais cela me fascine également.

Pourquoi la théorie de la programmation impérative est considérée comme moins réglée que celle de la programmation fonctionnelle m'évite. Cela a probablement commencé à devenir sérieux avec Scott et de Bakker en 1969 avec leur analyse du sens de la récursion dans un langage simple et impératif [1]. Lorsque le langage impératif gagne des fonctionnalités, l'histoire devient un peu plus compliquée, mais ce n'est que le prix à payer pour être plus proche du métal. Pour citer l’un des efforts les plus complets, en 1980, de Bakker, de Bruin et Zucker ont écrit une monographie sur le sujet [2]. D'autres ont été mentionnés ci-dessus. Bien que ces références soient antérieures à la logique de séparation mais [2], elles abordent néanmoins des tableaux et des procédures mutuellement récursives.

[1]: non publié en 1969 mais paru sous le nom de Jaco W. de Bakker et Dana S. Scott. Une théorie des programmes , pages 1-30. Dans Klop et al. JW de Bakker, 25 ans. CWI, Amsterdam, 1989. Liber Amoricum.

[2]: Jacobus W. de Bakker, Arie de Bruin, Jeffrey Zucker: Théorie mathématique de la correction de programme. Prentice Hall 1980.

Kai
la source
1
Il est clair que la programmation impérative est extrêmement bien comprise. Je pense que ce que les gens veulent dire quand ils disent que c'est moins établi, c'est que, structurellement, la programmation impérative est plus riche que la programmation fonctionnelle pure, et beaucoup moins de structure mathématique a été découverte qui apparaît dans telle ou telle forme de programmation impérative. Par exemple, certains types de programmes impératifs peuvent être raisonnés pour bien utiliser la logique de séparation. Ceci est probablement dû aux formes de partage. Peut-être que ces types de programmes ont une belle caractérisation mathématique abstraite?
Martin Berger
1
Personnellement, je veux dire que la théorie de la modularité dans les langages impératifs est très peu claire. Nous savons ce que la modularité signifie pour les langages fonctionnels: la paramétrie relationnelle. Pour les langages impératifs, il existe de nombreux idiomes masquant des informations qui (a) fonctionnent clairement, mais (b) pour lesquels nous manquons de bonnes techniques de preuve. Il y a des allusions séduisantes à une théorie profonde: par exemple, lorsque je fais des preuves modulaires de programmes séquentiels impératifs, je finis par avoir besoin de techniques de concurrence. De manière informelle, le pseudonyme est comme une concurrence, mais je ne sais pas vraiment comment formaliser cette idée ...
Neel Krishnaswami
@ Kai. Bienvenue sur le fil! Cela fait longtemps que je n’ai pas regardé le travail de Bakker, mais je pense que le problème fondamental est que l’approche n’a pas été étendue. Pour un résumé rapide des progrès accomplis en matière de programmation impérative depuis lors, consultez mon article dans la rubrique "Qu'est-ce qui constitue la sémantique dénotationnelle?" lien de fil .
Uday Reddy
@ NeelKrishnaswami. J'aimerais voir ces preuves. Sont-ils sur votre page Web? L'aliasing s'apparente à la simultanéité en ce sens que les deux impliquent un partage et un entrelacement sophistiqués. En simultanéité, vous éliminez l'entrelacement et présumez le non-déterminisme (ce qui est bien). En aliasing, vous vous forcez à gérer l'entrelacement. La sémantique des jeux est un excellent exemple de cet entrelacement forcé, raison pour laquelle je ne l'aime pas.
Uday Reddy
3

Peu de temps après avoir posé votre question, Mark Bender de l'Université McMaster a publié une thèse: Calcul du devoir: Un langage de raisonnement impératif pur (8 septembre 2010). Cette thèse décrit un langage simple et impératif correspondant au lambda calcul.

Le calcul d'affectation consiste en seulement quatre constructions de base, affectation X:=t, séquence t;u, formation de ¡tprocédure et invocation de procédure !t. Trois interprétations sont données pour AC: une sémantique opérationnelle, une sémantique dénotationnelle et un système de réécriture de termes. Les trois sont montrés équivalents.

La thèse de Mark Bender explore par la suite des variantes étendues à une évaluation paresseuse, à un retour en arrière, à une composition de procédure. Ceci est similaire à l'exploration du lambda calcul en utilisant de petites extensions.

Dans l’ensemble, la thèse apporte une réponse relativement directe à la question du PO.

dmbarbour
la source
lien pdf est cassé
Quinn Wilson