मैं एक पेड़ और इसके ट्रैवर्सल के बीच एक विभाजन कैसे स्थापित कर सकता हूं?

Question

मैं How does inorder+preorder construct unique binary tree? पर देख रहा था और सोचा था कि इडिस में इसका औपचारिक सबूत लिखना मजेदार होगा। दुर्भाग्य से, मैं साबित करने की कोशिश कर रहा हूं कि पेड़ में एक तत्व खोजने के तरीके इसके अंदरूनी ट्रैवर्सल में खोजने के तरीकों से मेल खाते हैं (बेशक, मुझे प्रीऑर्डर ट्रैवर्सल के लिए भी ऐसा करने की आवश्यकता होगी) । किसी भी विचार का स्वागत है। मैं विशेष रूप से एक पूर्ण समाधान में रूचि नहीं रखता हूं- बस सही दिशा में शुरू करने में मदद करें।

को देखते हुए

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 (::) [] 

दूसरा दृष्टिकोण काफी सब कुछ करने के लिए लगता है मुश्किल है, इसलिए मेरे अधिकांश प्रयासों ने पहले पर ध्यान केंद्रित किया है।

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

लिखने के लिए (inorder की पहली परिभाषा का उपयोग)

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 

यह काफी आसान है और परिणाम एक बहुत सरल संरचना है कि सबूत के लिए उचित रूप से अच्छी लगती है है: मैं इस तरह पेड़ में स्थानों का वर्णन ।

यह भी

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

दुर्भाग्य का एक संस्करण लिखने के लिए बहुत मुश्किल नहीं है, मैं नहीं, अभी तक, ऊपर किसी भी तरह से साथ inorderThenInTree का एक संस्करण लिखने के लिए है कि मैं साबित करने के लिए है कर लिया है आए हैं inTreeThenInorder के विपरीत। केवल

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

और मैं वहां से वापस आने की कोशिश में परेशानी में भाग गया।

कुछ सामान्य विचारों मैंने कोशिश की:

1. VectList के बजाय का उपयोग करते हुए यह आसान बाहर काम करने के क्या बाईं तरफ है और क्या सही पर है बनाने के लिए प्रयास करने के लिए। मैं इसके "हरे रंग की कीचड़" में फंस गया।

2. वृक्षारोपण के साथ चारों ओर बजाना, यह साबित करने के लिए कि पेड़ की जड़ पर घूर्णन एक अच्छी तरह से स्थापित संबंध में जाता है। (मैंने नीचे घूर्णन के साथ नहीं खेला था, क्योंकि मैं इन रोटेशन के बारे में कुछ भी उपयोग करने में कभी भी सक्षम नहीं था)।

3. पेड़ नोड्स को कैसे सजाने के बारे में जानकारी के साथ सजाने की कोशिश कर रहा है। मैंने इस पर बहुत लंबा खर्च नहीं किया क्योंकि मैं उस दृष्टिकोण के माध्यम से कुछ भी दिलचस्प व्यक्त करने का तरीका नहीं सोच सका।

4. इस सबूत का निर्माण करने की कोशिश कर रहा है कि हम वापस जा रहे हैं जहां हमने ऐसा कार्य करने के दौरान शुरू किया था। यह बहुत गन्दा हो गया, और मैं कहीं या दूसरे अटक गया।

Answer 1

आप अपने listSplit लेम्मा के साथ सही रास्ते पर थे। आप उस कार्य का उपयोग यह जानने के लिए कर सकते हैं कि लक्ष्य तत्व वृक्ष के बाएं या दाएं किनारे पर है या नहीं।

यह मेरा कार्यान्वयन

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

से प्रासंगिक लाइन यहाँ पूरा कार्यान्वयन है। मैंने इसे अवांछित spoilers से बचने के लिए एक बाहरी लिंक के रूप में शामिल किया है और Agda के अद्भुत HTML हाइपरलिंक्ड, वाक्यविन्यास हाइलाइट आउटपुट का लाभ उठाने के लिए भी शामिल किया है।

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

Answer 2

मैं बाहर काम करने के साबित करने के लिए कैसे है कि यह lemmas glguy's answer में संदर्भित के प्रकार पढ़ने से एक सूची स्थान पर एक पेड़ के स्थान से जाने के लिए और वापस करने के लिए संभव है में सक्षम था। आखिरकार, मैं दूसरी तरफ भी जाने में कामयाब रहा, हालांकि कोड (नीचे) काफी भयानक है। सौभाग्य से, मैं भयानक सूची लेमास का पुन: उपयोग करने में सक्षम था ताकि प्रीऑर्डर ट्रैवर्सल के बारे में संबंधित प्रमेय भी साबित हो सके।

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 

Answer 3

मैं inorderToFro और inorderFroTo और इदरिस में जुड़े lemmas लिखा था।

पहले, splitMiddle वास्तव में आवश्यक नहीं है: Here's the link.

मैं अपने समाधान के बारे में (विवरण में ज्यादा जा रहा बिना) कर सकते हैं अंक के एक जोड़े हैं। यदि आप अधिक सामान्य Right p = listSplit xs ys loc -> elemAppend xs ys p = locsplitRight के लिए टाइप करते हैं, तो वह उसी ग्राउंड को कवर कर सकता है।

दूसरा, आप स्पष्ट _lem कार्यों के बजाय with पैटर्न का उपयोग कर सकते हैं; मुझे लगता है कि यह स्पष्ट और अधिक संक्षिप्त होगा।

तीसरा, आप 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 में इसके प्रकार में फ़ंक्शंस नहीं हैं, इसलिए मुझे लगता है कि यही कारण है कि यह अधिक आसानी से काम करता है।

सामान्य रूप से, इस समय मैं इस तरह के सबूत लिखने के लिए इडिस पर एजडा की सलाह देता हूं। यह बहुत तेजी से जांचता है और यह बहुत अधिक मजबूत और सुविधाजनक है। मैं बहुत आश्चर्यचकित हूं कि आप यहाँ इडिस लिखने में कामयाब रहे और पेड़ के ट्रैवर्स के बारे में दूसरे प्रश्न के लिए।