Systeme de type non dénombrable(Was: Tableaux multidimensionnels et déréférencement)
Marc Boyer
> On 15 juin, 15:12, Marc Boyer <Marc.Bo...@cert.onera.fr.invalid>
> wrote:
>> On 2009-06-15, Marc Espie <es...@lain.home> wrote:
>>
>> > In article <h0qqis$tc...@shakotay.alphanet.ch>,
>> > Antoine Leca �<r...@localhost.invalid> wrote:
>> >>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...
Marc Espie
Marc Boyer <Marc....@cert.onera.fr.invalid> wrote:
> 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...