Efficient Full Higher-Order Unification

[sazare]

https://arxiv.org/abs/2011.09507 by PETAR VUKMIROVIC ́, ALEXANDER BENTKAMP, AND VISA NUMMELIN

高階のユニフィケーションの高速化だそうだ。 面白そう

unificationだけ速いといっても、代入とかそれを使うシステムがちゃんと高速になることが大切な気がする。どうなっているのか。

[sazare]

読破力がたりないので、読み終われない。 ふと思ったのだが、高階のunificationは、新しい述語、例えばMを導入して X(y)を、M(X,y)という対応で一階に翻訳できるのでないか？ 関数についても、mという関数記号を導入して、 v(x)を、m(v,x)という対応を作って翻訳して、このように翻訳された式で一階のunification すればよいはず。 このとき、unificationは一階なので処理量は変わらない？ 変わるとしたら、この翻訳の処理分だが、それは元の式に対して定数のオーダーであろうかと思う。

[sazare]

関数変数へλ式の代入があったりして、もともとの表現にないものが出てくるのが違いみたい。 それは、λ計算システムの上でのunificationであるなあ。 意味論がはいってるのは、許容されるのか。 前の論文から読まないとついていけないのかも。