なろーいんぐ

http://www.jaist.ac.jp/library/thesis/is-master-1997/abstract/matsuno/jabstract.pdf
によると、E-単一化問題を解くのがnarrowingと書いてあるけど、なんでE-単一化と呼ばないのか

Higher-Order Equational Logic
面白いな〜。Basic Narrowingとかは、多分first-orderの問題しか扱えないので、mapとかくると弱い気がする。高階関数をinline展開して一階に持ち込める場合もあると思うけど。例としてあがってた

father(mary) = john
father(john) = art

から、F(mary)=artの解Fを求めるとかいうのは、結構印象的。こういうのはPrologでは書けない(多分)。あと、微分は適切な関係式を与えておくと、
\x->diff(\y->ln(F(y)) , x)=\x->cos(x)/sin(x)
の解Fが見つけれるとか。数式処理で便利かもしれんな〜