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

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 ?

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.

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.

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).

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.

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.

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.

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

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.

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 .

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.

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.

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.