Systeme de type non dénombrable(Was: Tableauxmultidimensionnels et déréférencement)

La question :

On 2009-06-15, ld a écrit :
On 15 juin, 15:12, Marc Boyer <Marc.Bo...@cert.onera.fr.invalid>
a écrit :
On 2009-06-15, Marc Espie <es...@lain.home> a écrit :

> In article <h0qqis$tc...@shakotay.alphanet.ch>,
> Antoine Leca  <r...@localhost.invalid> a écrit :
>>Que veut dire « tous » ? Les types du C décrivent un ensemble infini
>>(peut-être même non dénombrable, mais cela fait trop longtemps que ce
>>sujet ne me préoccupe plus pour que je ne sois pas 100% sûr).


> N'importe quoi.


 Disons qu'il faut arriver à exprimer un infini non dénombrable avec
un nombre fini de symbole, et c'est pas évident à faire avec
une sémantique raisonnable.


Sans aller chercher bien, loin, le lambda calcul le permet parce
qu'une fonction peut se renvoyer elle-même. Par exemple \x.xx ne peut
pas être type parce qu'il ne peut pas être réduit (expansion infinie).


Faut encore prouver que cet infini là est non dénombrable.
Est-ce qu'on arrive à le mettre en isomorphisme avec N^* ou N^N ?
Je ne m'avancerais pas.

> Oui, il y a des trucs marrants en theorie des types. Mais il faut du typage
> automatique pour sortir des trucs exprimables par le systeme de types... et
> c'est bien le souci, en general.


   Voui, avec des constructeurs universels et existentiels, et
un petit point fixe, on doit pouvoir jouer...
   M'enfin, on doit être loi du C...


Si c'est typé, ça devrait être dénombrable.


Parce que tu manques d'ambition
Non, c'est clair qu'on préfère un système de type qui soit
décidable (histoire de pouvoir faire de la vérif des types avec
un compilateur), où au moins pas trop indécidable (pour pouvoir
"en général" trouver le type), et qu'intutivement, ça va
nous rammener dans un truc pas trop compliqué à gérer avec
un ordinateur (machine discrete), donc dénombrable surement.

Mais bon... Ce devrait être un exercice d'info théo que
de définir un langage dont le système de types est continu.

Marc Boyer
--
Au XXIème siècle, notre projet de société s'est réduit
à un projet économique...

Poser votre question sur le forum Programmation

La réponse :

In article ,
Marc Boyer <d> a écrit :


Parce que tu manques d'ambition
Non, c'est clair qu'on préfère un système de type qui soit
décidable (histoire de pouvoir faire de la vérif des types avec
un compilateur), où au moins pas trop indécidable (pour pouvoir
"en général" trouver le type), et qu'intutivement, ça va
nous rammener dans un truc pas trop compliqué à gérer avec
un ordinateur (machine discrete), donc dénombrable surement.

Mais bon... Ce devrait être un exercice d'info théo que
de définir un langage dont le système de types est continu.


Hum, pas sur que ca soit si loin. Des que tu veux faire du 1er ordre,
tu te retrouves en general coince entre deux extremes, soit un type
trop precis (qui ne recouvre pas certains cas d'utilisation d'une fonction),
soit un type trop general (qui te type comme correct des expressions qui
ne le sont pas). La plupart des systemes "interessants" vont
etre indecidables (de toutes facons, c'est normal, les problemes informatiques
se divisent en problemes triviaux, et en problemes impossibles, ou presque).

Les approches pratiques pour resoudre ce dilemne reposent le plus souvent
sur des hierarchies de systemes de type (ca ressemble furieusement a des
filtres dans une topologie adaptee), que tu construis par recurrence...
Doit bien y avoir moyen d'utiliser une ou deux limites projectives pour
obtenir un modele continue...

Poser votre question sur le forum Programmation

Questions similaires :

Nom global des fonctions système de Linux ?

JM writes: [/color] From: JM Subject: Nom global des fonctions système de Linux ? Newsgroups: fr.comp.lang.general Followup-To: fr.comp.developpement Date: Tue, 28 Jun 2005 18:46:32 +0200 --drkm