Date : 1996
Editeur / Publisher : [S.l.] : [s.n.] , 1996
Format : 230 P.
Type : Livre / Book
Type : Thèse / ThesisLangue / Language : français / French
Résumé / Abstract : LE LAMBDA CALCUL AVEC RESSOURCES, DEFINI PAR G. BOUDOL EN CONNEXION AVEC LE CODAGE DU LAMBDA CALCUL DANS LE PI CALCUL DE R. MILNER, EST UN RAFFINEMENT NON-DETERMINISTE DU CALCUL FAIBLE A LA ABRAMSKY, INTRODUISANT LA NOTION DE BLOCAGE PENDANT L'EVALUATION PAR LE MOYEN D'ARGUMENTS CONSTITUES D'UN NOMBRE POSSIBLEMENT FINI DE RESSOURCES. NOUS ABORDONS DANS CETTE THESE L'ETUDE DE LA SEMANTIQUE OPERATIONNELLE ET DES MODELES DU CALCUL AVEC RESSOURCES. L'EQUATION AUX DOMAINES STANDARD POUR LES CALCULS FAIBLES N'EST PAS ASSEZ EXPRESSIVE POUR PERMETTRE L'INTERPRETATION DES ARGUMENTS FINIS DU CALCUL AVEC RESSOURCES. NOUS PROPOSONS DEUX NOUVELLES EQUATIONS DE LA FORME D = M(D) D QUI DIFFERENT DANS LA CONSTRUCTION M(D). CETTE CONSTRUCTION CORRESPOND INTUITIVEMENT, DANS LES DEUX CAS, AU DOMAINE DES MULTI-ENSEMBLES D'ELEMENTS DE D. LES PRESENTATIONS LOGIQUES DES SOLUTIONS CANONIQUES DES EQUATIONS - DANS LA CATEGORIE DES TREILLIS COMPLETS ALGEBRIQUES, CONSTITUENT DES MODELES ADEQUATS DU CALCUL. LE PREMIER EST UN MODELE DE CONES, LE DEUXIEME UN MODELE DE FILTRES, QUI ONT, CHACUN, UN SYSTEME DE TYPES AVEC INTERSECTION A LA COPPO ASSOCIE. LA PARTICULARITE DE CES SYSTEMES EST LE TRAITEMENT MULTIPLICATIF DE LA CONJONCTION, AUTREMENT DIT L'IMPOSSIBILITE D'EFFECTUER DES CONTRACTIONS D'HYPOTHESES (QUI CORRESPOND AU CARACTERE FINI DES ARGUMENTS). AUCUN DES MODELES N'EST POURTANT COMPLETEMENT ADEQUAT POUR LE CALCUL DE RESSOURCES. L'AJOUT D'UN OPERATEUR DE TEST DE CONVERGENCE SUFFIT POUR LE MODELE DE CONES. NOUS CONJECTURONS QUE C'EST AUSSI SUFFISANT POUR LE MODELE DE FILTRES