Je pense que je suis assez confus à propos de ce qu'on appelle un calcul et ce qu'on appelle un langage de programmation.
J'ai tendance à penser, et on aurait pu le dire, qu'un calcul est un système formel de raisonnement sur l'équivalence des programmes. Les programmes ont une sémantique opérationnelle spécifiée par une machine, qui devrait (je pense?) Être déterministe. De cette façon, un calcul (correct) pour une langue est une méthode de preuve pour l'équivalence de programme.
Cela me semble une division raisonnable, mais est-ce le sens communément accepté? Ou peut-être que c'est même faux?
En relation, pourquoi certaines sémantiques opérationnelles sont-elles non déterministes (supposons qu'elles soient confluentes)? Quels sont les avantages à laisser le choix de la stratégie ouvert?
J'apprécierais vraiment des éclaircissements à ce sujet; et des références concrètes encore plus! Merci!
Réponses:
Le sens des mots n'est pas fixe, mais je peux vous donner mon interprétation.
Un calcul est quelque chose avec lequel nous calculons dans le sens de jongler avec des équations (pensez à la manipulation de séries de Taylor ou au calcul d'intégrales en analyse). Un calcul nous dit quelles sont les règles de manipulation, mais pas lesquelles nous devons utiliser dans une situation donnée.
Un langage de programmation est quelque chose qui nous dit comment calculer. Il nous indique précisément comment utiliser les règles. Nous laissons généralement l'ordinateur utiliser les règles, car c'est beaucoup plus rapide. Les règles peuvent être non déterministes et il peut y avoir de très bonnes raisons pour qu'elles ne soient pas déterministes. Il peut être dans la nature du calcul qu'il soit non déterministe (pensez aux processus de communication simultanés), ou la fixation d'une stratégie particulière peut être préjudiciable aux techniques de mise en œuvre et à l'optimisation.
Par exemple, le -calculus est une théorie équationnelle . Il y a des expressions et des équations qui nous disent quand les expressions sont égales. Les équations ne pas nous dire comment les appliquer, bien que les gens ont généralement des programmes cachés et ils présentent les équations de sorte que plus tard ils peuvent tirer des stratégies d'évaluation utiles de leur part . Mais dans son essence, λ -calculus est un tas d'équations. Ce n'est pas un langage de programmation.λ λ
En revanche, Standard ML est un langage de programmation. Elle est donnée en termes de sémantique opérationnelle, c'est-à-dire de règles de calcul. Il y a des notions dérivées d'égalité (équivalence contextuelle, équivalence observationnelle, etc.) que nous pouvons ajouter par dessus pour la considérer comme une sorte de calcul.
Bien sûr, il existe souvent des connexions utiles entre un calcul et sa manifestation en tant que langage de programmation. La normalisation conflictuelle n'est qu'un moyen de passer du calcul au langage de programmation (bien que malheureusement certaines personnes en aient fait une sorte de religion). L'interaction entre les calculs et les langages de programmation est importante: les langages de programmation peuvent effectivement être utilisés, mais les calculs expliquent en quoi consistent les programmes.
Juste pour ennuyer les gens, permettez-moi également de dire que prétendre qu'il n'y a pas de différence entre un calcul et sa manifestation opérationnelle conduit parfois à des visions biaisées de la programmation et des mini-religions au sein de la communauté de la programmation. Vous pouvez essayer de deviner quelle langue j'ai en tête. (C'est une langue très cool!)
la source
Le but des calculs n'est pas seulement d'étudier les équivalences de programmes, c'est d'étudier des programmes. Un exemple de calcul sophistiqué est celui où la stratégie (appel par valeur ou appel par nom) est déterminée localement. Il pourrait être implémenté un jour dans un langage de programmation mais il est d'abord étudié comme un calcul. Vous utilisez également des calculs pour étudier des systèmes de types (certains calculs tels que celui de la théorie des types de Martin-Löf calculant également des types).
Je crois que la principale différence est que les calculs sont censés être (relativement) faciles à étudier formellement tandis que les langages de programmation sont censés être (relativement) faciles à utiliser. Cela entraîne les différences suivantes:
Les calculs ont tendance à être minimalistes tandis que les PL ont tendance à avoir une redondance (pour une boucle lorsque vous avez déjà une boucle while, un commutateur lorsque vous en avez déjà un si, ...) pour faciliter l'expression de ce que vous voulez.
Les calculs ont une sémantique entièrement spécifiée, tandis qu'une sémantique PLs est souvent décrite par un interprète / compilateur par défaut.
Certaines sémantiques opérationnelles sont non déterministes car elles permettent:
Notez que l'appel par valeur n'est pas déterministe: vous pouvez choisir d'évaluer la fonction ou l'argument en premier.
la source
«Langage de programmation» et «calcul» sont des termes polysémiques, c'est-à-dire qu'ils signifient des choses différentes selon le contexte.
Dans certains contextes, les langages de programmation et les calculs ont convergé pour se référer au même concept, celui d'un système de réécriture basé sur un ensemble de règles formelles qui peuvent être appliquées "mécaniquement".
La raison pour laquelle cette convergence est parfois énigmatique pour nous (mais pas pour les développeurs de logiciels ou les mathématiciens) est que notre travail consiste à concevoir des langages de programmation concrets comme s'ils étaient des calculs et à incarner physiquement des calculs dans des langages de programmation concrets.
Pour répondre directement à votre question, la confusion entre calcul et langages de programmation (dans la mesure où elle existe) n'est pas un accident, mais un projet. Notre projet. Il témoigne de notre succès relatif en tant que discipline scientifique.
la source