Les données cycliques je les considère comme l'équivalent (pour les données) de la récursion mutuelle (pour les fonctions). Autant dire que je n'envisage pas d'y renoncer, ou alors il faudrait m'expliquer pourquoi la récursion mutuelle est devenue obsolète.
Ce n'est pas parce que vos utilisateurs actels ne vont pas prostester que "ça ne sert à rien", le langage doit bien entendu élargir sa base d'utilisateurs sans devenir trop permissif. Interdire n'est pas une qualité en soi, il n'y a rien de honteux à remplacer le comptage de références par un mark & sweep.
Ma liste du père noël pour le langage:
- une plus grande facilité pour créer des données cycliques
- une simulation des enregistrements (par les n-uplets) encore plus poussée
- une simulation des exceptions encore plus poussée
- le filtrage exhaustif
Et pourquoi pas des facilités de preuves (notamment pour les invariants structurels) avec égalités et inégalités.
Et puis ma liste du père noël pour l'implémentation:
- un ramasse-miettes mark & sweep
- un interpréteur interactif
- un compilateur vers du code natif
Du même auteur: mon projet, le dernier article publié, le blog dvp et le jeu vidéo.
Avant de poser une question je lis les règles du forum.
Je ne suis pas de cet avis, et je m'en expliquerai dans un prochain post consacré aux données cycliques.
En Anubis 2 il n'y aura pas de données cycliques, car cela mettrait à mal la logique. J'expliquerai tout cela comme je l'ai promis, et aussi pourquoi, quand on veut faire un graphe (comportant éventellement des cycles bien sûr), il vaut mieux le faire sans données cycliques.
Je ne vois pas très bien de quoi tu veux parler.
Ici aussi il faudra préciser ta pensée. Tu sais qu'en Anubis il n'y a pas d'exception et que c'est la façon de typer qui en tient lieu. En Anubis 2 ce sera encore différent à cause de la présence de nouveaux types qui permettent d'introduire la logique mathématique. Dans la proposition que j'ai envoyée au comité 'défis fonctionnels', je propose un jeu logique et fonctionnel qui décrit ces types.
Pas de problème. Il y aura possibilité de condenser les imbrications de conditionnelles (qui sont déjà exhaustives) sous forme de filtrage.
Il y aura mieux que cela, puisqu'il y aura toute la logique mathématique aussi bien constructive que classique.
J'ai prévu qu'on puisse choisir son type de GC à la compilation (sous forme d'option). Il y en aura plusieurs sortes. Peut-être qu'une au début, mais les collaborations seront bienvenues. Ceci-dit, le GC générationnel est le successeur logique du mark & sweep, qui présente aujourd'hui peu d'intérêt.
Tu le feras toi-même. Quand il y aura le système de macros (inspiré de Lisp) ça sera facile. Ce que je trouve plus intéressant (j'y travaille aussi) est un éditeur graphique sous lequel le compilateur travaille en continu, pour vérifier la syntaxe et la sémantique en temps réel.
Tu penses bien que je ne penses qu'à ça. C'est au centre de mon travail actuel.
Je n'insisterai pas davantage sur les données cycliques, je préfère vous laisser l'initiative de l'innovation et/ou de l'explication.
Voici les précisions demandées, l'une porte sur les agglomérations l'autre sur les alternatives:
- Il nous a été dit qu'il est prévu pour la version 1.8 de pouvoir accéder aux composantes d'une agglomération par la notation pointée, cette idée a été favorablement accueillie. Il serait élégant que la construction d'une agglomération soit également possible en associant une valeur à chacune des composantes, de sorte que l'ordre des composantes n'intervienne plus du tout dans la construction (cette idée a été proposée par alex_pi). De manière cohérente la même facilité serait offerte dans les motifs (d'un filtrage) de sorte que l'ordre des composantes n'intervienne plus du tout dans la déconstruction.
De cette façon on pourrait librement choisir entre la contrainte de respecter l'ordre de toutes les composantes ou la contrainte de nommer toutes les composantes.
L'ambition est de rendre, autant que possible, obsolète et redondant le type enregistrement tel qu'il existe en Caml.- Plusieurs intervenants ont fait la remarque selon laquelle il faut 'capturer' une sorte d'exception my_error("mon message d'erreur") dans toutes les fonctions (à cause du filtrage exhaustif), or la plupart du temps cette capture prends la forme suivante:
L'idée serait d'automatiser ce code en déclarant un filtrage par défaut pour certaines alternatives, lorsqu'il est compatible avec le type de la conditionnelle, exemple ici avec le type Expr:
Code : Sélectionner tout - Visualiser dans une fenêtre à part
1
2
3
4
5
6
7 if expr is { ... my_error1(msg) then my_error1(msg), my_error2(msg) then my_error2(msg) }
Le filtrage reste totalement exhaustif.
Code : Sélectionner tout - Visualiser dans une fenêtre à part
1
2
3
4
5 type Expr: ..., my_error1(String msg) then my_error1(msg), my_error2(String msg) then my_error2(msg).
L'ambition est de rendre, autant que possible, obsolète et redondant le type exception tel qu'il existe en Caml.
Bien entendu aucune de ces deux propositions n'a d'intérêt théorique, il ne s'agit que d'extensions de confort destinées à mieux recouvrir des facilités qui ont fait leurs preuves, sans recourir à l'ajout de nouvelles constructions.
Du même auteur: mon projet, le dernier article publié, le blog dvp et le jeu vidéo.
Avant de poser une question je lis les règles du forum.
Il est possible en effet que la définition que j'ai donnée de la notation pointée ne compile pas en version 1.7 (où le point ne doit pas être reconnu comme opérateur binaire).
Pour ce qui est des problèmes de lourdeur du genre:
ou
Code : Sélectionner tout - Visualiser dans une fenêtre à part
1
2 failure then failure,
on peut les résoudre en définissant un produit de Kleisli (un pour Maybe et un pour Result), de la façon suivante:
Code : Sélectionner tout - Visualiser dans une fenêtre à part
1
2 error(msg) then error(msg),
Pour Result, cela donne:
Code : Sélectionner tout - Visualiser dans une fenêtre à part
1
2
3
4
5
6
7
8
9 define $T -> Maybe($V) $T -> Maybe($U) f * $U -> Maybe($V) g = ($T x) |-> if f(x) is { failure then failure, success(y) then g(y) }.
Dès lors, on peut composer des fonctions produisant des exceptions en écrivant f * g sans se preoccuper de transmettre l'exception à chaque fonction. On remarquera que les monades d'Haskell ne sont pas loin. En fait (f * g)(x) correspond à quelquechose comme (f x) >>= g en Haskell, où >>= est le 'bind' de la monade de Maybe.
Code : Sélectionner tout - Visualiser dans une fenêtre à part
1
2
3
4
5
6
7
8
9 define $T -> Result($E,$V) $T -> Result($E,$U) f * $U -> Result($E,$V) g = ($T x) |-> if f(x) is { error(msg) then error(msg), ok(y) then g(y) }.
Mais là encore, je ne sais pas si la syntaxe de la version 1.7 le supporte.
Il est largement temps que la 1.8 sorte. Si elle ne sort pas, c'est qu'on a encore du travail dessus, et que par ailleurs on est débordé par toutes sortes d'autres activités. Je ne peux rien promettre, mais on fait le maximum.
J'en viens donc aux données cycliques.
Certains d'entre vous ont l'impression que c'est seulement le fait que j'ai choisi un
GC par incrément-décrément qui me fait avoir cette position anti-données cycliques, et
que cela serait donc une mauvaise raison. Ce n'est pas du tout cela. Je réalise des
interpréteurs et compilateurs depuis plus de 20 ans maintenant, et je sais que le GC
par incrément-décrément ne gère pas les cycles depuis que j'ai réfléchi à cette
question pour la première fois, c'est à dire vers 1985. A cette époque j'ai réalisé un
interpéteur Lisp avec un GC mark & sweep. En 1988, je l'ai bootstrapé en réécrivant le
compilateur en Lisp et je l'ai muni d'une machine virtuelle (écrite en assembleur 16
bits !) avec un GC par incrément-décrément. J'ai réalisé par ailleurs un compilateur
Prolog vers 1995, qui produisait du code pour une variante de la WAM (Warren's Abstract
Machine) et j'ai fait Anubis en 2000. Tout cela pour dire que j'ai eu de nombreuses
occasions d'être confronté au choix d'un GC, que je suis au courant de ce qui se fait
pour avoir lu de nombreux documents sur le sujet, et que si j'ai choisi
l'incrément-décrément pour Anubis, ce n'est pas au hazard.
En fait, mes motivations anti-données cycliques sont surtout de nature théorique (même
si je vais donner aussi plus loin quelques arguments de nature pratique). Mes
motivations pro-GC par incrément-décrément sont aussi essentiellement de nature
théorique. Mes arguments ne font que refléter ma formation de matheux (et de logicien)
alors que la position des pro-données cycliques est très clairement une conséquence de
leur culture essentiellement fondée sur la programmation (et sans doute aussi sur le
choix de certains langages de programmation).
Je comprends qu'on puisse penser ``pourquoi s'en priver puisqu'on l'a et que ça
marche''. Je pense que ceux qui commencent à me connaître auront compris que je ne
raisonne pas de cette façon, et que les maths et la logique mathématique (et en
particulier la logique constructive) jouent un rôle de premier plan dans ma façon de
voir les choses.
Je vais commencer par les arguments de nature pratique, parce que ce sont peut-être
ceux qui seront les plus convainquants pour des développeurs.
Alex_pi a parlé d'arbre et de pointeur pour remonter au père. J'ai très souvent
programmé avec des arbres et autres structures récursives similaires, et je n'ai jamais
eu besoin d'une telle chose. La programmation avec les données des types récursifs se
fait par des fonctions définies récursivement. C'est normal. D'ailleurs, en Théorie des
Catégories, on définit les types récursifs par un problème universel (un type récursif
est un objet initial dans une catégorie de diagrammes appropriée), et cette définition
définie en même temps un schéma de récursion (duquel on peut d'ailleurs déduire le
schéma de récursion primitive asssocié au type), qui nous dit comment programmer avec
les données de ce type. Comme les problèmes universels caractérisent les objets qu'ils
définissent, il est clair qu'on n'a besoin de rien d'autre pour programmer. La remontée
au père dans un arbre se fait au moment du retour de l'appel récursif (quand il est non
terminal). En fait, on sait comment revenir au père tout simplement parce qu'on a
empilé une addresse de retour dans la pile avant de quitter ce père. Remonter au père
par des pointeurs reviendrait à ignorer les principes mêmes de la programmation
récursive (c'est à dire essentiellement à faire des récursions sauvages ne satisfaisant
pas le schéma de récursion) et à les remplacer par des promenades dans un arbre devenu
un graphe, avec tous les alea que cela comporte. Dans ces conditions inutile de
continuer à utiliser un langage fonctionnel, on peut tout aussi bien le faire avec un
impératif de base. Cela ne sera pas plus dangereux.
Par ailleurs, si on implémente un graphe avec des cycles de références (i.e. de
pointeurs), on rencontre au moins deux problèmes (indépendamment du GC): (1) On doit
avoir au moins une référence sur un sommet de ce graphe, sinon on ne peut rien faire de
son graphe. On privilégie donc un sommet pour des raisons d'implémentation, alors que
le problème qu'on a à traiter ne l'impose sans doute pas. (2) C'est même pire que cela,
car si par exemple le graphe a trois sommets A, B et C et deux arêtes, une de A vers B
et une de C vers B:
Il n'existe aucun sommet du graphe qui permette d'atteindre tous les autres.
Code : Sélectionner tout - Visualiser dans une fenêtre à part
1
2 A -----> B <----- C
Evidemment, le problème se complique encore quand le graphe n'est pas connexe. En
définitive, on va être obligé de mettre tous les sommets du graphe dans une liste (non
cyclique) ou un tableau, et là on va s'apercevoir qu'en définitive les cycles de
pointeurs ne servent à rien.
La bonne façon de représenter des graphes est celle que j'ai toujours vue appliquer
partout, à savoir qu'on réserve un tableau (ou une liste ou un B-tree) pour y mettre
pour chaque sommet du graphe les informations liées à ce sommet, y compris la liste des
arêtes qui partent de ce sommet. La cible d'une de ces arêtes est tout simplement
l'indice du sommet cible dans le tableau (ou une clef dans le cas des listes ou des
B-tree). Autrement-dit, bien que le graphe soit tout à fait général et puisse contenir
des cycles d'arêtes, l'implémentation ne demande aucune donnée cyclique.
Si on regarde par exemple l'automate (qui est un graphe avec des cycles) fabriqué par
YACC/BISON, on constate qu'il sagit d'un ensemble de tableaux ne contenant que des
nombres. De même, bien sûr pour l'automate fabriqué par LEX/FLEX. J'ai réalisé en
Anubis un programme analogue à BISON (qui fabrique d'ailleurs exactement le même
automate que BISON pour la même grammaire) et bien entendu je suis obligé de gérer un
graphe qui contient des cycles. Le graphe n'est rien d'autre qu'une liste de ses
sommets, avec dans chaque élément de la liste les données pertinentes, y compris la
liste des transitions vers les autres états de l'automate. L'automate est plein de
cycles, mais il n'y a aucune donnée cyclique fabriquée en mémoire.
Je pourrais donner d'autres exemples, mais je crois que ceux-ci devraient suffire à
convaincre que même si on souhaite avoir des données cycliques, on peut s'en
passer. D'ailleurs, en ce qui concerne les graphes, je crois qu'on doit s'en passer, vu
les problèmes que j'ai évoqués plus haut.
Les données cycliques sont par ailleurs en lien avec la notion de programmation
déterministe. C'est une chose qui est bien connue depuis les débuts de Lisp. Si on fait
une paire en Lisp, disons (a . b) on calcule a, puis on calcule b, puis le système
alloue un petit segment de mémoire pour y mettre a et b cote à cote. Par la suite, les
deux emplacements contenant a et b ne changent jamais de valeur tant qu'on n'utilise
pas les fonction rplaca et rplacd (appellées ``chirurgicales'') qui opèrent un
remplacement destructif de la tête ou de la queue de la paire, et qui sont donc par
essence non déterministes. Autrement-dit, sans chirurgie (et sans effet de bord) la
programmation Lisp est complètement déterministe. C'est ce qu'on appelle du
``fonctionnel pur''. Il est facile de prouver que dans ces conditions, aucune donnée
cyclique ne peut être crée. En effet, ceci résulte du fait que le segment alloué pour
la paire (a . b) est ``plus jeune'' que les segments qui ont alloués pour construire a
et b. Les références vont donc toujours des plus jeunes vers les plus vieux, ce qui
interdit les cycles. Sauf bien sûr, si on fait de la chirurgie, car alors on peut
placer dans un segment un pointeur sur un segment plus jeune que lui.
D'ailleurs, à ce sujet, je ferai une remarque sur Haskell, qui se dit ``langage
fonctionnel pur'' tant qu'on n'utilise pas de monade (puisqu'il enferme les effets de
bord dans les monades). En Haskell, on peut écrire:
ce qui fabrique une liste ``infinie'' de 1. En fait, bien sûr c'est une donnée
Code : Sélectionner tout - Visualiser dans une fenêtre à part
1
2 ones = 1 : ones
cyclique. Cette donnée est nécessairement fabriquée par chirurgie, puisque ones ne peut
pas être contruit complètement au moment où on alloue le segment pour ones. Le fait de
mettre dans la queue de cette liste cette liste elle-même est une chirurgie. Par
conséquent, c'est non déterministe puisque c'est une affectation et par conséquent
Haskell n'est pas un langage fonctionnel pur, même sans utilisation des monades. C'est
un effet pervers des données cycliques.
J'en viens maintenant à des arguments en lien avec la volonté de concevoir un langage
incluant des mécanismes de preuve. Ce n'est pas le cas d'Haskell ni de Caml, ni
d'Anubis 1. Mais c'est le cas d'Anubis 2. Il existe, parait-il, 17 systèmes de
formalisation de preuves, dont COQ, Nuplr, HOL, Isabelle, PVS, etc... Ces systèmes sont
soumis à des contraintes bien plus sévères que les langages fonctionnels. En effet, si
on inclus des mécanismes de preuve, c'est pour prouver quelque chose à propos des
données qu'on manipule dans le langage, sinon ça ne sert à rien. On utilise donc ces
données dans les preuves. Si ces données créent des incohérences logiques, on rend
l'énoncé ``faux'' démontrable dans le système, donc tout énoncé devient démontrable, et
le système de preuve n'a plus aucun intérêt.
Parmi les mécanismes qui créent de telles incohérences et sont donc incompatibles avec
la présence d'un système de preuves, il y a les exceptions (non capturées) et les
données cycliques. En voici la preuve pour les données cycliques. Je reviens à mon
exemple en Haskell d'une liste infinie de 1. En Haskell, on a une fonction 'length' qui
calcule la longeur d'une liste. Cette fonction est hyper classique et elle est définie
exactement de la même façon en Haskell, en Caml et en Anubis. Je l'écris en Haskell
pour pouvoir m'en servir:
Dans un système avec des preuves, on doit avoir des axiomes exprimant les propriétés
Code : Sélectionner tout - Visualiser dans une fenêtre à part
1
2
3
4 length :: [a] -> Int length [] = 0 length x : y = 1 + length y
standard des données du système. Une fonction comme celle définie ci-dessus (par une
conditionnelle, car il y a deux cas) jouit d'un certain nombre de propriétés. Parmi
elles, on a sûrement celle qui est exprimée par l'égalité (où x et y sont
universellement quantifiés):
Maintenant, ma liste infinie ones a elle aussi une propriété:
Code : Sélectionner tout - Visualiser dans une fenêtre à part
1
2 length x : y = 1 + length y
A l'aide des deux équations ci-dessus, je peux faire le calcul suivant:
Code : Sélectionner tout - Visualiser dans une fenêtre à part
1
2 ones = 1 : ones
d'où je déduis: 0 = 1, c'est à dire ``faux'', et j'ai fait effondrer mon système
Code : Sélectionner tout - Visualiser dans une fenêtre à part
1
2 length ones = length (1 : ones) = 1 + length ones
logique.
Dès lors, il est facile de comprendre pourquoi on ne peut pas admettre les données
cycliques dans un système qui prétend maintenir sa cohérence logique. En fait, ces
données sont tout simplement des paradoxes, puisqu'elles permettent de démontrer
``faux''. Bien entendu, rien de tout cela n'arrive si on n'a pas de données cycliques.
On peut voir l'argumentation ci-dessus d'une autre façon. La fonction length est de
type [a] -> Int. Autrement-dit, elle associe un entier à chaque liste. Par ailleurs,
c'est une fonction sensée être totale (partout définie). Ce qui arrive, comme on le
voit est qu'elle n'est pas définie pour la liste ones, car l'infini n'est pas un
élément de Int. En fait, ma conclusion est que ones n'est tout simplement pas une
liste, car toute liste est finie par définition du type des listes (cela peut se
démontrer par induction). En fait, la construction de données cycliques détruit la
sémantique des types récursifs, et ce faisant, fait effondrer toute la logique du
système.
Je reviendrai sans doute sur les garbage collectors dans un prochain post.
Message très intéressant.
Mais qu'en est-il des fonctions récursives ? Rien n'empêche une fonction récursive de faire une récursion infinie (et ça me semble difficile de détecter ce cas, en général). Que penser alors du code (non testé) suivant ?
C'est la même chose que le précédent, sauf que la récursion passe par un appel de fonction. Le résultat me semble être le même, puisque Haskell est paresseux. Et pourtant, cela se fait sans effet de bord (sans chirurgie).
Code : Sélectionner tout - Visualiser dans une fenêtre à part ones x = 1 : ones x
Une fonction définie récursivement peut en effet tomber dans une boucle infinie, si la récursion est ``mauvaise''. Contôler ce phénomène n'est pas facile (ni Haskell, ni Caml ni Anubis 1 ne le font). Toutefois, les systèmes à preuves sont obligés de la faire. Je peux te fabriquer un paradoxe avec une fonction récursive ayant une mauvaise définition aussi facilement qu'avec une donnée cyclique.
J'en profite pour répondre à l'une des questions de SpiceGuid: l'analogie correcte n'est pas entre les données cycliques et les fonctions récursives (fusses-t-elles mutuelles, ce qui ne change rien), mais entre les données cycliques et les mauvaises récursions seulement.
En Théorie des fonctions récursives, on démontre que l'ensemble des fonctions récursives totales de N vers N n'est lui-même pas récursif. Ce que signifie ce théorème est qu'il n'existe pas d'algorithme capable de déterminer si une fonction définie récursivement est bonne (le calcul s'arrête pour toute valeur de l'argument) ou mauvaise. Si on veut contrôler la récursion, on est donc contraint de trouver un moyen de délimiter algorithmiquement un sous-ensemble de l'ensemble des fonctions de N vers N contenu dans (mais nécessairement non égal à) l'ensemble des fonctions récursives totales.
L'ensemble qu'on choisit logiquement est le plus petit qui contienne les fonctions ``primitivement récursives'' et qui soit stable par les opérations standard sur les fonctions. Pour être sûr que les fonctions définies par l'utilisateur restent dans ce sous-ensemble, il suffit de lui imposer (à l'utilisateur) de respecter le schéma de récursion primitive.
Cela peut se faire de plusieurs façons. La façon la plus facile pour l'implémenteur est d'interdire tout appel récursif, et de produire automatiquement pour chaque définition de type récursif le schéma de récursion primitive correspondant. Dès lors, si l'utilisateur veut définir une fonction récursive, il ne peut le faire que via ce schéma. La fonction length telle quelle est définie en Haskell satisfait le schéma, alors que
ne le satisfait pas. Par ailleurs, effectivement, cet exemple ne comporte pas de chirurgie, seulement une mauvaise récursion.
Comme je souhaite bien entendu faciliter le travail de l'utilisateur, j'ai étudié un moyen de faire détecter par le compilateur une large classe de fonctions satisfaisant les chémas de récursion, plutôt que de l'obliger à utiliser les schémas de récursion primitive à la main. Ce n'est pas facile, et je n'ai pas encore pris de décision définitive sur cette question.
Note: Pour ce qui est du 'if' avec un seul cas, on peut écrire 'since' à la place de 'if' en Anubis.
C'est à dire qu'en supposant que mon type soit défini par:Envoyé par SpiceGuid
on pourait écrire par exemple t((a: "toto", c:"baba", b:"zonzon") au lieu de t("toto","zonzon","baba"). Il me semble qu'il y a un langage de la fin des années 50 (ALGOL ?) qui le permet. Cela se rapprocherait assez de la langue naturelle. par exemple, on peut dire:
Code : Sélectionner tout - Visualiser dans une fenêtre à part
1
2 type T: t(String a, String b, String c).
Je vais à Lyon en train
ou
Je vais en train à Lyon
Ici c'est le groupe sujet-verbe Je vais qui joue le rôle de t, les deux arguments étant 'train' et 'Lyon'. Les mots 'à' et 'en' jouent le rôle des noms des composants.
Je ne suis pas opposé à cette facilité. D'ailleurs, ce n'est pas tellement le fait qu'on puisse changer l'ordre qui est intéressant, mais plutôt le fait qu'on peut rendre le texte plus lisible par l'indication du nom des composants.
Par contre pour ce qui est de permettre de mettre les cas des conditionnelles dans un ordre quelconque, je crois que c'est une mauvaise idée. Cela n'apporte pas plus de précision, et ne reduit pas la taille du texte. Je ne pense pas qu'il y ait un bénéfice à en tirer. Je pense même, que quand on définit un type somme, on choisit en général soigneusement l'ordre des alternatives. Le fait d'imposer le même dans les conditionnelles me semble être au contraire la garantie d'une meilleure clarté du texte.
Ah oui... et pourquoi ? Donc, d'après toi, le GC de OCaml est à foutre en partie à la poubelle ?Envoyé par DrTopos
Le faire sous forme de front-end pour GCC est peut-être une idée intéressante : ça évite d'avoir à coder tout plein de choses difficiles.Envoyé par DrTopos
When Colt produced the first practical repeating handgun, it gave rise to the saying God created men, but Colt made them equal.
Ma phrase était mal tournée. J'ai voulu dire qu'à cause des perfectionnement apportés par le générationnel, le mark & sweep a peu d'intérêt.
[EDIT]
En y regardant de plus près, je constate que ma phrase n'était pas du tout mal tournée. Elle l'aurait été si j'avais mis 'et' à la place de 'qui'. Il faudrait apprendre à lire le Français, jeune homme.
[/EDIT]
Il peut arriver que les structures que l'on manipule soient trop grosses pour la pile système, et que l'on veuille donc faire une récursion plus "manuelle". Ceci ne signifie pas que l'on a besoin de le faire à chaque fois, et surtout, ceci ne signifie en rien que l'on abandonne la programmation récursive. Simplement, on rend la récursion terminale en ne dupliquant pas la structure (garder le chemin d'appel dans la pile revient à dupliquer la partie de l'arbre entre la racine et l'endroit où l'on se trouve).
Il faut quand même parfois comprendre que l'informatique n'est pas *exactement* les mathématique, qu'on est parfois confronté, qu'on le veuille ou non, à certaines réalités et contraintes liées entre autre à l'implémentation ! Par exemple, une pile système de taille finie (plus limitée que la taille du tas typiquement)
Il s'avère aussi que l'on peut se limiter aux huit instructions de BrainFuck pour programmer, ceci ne signifie pas pour autant que l'on vise ce minimalisme...
Dans le cas classique de l'automate, on a quand même d'assez bonne raison de privilégier les états d'entrés...
C'est quoi le lien logique entre "il faut pouvoir acceder à tous les sommets" et "les cycles de pointeurs ne servent à rien". Pour moi, un des principes de base de la programmation (sauf quand je veux à tout prix aller chercher l'optimisation) est de faire une implémentation naturelle. Quand je pense "graphe", je pense petits ronds avec des fleches qui en sortent, donc je programme petit rond avec des fleches qui en sortent plutôt que matrice de transition...
Je trouve ça quand même ammusant pour quelqu'un qui clame faire un langage "à la pointe de la recherche", qui prétend continuellement qu'il permet de débuger 40 fois plus vite qu'en C, etc etc. de prendre comme exemple pour justifier "c'est évidement comme ça qu'il faut faire" un programme qui a été programmé il y a 20 ans, en C justement.
Bien sûr que l'on peut s'en passer, puisqu'encore une fois, on peut réduire un langage de programmation à 8 instructions... Et pourquoi n'avez vous pas répondu sur le coup de la liste doublement chaînée. Vous aurez peut être un peu plus de mal à justifier que ce n'est pas une structure de donnée *ultra-classique*
Là encore, je ne suis toujours pas convaincu par vos définitions... Le code
Est *parfaitement* déterministe. Vous pouvez danser la lambada devant votre PC, lancer firefox ou vous faire du café avec Anubis2, à la fin, j vaudra 42 et i vaudra 10.
Code : Sélectionner tout - Visualiser dans une fenêtre à part
1
2
3
4
5
6 int i = 0; int j = 0; for(i = 0; i <10; i++){ j = 42; }
Alors là, on atteind des sommets de n'importe quoi quand même
Une liste, en mémoire, c'est deux mots mémoire cote à cote, le premier contient la valeur, le second un pointeur vers la suite. Si vous avez une liste et que vous voulez rajouter "1" en tête, vous alouez deux mots mémoires, et vous mettez la valeur "1" dans le premier, et l'adresse de votre liste dans le second, puis vous retourner le pointeur qui vous a été donné lors de l'affectation. Quand vous voulez faire la liste one = 1 :: one, vous alouez deux mots mémoire, vous mettez "1" dans le premier, puis vous mettez la valeur retournée par l'allocation dans le second, et enfin vous retournez cette même valeur. J'avoue ne pas bien voir la différence profonde.
Il est évident qu'aucun langage n'a une implémentation fonctionelle, puisqu'au final, c'est de l'assembleur (enfin même du langage machine), et que c'est tout sauf fonctionnel. Donc dire qu'un langage n'est pas fonctionnel parce que son implémentation ne l'est pas est un non sens.
Ouille.... Les maths, c'est joli, mais encore faut-il savoir les adapter... Une fonction informatique de type "'a list -> int" est une fonction mathématique allant vers l'ensemble des entiers *PLUS* un élément particulier, botom, qui signifie "la fonction ne termine pas". En conséquence, la "fonction mathématique" length appelé sur une liste cyclique infinie a la "valeur" botom. Ensuite, botom + 1 vaut bel et bien botom. La logique est conservé, les maths ne s'effondrent pas, la physique tiens le coup, et on survit. Ouf...
Un second post arrive sur d'autres problèmes.
When Colt produced the first practical repeating handgun, it gave rise to the saying God created men, but Colt made them equal.
Tiens, je ne savais pas que finalement Anubis2 ne serait pas Turing-complet. Je croyais qu'il serait comme Anubis1 mais en encore mieux, et qu'il écraserait C et C++ au niveau temps d'exécution.
Et là, on se retrouve avec un langage où toutes les fonctions se terminent, et qui n'est donc notoirement pas Turing-complet, ou alors dont on ne peut pas écrire de compilo.... Dommage non ?
J'ai simplement fait remarquer à SpiceGuid, qu'un mark & sweep simple comme on en faisait dans le temps ne se fait plus, puisqu'il a été perfectionné par le concept générationnel. Cela n'empêche pas le GC d'être sur une base de mark & sweep, mais sur une base seulement.
Je ne sais pas si c'est clair. Je vais essayer autre chose. Il a proposé un mark & sweep. Je lui ai répondu qu'il vaudrait mieux faire un générationnel.
Je ne suis pas contre un mark & sweep générationnel pour Anubis 2, puisque j'ai prévu qu'on puisse choisir son GC. Par contre, je ne sais pas si j'aurai le temps et le courage de le faire moi-même. Si ce genre de projet t'intéresse, tu peux prendre contact avec moi par mp.
Je crois que jusqu'ici je n'avais pas vraiment réalisé à quel point pour entrer dans le monde des preuves il faut d'abord sortir du monde de la programmation.
Qui dit preuves dit type inductifs et qui dit types inductifs dit pas de données cycliques.
Ou qui dit preuve dit terminaison de preuve donc preuve de terminaison donc pas de données cycliques.
Je vois bien pourquoi si on commence par preuve de données on retombe forcément sur pas de données cycliques.
Et comme on autorise toujours les fonctions cycliques, on établit une nette distinction entre fonctions et données, on sort du cadre du lambda-calcul. Ou alors on est pas Turing-complet, ce qui semble être le choix des systèmes de preuve.
Après c'est certain les cycles que les types inductifs n'ont pas pu construire on n'aura pas besoin d'un mark & sweep pour les détruire.
Pas de cycle c'est très limitant pour l'impératif, ce qu'il faut voir c'est à quel point c'est limitant pour le fonctionnel et pour le multi-paradigme. Certaines expressions du lambda-calcul deviennent irréalisables, c'est tout un pan de l'expérience qui s'évanouit, on ne peut pas le prendre à la légère.
En tout cas c'est à l'heure actuelle, parmi les systèmes du genre, celui qui s'est fixé l'objectif le plus ambitieux en matière d'accessibilité.
Du même auteur: mon projet, le dernier article publié, le blog dvp et le jeu vidéo.
Avant de poser une question je lis les règles du forum.
Je crois plutôt que si on veut prouver quoi que ce soit à propos de programmes, il faut d'abord éliminer tout ce qui rendrait toute preuve vaine. Il ne faut donc pas sortir du monde de la programmation, il faut seulement avoir une discipline (beaucoup) plus stricte.
Cela dépend de quel lambda-calcul on parle. S'il s'agit de celui de Church, oui. Mais le lambda-calcul c'est aussi le lambda calcul avec couples (comme celui qu'utilise Girard dans le système F). Ceci signifie qu'on a un calcul qui ne se limite pas aux fonctions. On peut aller plus loin et introduire des constructions additives. Dans ce cas, on obtient un lambda-calcul qui traite les fonctions les couples et les données des types sommes. Evidemment avec un tel système on a trois règles de beta-réduction et trois règles de eta-réduction.
Pour un système de preuves, je ne crois pas que Turing-complet ait beaucoup de sens. Mais de toute façon, être Turing-complet n'est pas très important. Dans la programmation usuelle, on n'en a pas besoin.
Oui, mais il y a d'autres critères qui peuvent entrer en ligne de compte, par exemple de performances.
Aucune expression du lambda-calcul ne risque de devenir irréalisable, puisqu'une espression de n'importe quel langage est de toute façon un arbre donc sans cycle. Je parle de l'expression elle-même, pas de ce qu'elle construit ou représente.
Il faut aussi faire la distinction entre le lambda-calcul non typé et le lambda-calcul typé. La différence est très importante. En lambda-calcul non typé on peut écrire:
qui est un terme dont la beta-réduction ne s'arrête pas. C'est impossible en lambda-calcul typé où tous les calculs se terminent (théorème de W.W.Tait). Le lambda-calcul typé qui est sous une forme ou sous une autre (par exemple, sous la forme de la théorie de Martin-Löf pour COQ) à la base de tous les systèmes de preuves n'est donc pas Turing-complet.
Code : Sélectionner tout - Visualiser dans une fenêtre à part
1
2 (\x xx)(\x xx)
Je programme le plus souvent en Java, et voilà qu'un nouveau langage vient et que son créateur fort d'une nouvelle théorie "mathématique" nous dis que tout les langages à part le sien sont médiocres ou ne lui arrivent même pas à la cheville.
Ok, mais que nous apporte votre langage par rapport à Java, C++, C# ... ;
la rapidité de développement :ben s'il faut 1 million de lignes de code pour programmer un site Web ,je suis consterné ;
La sécurité :j'ai jamais essayé, donc je me prononcerai pas !
L'évolutivité :Je suis allé sur le site du Langage Anubis, et j'ai lu ceci sur la Programmation Orienté Objet
La POO a été inventée et adoptée par beaucoup de monde parceque elle se rapproche de la pensée humaine et de la vie autour de nous qui est faite d' objets de différentes natures. Je dirais plutôt qu'elle réduit le risque d'erreur parceque grâce à l'encapsulation, les objets ne communiquent entre eux que par le biais de d'interfaces externes.Or en informatique, il n'y a pas que des données concrètes, il n'y a donc pas de raison de tout traiter comme des objets. D'ailleurs, traiter les notion abstraites (de nature mathématique) comme des objets revient à introduire du non déterminisme là où il ne se justifie pas, ce qui non seulement complique inutilement la programmation, mais augmente considérablement le risque d'erreur. Bien sûr, dans le cas de données concrètes, appliquer le principe d'identité est indispensable.
D'un coté y a les mathématiques ou tout est preuve et l'informatique ou l'analyse prime sur tout et est basée sur des choix comme le choix d'un langage de programmation par exemple pour implémenter son système.un terme déterministe est beaucoup plus facile à comprendre qu'un terme non déterministe
C'est drôle, j'ai presque envi de dire que c'est la définition même de l'Objet exprimée d'une autre façon.Un module est destiné à être utilisé par d'autres modules. Il fournit donc aux autres modules ce qu'on peut appeler des outils. Il y a toujours deux points de vue sur un outil donné: le point de vue du constructeur et le point de vue de l'utilisateur. L'utilisateur ne s'intéresse pas à la façon dont l'outil est construit, mais seulement à la façon de s'en servir. C'est pour cette raison que chaque outil a son mode d'emploi.
Vous êtes entrain de critiquer l'Algorithmie sans le savoir, qui est la base de l'informatique.La morale est que la justification du programme récursif est beaucoup plus facile à faire que la justification de la boucle, et donc beaucoup moins sujette à erreurs. D'ailleurs, ce qui rend la boucle plus difficile à justifier est simplement le fait que les boucles (en langage C du moins, et dans les langages similaires) imposent une programmation non déterministe, car une boucle ne renvoit pas de valeur, et est par conséquent obligée de produire des effets pour avoir une utilité
Je suis pas d'accord avec votre pensée comme quoi il faut empêcher le programmeur de faire des erreurs pour développer .Un langage qui "peut" provoquer des erreurs implique selon moi qu'il permet de faire vraiment beaucoup de choses et qu'en acquérant de l'expérience on peut éviter ces mêmes erreurs tout en gardant la puissance du langage .
Conclusion: je ne suis pas du tout convaincu par ce langage, et je trouve que l'absence d'erreurs dans un programme est une utopie !
Where is my mind
Sur certains points.
Il me semble pas avoir lu qu'Anubis avait pour but de remplacer Java ou C#. C'est une philosophie différente.
Je crois que ton point de vue est biaisé, je pense que tu raisonnes en impératif (et Anubis est fonctionnel). J'aime beaucoup l'objet, en particulier quand un langage en profite réellement via un système tout-objet, mais je sais aussi que l'on peut très bien s'en passer. Les arguments qui ont été utilisés pour vendre la POO proviennent pour la plupart du monde impératif.
Si tu crois que faire des boucles est indispensable pour l'algorithmique, tu te trompes lourdement. Et tu as beaucoup de choses à apprendre, choses qui te seront utiles même si tu te limites à Java/C#/C++.
Quel est le problème avec un langage n'ayant pas d'exceptions ? Si toutes les valeurs de retour sont correctement utilisées (et surtout, ne jamais avoir la valeur "null", qui est un problème de beaucoup de langages), ça me semble réalisable.
Je crois pourtant qu'avoir des exceptions, limitées au minimum, est une bonne chose. Mais cela dépend surtout de la philosophie du langage. Les problèmes rencontrés dans Anubis 1 pourraient être résolus, théoriquement.
Je suis surpris, mais je ne demande qu'à voir.je ne crois pas que Turing-complet ait beaucoup de sens. Mais de toute façon, être Turing-complet n'est pas très important. Dans la programmation usuelle, on n'en a pas besoin.
Sera-t-il toujours possible, dans Anubis 2, de faire une boucle infinie ? Par exemple, comme dans le code du serveur (cf le défi).
Vous avez un bloqueur de publicités installé.
Le Club Developpez.com n'affiche que des publicités IT, discrètes et non intrusives.
Afin que nous puissions continuer à vous fournir gratuitement du contenu de qualité, merci de nous soutenir en désactivant votre bloqueur de publicités sur Developpez.com.
Partager