エイプリールではないユニフィケーションをしてる話

とくに嘘なネタはないので書いてません。面白くなくて申し訳ないんですけど。

ここのところ日記の更新出来てません。
型推論の基本はパターンマッチングとユニフィケーションです。
実はパターンマッチングは理解していたのだけど、ユニフィケーションは理解していなかったので、最近よく使っているPHPでunifyを書いてみてます。

参考: http://www.gesource.jp/weblog/?p=654

パターンマッチングは片方の式にだけ変数を入れる事が出来ます。
対してユニフィケーションでは、マッチする式の両方に変数が入れられます。

ここが大きく異なるところです。

そして、変数から変数への伝搬も起こる事があり得ます。
ここらへんの実装が難しいところのようです。

教科書的な説明が出来るといいんですけど、まだ全然出来てないので他のソースもいくつか読んで、サクっと作れるようになろうと思っています。

なんとなくは、分かるんですよ。Scalaのコードも読んだりはしてるし、何となく分かる。でも、完全に分かりたい。それにはまだ時間がかかりそうです。

まず、パターンマッチが出来て、それをユニフィケーション出来るように拡張していく。で、問題あるので対策した結果、ちゃんとうまく行くようになる。で、効率が悪いとか、immutableな環境で計算する為に、substとか使う。とかいう発展させていくというストーリーが欲しいのでそれを作れて、ダダダダダっとキーボード打ちまくって、実装出来るようになれれば、きっと本当に理解していると言えると思うので、とにかく何回も作ってみようと思ってます。

<?php
class unify {
  static $vars = array();
  static $buf1 = array();
  static $buf2 = array();
  static function apply($str1, $str2) {
    self::$vars = array();
    echo $str1."\n";
    echo $str2."\n";

    // 各々トークンに分ける
    self::$buf1 = preg_split("/\\s/", $str1);
    self::$buf2 = preg_split("/\\s/", $str2);

    // 数が異なったら失敗
    if (count(self::$buf1) != count(self::$buf2)) {
      return false;
    }
    foreach (self::$buf1 as $i => $b1) {
      if (!self::t_match($b1, self::$buf2[$i]))  return false;
    }
    var_export(self::$vars);
    return true;
  }

  static function t_match($t1, $t2) {
    if ($t1 == $t2) return true;
    if (is_var($a) && !is_var($b)) return self::var_match($a, $b);
    if (is_var($b)) return self::var_match($b, $a);
    if (is_var($a)) return self::var_match($a, $b);
    return false;
  }

  static function var_match($vt, $t) {
    if (isset(self::$vars[$vt])) return ($t == self::$vars[$vt]);
    self::replace_buf($vt, $t);
    if (in_array($vt, self::$vars)) self::replace_vars($vt, $t);
    self::$vars[$vt] = $t;
    return true;
  }

  static function replace_buf($s, $d) {
    foreach (self::$buf1 as &$b) if ($s == $b) $b = $d;
    foreach (self::$buf2 as &$b) if ($s == $b) $b = $d;
  }

  static function replace_vars($s, $d) {
    foreach (self::$vars as $k => $v) if ($s == $v) self::$vars[$k] = $d;
  }
}
function unify($a, $b) {
  return unify::apply($a, $b);
}
function is_var($str) {
  return substr($str,0,1)=="?";
}

function p($str) {
  var_export($str);
  echo "\n";
}

p(unify("Takayuki", "Takayuki"));
p(unify("Takayuki", "Takoyuki"));
p(unify("?x am Takayuki", "I am Takayuki"));
p(unify("?x is ?x", "a is b"));
p(unify("?x is ?x", "a is a"));
p(unify("?x is a", "b is ?y"));
p(unify("?x is a", "?y is ?x"));