• [^] # Re: Pourquoi du théorie des patch c'est bien

    Posté par . En réponse au journal Pijul, un nouveau gestionnaire de source. Évalué à 2.

    je considère un peu rapidement que les sommets d'un graphe et ses arêtes sont des ensembles

    Disons que la notion d'ensembles en mathématique est ambigüe (cf. le pardoxe de Russel), alors j'ai tendance à utiliser ce terme pour désigner les objets d'un modèle de la théorie des ensembles (ou les sommets d'un graphe qui est modèle de la théorie). Ce qu'il y a avec ZF (comme avec la théorie des catégories) est que l'on peut réflchir la métathéorie dans la théorie elle-même et aboutir à des théorèmes du style : si ZF est consistante alors elle a un modèle dénombrable (bien que le modèle en question possède des ensembles non dénombrables de son point de vue).

    Pour une présentation succincte de la théorie des catégories, il y a le cours Inititation à la théorie des catégories de Gérad Huet qui commence ainsi :

    Une catégorie C se compose d'objets et de flèches. On écrit A : C pour dire que A est un objet de C, et f : C(A,B) pour dire que f est une flèche de C reliant l'objet A à l'objet B. En général la catégorie dans laquelle on travail est sous-entendue, et on écrit plus simplement f : A -> B.

    Jusqu'ici, une catégorie est un graphe orienté dont les nœuds sont les objets et les arcs sont les flèches. Mais les catégories possèdent la structure minimale donnée par l'associativité de la composition des flèches. Les flèches doivent donc être vue comme les chemins du graphe, quotientés par l'égalité des flèches.

    Comme les notations ci-dessus te rappellerons celles utilisées pour les annotations de typage en OCaml, et que CAML signifie Categorical Abstract Machine Language (c'est la machine abstraite du bytecode OCaml), tu pourras aussi jeter un œil à De la déduction naturelle a la machine categorique :

    Le titre de cet article résume trois slogans :

    • La Déduction naturelle, c'est du lambda-calcul.
    • Le lambda-calcul, c'est la théorie des Catégories Cartésiennes Fermées.
    • La théorie des Catégories Cartésiennes Fermées, c'est du langage machine.

    On réalise ainsi le Programme de Constructivation des Mathématiques :

     preuve ----> programme ----> combinateur ---> code
intuitionniste fonctionnel catégorique exécutable

    Sinon, pour en revenir à pijul, j'ai eu une nouvelle idée pour présenter la notion de fusion dans ce système. Quand on a une relation reflexive et transitive (un préodre), on peut la voir comme une catégorie (en réalité ce sont les catégories ayant au plus une flèche entre deux objets). Prenons, par exemple, la catégorie dont les objets sont les entiers et la relation de préodre « être un multiple de ». Ainsi le schéma de fusion suivant :

    fusion

    peut se lire : A et B sont des mutliples de O (A = p * O et B = q * O) et M (M = r * A = s * B) est un multiple commun de A et B. Mais parmi tous les mutliples communs de A et B, il y en a un qui est plus petit que les autres : c'est lui la fusion !!! Ce qu'exprime ce diagramme :

    fusion parfaite

    si je prends un autre multiple F de A et B alors il est multiple de leur ppcm M.

    Cette notion, qui est une généralisation de la notion de borne supérieure (le plus petit des majorants si on y voit une relation d'ordre, le descendant minimal dans l'historique du dépôt) est ce que les catégoriciens appellent une somme amalgamée. Comme une telle somme n'existe pas toujours si on prend pour objets des fichiers, il faut prendre pour objets des digles.

    Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.