Поиск элемента в дереве в Isabelle

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))" 

Я получаю сообщение об ошибке Тип объединения не удалась: Clash типов «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, который дублирует то, о чем вы говорите.

Вы дали мне эту фразу в своем комментарии: «импортирует главное дерево». Однако после создания 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 

Кроме того, в этом Авиалиний, 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, я знал, где взять Tree от того, что сказал Андреас.

Андреас - это человек ответа для таких людей, как я и ты. Если вы хотите увеличить вероятность того, что кто-то вроде него отвечает на вопросы, тогда вы хотите, чтобы он работал как можно меньше, чтобы выяснить свой вопрос.

Минимальный рабочий пример может помочь убедиться, что все находятся на одной странице и даже поймают некоторые ошибки на вашем конце, прежде чем задавать вопрос.