搜索元素在樹中伊莎貝爾

Question

我有這個功能測試羯羊元素是二叉樹或不：

fun lookup::"int⇒bst⇒bool" where 
"lookup x _ = false" | 
"lookup x bst = (if x = root(bst) then true else if x≤root(bst) then lookup x left(bst) else lookup x right(bst))" 

我得到錯誤信息 類型統一失敗： 衝突的類型「BST」和 「INT」

數據類型BST被定義爲

datatype bst = Leaf | Node int bst bst 

這裏有什麼問題？

Answer 1

它看起來像你的數據類型聲明沒有提及葉的任何關聯值。因此，它可能看起來像

datatype_new bst = Leaf int | Node int bst bst 

然後函數只檢查當前節點的所有構造函數：

fun lookup :: "int ⇒ bst ⇒ bool" where 
    "lookup x (Leaf y) = x = y" | 
    "lookup x (Node y leftbst rightbst) = 
     (if x = y then True 
     else (if x ≤ y then lookup x leftbst else lookup x rightbst))" 

Answer 2

簡短的回答是，你濫用root。這是NthRoot.root，從src/HOL/NthRoot.thy，並root該類型是在錯誤信息中顯示：

root :: nat => real => real 

我CNTL-點擊root，它帶我去功能NthRoot.thy。

從這裏，我基本上抱怨說，你讓我比我想要的更努力，回答你的問題，甚至現在，我假設我讓我變成了你正在談論的重複內容。

你在評論中給了我這句話：「進口主樹」。但是，在THY僅使用Main之後，THY顯然不是您正在做的，因爲我沒有收到錯誤消息Type unification failed: Clash of types "bst" and "nat"。

theory Scratch 
imports Main "~~/src/HOL/Library/Tree" 
begin 
datatype bst = Leaf | Node int bst bst 

fun lookup :: "int ⇒ bst ⇒ bool" where 
    "lookup x _ = false" | 
    "lookup x bst = (if x = root(bst) then true else if x ≤ root(bst) 
        then lookup x left(bst) else lookup x right(bst))"    
end 

此外，在THY中，root沒有定義，它是一個變量。我以兩種方式看到了這一點。我試圖讓CNTL點擊它，但什麼都沒發生。然後我注意到它是藍色的，這意味着它是一個局部變量。

因此，我導入了Complex_Main，如下所示，並且我收到了您所說的錯誤消息。我對二叉樹一無所知，但錯誤消息中顯示的root類型可以很快告訴您，root很可能不是您想要的，因爲它使用的是real。

theory Scratch2 
imports Complex_Main 
begin 
datatype bst = Leaf | Node int bst bst 

fun lookup :: "int => bst => bool" where 
    "lookup x _ = false" | 
    "lookup x bst = (if x = root(bst) then true else if x ≤ root(bst) 
        then lookup x left(bst) else lookup x right(bst))" 
(*Type unification failed: Clash of types "bst" and "nat" 

    Type error in application: incompatible operand type 

    Operator: root :: nat => real => real*) 
end 

無論如何，人們不想看到太多的問題來源，他們不想看到太少。如果你提供魔術數量，而他們所要做的只是剪切和粘貼，那麼他們不需要努力回答你的問題。

從你上一個問題，Predefined functions for Binary trees in Isabelle，我知道從Andreas說什麼Tree。

安德烈亞斯是像我和你這樣的人的答案。如果你想增加像他這樣的人回答問題的機會，那麼你希望他必須儘可能少地工作以找出你的問題。

一個最簡單的工作示例可以幫助確保每個人都在同一頁面上，甚至在提出問題之前在您的結尾處發現一些錯誤。