matita/matita/projdat/hypergraph.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "projdat/database.ma".
  16
  17 definition eqbD ≝ λD:DeqSet.λa,b:D. eqb D a b.
  18
  19 let rec nomismatch_id (A,B:DeqSet) (l:DeqList (DeqProd A B)) on l ≝
  20   match l with
  21   [ nil ⇒ true
  22   | cons a b ⇒ andb (notb (exists ? (λp. andb (eqbD A (fst ?? a) (fst ?? p))
  23                                               (notb (eqbD ? (snd ?? a) (snd ?? p))))
  24                                   l))
  25                     (nomismatch_id A B b)].
  26
  27
  28 (* Definizione dell'insieme degli archi *)
  29 record HyperEdge (Tlabelmap: DeqList DeqType) (Tvaluemap: DeqList DeqCoer)  : Type[0] ≝ {
  30   Hid    : ℕ;
  31   Hids   : DeqList DeqNat;                    (* Lista di id dei valori *)
  32   HTids  : DeqList DeqNat;                    (* Lista di id dei tipi   *)
  33   HLen   : (length ? Hids)=(length ? HTids);  (* Le tabelle hanno stessa lunghezza *)
  34   HPTypes: (getSchema (selection  Hids  ? Tvaluemap))=
  35            (selection HTids  ? Tlabelmap);
  36            (* Impongo che agli identificativi di valori corrispondano gli stessi
  37               tipi *)
  38   Htuple : tuple (getSchema (selection Hids  ? Tvaluemap))
  39 }.
  40
  41 (* XXX: riscrivibile come Σ-Type *)
  42 (* Definizione dell'insieme degli archi *)
  43 record HyperEdge_SET (Tlabelmap: DeqList DeqType) (Tvaluemap: DeqList DeqCoer)
  44                      (HSet: list (HyperEdge Tlabelmap Tvaluemap)) : Type[0] ≝ {
  45
  46   (* XXX: Controllo che ad uno stesso ID corrisponda un unico schema. Garantisce
  47   l'unicità degli schemi per quello stesso ID ad ogni arco *)
  48   CheckID_to_Schema: nomismatch_id ?? (map ? ( (DeqProd DeqNat (DeqList DeqType)))
  49                               (λx. 〈(Hid ?? x), (selection  (HTids ?? x)?  Tlabelmap)〉)
  50                               HSet)
  51                                =true
  52
  53 }.
  54
  55 (*
  56 definition is_HyperEdge_SET ≝
  57  (λTlabelmap: DeqList DeqType) (λTvaluemap: DeqList DeqCoer)
  58  (λHSet: list (HyperEdge Tlabelmap Tvaluemap)).
  59   nomismatch_id ?? (map ? ( (DeqProd DeqNat (DeqList DeqType)))
  60      (λx. 〈(Hid ?? x), (selection  (HTids ?? x)?  Tlabelmap)〉)  HSet).
  61 *)
  62
  63 (* Definizione dell'ipergrafo *)
  64 record HyperGraph (Tlabelmap : DeqList DeqType) (Nodes : DeqList DeqCoer) : Type[0] ≝ {
  65    GSet: list (HyperEdge Tlabelmap Nodes);
  66     (* Lista delle associazioni di tipo *)
  67     (* Lista delle associazioni di valore *)
  68    Edges  : HyperEdge_SET Tlabelmap Nodes GSet
  69 }.