Discussion :

[HanLee]

Salut,

Vous auriez un site qui décrit la formalisation mathématique des différents paradigmes de programmation ?

Par exemple pour la programmation orientée objet on pourrait dire qu'un objet c'est un n-uplet composé de fonctions et d'éléments primitifs (ex : entiers naturels, flottants...).
Parce que sur google j'trouve que des sites de maths, ou alors alors des sites qui expliquent pas de manière précise la programmation orientée objet.
Par exemple, une procédure, comment ça se formalise ?

Voilà, c'était par curiosité...

[DrTopos]

Vous auriez un site qui décrit la formalisation mathématique des différents paradigmes de programmation ?
...
Parce que sur google j'trouve que des sites de maths,

En sommes, tu veux une formalisation mathématique, mais sans maths. Ca va être difficile.

ou alors alors des sites qui expliquent pas de manière précise la programmation orientée objet.

La programmation orientée objet est un ensemble assez hétérogène de principes. De plus, les objets de la POO ne sont pas des choses abstraites comme les données (objets) mathématiques. Cela rend la formalisation difficile. D'ailleurs, je ne connais pas aujourd'hui de modélisation mathématique satisfaisante des objets. Il existe bien des articles dans les milieux universitaires d'informatique théorique sur ces questions, mais ils ne sont pas très convainquants.

Par exemple, une procédure, comment ça se formalise ?

Je crois qu'il faut faire la différence entre 'fonction' (qui est une notion mathématique) et 'procédure'. Pour ce qui est des fonctions, tu peux voir du coté du lambda-calcul, ou de la théorie des catégories. Pour les procédures, c'est à dire les mécanismes qui réalisent l'exécution des fonctions, je pense que la meilleure approche est celle des machines de Turing et des fonctions récursives. Il y a une abondante littérature sur ce sujet. Par exemple, l'excellent livre de Marvin Minski: Finite and infinite machines.

Il y a de nombreux logiciens à l'INRIA et à Paris 7 (entre autres), dont l'un des objectifs est justement de formaliser les langages de programmation. Bien sûr, tout le monde n'est pas du même avis. Pour ma part, je crois que la théorie des catégories, de par son caractère béhavioriste est la voie la plus naturelle et la plus efficace pour une telle formalisation.

Maintenant, il y a aussi la formalisation de la syntaxe elle-même et des problèmes que pose la réalisation des compilateurs. Je crois que le livre de Aho, Sethi et Ullman: Compilers. Principles, techniques and tools. est une bonne façon d'aborder ces question d'une manière pas trop mathématique.

Bref, c'est un très vaste sujet, et il ne faut surtout pas croire que tout est résolu et qu'il est figé.

[HanLee]

Ah merci d'avoir répondu, ça fait plaisir ! J'pensais que y'avait que moi qui m'y intéressait

Non non, j'veux voir des maths, mais j'veux pas un site de maths si tu vois ce que j'veux dire .
J'voulais dire que je tombais sur des sites qui ne parlait que des maths en général sans aucune référence à de la programmation.

Et c'est plutôt ce dont tu parlais en premier qui m'intéressait (et non pas la formalisation de la syntaxe).
A propos de la programmation orientée objet, je veux bien des liens quand même, si tu as .

Oui oui je connais la différence entre fonction et procédure . Et moi dans ma tête par exemple je pensais qu'une procédure c'était une fonction qui prenait l'état de la machine (au temps t1) et renvoyait un nouvel état (temps t2).
Hum, t'as des liens sinon à part le livre ? (oui je sais... Mais avec les livres de Maths Spé, ça fait déjà un peu cher...)

Bon bah j'vais essayer de chercher plus dans cette direction =)

[DrTopos]

Ah merci d'avoir répondu, ça fait plaisir ! J'pensais que y'avait que moi qui m'y intéressait

Cela fait plus de 20 ans que cette question me taraude jour et nuit...

Il y a sûrement des tas de documents sur le net que tu sauras trouver aussi bien que moi. Si je t'ai conseillé des livres, c'est parce qu'ils constituent mes références perso. J'étais moi-même en Maths Spé en 1969, et à l'époque on n'avait que les livres. Il est vrai qu'ils étaient beaucoup moins chers que maintenant. On pouvait en acheter au moins une vingtaine par an même avec un budget d'étudiant. Ceci-dit, il y a des bibliothèques où ces livres peuvent être empruntés.

Maintenant, il faut aussi voir que des textes qui n'ont l'air d'être que des maths, recèlent parfois des considérations facilement transposables en informatique. Je te signale aussi que les leçons de logiques catégoriques qui se trouvent sur ma page enseignement sont plutôt orientées informatique.

[HanLee]

Ouaip j'ai lu ta page enseignement dans la partie logique catégorique, c'est intéressant .

[Steki-kun]

Pour info, spécifiquement sur la POO, voilà un lien vers le cours que Giuseppe Castagna donne au Master Parisien de Recherche en Informatique :
ftp://ftp.di.ens.fr/pub/users/castag.../dea-spp.ps.gz

Bon c'est pas accessible à n'importe qui, j'espere que tu as le bagage suffisant en lambda calcul, notion de points fixes et de choses comme ça.

Sinon, de manière générale pour de la théorie sur les langages de prog, tu peux consulter les papiers de gens comme Luca Cardelli ou Benjamin Pierce.

[HanLee]

Ah merci c'est gentil

Heu, lambda calcul non, j'me renseignerai, notion de point fixe... Comme en Topologie ? Le x tel que f(x) = x ?

Bah tu sais, l'important c'est que j'ai ce que j'trouve, après j'vais me donner les moyens de comprendre.

[Steki-kun]

oui c'est ça, mais c'est pas des fonctions de R dans R hein :-)
en gros le problème dans la théorie des langages de programmation, c'est qu'estce que ca veut dire que les définitions récursives ?
parce que pour un humain, c'est (assez) intuitif mais pas trop pour une machine ;-)

si tu écris:

f = Expression faisant intervenir f

l'idée c'est d'écrire lexpression en question G(f) où G est une fonction du type de f vers le type de f, et de dire que cette définition veut dire

f = Point fixe de G

Mais ca suppose que G a un (et un seul) point fixe par exemple, donc G ne devrait pas être n'importe quoi :-) En sémantique des langages de prog, ce point fixe va souvent être égal à la limite des G(G( ....(Bottom))) où Bottom c'est une fonction qui fait rien. Bon tout ça c'est très flou hein, mais c'est un vaste (et très intéressant, j'y passe ma vie ) sujet qu'on peut pas trop expliquer en 30 lignes !

Bon courage !