Cours informatique l'analyse des dépendances
... ... ...
Introduction
Cette analyse des dépendances est la deuxième phase de l'analyse des données. Elle a pour but de préparer la phase suivante, à savoir le MCD en recherchant les liens entre les différentes données également appelés les dépendances.
L'analyse de ces liens produira comme document un diagramme ou un graphe des dépendances. Cet outil est assez peu utilisé dans le monde professionnel, le placement des données étant réalisé insitu au moment de la conception du MCD. Cette étape reste néanmoins import nte en phase de démarrage dans l'analyse des données.
Les notions de dépendances fonctionnelles
Soient A et B les ensembles de valeurs prises par deux données.
Il y a dépendance fonctionnele entre A et B lorsque, connaissant une valeur de A, quelque soit cette valeur, on détermine une et une seule valeur de B. Dans ce qui suit, dépendance fonctionnelle sera abrégée par DF
On symbolise la dépendance fonctionnelle par A → B où
- A est appelé source de la DF (on dit aussi déterminant ou partie gauche)
- et B la cible (on dit aussi but, déterminé ou partie droite) de la DF.
Exemple :
NumClient→ NomClient
NumCLient → AdresseClient
RefProduit → LibProduit
Cela signifie qu’à un numéro de client ne correspondent qu’un et un seul nom et une et une seule adresse. En revanche, il n’est pas impossible qu’à une adresse, résident plusieurs clients, d'où l'importance de bien définir le sens de la dépendance.
Par contre, la DF RefProduit → NumClient n’est pas avérée. En effet, un produit peut avoir été commandé par plusieurs clients. Il faut dans ce cas de plus invoquer la notion de commande.
2.1 Dépendance fonctionnelle forte et faible
La définition de la dépendance fonctionnelle peut être affinée :
• Définition stricte DF forte :
o la DF associe à chaque valeur de A une et une seule de B : il y a unicité au départo la DF est vérifiée pour toutes les valeurs de A : il y a totalité au départ (toutes les valeurs de A ont une image dans l’ensemble d’arrivée B)
Exemple :
la dépendance fonctionnelle NumCommande → NumClient est une DF forte car il n’y a pas de commande sans client.
• Définition large DF faible :
o Il y a dépendance fonctionnelle entre A et B lorsque, connaissant une valeur de A, quelque soit cette valeur, on détermine au plus une valeur de B.
o Cette définition supprime la contrainte de totalité au départ. On parle de DF faible. Certaines valeurs de A n'ont pas de valeurs de B
Exemple :
La dépendance fonctionnelle NoInsee → NomJeuneFille est une DF faible car certaines
valeurs de NoInsee n’ont pas de correspondance dans l’ensemble d’arrivée ; c’est le cas pour les hommes pour lesquels la propriété NomJeuneFille n’a pas de sens.
2.2 Dépendance fonctionnelle à partie gauche composée
Une dépendance fonctionnelle peut comporter dans sa partie gauche plusieurs attributs. On parle dans ce cas de dépendance fonctionnelle à partie gauche composée. Pour connaître une valeur de l’ensemble d’arrivée C, il faut connaître un couple (ou plus) de valeurs provenant de A et de B.
Ce type de DF est noté : (d1, d2) → d3
Exemples :
(NoFacture, CodeProduit) → QtéFacturée, (NoElève, Matière, Date) → Note
Je ne peux connaître la note de Pierre en Français pour le devoir du 10 mai que si je connais ces trois éléments : Le code de l'élève , la matière concernée et la date. S'il manque l'un quelconque de ces éléments, je ne peux déterminer avec exactitude la note correspondante.
2.3 Dépendance fonctionnelle élémentaire
Une dépendance fonctionnelle est élémentaire s’il n’existe aucune donnée ou sous-ensemble de données de la partie gauche assurant une dépendance fonctionnelle vers le même but. Autrement dit, il ne doit pas y avoir de propriété superflue dans la source de la DF.
Par définition les dépendance fonctionnelle à deux rubriques (A B) sont toujours élémentaires.
Exemples :
RefProduit→ LibProduit est élémentaire (deux rubriques)
(NumFacture, RefProduit) → QtéFacturée est élémentaire (ni la référence produit seule, ni le numéro de facture seul permettent de déterminer la quantité)
(NumFacture, RefProduit) → LibProduit n’est pas élémentaire puisque la référence du produit suffit à déterminer le libellé.
2.4 Dépendance fonctionnelle directe
Une dépendance fonctionnelle d1 → d2 est directe s’il n’existe aucune donnée d3 qui engendrerait une dépendance fonctionnelle transitive telle que d1 → d2 → d3
Par exemple, soient les dépendances fonctionnelles :
NumFacture → NumReprésentant et NumReprésentant → NomReprésentant
NumFacture → NomReprésentant n’est pas une dépendance fonctionnelle directe puisqu’elle est obtenue par transitivité. Il conviendra alors de ne considérer que la premiére DF.
2.5 Dépendances fonctionnelles symétriques
Certaines dépendances fonctionnelles sont symétriques, c’est à dire que la partie gauche détermine la partie droite et inversement.
Par exemple :
NoSérieVéhicule→ NoImmatriculation et NoImmatriculation→ NoSérieVéhicule
Dans ce cas, il faut choisir de privilégier une des dépendances fonctionnelles, en fonction des règles de gestion.
S'il s'agit d'assurer le suivi du véhicule tout au long de sa vie, le no d'Immatriculation pouvant changer, on choisira la premiére DF (NoSérieVéhicule→ NoImmatriculation).
3 La recherche et la formalisation des dépendances fonctionnelles
La recherche passe par deux phases, à savoir quels sont les objets du domaine de gestion observé, quels éléments du dictionnaire des données sont rattachés à cet objet, puis ensuite l'analyse des DF entre ces éléments. Le tout sera ensuite formalisé dans un diagramme ou un graphe des DF.
3.1 La recherche des objets
Un objet est un élément du système d’information pourvu d’une existence propre, conforme aux règles de gestion de l’organisation. Le repérage des objets de gestion permet ensuite de faciliter la recherche des DF et la construction du diagramme des DF.
Exemple :
Les véhicules …. font l'objet d'un suivi dans des garages …
Ce texte fait apparaître 2 objets qui sont VEHICULE et GARAGE.
3.2 La recherche des dépendances fonctionnelles
Un objet est représenté par une donnée particulière : l’identifiant. Par définition, l’identifiant est en dépendance fonctionnelle avec toutes les autres propriétés de l’objet.
Repérer les objets du système d’information permet d’avancer très vite dans l’étude des dépendances fonctionnelles. La démarche consistera alors à partir du dictionnaire des données et du repérage des identifiants à rechercher les DF élémentaires et directes
Exemple :
Les véhicules sont repérés par leur numéro d'immatriculation et caractérisé par une couleur…
Le dictionnaire des données comprendra comme information Immat et couleur. Immat étant repéré comme un identifiant, on en déduira la DF Immat Couleur
3.3 La représentation des dépendances fonctionnelles
Cette représentation se fait à l'aide de deux outils qui sont la matrice ou le graphe des DF. Le graphe des DF permettant de mieux représenter les liens, et surtout les DF à partie gauche composée.
Exemple à partir d'une gestion de commande réduite (Matrice puis graphe des DF)
No Propriété
Signification
... ... ...
Analyse de dépendances et correction de réseaux de preuve
-
Introduction
Les fruits de Curry-Howard.
Depuis la mise en évidence via la correspondance de Curry-
Howard [21], des relations entre démonstrations mathématiques et programmes informatiques, théorie de la programmation et théorie de la démonstration s’enrichissent mutuellement. Parmi les nombreux allersretours fructueux entre preuves et programmes, la logique linéaire [13] tient une place exemplaire.
Girard a introduit le système F [11] alors qu’il travaillait sur l’arithmétique du second ordre. Ce système, redécouvert de manière indépendante par Reynolds [27], fournit un λ calcul polymorphe (ou λ-calcul du second-ordre).
Une quinzaine d’années plus tard, Girard mit en évidence la sémantique cohérente du système F [12] qui élabore sur la sémantique stable de Berry [2]. Les espaces cohérents ont conduit à la décomposition linéaire à l’origine de LLe [13] : A ⇒ B = ! A ( B. Cette décomposition linéaire, observée dans la sémantique du système F, se reflète syntaxiquement en un système de déduction bien structuré. S’est alors ouvert un champ original où se sont renouvelés les points de vue sur les preuves et les programmes.
Du côté logique, sont apparus les réseaux de preuve [13, 15, 7], les sémantiques interactives (géométrie de l’interaction, sémantique de jeux, ludique), les logiques polarisées [24], allégées et plus récemment différentielles [10].
Du côté programmation, l’étude de la linéarité a eu des conséquences sur de nombreux problèmes :
optimalité et partage [18, 22], interprétations calculatoires de la logique classique [14, 6, 24], systèmes de type fournissant des bornes de complexité [23], lien entre focalisation et langages logiques [1, interprétation logique du filtrage [28, 4].
De la logique linéaire aux réseaux de preuve.
La décomposition linéaire mentionnée plus haut
fait donc apparaître des connecteurs, dits exponentiels (!, ?), qui contrôler l’usage des hypothèses (via les règles structurelles de contraction et affaiblissement). Une conséquence importante du contrôle des règles structurelles réside dans le fait que les diverses présentations des inférences pour la conjonction et la disjonction, équivalentes en logique classique, ne le sont plus dans le cadre linéaire. On voit alors appraître deux disjonctions et deux conjonctions, deux constantes logiques pour le vrai et deux pour le faux, répartis en un groupe dit multiplicatif ( , ⊗, 1, ⊥) et un groupe additif (⊕, &, >, O0). La linéarité permet également de récupérer une négation involutive (A⊥⊥ = A) et les lois de de Morgan permettent alors de restreindre la négation aux formules atomiques tout en considérant des séquents dont toutes les formules sont à droite. LL possède une bonne notion de fragments logiques : on peut ainsi considérer le fragment restreint aux connecteurs multiplicatifs (avec ou sans les constantes) appelé MLL ou bien le fragment multiplicatif exponentiel, appelé MELL.
Les réseaux de preuve constituent l’une des innovations les plus originales de la logique linéaire.
Fondés de manière essentielle sur la linéarité, les réseaux de preuve constituent une syntaxe graphique pour les preuves constituant des objets de preuve très canoniques 1 et l’élimination des coupures y est particulièrement élégante.
L’élégance et la simplicité des réseaux sont particulièrement frappant dans le fragment multiplicatif et sans unités de la logique linéaire (MLL) sur lequel l’article va se concentrer. Il s’agit d’ailleurs plus d’une simplification de présentation qu’une véritable restriction puisque nos résultats s’étendent tous à MELL de manière directe, capturant ainsi le lambda-calcul typé.
Réseaux de preuve et correction logique.
Abandonnant une notation séquentielle au profit d’une représentation de la preuve comme un graphe, les réseaux de preuve s’éloignent de l’idée habituelle qu’on se fait d’une démonstration (typiquement un raisonnement qui se déroule progressivement, de manière ordonnée, de son point de départ jusqu’à sa conclusion, structuré par des lemmes intermédiaires).
L’une des conséquences de cette non-séquentialité est que s’ils contiennent des erreurs de raisonnement (ou paralogismes), celles-ci ne sont pas forcément faciles à détecter, contrairement à la plupart des systèmes de déduction (systèmes de Hilbert, déduction naturelle, calcul des séquents,) où la correction logique d’une preuve se vérfie de manière purement locale. On parlera de structure de preuve pour un objet qui ressemble à un réseau mais n’est pas forcément logiquement correct.
C’est le prix à payer pour avoir la syntaxe graphique et les bonnes propriétés des réseaux : on passe en effet d’objets inductifs (les arbres des preuves en calcul des séquents par exemple) à des objets de nature plus géométrique (les structures de preuve) dont les propriétés comme l’acyclicité ou la connexité ne sont plus locales mais sont globales.
Pourtant, les démonstrations sont avant tout (et même avant d’être des objets calculatoires !) des objets qui servent à se forger une conviction et à la transmettre. Reformulé en ces termes, le problème de la correction des structures de preuve se résume à ceci : si l’on communique à quelqu’un une structure de preuve R, il doit disposer des moyens pour être sûr que la structure est logiquement correct et qu’elle ne contient pas un raisonnement erroné 2. Il faudra éventuellement fournir à cette personne, en même temps qu’on lui communique la structure de preuve, un certificat de correction de cette structure de preuve 3.
On souhaite donc disposer de conditions sur les réseaux, a priori de nature graphique et géométrique, assurant de la correction des réseaux, c’est-à-dire qui permette de discriminer les réseaux de preuve qui sont logiquement corrects de ceux qui contiennent des erreurs de raisonnement.
C’est toute la problématique de la correction des réseaux de preuve auquel cet article se veut une contribution : nous proposons un nouveau critère particulièrement simple qui permet de déterminer si une structure de preuve représente bien une preuve. Notre critère simplifie un critère récemment publié par Mogbil et Naurois.
Organisation de l’article.
On commence par rappeler les bases de la logique linéaire et des réseaux de preuve. On rappelle le critère de correction de Danos et Régnier. On considère ensuite le critère
- Contrairement aux preuves du calcul des séquents qui contiennent beaucoup d’information non pertinente sur
l’ordonnancement des règles d’inférence.
- Ou encore, vu sous l’angle calculatoire, qu’il s’agit d’un programme bien typé
- L’idée la plus simple est bien sûr de transmettre une preuve séquentialisée de la structure R, mais on voit vite les limites de cette idée : non seulement parce qu’elle nous fait nous reposer sur le calcul des séquents mais aussi parce que le réseau qu’on souhaite transmettre peut résulter d’une élimination des coupures et dans ce cas on ne dispose pas forcément d’une version séquentialisée de la preuve.2
