高階統一

我正在研究一個更高階的定理證明器，其中統一似乎是最困難的子問題。高階統一

如果Huet的算法仍然被認爲是最先進的，那麼是否有人有解釋它的任何鏈接，這些鏈接被程序員而不是數學家所理解？

甚至任何它在哪裏工作的例子和通常的一階算法都沒有？藝術—的

2009-12-20 rwallace

狀態不錯，所以據我所知，所有的算法或多或少採取相同的形狀，休特的（按照邏輯程序設計的理論，雖然我的專長是切線）提供你需要完整的高階匹配：子問題如高階匹配（統一一個術語被關閉）和Dale Miller的模式演算是可判定的。

請注意，Huet的算法在下列意義上是最好的—它就像是一個半決策算法，因爲如果它們存在，它將找到統一者，但如果它們不存在則不保證終止。既然我們知道高階統一（事實上，二階統一）是不可判定的，你不能做得比這更好。

解釋：Conal Elliott的博士論文前四章Extensions and Applications of Higher-Order Unification應該符合法案。這部分重達近80頁，有一些密集型理論，但它的動機很好，而且是我見過的最易讀的賬戶。例如：Huet的算法會爲這個例子提供商品：[X（o），Y（succ（0））];這必然會困擾一階統一算法。

來源

2009-12-23 22:44:32

其中一個真正好（不可谷歌或難以谷歌）問題的罕見情況被問及難以得到，高質量的答案給出了。 – 2009-12-24 13:12:16

+1對你們兩個 - 大聲笑這可能是爲什麼你的統計是300-600而不是31.2K或類似的東西。你可能只回答很少有人能回答的問題。 – 2009-12-24 13:14:04

您引用的確切的Conal Elliott提供了另一個答案： - D. – Blaisorblade 2014-05-18 23:11:58

高階統一（真正的二階匹配）的一個例子是：f 3 == 3 + 3，其中==是模阿爾法，貝塔和eta轉換（但沒有給「+」賦予任何意義）。有四種解決方案：

相比之下，一階統一/匹配不會給出解決方案。與人道主義組織（高階抽象語法），用於編碼具有可變的語言，同時避免變量捕捉的複雜性結合時

侯是非常方便等

我第一次接觸到的題目是紙「證明和由Gerard Huet和Bernard Lang應用程序變換用二階模式表示。我記得，這篇論文是「寫給程序員理解的」。一旦你理解了二階匹配，HOU並沒有太多進展。 Huet的一個關鍵結果是靈活/靈活的情況（變量作爲一個術語的頭部，而唯一的情況不會出現在匹配中）總是可以解決的。

來源

2010-03-23 23:19:44 Conal

我很確定這些算法是否適用於「漏洞」。假設我有T == \ f \ x。（f x）= x + x。然後（T_），即具有f的「孔」的原始T具有\ x的形式。（_ x）= x + x。但是由於捕獲規則，現在還有一個側面約束，現在x不應該出現在_中，所以唯一的解決方案是_ = \ y.y + y而不是\ y.y + x，\ y.x + y，\ y.x + x。 DId沒有找到一篇文章，卻沒有顯示出這樣的「漏洞」。 – 2015-02-03 15:22:43

我會在自動推理手冊第2卷的章節中添加一章。本章可能是更易於初學者訪問，並以λΠ演算結束，其中 Conal Elliott論文開始。

預印本在這裏找到：

高階統一和匹配
吉爾斯Dowek，2001年
http://www.lsv.fr/~dowek/Publi/unification.ps

Conal埃利奧特紙更正式和concerntrated的一個變體，也在最後引入了一個λΠΣ演算，除了產品類型之外，它還總結了。

再見

來源

2015-02-05 08:54:51

還有託拜厄斯尼普科夫1993年紙Functional Unification of Higher-Order Patterns（僅11頁，其中4是參考書目和代碼附錄）。摘要：

一個統一算法的全面發展爲所謂高階模式的$ \ $拉姆達一組術語子類，給出。起點是一個通過轉換的統一公式化，結果是一個直接可執行的功能程序。在最後的開發步驟中，結果適用於de Bruijn表示法中的$ \ lambda $ -terms。這些算法適用於簡單類型和無類型的術語。

來源

2016-06-07 20:00:04 Nathan

回答

相關問題