Как я могу установить биекцию между деревом и его обходом?

Question

Я смотрел на то, как inorder + preorder создает уникальное двоичное дерево? и подумал, что было бы интересно написать формальное доказательство этого в Идрисе. К сожалению, я застрял довольно рано, пытаясь доказать, что способы найти элемент в дереве соответствуют способам его поиска в обходе по порядку (конечно, мне также нужно сделать это для обхода по предзаказу), Любые идеи будут приветствоваться. Меня не особенно интересует полное решение - больше просто помочь начать работу в правильном направлении.

Дано

data Tree a = Tip
            | Node (Tree a) a (Tree a)

Я могу преобразовать его в список по крайней мере двумя способами:

inorder : Tree a -> List a
inorder Tip = []
inorder (Node l v r) = inorder l ++ [v] ++ inorder r

или же

foldrTree : (a -> b -> b) -> b -> Tree a -> b
foldrTree c n Tip = n
foldrTree c n (Node l v r) = foldr c (v `c` foldrTree c n r) l
inorder = foldrTree (::) []

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

data InTree : a -> Tree a -> Type where
  AtRoot : x `InTree` Node l x r
  OnLeft : x `InTree` l -> x `InTree` Node l v r
  OnRight : x `InTree` r -> x `InTree` Node l v r

Это довольно легко (используя первое определение inorder) написать

inTreeThenInorder : {x : a} -> (t : Tree a) -> x `InTree` t -> x `Elem` inorder t

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

Также не очень сложно написать версию

inorderThenInTree : x `Elem` inorder t -> x `InTree` t

К сожалению, я до сих пор не нашел способа написать версию inorderThenInTree что я смог доказать обратное inTreeThenInorder, Единственный, который я придумал, использует

listSplit : x `Elem` xs ++ ys -> Either (x `Elem` xs) (x `Elem` ys)

и я столкнулся с проблемой, пытаясь вернуться туда.

Несколько общих идей, которые я попробовал:

1. С помощью Vect вместо List чтобы было проще разобраться, что слева, а что справа. Я увяз в "зеленой слизи" этого.

2. Играя с вращениями деревьев, доходя до того, чтобы доказать, что вращение в корне дерева приводит к обоснованному отношению. (Я не играл с вращениями ниже, потому что я никогда не мог найти способ использовать что-либо об этих вращениях).

3. Попытка украсить узлы дерева информацией о том, как их достичь. Я не потратил много времени на это, потому что не мог придумать способ выразить что-то интересное с помощью этого подхода.

4. Попытка построить доказательство того, что мы возвращаемся к тому, с чего начали, создавая функцию, которая делает это. Это стало довольно грязно, и я застрял где-то.

Answer 1

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

Это соответствующая строка из моей реализации

inTreeThenInorder x (branch y l r) e with listSplit x (inOrder l) (y ∷ inOrder r) e

Вот полная реализация. Я включил его в качестве внешней ссылки, чтобы избежать нежелательных спойлеров, а также воспользоваться замечательным HTML-выводом Agda с гиперссылкой и выделенным синтаксисом.

http://www.galois.com/~emertens/agda-tree-inorder-elem/TreeElem.html

Answer 2

Я написал inorderToFro а также inorderFroTo и связанные леммы в Идрисе. Вот ссылка.

Я могу сделать пару замечаний относительно вашего решения (не вдаваясь в подробности):

Первый, splitMiddle не действительно нужно. Если вы используете более общий Right p = listSplit xs ys loc -> elemAppend xs ys p = loc тип для splitRight, то это может покрыть ту же землю.

Во-вторых, вы могли бы использовать больше with шаблоны вместо явных _lem функции; Я думаю, что это будет яснее и лаконичнее.

В-третьих, вы делаете значительную работу, доказывая splitLeft и Часто имеет смысл перемещать свойства функции внутри функции. Итак, вместо того, чтобы писать listSplit и доказательства о его результате отдельно, мы можем изменить listSplit вернуть необходимые доказательства. Это часто проще реализовать. В своем решении я использовал следующие типы:

data SplitRes : (x : a) -> (xs, ys : List a) -> (e : Elem x (xs ++ ys)) -> Type where
  SLeft  : (e' : Elem x xs) -> e' ++^ ys = e -> SplitRes x xs ys e
  SRight : (e' : Elem x ys) -> xs ^++ e' = e -> SplitRes x xs ys e

listSplit : (xs, ys : List a) -> (e : Elem x (xs ++ ys)) -> SplitRes x xs ys e

Я мог бы также использовать Either (e' : Elem x xs ** (e' ++^ ys = e)) (e' : Elem x ys ** (xs ^++ e' = e)) вместо SplitRes, Тем не менее, я столкнулся с проблемами с Either, Мне кажется, что объединение высшего порядка в Идрисе слишком шатко; Я не мог понять, почему мой unsplitLeft функция не будет проверять с Either, SplitRes не содержит функций в своем типе, поэтому я думаю, поэтому он работает более плавно.

В общем, сейчас я рекомендую Agda over Idris для написания таких доказательств. Это проверяет намного быстрее, и это намного более надежно и удобно. Я очень удивлен, что вам удалось написать так много Идриса здесь и для другого вопроса о обходах деревьев.

Answer 3

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

module PreIn
import Data.List
%default total

data Tree : Type -> Type where
  Tip : Tree a
  Node : (l : Tree a) -> (v : a) -> (r : Tree a) -> Tree a
%name Tree t, u

data InTree : a -> Tree a -> Type where
  AtRoot : x `InTree` (Node l x r)
  OnLeft : x `InTree` l -> x `InTree` (Node l v r)
  OnRight : x `InTree` r -> x `InTree` (Node l v r)

onLeftInjective : OnLeft p = OnLeft q -> p = q
onLeftInjective Refl = Refl

onRightInjective : OnRight p = OnRight q -> p = q
onRightInjective Refl = Refl

noDups : Tree a -> Type
noDups t = (x : a) -> (here, there : x `InTree` t) -> here = there

noDupsList : List a -> Type
noDupsList xs = (x : a) -> (here, there : x `Elem` xs) -> here = there

inorder : Tree a -> List a
inorder Tip = []
inorder (Node l v r) = inorder l ++ [v] ++ inorder r

rotateInorder : (ll : Tree a) ->
                (vl : a) ->
                (rl : Tree a) ->
                (v : a) ->
                (r : Tree a) ->
                inorder (Node (Node ll vl rl) v r) = inorder (Node ll vl (Node rl v r))
rotateInorder ll vl rl v r =
   rewrite appendAssociative (vl :: inorder rl) [v] (inorder r)
   in rewrite sym $ appendAssociative (inorder rl) [v] (inorder r)
   in rewrite appendAssociative (inorder ll) (vl :: inorder rl) (v :: inorder r)
   in Refl


instance Uninhabited (Here = There y) where
  uninhabited Refl impossible

instance Uninhabited (x `InTree` Tip) where
  uninhabited AtRoot impossible

elemAppend : {x : a} -> (ys,xs : List a) -> x `Elem` xs -> x `Elem` (ys ++ xs)
elemAppend [] xs xInxs = xInxs
elemAppend (y :: ys) xs xInxs = There (elemAppend ys xs xInxs)

appendElem : {x : a} -> (xs,ys : List a) -> x `Elem` xs -> x `Elem` (xs ++ ys)
appendElem (x :: zs) ys Here = Here
appendElem (y :: zs) ys (There pr) = There (appendElem zs ys pr)

tThenInorder : {x : a} -> (t : Tree a) -> x `InTree` t -> x `Elem` inorder t
tThenInorder (Node l x r) AtRoot = elemAppend _ _ Here
tThenInorder (Node l v r) (OnLeft pr) = appendElem _ _ (tThenInorder _ pr)
tThenInorder (Node l v r) (OnRight pr) = elemAppend _ _ (There (tThenInorder _ pr))

listSplit_lem : (x,z : a) -> (xs,ys:List a) -> Either (x `Elem` xs) (x `Elem` ys)
  -> Either (x `Elem` (z :: xs)) (x `Elem` ys)
listSplit_lem x z xs ys (Left prf) = Left (There prf)
listSplit_lem x z xs ys (Right prf) = Right prf


listSplit : {x : a} -> (xs,ys : List a) -> x `Elem` (xs ++ ys) -> Either (x `Elem` xs) (x `Elem` ys)
listSplit [] ys xelem = Right xelem
listSplit (z :: xs) ys Here = Left Here
listSplit {x} (z :: xs) ys (There pr) = listSplit_lem x z xs ys (listSplit xs ys pr)

mutual
  inorderThenT : {x : a} -> (t : Tree a) -> x `Elem` inorder t -> InTree x t
  inorderThenT Tip xInL = absurd xInL
  inorderThenT {x} (Node l v r) xInL = inorderThenT_lem x l v r xInL (listSplit (inorder l) (v :: inorder r) xInL)

  inorderThenT_lem : (x : a) ->
                     (l : Tree a) -> (v : a) -> (r : Tree a) ->
                     x `Elem` inorder (Node l v r) ->
                     Either (x `Elem` inorder l) (x `Elem` (v :: inorder r)) ->
                     InTree x (Node l v r)
  inorderThenT_lem x l v r xInL (Left locl) = OnLeft (inorderThenT l locl)
  inorderThenT_lem x l x r xInL (Right Here) = AtRoot
  inorderThenT_lem x l v r xInL (Right (There locr)) = OnRight (inorderThenT r locr)

unsplitRight : {x : a} -> (e : x `Elem` ys) -> listSplit xs ys (elemAppend xs ys e) = Right e
unsplitRight {xs = []} e = Refl
unsplitRight {xs = (x :: xs)} e = rewrite unsplitRight {xs} e in Refl

unsplitLeft : {x : a} -> (e : x `Elem` xs) -> listSplit xs ys (appendElem xs ys e) = Left e
unsplitLeft {xs = []} Here impossible
unsplitLeft {xs = (x :: xs)} Here = Refl
unsplitLeft {xs = (x :: xs)} {ys} (There pr) =
  rewrite unsplitLeft {xs} {ys} pr in Refl

splitLeft_lem1 : (Left (There w) = listSplit_lem x y xs ys (listSplit xs ys z)) ->
                 (Left w = listSplit xs ys z) 

splitLeft_lem1 {w} {xs} {ys} {z} prf with (listSplit xs ys z)
  splitLeft_lem1 {w}  Refl | (Left w) = Refl
  splitLeft_lem1 {w}  Refl | (Right s) impossible

splitLeft_lem2 : Left Here = listSplit_lem x x xs ys (listSplit xs ys z) -> Void
splitLeft_lem2 {x} {xs} {ys} {z} prf with (listSplit xs ys z)
  splitLeft_lem2 {x = x} {xs = xs} {ys = ys} {z = z} Refl | (Left y) impossible
  splitLeft_lem2 {x = x} {xs = xs} {ys = ys} {z = z} Refl | (Right y) impossible

splitLeft : {x : a} -> (xs,ys : List a) ->
            (loc : x `Elem` (xs ++ ys)) ->
            Left e = listSplit {x} xs ys loc ->
            appendElem {x} xs ys e = loc
splitLeft {e} [] ys loc prf = absurd e
splitLeft (x :: xs) ys Here prf = rewrite leftInjective prf in Refl
splitLeft {e = Here} (x :: xs) ys (There z) prf = absurd (splitLeft_lem2 prf)
splitLeft {e = (There w)} (y :: xs) ys (There z) prf =
  cong $ splitLeft xs ys z (splitLeft_lem1 prf)

splitMiddle_lem3 : Right Here = listSplit_lem y x xs (y :: ys) (listSplit xs (y :: ys) z) ->
                   Right Here = listSplit xs (y :: ys) z

splitMiddle_lem3 {y} {x} {xs} {ys} {z} prf with (listSplit xs (y :: ys) z)
  splitMiddle_lem3 {y = y} {x = x} {xs = xs} {ys = ys} {z = z} Refl | (Left w) impossible
  splitMiddle_lem3 {y = y} {x = x} {xs = xs} {ys = ys} {z = z} prf | (Right w) =
    cong $ rightInjective prf  -- This funny dance strips the Rights off and then puts them
                               -- back on so as to change type.


splitMiddle_lem2 : Right Here = listSplit xs (y :: ys) pl ->
                   elemAppend xs (y :: ys) Here = pl

splitMiddle_lem2 {xs} {y} {ys} {pl} prf with (listSplit xs (y :: ys) pl) proof prpr
  splitMiddle_lem2 {xs = xs} {y = y} {ys = ys} {pl = pl} Refl | (Left loc) impossible
  splitMiddle_lem2 {xs = []} {y = y} {ys = ys} {pl = pl} Refl | (Right Here) = rightInjective prpr
  splitMiddle_lem2 {xs = (x :: xs)} {y = x} {ys = ys} {pl = Here} prf | (Right Here) = (\Refl impossible) prpr
  splitMiddle_lem2 {xs = (x :: xs)} {y = y} {ys = ys} {pl = (There z)} prf | (Right Here) =
    cong $ splitMiddle_lem2 {xs} {y} {ys} {pl = z} (splitMiddle_lem3 prpr)

splitMiddle_lem1 : Right Here = listSplit_lem y x xs (y :: ys) (listSplit xs (y :: ys) pl) ->
                   elemAppend xs (y :: ys) Here = pl

splitMiddle_lem1 {y} {x} {xs} {ys} {pl} prf with (listSplit xs (y :: ys) pl) proof prpr
  splitMiddle_lem1 {y = y} {x = x} {xs = xs} {ys = ys} {pl = pl} Refl | (Left z) impossible
  splitMiddle_lem1 {y = y} {x = x} {xs = xs} {ys = ys} {pl = pl} Refl | (Right Here) = splitMiddle_lem2 prpr

splitMiddle : Right Here = listSplit xs (y::ys) loc ->
              elemAppend xs (y::ys) Here = loc

splitMiddle {xs = []} prf = rightInjective prf
splitMiddle {xs = (x :: xs)} {loc = Here} Refl impossible
splitMiddle {xs = (x :: xs)} {loc = (There y)} prf = cong $ splitMiddle_lem1 prf

splitRight_lem1 : Right (There pl) = listSplit (q :: xs) (y :: ys) (There z) ->
                  Right (There pl) = listSplit xs (y :: ys) z

splitRight_lem1 {xs} {ys} {y} {z} prf with (listSplit xs (y :: ys) z)
  splitRight_lem1 {xs = xs} {ys = ys} {y = y} {z = z} Refl | (Left x) impossible
  splitRight_lem1 {xs = xs} {ys = ys} {y = y} {z = z} prf | (Right x) =
    cong $ rightInjective prf  -- Type dance: take the Right off and put it back on.

splitRight : Right (There pl) = listSplit xs (y :: ys) loc ->
             elemAppend xs (y :: ys) (There pl) = loc
splitRight {pl = pl} {xs = []} {y = y} {ys = ys} {loc = loc} prf = rightInjective prf
splitRight {pl = pl} {xs = (x :: xs)} {y = y} {ys = ys} {loc = Here} Refl impossible
splitRight {pl = pl} {xs = (x :: xs)} {y = y} {ys = ys} {loc = (There z)} prf =
  let rec = splitRight {pl} {xs} {y} {ys} {loc = z} in cong $ rec (splitRight_lem1 prf)


---------------------------
-- tThenInorder is a bijection from ways to find a particular element in a tree
-- and ways to find that element in its inorder traversal. `inorderToFro`
-- and `inorderFroTo` together demonstrate this by showing that `inorderThenT` is
-- its inverse.

||| `tThenInorder t` is a retraction of `inorderThenT t`
inorderFroTo : {x : a} -> (t : Tree a) -> (loc : x `Elem` inorder t) -> tThenInorder t (inorderThenT t loc) = loc
inorderFroTo Tip loc = absurd loc
inorderFroTo (Node l v r) loc with (listSplit (inorder l) (v :: inorder r) loc) proof prf
  inorderFroTo (Node l v r) loc | (Left here) =
    rewrite inorderFroTo l here in splitLeft _ _ loc prf
  inorderFroTo (Node l v r) loc | (Right Here) = splitMiddle prf
  inorderFroTo (Node l v r) loc | (Right (There x)) =
    rewrite inorderFroTo r x in splitRight prf

||| `inorderThenT t` is a retraction of `tThenInorder t`
inorderToFro : {x : a} -> (t : Tree a) -> (loc : x `InTree` t) -> inorderThenT t (tThenInorder t loc) = loc
inorderToFro (Node l v r) (OnLeft xInL) =
  rewrite unsplitLeft {ys = v :: inorder r} (tThenInorder l xInL)
  in cong $ inorderToFro _ xInL
inorderToFro (Node l x r) AtRoot =
  rewrite unsplitRight {x} {xs = inorder l} {ys = x :: inorder r} (tThenInorder (Node Tip x r) AtRoot)
  in Refl
inorderToFro {x} (Node l v r) (OnRight xInR) =
  rewrite unsplitRight {x} {xs = inorder l} {ys = v :: inorder r} (tThenInorder (Node Tip v r) (OnRight xInR))
  in cong $ inorderToFro _ xInR