Algebraic property graphの定義
221日前、と聞くとずいぶん昔のようにも感じますが、Algebraic property graphについて書いています。とはいえ見直してみると具体的な中身にはあまり言及していないみたいなので、踏み込んでみます。
論文については上記の記事からもリンクを貼っていて誰でも見られるので参照いただければと思います。
Algebraic property graphを端的にイメージするためには上の可換図式がよいかと思います。上記、それぞれの頂点は集合で、矢印は写像です。
• a set 𝐺(L), the members of which we call the labels of 𝐺; and,
• a set 𝐺(T), the members of which we call the types of 𝐺. Each type 𝑡 is a term in the grammar: 𝑡 ::= 0 | 1 | 𝑡1 + 𝑡2 | 𝑡1 × 𝑡2 | Prim 𝑝 (𝑝 ∈ P) | Lbl 𝑙 (𝑙 ∈ 𝐺 (L)) where we may omit writing Prim and Lbl when they are clear from the context; and,
• a set 𝐺 (E), the members of which we call the elements10 of 𝐺; and,
• a set 𝐺 (V), the members of which we call the (typed) values11 of 𝐺. Values are terms in the (typed) grammar: 𝑣:𝑡 ::= ():1|inl𝑡2(𝑣:𝑡1):𝑡1+𝑡2 |inr𝑡1(𝑣:𝑡2):𝑡1+𝑡2 | (𝑣1,𝑣2) :𝑡1 ×𝑡2 |Prim𝑣𝑡:𝑡 (𝑡∈P,𝑣∈V(𝑡)) |Elmt𝑒:𝐺(𝝀)(𝑒) (𝑒∈𝐺(E)) where we will omit type information, and Prim and Elmt, from values when they can be inferred from context; and,
論文の文面をうまく持ってくることができず申し訳ないですが、L、T、E、Vの４つの集合があり、それぞれLabel、Type、Element、Valueの集合です。ざっくりいうとLabelとTypeは「スキーマ」側です。一方でElementとValueは「インスタンス」側ですね。
LabelとTypeは何が違うのか。まずTypeは、元になる「プリミティブ」の集合と、あとは0と1という2つの型しか持っていません。その代わり、それらは代数的データ型を作ることができます。
そしてLabelはそれを指し示す「型の名前」ですね。同じ1でも、それぞれ違うLabelをつけることができます。別の言い方をすると、structural typingではなくてnominal typingなわけですね。実際の例でも、他のプログラミング言語だとenumにあたるものを作るときにそれぞれの要素に別のLabelが与えられています。
ElementとValueの関係は、雑にいうと、変数と値だと思うと楽かもです。
定義には上記の４つの集合を結ぶ写像も定義されていますが、要するにそれらが可換であることが定義に含まれています。
𝐺(𝝉)◦𝐺(𝝊) =𝐺(𝝈)◦𝐺(𝝀)
ということで、これを使って多様なグラフ構造を型を付けた状態で表現できる、しかもそれらのグラフ同士の演算が定義でき、Algebraic property graph全体が圏とみなせるという話につながっていきますが、長くなりそうなのでいったんここまで。
