邏輯程式語的單一化
Unification：A Multidisciplinary Survey

單一化的問題在電腦科學的許多相關領域中皆有出現，包括：定理證明 (theorem proving)，邏輯程式 (logic programming)，及自然語言處理 (natural language processing)。在此篇論文中許多與單一化有關的演算法與資料結構都被提出討論，然而在此我們將著重於與邏輯程式語言相關的部份做一簡單的介紹。

首先介紹何謂單一化問題：對於含有變數的兩個語辭(terms)，是否有一適當的替代使得這兩個語辭變得相同？舉例來說：對於f(x, y) 及f(g(y, a), h(a))這兩個語辭來說，如果讓x以g(h(a),a)替代，y以h(a)替代，則這兩個語辭將變得相同，即：f(g(h(a), a), h(a))。

而在Prolog語言中何處會用到單一化呢？底下舉一個例子：

• like(mary, food).
• like(mary, wine).
• likes(john, wine).
• likes(john, mary).
• ？- likes(mary, X), likes(john, X).

如何找到 X 同時滿足 likes(mary, X) 及 likes(john, X) 就需要單一化來解決。

因此單一化在邏輯程式語言這個領域來說就有幾個方向可以研究：

1. Occur check：程式中如果包含了occur check，則替代語辭不可為無窮長，這樣會增加程式的正確性，但卻會使得程式執行效率變差。
2. Backtracking：好的backtracking方法可增加單一化的執行效率。
3. Concurrent programming and parallel execution：此為研究單一化在多處理機系統的執行效率問題。

更詳細的內容可參閱參考文獻。

<¤W¤@­¶>                                                                                     <¦^¥D­¶>                                                                                             <¤U¤@­¶>