hl: ハイパーリンクを含む初期状態の同型性判定関連のバグ

[seelx3]

次の LMNtal コードで問題を再現できる。

% init. init :-

a(!L0), b(!L0).

rule_1@@
a(!L), b(!L) :- a, b.

rule_2@@
a, b :- a(!L), b(!L).

• 1 行目 有効時
  • init, a(!H23), b(!H23), a, b の 3 つの状態が得られる。
  • 振る舞いとしては正しいが、無駄な記述は省略したい。
• 1 行目 無効時
  • a(!H23), b(!H23), a, b の 2 つの状態が得られるべきであるが、a(!H23), b(!H23), a, b, a(!H23), b(!H23) の 3 つの状態が確認できる。
  • つまり、 a(!H23), b(!H23) の状態が 2 つ存在してしまっている。
  • LaViT StateViewer で下図のような状態遷移図が得られる。青色と緑色の表す状態は同じ状態である。
  • 

[seelx3]

• 原因
  • 初期状態において, ハイパーリンクに所属するアトム数が不正。(2であるべきだが, 4となっている)
  • 状態展開後は, 正しく, 所属アトム数が2となっている。
  • これにより, 同一状態でも,ハッシュ関数が異なるハッシュ値を返す.
  • 膜(状態)のハッシュ値計算では, アトム起点でリンクをD回(depth=D)たどり, リンク属性に応じたハッシュ値を乗算したり加算したりする.
  • 現在, ハイパーリンクのハッシュ値は, 同一ハイパーリンクに所属するアトムの数としている. (らしい)
  • 以上より, 初期状態がハイパーリンクを持つ場合, 適切に所属アトムの数がカウントされず, 同一状態から異なるハッシュ値が産まれる.
  • ハッシュテーブルは, 異なる状態のハッシュ値が一致することは「ハッシュ衝突」として想定するが, 同一状態から異なるハッシュ値が産まれることは想定していない。このため、等価な状態が異なる状態として扱われることになる。

• 対処方法

  • ファイル名: src/verifier/mc.cpp
  • 関数名: do_mc
  • world_mem_org->copy() を world_mem_org->copy_ex() に変更する.
  • 両者の違いは、よく知らないけど、membraneクラスにて、ハイパーリンクを考えないコピー関数 or 考えるっぽいコピー関数 に分岐してる。

  (gocho さんの日誌より引用)