To see the other types of publications on this topic, follow the link: Calculs explicites.
Dissertations / Theses on the topic 'Calculs explicites'
Create a spot-on reference in APA, MLA, Chicago, Harvard, and other styles
Consult the top 42 dissertations / theses for your research on the topic 'Calculs explicites.'
Next to every source in the list of references, there is an 'Add to bibliography' button. Press on it, and we will generate automatically the bibliographic reference to the chosen work in the citation style you need: APA, MLA, Harvard, Chicago, Vancouver, etc.
You can also download the full text of the academic publication as pdf and read online its abstract whenever available in the metadata.
Browse dissertations / theses on a wide variety of disciplines and organise your bibliography correctly.
1
Varescon, Firmin. "Calculs explicites en théorie d'Iwasawa." Thesis, Besançon, 2014. http://www.theses.fr/2014BESA2019/document.
Full textAbstract:
Dans le premier chapitre de cette thèse on rappelle l'énoncé ainsi que des équivalents de la conjecture de Leopoldt puis l'on donne un algorithme permettant de vérifier cette conjecture pour un corps de nombre et premier donnés. Pour la suite on suppose cette conjecture vraie pour le premier p fixé Et on étudie la torsion du groupe de Galois de l'extension abélienne maximale p-ramifiée. On présente une méthode qui détermine effectivement les facteurs invariants de ce groupe fini. Dans le troisième chapitre on donne des résultats numériques que l'on interpréte via des heuristiques à la Cohen-Lenstra. Dans le quatrième chapitre, à l'aide de l'algorithme qui permet le calcul de ce module, on donne des exemples de corps et de premiers vérifiant la conjecture de GreenbergIn the first chapter of this thesis we explain Leopoldt's conjecture and some equivalent formulations. Then we give an algorithm that checks this conjecture for a given prime p and a number field. Next we assume that this conjecture is true, and we study the torsion part of the Galois group of the maximal abelian p-ramified p-extension of a given number field. We present a method to compute the invariant factors of this finite group. In the third chapter we give an interpretation of our numrical result by heuristics “à la” Cohen-Lenstra. In the fourth and last chapter, using our algorithm which computes this torsion submodule, we give new examples of numbers fields which satisfy Greenberg's conjecture
2
RIOS, ALEJANDRO. "Contributions a l'etude des lambda-calculs avec substitutions explicites." Paris 7, 1993. http://www.theses.fr/1993PA077091.
Full textAbstract:
Le lambda-sigma-calcul (ls) a deux sortes de termes: terme propre et substitution. Le ls-calcul est confluent sur les termes clos, mais il n'est pas localement confluent sur tous les termes. La confluence locale est atteinte en ajoutant quatre regles. Le calcul ainsi obtenu est appele lsp, et sa non-confluence sur la totalite des termes a ete recemment montree. Cependant, le lsp-calcul et le lsp-calcul extensionnel sont confluents sur l'ensemble des termes semi-clos (ceux qui n'admettent que de variables de sorte terme propre). Ces resultats sont obtenus en utilisant la methode d'interpretation; pour l'appliquer, la normalisation forte du sp-calcul de substitutions associe est necessaire. Une nouvelle technique est developpee pour l'assurer. Dans le cadre type, on introduit une interpretation du ls-calcul type du premier ordre dans le lambda-calcul, pour laquelle la correction et la completude sont etablies. La normalisation forte du tau-calcul est un probleme ouvert. Un premier pas est franchi en montrant la normalisation faible. Le lambda-nu-calcul (ln) traite la substitution explicite en abandonnant la notation de de bruijn. La correction de ln ne peut etre obtenue qu'en imposant des restrictions aux variables du terme de depart. On introduit une condition et une strategie de reduction qui la preserve, pour laquelle ln est correct et confluent modulo alpha-conversion
3
Benaissa, Zine-EI-Abidine. "Les calculs de substitutions explicites comme fondement des implantations des langages fonctionnels." Nancy 1, 1997. http://www.theses.fr/1997NAN10173.
Full textAbstract:
Les langages de programmation fonctionnels font partie des langages de très haut niveau. Ils peuvent être vus comme des extensions ou des variantes du lambda-calcul, un formalisme mathématique puissant qui a donné lieu à d'innombrables travaux durant les vingt dernières années. Ils bénéficient de ce fait assez directement, pour la définition de leur sémantique, du riche corps de doctrine qui a été constitué autour de celui-ci. Si ce formalisme, au départ simple, donne lieu à tant de variations, c'est en particulier à des fins d'implantation. Notamment, au travers de la béta-réduction (une opération fondamentale du lambda-calcul) différentes stratégies d'évaluation peuvent être définies : elles constituent autant de spécifications possibles pour les implantations de ces langages. La béta-réduction est une opération complexe comparée aux instructions machines utilisées pour la mettre en oeuvre et, de ce fait, il existe un fossé assez important entre la spécification d'une stratégie d'évaluation et sa réalisation. En conséquence, les preuves de corrections des implantations de langages fonctionnels restent limitées, rendant difficile les comparaisons formelles entre les différentes implantations. Les calculs de substitutions explicites, introduits par Curien, remplacent l'opération de substitution intervenant dans la béta-réduction par des opérations plus élémentaires. Ces calculs décomposent la béta-réduction en une règle de déclenchement de la substitution et un ensemble de règles de propagation de cette substitution. Ces règles de propagation ont un grain fin qui rapprochent la béta-réduction des instructions qui l'implantent. L'introduction de ces calculs a ouvert une voie nouvelle de recherche d'un formalisme mieux adapté à la description unifiée de sémantique, de stratégie d'évaluation et d'implantations associées. [. . . ]
4
Doray, Franck. "Calculs explicites dans les groupes de Grotendieck et de Chow des variétés homogènes projectives." Phd thesis, Université Joseph Fourier (Grenoble), 2006. http://tel.archives-ouvertes.fr/tel-00120949.
Full textAbstract:
Les variétés homogènes projectives sous un groupe algébrique déployéont une géométrie assez simple. La décomposition de Bruhat fournit, en
effet, une décomposition cellulaire de ces variétés. Il en résulte que
l'anneau de Chow de telles variétés admet une base formée des classes
des adhérences de ces cellules, appelées variétés de Schubert.
Il en est de même pour l'anneau de Grothendieck de telles variétés.
Cela entraîne en particulier que ces deux anneaux sont sans torsion.
Plus précisément, la base ainsi obtenue pour l'anneau de Grothendieck
fournit la filtration topologique de cette anneau et redonne
la base de l'anneau de Chow par passage au gradué. D'autre part,
il existe une seconde base due à Pittie et Steinberg de l'anneau
de Grothendieck de ces variétés, invariante sous l'action du groupe de Galois.
Le Chapitre II de la thèse revient, dans le cas des drapeaux complets
associés à un espace vectoriel, sur les résultats connus concernant
la combinatoire donnant les expressions des faisceaux structuraux des
variétés de Schubert dans l'anneau de Grothendieck, ce qui permet, en
suivant les travaux de Lascoux notamment, d'exprimer combinatoirement
la matrice de changement de bases entre les deux bases ci-dessus. Dans
le cas de la variété de drapeaux complets d'un espace vectoriel de
dimension trois, nous donnons des résolutions explicites des faisceaux
structuraux des variétés de Schubert en termes des fibrés de la base
de Pittie.
Les groupes de Chow sont connus en codimension un et ont été étudiés
en codimension deux par Karpenko dans le cas des variétés de
Severi-Brauer. Le calcul des motifs des varietés homogènes projectives
sous le groupe projectif linéaire d'une algébre simple centrale sur un
corps se ramène sous certaines conditions au calcul de motifs de
variétés de Severi-Brauer généralisées, formes de grassmaniennes,
comme l'ont montré Calmès, Petros, Semenov et Zainouline. Dans le
chapitre II, nous construisons des isomorphismes de variétés
explicites qui permettent de ramener le calcul des groupes de Chow de
ces variétés au calcul de groupes de Chow de variétés de Severi-Brauer
généralisées.
Les techniques décrites dans le chapitre III sont réutilisées au
chapitre IV pour redémontrer un résultat de Karpenko sur la
décomposition du motif de Chow de variétés de Severi-Brauer associée
à une algèbre de matrices à coefficients dans une algèbre simple
centrale.
5
Gomez, Xavier. "Quelques calculs explicites sur les groupes quantiques de petit rang aux racines de l'unité." Aix-Marseille 2, 2000. http://www.theses.fr/2000AIX22046.
Full text
6
Faure, Germain. "Structures et modèles de calculs de réécriture." Phd thesis, Université Henri Poincaré - Nancy I, 2007. http://tel.archives-ouvertes.fr/tel-00164576.
Full textAbstract:
Le calcul de réécriture ou rho-calcul est une généralisation du lambda-calcul avec filtrage et agrégation de termes. L'abstraction sur les variables est étendue à une abstraction sur les motifs et le filtrage correspondant peut être effectué modulo une théorie équationnelle a priori arbitraire. L'agrégation est utilisée pour collecter les différents résultats possibles.
Dans cette thèse, nous étudions différentes combinaisons des ingrédients fondamentaux du rho-calcul: le filtrage, l'agrégation et les mécanismes d'ordre supérieur.
Nous étudions le filtrage d'ordre supérieur dans le lambda-calcul pur modulo une restriction de la beta-conversion appelée super-développements. Cette nouvelle approche est suffisamment expressive pour traiter les problèmes de filtrage du second-ordre et ceux avec des motifs d'ordre supérieur à la Miller.
Nous examinons ensuite les modèles catégoriques du
lambda-calcul parallèle qui peut être vu comme un enrichissement du lambda-calcul avec l'agrégation de termes. Nous montrons que ceci est une étape significative vers la sémantique dénotationnelle du calcul de réécriture.
Nous proposons également une étude et une comparaison des calculs avec motifs éventuellement dynamiques, c'est-à-dire qui peuvent être instanciés et réduits. Nous montrons que cette étude, et plus particulièrement la preuve de confluence, est suffisamment générale pour
s'appliquer à l'ensemble des calculs connus. Nous étudions ensuite l'implémentation de tels calculs en proposant un calcul de réécriture avec filtrage et substitutions explicites.
7
Polonovski, Emmanuel. "Substitutions explicites, logiques et normalisation." Paris 7, 2004. https://tel.archives-ouvertes.fr/tel-00007962.
Full text
8
Briaud, Daniel. "Substitutions explicites et unification d'ordre supérieur." Nancy 1, 1997. http://www.theses.fr/1997NAN10251.
Full textAbstract:
Les lambda-calculs à substitutions explicites fournissent un cadre formel pour l'étude de la théorie des substitutions. Ils constituent ainsi un pont entre le lambda-calcul et les programmes. Notre contribution, composée de deux volets, porte sur l'étude en soi des lambda-calculs à substitutions explicites et sur l'emploi d'un tel calcul comme pont entre théorie et pratique. Le premier volet a pour but l'explicitation de la eta-réduction, le second à trait à l'unification d'ordre supérieur. Notre travail sur la eta-réduction se résume ainsi. La beta-réduction du lambda-calcul distingue certaines fonctions extensionnellement égales. En ajoutant la règle de eta-réduction, on obtient une égalité extensionnelle. Nous définissons et étudions une règle eta opératoire et indépendante d'un calcul a substitutions explicites donne. Ceci nous conduit à une variante non-conditionnelle de eta, nommée eta. Nous montrons que la réduction générée est une extension conservative de la beta-eta-réduction, cela sur l'ensemble des lambda-termes typables avec l'intersection. Le second problème qui nous intéresse, l'unification d'ordre supérieur, consiste à résoudre des équations entre lambda-termes simplement types. Sa programmation demeure difficile à vérifier car l'algorithme classique est formellement défini au moyen de la substitution du lambda-calcul. Décrire une procédure d'unification d'ordre supérieur à l'aide de substitutions explicites établit une passerelle entre l'unification d'ordre supérieur et son implantation. Une approche précédente se fonde sur le système lambda-sigma' et s'appuie sur la composition et la confluente ouverte. Notre approche, basée sur le système lambda-upsilon, montre que ni l'une ni l'autre ne sont nécessaires pour exprimer l'unification d'ordre supérieur au moyen d'un lambda-calcul à substitutions explicites. Notre travail à ce sujet simplifie, sur plusieurs plans, les travaux précédents sur ce thème
9
Polonovski, Emmanuel. "Subsitutions explicites, logique et normalisation." Phd thesis, Université Paris-Diderot - Paris VII, 2004. http://tel.archives-ouvertes.fr/tel-00007962.
Full textAbstract:
Les substitutions explicites ont été introduites comme un raffinement du lambda-calcul, celui-ci étant leformalisme utilisé pour étudier la sémantique des langages de programmation. L'objet de cette thèse
est l'étude de leurs propriétés de normalisation forte et de préservation de la normalisation forte. Ce
manuscrit rend compte de plusieurs travaux autour de ces propriétés de normalisation, regroupés en
trois volets.
Le premier d'entre eux formalise une technique générale de preuve de normalisation forte utilisant
la préservation de la normalisation forte. On applique cette technique à un spectre assez large de calculs
avec substitutions explicites afin de mesurer les limites de son utilisation. Grâce à cette technique, on
prouve un résultat nouveau : la normalisation forte du lambda-upsilon-calcul simplement typé.
Le deuxième travail est l'étude de la normalisation d'un calcul symétrique non-déterministe issu de
la logique classique formulée dans le calcul des séquents, auquel est ajouté des substitutions explicites.
La conjonction des problèmes posés par les calculs symétriques et ceux posés par les substitutions
explicites semble vouer à l'échec l'utilisation de preuves par réductibilité. On utilise alors la technique
formalisée dans le premier travail, ce qui nous demande de prouver tout d'abord la préservation de la
normalisation forte. A cette fin, on utilise un fragment de la théorie de la perpétuité dans les systèmes
de réécriture.
La définition d'une nouvelle version du lambda-ws-calcul avec nom, le lambda-wsn-calcul, constitue le troisième
volet de la thèse. Pour prouver sa normalisation forte par traduction et simulation dans les réseaux
de preuve, on enrichit l'élimination des coupures de ceux-ci avec une nouvelle règle, ce qui nous oblige
à prouver que cette nouvelle notion de réduction est fortement normalisante.
10
Doguy, Ayman. "Modélisation explicite de l'adaptation sémantique entre modèles de calcul." Phd thesis, Supélec, 2013. http://tel.archives-ouvertes.fr/tel-00935157.
Full textAbstract:
Ce travail traite de la modélisation de systèmes complexes constitués de plusieurs composants impliquant des domaines techniques différents. Il se place dans le contexte de la modélisation hétérogène hiérarchique, selon l'approche à base de modèles de calcul. Chaque composant faisant appel à un domaine technique particulier, son comportement peut être modélisé selon un paradigme de modélisation approprié, avec une sémantique différente de celle des autres composants. La modélisation du système global, qui intègre les modèles hétérogènes de ces composants, nécessite donc une adaptation sémantique permettant l'échange entre les divers sous-modèles. Ce travail propose une approche de modélisation de l'adaptation sémantique où les sémantiques du temps et du contrôle sont explicitement spécifiées par le concepteur en définissant des relations sur les occurrences d'évènements d'une part et sur les étiquettes temporelles de ces occurrences d'autre part. Cette approche est intégrée dans la plateforme ModHel'X et testée sur un cas d'étude : un modèle de lève-vitre électrique.
11
Dogui, Ayman, and Ayman Dogui. "Modélisation explicite de l'adaptation sémantique entre modèles de calcul." Phd thesis, Supélec, 2013. http://tel.archives-ouvertes.fr/tel-00995072.
Full textAbstract:
Ce travail traite de la modélisation de systèmes complexes constitués de plusieurs composants impliquant des domaines techniques différents. Il se place dans le contexte de la modélisation hétérogène hiérarchique, selon l'approche à base de modèles de calcul. Chaque composant faisant appel à un domaine technique particulier, son comportement peut être modélisé selon un paradigme de modélisation approprié, avec une sémantique différente de celle des autres composants. La modélisation du système global, qui intègre les modèles hétérogènes de ces composants, nécessite donc une adaptation sémantique permettant l'échange entre les divers sous-modèles.Ce travail propose une approche de modélisation de l'adaptation sémantique où les sémantiques du temps et du contrôle sont explicitement spécifiées par le concepteur en définissant des relations sur les occurrences d'évènements d'une part et sur les étiquettes temporelles de ces occurrences d'autre part. Cette approche est intégrée dans la plateforme ModHel'X et testée sur un cas d'étude : un modèle de lève-vitre électrique.
12
Dogui, Ayman. "Modélisation explicite de l'adaptation sémantique entre modèles de calcul." Thesis, Supélec, 2013. http://www.theses.fr/2013SUPL0030/document.
Full textAbstract:
Ce travail traite de la modélisation de systèmes complexes constitués de plusieurs composants impliquant des domaines techniques différents. Il se place dans le contexte de la modélisation hétérogène hiérarchique, selon l’approche à base de modèles de calcul. Chaque composant faisant appel à un domaine technique particulier, son comportement peut être modélisé selon un paradigme de modélisation approprié, avec une sémantique différente de celle des autres composants. La modélisation du système global, qui intègre les modèles hétérogènes de ces composants, nécessite donc une adaptation sémantique permettant l’échange entre les divers sous-modèles.Ce travail propose une approche de modélisation de l’adaptation sémantique où les sémantiques du temps et du contrôle sont explicitement spécifiées par le concepteur en définissant des relations sur les occurrences d’évènements d’une part et sur les étiquettes temporelles de ces occurrences d’autre part. Cette approche est intégrée dans la plateforme ModHel’X et testée sur un cas d’étude : un modèle de lève-vitre électriqueThis work takes place in the context of hierarchical heterogeneous modeling using the model of computation approach in order to model complex systems which includes several components from different technical fields.Each of these components is usually designed according to a modeling paradigm that suits the technical domain and is based on specific semantics. Therefore, the overall system, which integrates the heterogeneous models of the components, requires semantic adaptation to ensure proper communication between its various sub-models.In this context, the aim of this thesis is to propose a new approach of semantic adaptation modeling where the semantic adaptation of time and control is specified by defining relationships between the occurrences of events as well as the time tags of these occurrences. This approach was integrated into the ModHel’X platform and tested on the case study of a power window system
13
Nguyen, Tan trung. "Schémas numériques explicites à mailles décalées pour le calcul d'écoulements compressibles." Thesis, Aix-Marseille, 2013. http://www.theses.fr/2013AIXM4705/document.
Full textAbstract:
We develop and analyse explicit in time schemes for the computation of compressible flows, based on staggered in space. Upwinding is performed equation by equation only with respect to the velocity. The pressure gradient is built as the transpose of the natural divergence. For the barotropic Euler equations, the velocity convection is built to obtain a discrete kinetic energy balance, with residual terms which are non-negative under a CFL condition. We then show that, in 1D, if a sequence of discrete solutions converges to some limit, then this limit is the weak entropy solution. For the full Euler equations, we choose to solve the internal energy balance since a discretization of the total energy is rather unnatural on staggered meshes. Under CFL-like conditions, the density and internal energy are kept positive, and the total energy cannot grow. To obtain correct weak solutions with shocks satisfying the Rankine-Hugoniot conditions, we establish a kinetic energy identity at the discrete level, then choose the source term of the internal energy equation to recover the total energy balance at the limit. More precisely speaking, we prove that in 1D, if we assume the L∞ and BV-stability and the convergence of the scheme, passing to the limit in the discrete kinetic and internal energy equations, we show that the limit of the sequence of solutions is a weak solution. Finally, we consider the computation of radial flows, governed by Euler equations in axisymetrical (2D) or spherical (3D) coordinates, and obtain similar results to the previous sections. In all chapters, we show numerical tests to illustrate for theoretical resultsWe develop and analyse explicit in time schemes for the computation of compressible flows, based on staggered in space. Upwinding is performed equation by equation only with respect to the velocity. The pressure gradient is built as the transpose of the natural divergence. For the barotropic Euler equations, the velocity convection is built to obtain a discrete kinetic energy balance, with residual terms which are non-negative under a CFL condition. We then show that, in 1D, if a sequence of discrete solutions converges to some limit, then this limit is the weak entropy solution. For the full Euler equations, we choose to solve the internal energy balance since a discretization of the total energy is rather unnatural on staggered meshes. Under CFL-like conditions, the density and internal energy are kept positive, and the total energy cannot grow. To obtain correct weak solutions with shocks satisfying the Rankine-Hugoniot conditions, we establish a kinetic energy identity at the discrete level, then choose the source term of the internal energy equation to recover the total energy balance at the limit. More precisely speaking, we prove that in 1D, if we assume the L∞ and BV-stability and the convergence of the scheme, passing to the limit in the discrete kinetic and internal energy equations, we show that the limit of the sequence of solutions is a weak solution. Finally, we consider the computation of radial flows, governed by Euler equations in axisymetrical (2D) or spherical (3D) coordinates, and obtain similar results to the previous sections. In all chapters, we show numerical tests to illustrate for theoretical results
14
Kervarc, Romain. "Systèmes de types purs et substitutions explicites." Lyon, École normale supérieure (sciences), 2007. http://www.theses.fr/2007ENSL0399.
Full textAbstract:
La théorie des types est actuellement considérée comme un outil fondamental en informatique, car elle établit un lien entre un calcul d'une part et un système logique d'autre part, ce qui permet d'exprimer des propriétés variées. Les systèmes de types purs sont un formalisme général dans lequel on peut définir un grand nombre de systèmes logiques. Cette thèse présente l'extension de ces systèmes dans deux cadres : un calcul à substitutions explicites et un calcul de séquents classique, et étudie les propriétés des systèmes obtenus, en particulier la correction des types, la reconstruction de dérivations, la réduction du sujet et la normalisation forte. Dans le premier cas, on introduit une nouvelle règle d'inférence de type inspirée de la synthèse de type et une nouvelle technique de démonstration avec un ordre sur les dérivations. Dans le second cas, on étudie en particulier la notion de bonne formation et l'on s'intéresse à des réorganisations perpétuelles de chemin de réductionType theory is currently considered as a fundamental tool in computer science, since it establishes a link between a calculus on the one hand and a logical system on the other hand, which allows to state various properties. Pure type systems are a very general formalism in terms of which many logical systems may be expressed. This thesis presents the extension of those systems in two frameworks: a calculus with explicit substitutions and a classical sequent calculus, and studies the properties of the obtained systems, especially type correction, derivation reconstruction, subject reduction, and strong normalisation. In the first case, a new typing rule is introduced, inspired by type inference considerations, and also a new proof method, relying on an order upon derivations. In the second case, the notion of well-formedness is more particularly studied, and one also considers perpetual reorganisations of reduction paths
15
Foo, Wei Guo. "Explicit Calculations of Siu’s Effective Termination of Kohn’s Algorithm and the Hachtroudi-Chern-Moser Tensors in CR Geometry." Thesis, Université Paris-Saclay (ComUE), 2018. http://www.theses.fr/2018SACLS041/document.
Full textAbstract:
La première partie présente des calculs explicites de terminaison effective de l'algorithme de Kohn proposée par Siu. Dans la deuxième partie, nous étudions la géométrie des hypersurfaces réelles dans Cⁿ, et nous calculons des invariants explicites avec la méthode d'équivalences de Cartan pour déterminer les lieux CR-ombilicsThe first part of the thesis consists of calculations around Siu's effective termination of Kohn's algorithm. The second part of the thesis studies the CR real hypersurfaces in complex spaces and calculates various explicit invariants using Cartan's equivalence method to study CR-umbilical points
16
Kim, Nguyen. "Explicit arithmetic of Brauer groups ray class fields and index calculus /." [S.l.] : [s.n.], 2001. http://deposit.ddb.de/cgi-bin/dokserv?idn=963601687.
Full text
17
Lopez, Philippe. "Conception et validation d'une paramétrisation explicite des hydrométéores de grande échelle : évaluation de son potentiel dans les calculs adjoints." Toulouse 3, 2001. http://www.theses.fr/2001TOU30081.
Full text
18
Renaud, Fabien. "Les ressources explicites vues par la théorie de la réécriture." Phd thesis, Université Paris-Diderot - Paris VII, 2011. http://tel.archives-ouvertes.fr/tel-00697408.
Full textAbstract:
Cette thèse s'articule autour de la gestion de ressources explicites dans les langages fonctionnels, en mettant l'accent sur des propriétés de calculs avec substitutions explicites raffinant le lambda-calcul. Dans une première partie, on s'intéresse à la propriété de préservation de la beta-normalisation forte (PSN) pour le calcul lambda s. Dans une seconde partie, on étudie la propriété de confluence pour un large ensemble de calculs avec substitutions explicites. Après avoir donné une preuve générique de confluence basée sur une série d'axiomes qu'un calcul doit satisfaire, on se focalise sur la métaconfluence de lambda j, un calcul où le mécanisme de propagation des substitutions utilise la notion de multiplicité, au lieu de celle de structure. Dans la troisième partie de la thèse on définit un prisme des ressources qui généralise de manière paramétrique le lambda-calcul dans le sens où non seulement la substitution peut être explicite, mais également la contraction et l'affaiblissement. Cela donne un ensemble de huit calculs répartis sur les sommets du prisme pour lesquels on prouve de manière uniforme plusieurs propriétés de bon comportement comme par exemple la simulation de la beta-réduction, la PSN, la confluence, et la normalisation forte pour les termes typés. Dans la dernière partie de la thèse on montre différentes ouvertures vers des domaines plus pratiques. On s'intéresse à la complexité d'un calcul avec substitutions en premier lieu. On présente des outils de recherche et on conjecture des bornes maximales. Enfin, on finit en donnant une spécification formelle du calcul lambda j dans l'assistant à la preuve Coq.
19
Pagano, Bruno. "Des calculs de substitution explicite et de leur application a la compilation et de leur application a la compilation des langages fonctionnels." Paris 6, 1998. http://www.theses.fr/1998PA066272.
Full textAbstract:
Les calculs de substitutions explicites, offrent un intermediaire entre le lambda-calcul et son implantation. Ils ont ete utilises avec succes pour la conception et la preuve de correction de machines abstraites, l'unification d'ordre superieur ou encore pour la construction incrementale de preuves. Cette these est fondee sur le calcul de substitution explicite de hardin et levy, qui est le seul calcul a ce jour qui soit confluent sur les termes ouverts (ou meta-termes). Elle explore ce formalisme suivant trois axes : 1. La reecriture d'ordre superieur. Dans un premier temps nous montrons que l'adjonction de symboles et de regles confluentes du premier ordre conserve la confluence du calcul de hardin-levy. Nous developpons ensuite un formalisme de reecriture d'ordre superieur, baptise explicit reduction system, dont les mecanismes de substitution sont ceux du calcul avec substitution explicite etendus a des lieurs quelconques. Nous definissons une notion d'arite de liaison basee sur le comportement du passage de la substitution a travers les lieurs. Des conditions suffisantes sont donnees pour la confluence. 2. La theorie de la demonstration. Dans cette partie, nous nous sommes attaches a decrire le systeme de deduction associe par isomorphisme (a la curry-howard) au calcul de hardin-levy. Nous obtenons un calcul equivalent a la deduction naturelle et le nommons calcul de multi-sequents avec variables de jugement. Il permet de manipuler conclusions ou hypotheses ainsi que des variables de preuve. 3. La compilation. Nous montrons comment les calculs de substitutions explicites permettent de representer des machines abstraites, leur correction et la strategie qu'elles suivent. Nous decrivons en detail quatre machines abstraites : la kam, la secd, la cam et la fam. Pour cette derniere, nous montrons comment les substitutions explicites sont utiles pour exprimer la compilation de programmes fonctionnels.
20
Guenot, Nicolas. "Deduction Imbriquée et Fondements Logiques du Calcul." Phd thesis, Ecole Polytechnique X, 2013. http://pastel.archives-ouvertes.fr/pastel-00929908.
Full textAbstract:
Cette thèse s'intéresse à l'usage des formalismes d'inférence profonde comme fondement des interprétations calculatoires des systèmes de preuve, en suivant les deux approches principales: celle des preuves comme programmes et celle de la recherche de preuve comme calcul. La première contribution est le développement d'une famille de systèmes de preuve pour la logique intuitionniste dans le calcul des structures et dans les séquents imbriqués. pour lesquels des procédures de normalisation internes sont fournies. L'une de ces procédures est alors interprétée en termes calculatoires, comme un raffinement de la correspondance de Curry-Howard permettant d'introduire une forme de partage ainsi que des opérateurs de communication dans un lambda-calcul avec substitution explicite. Du coté de la recherche de preuve, la notion de preuve focalisée en logique linéaire est transférée du calcul des séquents au calcul des structures, où elle induit une forme incrémentale de focalisation, dotée d'une preuve de complétude très simple. Enfin, une autre interprétation de la recherche de preuve est donnée par l'encodage de la réduction d'un lambda-calcul avec substitution explicite dans les règles d'inférence d'un sous-système de la logique intuitionniste dans le calcul des structures.
21
Goueygou, Marc. "Formulation explicite de la réponse impulsionnelle de sources planes non bafflées : application au calcul du rayonnement acoustique des structures vibrantes." Valenciennes, 1997. https://ged.uphf.fr/nuxeo/site/esupversions/01f4b2b2-cfee-44ed-9ff4-28b2d7bc04f8.
Full textAbstract:
Le travail présenté dans ce mémoire consiste à développer et a valider une nouvelle méthode de calcul du rayonnement acoustique des structures vibrantes. Cette méthode s'applique au cas de sources planes non bafflées de géométrie quelconque. Contrairement aux méthodes basées sur l'équation intégrale (BIE), elle repose sur une formulation explicite de la réponse impulsionnelle du système source, milieu de propagation, point d'observation. Cette formulation constitue une généralisation de l'intégrale de Rayleigh au cas de sources non bafflées. D’autre part, le calcul numérique de la réponse est effectue directement dans le domaine temporel, en utilisant l'algorithme de la représentation discrète. Cette méthode est utilisée pour étudier la réponse large bande de sources de forme simple. Nos calculs sont ensuite confrontes avec des solutions analytiques et des résultats obtenus par un code éléments finis. Enfin, les réponses calculées par notre méthode sont comparées avec celles enregistrées sur une structure vibrante réelle. Ces différentes comparaisons s'avèrent globalement satisfaisantes et démontrent la validité de notre approche. Par rapport aux méthodes éléments finis, la méthode développée présente l'avantage d'un formalisme simple et d'une mise en œuvre aisée. Contrairement à d'autres méthodes basées sur une formulation explicite, elle ne se limite pas seulement au cas de sources bafflées. Ainsi, elle peut être utilisée comme un moyen de prévision du bruit impulsionnel, ou bien comme un outil simple et rapide pour la modélisation de transducteurs large bande.
22
Javan, Peykar Ariyan. "Bornes polynomiales et explicites pour les invariants arakeloviens d'une courbe de Belyi." Phd thesis, Université Paris Sud - Paris XI, 2013. http://tel.archives-ouvertes.fr/tel-00840828.
Full textAbstract:
On borne explicitement la hauteur de Faltings d'une courbe sur le corps de nombres algèbriques en son degré de Belyi. Des résultats similaires sont démontré pour trois autres invariants arakeloviennes : le discriminant, l'invariant delta et l'auto-intersection de omega. Nos résultats nous permettent de borner explicitement les invariantes arakeloviennes des courbes modulaires, des courbes de Fermat et des courbes de Hurwitz. En plus, comme application, on montre que l'algorithme de Couveignes-Edixhoven-Bruin est polynomial sous l'hypothèse de Riemann pour les fonctions zeta des corps de nombres. Ceci était connu uniquement pour certains sous-groupes de congruence. Finalement, on utilise nos résultats pour démontrer une conjecture de Edixhoven, de Jong et Schepers sur la hauteur de Faltings d'un revêtement ramifié de la droite projective sur l'anneau des entiers.
23
Monroy-Borja, Raul. "Planning proofs of correctness of CCS systems." Thesis, University of Edinburgh, 1997. http://hdl.handle.net/1842/584.
Full textAbstract:
The specification and verification of communicating systems has captured increasing interest in the last decades. CCS, a Calculus of Communicating Systems [Milner 89a], was especially designed to help this enterprise; it is widely used in both industry and academia. Most efforts to automate the use of CCS for verification have centered around the explicit construction of a bisimulation [Park 81]. This approach, however, presents severe limitations to deal with systems that contain infinite states (e.g. systems with evolving structure [Milner 89a] or that comprise a finite but arbitrary number of components (e.g. systems with inductive structure [Milner 89a]). There is an alternative approach to verification, based on equational reasoning, which does not exhibit such limitations. This formulation, however, introduces significant proof search control issues, and, hence, has remained far less explored. This thesis investigates the use of explicit proof plans [Bundy 88] for problems of automatic verification in the context of CCS. We have conducted the verification task using equational reasoning, and centred on infinite state systems, and parameterised systems. A parameterised system, e.g. a system with inductive structure, circumscribes a family of CCS systems, which have fixed struture and finitely many states. To reason about theses systems, we have adopted Robin Milner's approach [Milner 89a], which advocates the use of induction to exploit the structure and/or the behavior of a system during its verification. To automate this reasoning, wehave used proof plans for induction [Bundy 88]- built within CLAM [Bundy et al 90b], and extended it with special CCS proof plans. We have implemented a verification planner by adding these special proof plans to CLAM. The system handles the search control problems prompted by CCS verification satisfactorily, though it is not complete. Moreover, the system is capable of dealing with the verification of finite state systems, infinite state systems, and parameterised systems, hence, providing a uniform method to analyse CCS systems, regardless of their state space. Our results are encouraging: the verification planner has been successfully tested on a number of examples drawn from the litereature. We have planned proofs of conjectures that are outside the domain of existing verification methods. Furthernore; the verification planning is fully automated. Because of this, even though the verification plan has still got plenty of room for improvement, we can state that proof planning can handle the equational verication of CCS systems, and, therefore, advocate its use within this interesting field.
24
Armengaud, Gérard. "Calcul explicite (analytique et numérique) des champs de contraintes dans des structures élancées homogènes et composites à l'aide de méthodes énergétiques." Toulouse 3, 1996. http://www.theses.fr/1996TOU30004.
Full textAbstract:
Nous avons developpe et applique a differents problemes de calcul des structures elastiques, une methode permettant de determiner une approximation optimale du champ des contraintes. Cette methode est basee sur l'utilisation de theoremes energetiques associes a la construction de champs de contraintes statiquement admissibles. Dans une premiere partie, pour des poutres composites rectilignes soumises a la flexion avec effort tranchant, nous proposons une methode de determination des contraintes de cisaillement et nous donnons une formulation analytique permettant de calculer les coefficients de cisaillement associes aux differentes sections etudiees en exemples d'application. Dans une seconde partie, nous presentons une analyse de la distribution des contraintes dans des assemblages colles plan a double recouvrement, tubulaires et cylindriques soumis a des chargements axiaux de traction. Les champs de contraintes developpes respectent toutes les conditions aux limites et de continuite. L'etude de deux problemes supplementaires, traitant pour le premier d'un assemblage precontraint et pour le second de l'ecrasement d'une couche mince entre deux plans paralleles, nous a permis d'evaluer l'interet de notre methode en comparant avec d'autres approches analytiques. Enfin une derniere partie est consacree a la mise en place d'une formulation permettant de determiner le champ des contraintes dans des poutres courbes composites soumises a des sollicitations de flexion-traction avec effort tranchant
25
BRES, Yannis. "Exploration implicite et explicite de l'espace d'´etats atteignables de circuits logiques Esterel." Phd thesis, Université de Nice Sophia-Antipolis, 2002. http://tel.archives-ouvertes.fr/tel-00003600.
Full textAbstract:
Cette thèse traite des approches implicites et explicites, ainsi que de leur convergence, de l'exploration d'espace d'états atteignables de circuits logiques provenant de programmes réactifs synchrones écrits en Esterel, ECL ou SyncCharts. Nos travaux visent à réduire les coûts de ces explorations à l'aide detechniques génériques ou spécifiques à notre cadre de travail. Nous utilisons les résultats de ces explorations à des fins de vérification formelle de propriétés de sûreté, de génération d'automates explicites ou de génération de séquences de tests exhaustives. Nous décrivons trois outils.
Le premier outil est un vérificateur formel implicite, à base de Diagrammes de Décisions Binaires (BDDs). Ce vérificateur présente plusieurs techniques permettant de réduire le nombre de variables impliquées dans les calculs d'espace d'états. Nous proposons notamment l'abstraction de variables à l'aide d'une logique trivaluée. Cette nouvelle méthode étend la technique usuelle de remplacement de variables d'états par des entrées libres. Ces deux méthodes calculant des sur-approximations de l'espace d'états atteignables, nous proposons différentes techniques utilisant des informations concernant la structure du modèle et permettant de réduire la sur-approximation.
Le deuxième outil est un moteur d'exploration explicite, basé sur l'énumération des états accessibles.
Ce moteur repose sur la simulation de la propagation du courant électrique dans les portes du circuit et supporte les circuits cycliques. Ce moteur comporte de nombreuses optimisations et fait appel à différentes heuristiques visant à éviter les explosions en temps ou en espace inhérentes à cette approche, ce qui lui
confère de très bonnes performances. Ce moteur a été appliqué à la génération d'automates explicites et à la vérification formelle.
Enfin, le troisième outil est une évolution hybride implicite/explicite du moteur purement explicite. Dans cette évolution, les états sont toujours analysés individuellement mais symboliquement à l'aide de BDDs. Ce moteur a également été appliqué à la génération d'automates explicites, mais il est plutôt destiné à la vérification formelle ou la génération de séequences de tests exhaustives.
Nous présentons des résultats d'expérimentations de ces différentes approches sur plusieurs exemples industriels.
26
Taylor, Amelia V. "A unifying framework for Lambda Calculi and their extensions with explicit substitution operators that is useful for verifying confluence." Thesis, Heriot-Watt University, 2006. http://hdl.handle.net/10399/119.
Full text
27
Marchais, Jérémy. "Couplage de modèles multi-échelles pour la représentation de phénomènes localisés en dynamique transitoire explicite." Thesis, Cachan, Ecole normale supérieure, 2014. http://www.theses.fr/2014DENS0023/document.
Full textAbstract:
La représentation de phénomènes de rupture localisée (fissure, décohésion…) rend nécessaire l'utilisation de modèle de plus en plus fin et couteux en calcul. Pour pallier à ce problème de nombreux modèles multi-échelles ont permis de faire cohabiter deux échelles de modèles différents dont l'un plus grossier permet des gains de calculs substantiels. Cependant, coupler deux modèles différents peut entrainer un certain nombre d'incompatibilités qui peuvent générer notamment des réflexions parasites au niveau des interfaces. La première partie de mes travaux traite de l'incompatibilité issue du passage d'un comportement non-local à un comportement local dans un milieu discret. De nouveaux schémas de construction à l'interface sont proposés afin de réduire in fine les phénomènes de réflexions. La deuxième partie aborde une seconde source d'incompatibilité due au changement d'échelle de discrétisation dans un milieu continu local. Une nouvelle méthode de dissipation sélective permet de réduire les phénomènes de réflexions en absorbant les phénomènes microscopiques. Finalement, l'ensemble de ces démarches sera mis en place sur un modèle de béton fibré pour observer l'évolution de phénomène localisé en dynamique expliciteRepresentation of localized phenomena like failures or cracks requires models increasingly precise and cpu consuming. To overcome this problem many multiscale models allowed to coexist two scales of different models including a coarser one that enables to gain substantial time calculations. However, coupling two different models may cause a number of incompatibilities that can generate difficulties such as spurious reflections at the interfaces. The first part of my work deals with the incompatibility after the passage of a non-local behavior at a local behavior in a discreet environment. New construction schemes at the interface are proposed to reduce the reflection phenomena. The second part deals with a second source of incompatibility due to the scaling of discretization in a local continuum. A new method for selective dissipation reduces reflection phenomena absorbing microscopic phenomena. Finally, all of these steps will be implemented on a model of fiber-reinforced concrete to observe the evolution of localized phenomenon in explicit dynamics
28
Abdennadher, Salim. "Etude de l'écrasement de structures alvéolaires sous sollicitation dynamique rapide : application aux matériaux cellulaires." Paris 6, 2004. http://www.theses.fr/2004PA066425.
Full text
29
Guenot, Nicolas. "Nested Deduction in Logical Foundations for Computation." Palaiseau, Ecole polytechnique, 2013. http://pastel.archives-ouvertes.fr/docs/00/92/99/08/PDF/thesis.pdf.
Full textAbstract:
Cette thèse s'intéresse à l'usage des formalismes d'inférence profonde comme fondement des interprétations calculatoires des systèmes de preuve, en suivant les deux approches principales: celle des preuves comme programmes et celle de la recherche de preuve comme calcul. La première contribution est le développement d'une famille de systèmes de preuve pour la logique intuitionniste dans le calcul des structures et dans les séquents imbriqués. Pour lesquels des procédures de normalisation internes sont fournies. L'une de ces procédures est alors interprétée en termes calculatoires, comme un raffinement de la correspondance de Curry-Howard permettant d'introduire une forme de partage ainsi que des opérateurs de communication dans un lambda-calcul avec substitution explicite. Du coté de la recherche de preuve, la notion de preuve focalisée en logique linéaire est transférée du calcul des séquents au calcul des structures, où elle induit une forme incrémentale de focalisation, dotée d'une preuve de complétude très simple. Enfin, une autre interprétation de la recherche de preuve est donnée par l'encodage de la réduction d'un lambda-calcul avec substitution explicite dans les règles d'inférence d'un sous-système de la logique intuitionniste dans le calcul des structuresThis thesis investigates the use of deep inference formalisms as basis for a computational interpretation of proof systems, following the two main approaches: proofs-as-programs and proof-search-as-computation. The first contribution is the development of a family of proof systems for intuitionistic logic in the calculus of structures and in nested sequents, for which internal normalisation procedures are given. One of these procedure is then interpreted in terms of computation, as a refinement of the Curry-Howard correspondence allowing to introduce a form of sharing and communication operators in a lambda-calculus with explicit substitution. On the side of proof-search, the notion of focused proof in linear logic is transferred from the sequent calculus into the calculus of structures, where it yields an incremental form of focusing, with a simple proof of completeness. Finally, another interpretation of proof-search is given through the encoding of reduction in a lambda-calculus with explicit substitution into the inference rules of a subsystem of intuitionistic logic in the calculus of structures
30
Sinot, François-Régis. "Stratégies Efficaces et Modèles d'Implantation pour les Langages Fonctionnels." Phd thesis, Ecole Polytechnique X, 2006. http://pastel.archives-ouvertes.fr/pastel-00001952.
Full textAbstract:
Dans les langages fonctionnels, l'efficacité dépend crucialement du choix de la stratégie d'évaluation et d'un modèle d'implantation adapté. Nous développons d'abord un λ-calcul avec substitutions explicites qui évite les problèmes habituels liés à la substitution et à l'α-conversion, dans lequel on peut définir les stratégies usuelles, mais aussi des stratégies avec un meilleur partage de calcul. Ensuite, nous développons un modèle d'implantation efficace pour ce calcul. Pour cela, nous proposons une représentation innnovante des variables libres, d'abord dans le cadre très général de la récriture d'ordre supérieur, puis avec plus de détails dans notre cas particulier. Nous obtenons ainsi un λ-calcul avec substitutions explicites sans noms ni indices, dans lequel les te! rmes sont annotés avec de l'information qui indique comment les substitutions doivent être propagées, et qui constitue un modèle d'implantation efficace pour nos stratégies. Des machines abstraites sont alors définies, implantées et comparées expérimentalement aux meilleurs évaluateurs connus. Finalement, nous étudions les relations entre machines abstraites traditionnelles et réseaux d'interaction, deux modèles d'implantation courants mais très différents. Plus précisément, nous montrons comment certaines stratégies peuvent être implantées dans les réseaux d'interaction d'une façon très naturelle, rapprochant ainsi deux modèles utilisés pour l'implantation de stratégies efficaces.
31
Narainen, Rodrigue. "Comparaison de trois méthodes de calcul pour la simulation de l'emboutissage de tôles axisymétriques." Compiègne, 1993. http://www.theses.fr/1993COMPD668.
Full textAbstract:
L'objectif de cette thèse est la mise au point de différents outils numériques destinés à la simulation de l'emboutissage de tôles axisymétriques dans lesquelles apparaissent de grandes déformations élasto-plastiques. Trois approches non linéaires basées sur la méthode des éléments finis. Les deux premières approches sont des méthodes incrémentales de type implicite et explicite pour l'analyse statique et dynamique. Ces méthodes ont pour fonction de simuler le plus fidèlement possible l'emboutissage. Le comportement en membrane flexion et cisaillement transversal de la tôle est représenté ainsi que l'anisotropie transverse du matériau. Les conditions de contact entre la tôle et les outils sont représentées à l'aide des méthodes de pénalisation (implicite statique) et des multiplicateurs de Lagrange (explicite dynamique) où le frottement obéit à la loi de Coulomb. La troisième méthode est l'approche inverse qui permet d'estimer les déformations de membrane de la tôle emboutie en comparant directement les formes initiale et finale de la pièce. On détermine par le calcul les positions initiales des points matériels situés sur la forme finale. La loi de comportement est basée sur la théorie de déformation totale. Les comparaisons de ces trois formulations portent sur leurs efficacités (temps calcul) et leurs précisions a travers différents exemples.
32
Ezrailson, Cathy Mariotti. "EMIT: explicit modeling of interactive-engagement techniques for physics graduate teaching assistants and the impact on instruction and student performance in calculus-based physics." Diss., Texas A&M University, 2004. http://hdl.handle.net/1969.1/1467.
Full textAbstract:
This study measures the effect of a model of explicit instruction (EMIT) on the: 1) physics graduate teaching assistants adherence to reformed teaching methods, 2) impact of the instructional model on GTAs beliefs about the nature of physics and physics problem solving and 3) undergraduate physics students understanding and performance in an introductory calculus-based physics course. Methods included explicit modeling for the treatment group GTAs of the Reformed Teaching Observation Protocol (RTOP) and assessment of treatment and control GTAs and their students throughout the semester. Students understanding was measured using the Force Concept Inventory (FCI) and Flash-mediated Force and Motion Concept Inventory (FM2CA). Students were surveyed about performance of GTAs using the Student Survey (SS). Results indicated changes were tied to individual GTAs beliefs about the nature of physics. Student conceptual understanding reflected a two-fold Hake gain compared to the control group. General application of the EMIT model presupposes explicit instruction of the model for GTAs.
33
Jeanmasson, Guillaume. "Méthode explicite à pas de temps local pour la simulation des écoulements turbulents instationnaires." Thesis, Bordeaux, 2019. http://www.theses.fr/2019BORD0458.
Full textAbstract:
La simulation instationnaire d'écoulements turbulents (LES : Large Eddy Simulation, par exemple) reste à l'heure actuelle coûteuse en terme de temps de calcul. Un travail sur les méthodes numériques d'intégration temporelle des équations de la mécanique des fluides peut rendre de type de simulation plus accessible. Les méthodes d'intégration temporelle explicites présentent des propriétés intéressantes telles qu'une bonne précision et une bonne compatibilité avec les techniques HPC (parallélisation, vectorisation...). Néanmoins, le pas de temps de ces méthodes est fortement limité : il est choisi de manière à respecter la contrainte CFL la plus restrictive sur le maillage. Ceci rend ces méthodes généralement très coûteuses. Dans le cas des méthodes explicites à pas de temps local, le pas de temps varie sur le maillage en s'adaptant à différentes contraintes CFL locales. Le pas de temps est plus optimal sur l'ensemble du maillage, ce qui réduit les temps de simulation par rapport à une méthode explicite à pas de temps global (uniforme). Les schémas à pas de temps local de la littérature sont essentiellement utilisés sur des cas-test académiques, et on recense peu d'applications de ces schémas en CFD. L'objectif de cette thèse est de montrer que ce type de schéma peut être utilisé de manière efficace pour la LES. Pour atteindre cet objectif, deux nouveaux schémas à pas de temps local ont d'abord été mis en place. Deux simulations LES ont ensuite été réalisées à l'aide de notre schéma à pas de temps local le plus performant. Ces deux simulations ont démontré la bonne précision et l'efficacité de notre schéma à pas de temps local pour la simulation d'écoulements turbulentsUnsteady simulations of turbulent flows (LES : Large Eddy Simulation, for instance) still present an important computational cost. Improvement of numerical time integration methods could reduce the computational effort needed by these simulations. Explicit time integration methods present attractive properties such that accuracy and good compatibility with HPC (parallelization, vectorization…). Nevertheless, the time step used by these methods is strongly restricted : it is chosen to respect the most severe CFL condition over the mesh. This makes explicit time integration methods very expensive in terms of computational cost. Explicit local time stepping methods use a non uniform time step to satisfy several local CFL conditions over the mesh. The time step is more optimal over the mesh, which leads to a reduction of computational cost with respect to an explicit time integration method with a uniform time step. Most of the local time stepping schemes proposed in the literature are applied to academical test cases, and very few applications are performed in CFD. This thesis's goal is to show the ability of explicit local time stepping schemes to carry out efficient and accurate simulations of turbulent flows. To reach this goal, two new explicit local time stepping schemes have been developed. Then, two LES have been carried out with our most efficient local time stepping scheme. Both cases have demonstrated the accuracy and the efficiency of our local time stepping scheme for the computations of turbulent flows
34
Javan, Peykar Ariyan. "Explicit polynomial bounds for Arakelov invariants of Belyi curves." Thesis, Paris 11, 2013. http://www.theses.fr/2013PA112075/document.
Full textAbstract:
On borne explicitement la hauteur de Faltings d'une courbe sur le corps de nombres algèbriques en son degré de Belyi. Des résultats similaires sont démontré pour trois autres invariants arakeloviennes : le discriminant, l'invariant delta et l'auto-intersection de omega. Nos résultats nous permettent de borner explicitement les invariantes arakeloviennes des courbes modulaires, des courbes de Fermat et des courbes de Hurwitz. En plus, comme application, on montre que l'algorithme de Couveignes-Edixhoven-Bruin est polynomial sous l’hypothèse de Riemann pour les fonctions zeta des corps de nombres. Ceci était connu uniquement pour certains sous-groupes de congruence. Finalement, on utilise nos résultats pour démontrer une conjecture de Edixhoven, de Jong et Schepers sur la hauteur de Faltings d'un revêtement ramifié de la droite projective sur l'anneau des entiersWe explicitly bound the Faltings height of a curve over the field of algebraic numbers in terms of the Belyi degree. Similar bounds are proven for three other Arakelov invariants: the discriminant, Faltings' delta invariant and the self-intersection of the dualizing sheaf. Our results allow us to explicitly bound these Arakelov invariants for modular curves, Hurwitz curves and Fermat curves. Moreover, as an application, we show that the Couveignes-Edixhoven-Bruin algorithmtime under the Riemann hypothesis for zeta-functions of number fields. This was known before only for certain congruence subgroups. Finally, we utilize our results to prove a conjecture of Edixhoven, de Jong and Schepers on the Faltings height of a branched cover of the projective line over the ring of integers
35
Guiraud, Yves. "Présentations d'opérades et systèmes de réécriture." Phd thesis, Université Montpellier II - Sciences et Techniques du Languedoc, 2004. http://tel.archives-ouvertes.fr/tel-00006863.
Full textAbstract:
Cette thèse étudie les propriétés calculatoires des présentations d'opérades, ou systèmes de réécriture de diagrammes de Penrose, et leurs liens avec divers types de systèmes de réécriture classiques. Grâce à des nouveaux critères pour la terminaison et la confluence, on démontre la conjecture sur la convergence de la présentation L(Z2) des Z/2Z-espaces vectoriels, une théorie équationnelle commutative. On montre que les présentations d'opérades sont des généralisations des systèmes de réécriture de mots et des réseaux de Petri et qu'elles fournissent un calcul de gestion explicite des ressources pour les systèmes de réécriture de termes linéaires à gauche. Enfin, on étudie les obstructions à ce même résultat concernant le lambda-calcul. Des annexes présentent les liens entre les opérades et d'autres structures de l'algèbre universelle, ainsi qu'un calcul de substitutions explicites.
36
Delmas, Josselin. "Stratégies de contrôle d'erreur en calcul de structures industrielles : Mise en oeuvre d'estimation d'erreur en quantité d'intérêt et d'adaptation de maillage." Phd thesis, Université de Picardie Jules Verne, 2008. http://tel.archives-ouvertes.fr/tel-00311947.
Full textAbstract:
Pour les problèmes linéaires, différentes démarches existent pour estimer la qualité de la solution éléments finis. Elles conduisent généralement à l'estimation d'une norme de l'erreur globale. Mais le choix d'une précision globale fondée sur une norme du déplacement est souvent délicat car il n'y a pas de lien direct quantitatif avec une erreur sur des quantités mécaniques locales (appelées quantités d'intérêt) ayant un intérêt pour l'ingénieur. L'objectif de ce travail est de développer et de mettre en oeuvre dans Code_Aster une méthode d'estimation d'erreur en quantité d'intérêt pour le calcul de structures industrielles.Une étude bibliographique a permis de situer l'état de l'art et de faire le point sur les méthodes d'estimation d'erreur globale et locale et sur les techniques d'adaptation de maillages afin de déterminer celles qui sont les plus adaptées pour le calcul de structures en milieu industriel.
Ensuite, une comparaison a été faite afin de déterminer la pertinence de l'utilisation de l'erreur en quantité d'intérêt dans un processus adaptatif par rapport à l'utilisation de l'erreur en norme de l'énergie, d'un raffinement uniforme ou d'un raffinement local dans la zone d'intérêt. L'étude a montré que l'utilisation de l'erreur en quantités d'intérêt est la stratégie qui permet toujours d'obtenir la meilleure précision pour un nombre d'éléments donné : cette stratégie est la plus pertinente dans un contexte de calcul de structures industrielles.
Compte tenu des résultats précédents, une méthode d'estimation d'erreur en quantité d'intérêt a été développée et implémentée dans Code_Aster. Elle est basée sur la relation fondamentale de l'erreur en quantité d'intérêt et sur un estimateur d'erreur globale en norme de l'énergie de type résidus explicites. Cet estimateur ne permettant pas d'accéder à des bornes de l'erreur mais à une valeur approchée, il s'apparente donc à un indicateur d'erreur. Pour réaliser cette estimation, la résolution d'un problème dual est nécessaire. Les chargements de ce problème, particulier pour chaque quantité d'intérêt considérée, sont fournis pour de nombreuses quantités d'intérêt (notamment pour la contrainte de Von Mises). Le calcul final de l'erreur en quantité d'intérêt, à partir du calcul primal et du calcul dual est automatique. Une quantité d'intérêt pour l'estimation de l'erreur sur les facteurs d'intensité des contraintes a également été développée en 2D et 3D. Des exemples numériques ont montré le bon comportement de cet indicateur pour guider un processus d'adaptation de maillage pour les différentes quantités d'intérêt.
Enfin, la stratégie de contrôle d'erreur développée a été utilisée, avec Code_Aster, dans le cadre d'études de structures industrielles. Deux études effectuées au département AMA, à EDF R&D sont présentées. La première consiste à étudier la contrainte de Von Mises dans un rotor HP, la seconde s'intéresse à la contrainte verticale dans les goujons d'un assemblage boulonné.
37
Fekak, Fatima-Ezzahra. "Étude de la réponse dynamique des ponts roulants soumis à des chocs multiples pendant un séisme : Co-simulation implicite / explicite multi-échelle en temps pour la dynamique du contact." Thesis, Lyon, 2017. http://www.theses.fr/2017LYSEI037/document.
Full textAbstract:
Les ponts roulants sont des engins de levage situés en haut des bâtiments qu'ils équipent. Ils servent à manutentionner des charges très lourdes et parfois critiques. Pendant un séisme, un pont roulant est exposé à des chocs multiples. Ces impacts peuvent causer des dommages importants dans la structure pouvant conduire à une chute de la charge manutentionnée ou du pont roulant lui-même. Donc, la vérification de la tenue des ponts roulants au séisme est une question primordiale. Actuellement, cette vérification est basée sur des méthodes de calcul statiques. Ces méthodes font l'hypothèse d'un comportement purement linéaire des ponts roulants ce qui les rend très conservatives. Depuis quelques années les niveaux sismiques imposés par les autorités nationales augmentent chaque année, et les constructeurs de ponts roulants se trouvent dans l'incapacité de construire à partir des efforts sur-estimés fournis par les méthodes statiques. L'objectif de la thèse est l'étude de la réponse dynamique d'un pont roulant pendant un séisme en prenant en compte les non-linéarités géométriques et matériau. Afin de modéliser ces phénomènes, une analyse dynamique temporelle avec une approche multi-échelle en temps est adoptée. Pour prendre en compte l'aspect haute fréquence des chocs, un intégrateur temporel variationnel explicite, basé sur la méthode des multiplicateurs de Lagrange et dédié au contact/impact, est développé. Ensuite, un intégrateur hétérogène (différents schémas d'intégration) asynchrone (différents pas de temps), basé sur la méthode de couplage GC, est appliqué au problème du pont roulant. Cette stratégie multi-échelle en temps permet d'adapter le schéma d'intégration et le pas de temps au sous domaine considéré. Par conséquent, l'intégrateur explicite est adopté dans les zones de contact et un schéma implicite de type accélération moyenne, est adopté dans le reste de la structure. Finalement, un démonstrateur de co-simulation entre les logiciels Cast3M et Europlexus est mis en place pour montrer le gain très significatif en temps de calcul dans le cas d'un modèle élément finis tridimensionnel d'un pont roulant industrielBridge cranes are hoisting appliances located overhead in buildings. They are used to handle very heavy and sometimes critical loads. During an earthquake, a bridge crane may be subjected to multiple impacts between wheels and rails. These impacts can cause significant damage to the structure leading to a fall of the handled load or the bridge crane itself. Therefore, the qualification of such equipment, subjected to an earthquake, is very important. Currently, this qualification is based on static methods. These methods assume a purely linear behavior of the bridge cranes, which leads to a very conservative forces. Consequently, the bridge cranes manufacturers are sometimes unable to design the equipement from the over-estimated efforts provided by the static methods. The aim of this work is to study the dynamic response of a bridge crane during an earthquake by taking into account the geometric and material non-linearities. In order to model such phenomena, a time-history dynamic analysis with a multi-scale approach is performed. To take into account the high frequency aspect of the impacts between wheels and rails, a Lagrange explicit contact/impact time integrator is proposed. This work has also led to the development of an explicit–implicit HATI (Heterogeneous Asynchronous Time Integrator) for contact/impact dynamics. This method allows us to adopt an explicit contact/impact time integrator in the contact area and an implicit time integrator with a coarse mesh in the rest of the domain. Finally, a co-simulation demonstrator between Cast3M and Europlexus softwares is set up to show the very significant gain in computation time for a three-dimensional finite element model of an industrial bridge crane
38
Letellier, Guillaume. "Modélisation du complexe récepteur muscarinique/ toxique MT7 à partir de données thermodynamiques." Phd thesis, Université Paris-Diderot - Paris VII, 2008. http://tel.archives-ouvertes.fr/tel-00447060.
Full textAbstract:
Les récepteurs muscariniques à l'acétylcholine sont des protéines transmembranaires jouant des rôles dans de nombreux processus physiologiques. La toxine MT7 est un puissant modulateur allostérique de ces récepteurs. De plus, cette toxine est le seul ligand connu spécifique du sous-type 1 des récepteur muscariniques (hM1). Nous avons étudié les bases moléculaires de l'interaction entre la toxine MT7 et le récepteur hM1 par modélisation. Tout d'abord un échantillonnage des structures des deux partenaires a été réalisé par dynamique moléculaire. Les mouvements de grande amplitude de la boucle e2 du récepteur ont été prédits par dynamique activée. Puis la toxine a été arrimée sur le récepteur par des calculs de dynamique moléculaire sous contraintes ambigües dérivées de données de mutagénèse. Ce modèle a ensuite été optimisé par une simulation de dynamique moléculaire libre, en environnement membranaire explicite. Enfin, des calculs en retour des valeurs d'énergie libre de liaison ont été effectués afin de valider le modèle. Nous prédisons que la toxine se lie sur un dimère de récepteurs hM1. Le cœur de l'interaction est localisé sur un des monomères en contact avec les boucles II et III de la toxine. Cette interaction est complétée par des interactions hydrophobes au niveau de la boucle I sur le second monomère. L'analyse de ce modèle apporte des éléments de compréhension à la fois sur bases structurale de la haute affinité de cette toxine ainsi que sur sa sélectivité pour ce sous-type de récepteur. Il apparaît que cette sélectivité est essentiellement portée par la boucle extracellulaire e2 du récepteur.
39
Brage, Jens. "A Natural Interpretation of Classical Proofs." Doctoral thesis, Stockholm : Dept. of mathematics, Stockholm university, 2006. http://urn.kb.se/resolve?urn=urn:nbn:se:su:diva-913.
Full text
40
Gokpi, Kossivi. "Modélisation et Simulation des Ecoulements Compressibles par la Méthode des Eléments Finis Galerkin Discontinus." Thesis, Pau, 2013. http://www.theses.fr/2013PAUU3005/document.
Full textAbstract:
L’objectif de ce travail de thèse est de proposer la Méthodes des éléments finis de Galerkin discontinus (DGFEM) à la discrétisation des équations compressibles de Navier-Stokes. Plusieurs challenges font l’objet de ce travail. Le premier aspect a consisté à montrer l’ordre de convergence optimal de la méthode DGFEM en utilisant les polynômes d’interpolation d’ordre élevé. Le deuxième aspect concerne l’implémentation de méthodes de ‘‘shock-catpuring’’ comme les limiteurs de pentes et les méthodes de viscosité artificielle pour supprimer les oscillations numériques engendrées par l’ordre élevé (lorsque des polynômes d’interpolation de degré p>0 sont utilisés) dans les écoulements transsoniques et supersoniques. Ensuite nous avons implémenté des estimateurs d’erreur a posteriori et des procédures d ’adaptation de maillages qui permettent d’augmenter la précision de la solution et la vitesse de convergence afin d’obtenir un gain de temps considérable. Finalement, nous avons montré la capacité de la méthode DG à donner des résultats corrects à faibles nombres de Mach. Lorsque le nombre de Mach est petit pour les écoulements compressibles à la limite de l’incompressible, la solution souffre généralement de convergence et de précision. Pour pallier ce problème généralement on procède au préconditionnement qui modifie les équations d’Euler. Dans notre cas, les équations ne sont pas modifiées. Dans ce travail, nous montrons la précision et la robustesse de méthode DG proposée avec un schéma en temps implicite de second ordre et des conditions de bords adéquatsThe aim of this thesis is to deal with compressible Navier-Stokes flows discretized by Discontinuous Galerkin Finite Elements Methods. Several aspects has been considered. One is to show the optimal convergence of the DGFEM method when using high order polynomial. Second is to design shock-capturing methods such as slope limiters and artificial viscosity to suppress numerical oscillation occurring when p>0 schemes are used. Third aspect is to design an a posteriori error estimator for adaptive mesh refinement in order to optimize the mesh in the computational domain. And finally, we want to show the accuracy and the robustness of the DG method implemented when we reach very low mach numbers. Usually when simulating compressible flows at very low mach numbers at the limit of incompressible flows, there occurs many kind of problems such as accuracy and convergence of the solution. To be able to run low Mach number problems, there exists solution like preconditioning. This method usually modifies the Euler. Here the Euler equations are not modified and with a robust time scheme and good boundary conditions imposed one can have efficient and accurate results
41
Kim, Nguyen [Verfasser]. "Explicit arithmetic of Brauer groups : ray class fields and index calculus / Kim Nguyen." 2001. http://d-nb.info/963601687/34.
Full text
42
Lu, Chia-Hung, and 陸家弘. "Explicit Solutions of Some Certain Class of Fractional Partial Differential Equations by Means ofFractional Calculus." Thesis, 2013. http://ndltd.ncl.edu.tw/handle/10529417387026064345.
Full textAbstract:
博士中原大學
應用數學研究所
101
In recent years,various operators of fractional calculus(thatis,calculus of integrals and deriva-tives of arbitrary real or complex orders)have been investigated and applied in many remarkably diverse fields of science and engineering. Many authors have demonstrated the usefulness of fractional calculus in the derivation of particular solutions of anumber of linear ordinary and partial differential equations of the second and higher orders. The purpose of this paper is to present a certain class of the explicit particular solutions of associated Cauchy-Euler fractional partial differential equation of arbitrary real or complex orders and their applications.And to show how this simple fractional calculus method to the solutions of some families of fractional partial differential equations would lead naturally to several interesting consequences. The methodology presented here is based chiefly upon some general theorems on explicit particular solutions of some families of fractional differential equations with Laplace transform and the expansion coefficients of binomial series. One open question for the wave(diffusion)equation,we can use fractional calculus and seperated variable methods to solve the classical Cauchy problem with the functional initial conditions. We also can use Fourier series to obtain the particular solution.