हाय, हैब्र।

दूसरे दिन, मैं एक गंभीर कंपनी में एक साक्षात्कार के लिए गया, और वहाँ उन्होंने मुझे बस कनेक्ट की गई सूची को चालू करने की पेशकश की। दुर्भाग्य से, इस कार्य ने साक्षात्कार के पूरे पहले दौर में ले लिया, और साक्षात्कार के अंत में, साक्षात्कारकर्ता ने कहा कि बाकी सभी लोग आज बीमार थे, और इसलिए मैं घर जा सकता हूं। फिर भी, इस समस्या को हल करने की पूरी प्रक्रिया, जिसमें एल्गोरिथ्म के कुछ विकल्पों और उनके बाद की चर्चा के साथ-साथ सूची उलटा क्या है, इसके बारे में चर्चा बिल्ली के नीचे है।

हम समस्या का समाधान करते हैं

साक्षात्कारकर्ता बहुत अच्छा और दोस्ताना था:

- ठीक है, चलो पहले इस समस्या को हल करें: एक बस कनेक्टेड सूची दी गई है, आपको इसे चारों ओर मोड़ने की आवश्यकता है।

- मैं अभी करूँगा! और ऐसा करना किस भाषा में बेहतर है?

- कौन सा आपके लिए अधिक सुविधाजनक है?

मैंने C ++ डेवलपर का साक्षात्कार लिया, लेकिन सूचियों पर एल्गोरिदम का वर्णन करने के लिए, यह सबसे अच्छी भाषा नहीं है। इसके अलावा, मैंने कहीं पढ़ा है कि साक्षात्कारों में आपको पहले एक अप्रभावी समाधान की पेशकश करने की आवश्यकता होती है, और फिर इसे क्रमिक रूप से सुधारते हैं, इसलिए मैंने लैपटॉप खोला, विम लॉन्च किया और दुभाषिया और इस कोड को स्केच किया:

revDumb : List a -> List a
revDumb [] = []
revDumb (x :: xs) = revDumb xs ++ [x]

, , , - , , :

revOnto : List a -> List a -> List a
revOnto acc [] = acc
revOnto acc (x :: xs) = revOnto (x :: acc) xs

revAcc : List a -> List a
revAcc = revOnto []

— , , , .

- , . , ( ?) - , :

— , , , , , , , .

revsEq : (xs : List a) -> revAcc xs = revDumb xs

, :

— , case split .

— generate definition, case split, obvious proof search —

revsEq : (xs : List a) -> revAcc xs = revDumb xs
revsEq [] = Refl
revsEq (x :: xs) = ?revsEq_rhs_1

, , , :

— , , , . , , , :

revsEq : (xs : List a) -> revAcc xs = revDumb xs
revsEq [] = Refl
revsEq (x :: xs) = let rec = revsEq xs in ?wut

— ?wut,

  rec : revOnto [] xs = revDumb xs
--------------------------------------
wut : revOnto [x] xs = revDumb xs ++ [x]

— revDumb xs , rec. :

revsEq (x :: xs) = let rec = revsEq xs in
                   rewrite sym rec in ?wut

--------------------------------------
wut : revOnto [x] xs = revOnto [] xs ++ [x]

— c :

lemma1 : (x0 : a) -> (xs : List a) -> revOnto [x0] xs = revOnto [] xs ++ [x0]

generate definition, case split xs, obvious proof search

lemma1 : (x0 : a) -> (xs : List a) -> revOnto [x0] xs = revOnto [] xs ++ [x0]
lemma1 x0 [] = Refl
lemma1 x0 (x :: xs) = ?lemma1_rhs_2

— , . lemma1 x xs, lemma1 x0 xs. , , ,

lemma1 x0 (x :: xs) = let rec = lemma1 x xs in ?wut

?wut:

  rec : revOnto [x] xs = revOnto [] xs ++ [x]
--------------------------------------
wut : revOnto [x, x0] xs = revOnto [x] xs ++ [x0]

— revOnto [x] xs rec. :

lemma1 x0 (x :: xs) = let rec = lemma1 x xs in
                      rewrite rec in ?wut

— , :

--------------------------------------
wut : revOnto [x, x0] xs = (revOnto [] xs ++ [x]) ++ [x0]

— , . :

lemma1 x0 (x :: xs) = let rec = lemma1 x xs in
                      rewrite rec in
                      rewrite sym $ appendAssociative (revOnto [] xs) [x] [x0] in ?wut

— -:

--------------------------------------
wut : revOnto [x, x0] xs = revOnto [] xs ++ [x, x0]

— ! , , , . , , :

lemma2 : (acc, lst : List a) -> revOnto acc lst = revOnto [] lst ++ acc

IDE . case split lst, acc, revOnto lst:

lemma2 : (acc, lst : List a) -> revOnto acc lst = revOnto [] lst ++ acc
lemma2 acc [] = Refl
lemma2 acc (x :: xs) = ?wut1

wut1

--------------------------------------
wut1 : revOnto (x :: acc) xs = revOnto [x] xs ++ acc

lemma2 acc (x :: xs) = let rec = lemma2 (x :: acc) xs in ?wut1

  rec : revOnto (x :: acc) xs = revOnto [] xs ++ x :: acc
--------------------------------------
wut1 : revOnto (x :: acc) xs = revOnto [x] xs ++ acc

rec:

lemma2 acc (x :: xs) = let rec = lemma2 (x :: acc) xs in
                       rewrite rec in ?wut1

--------------------------------------
wut1 : revOnto [] xs ++ x :: acc = revOnto [x] xs ++ acc

— - . , lemma1 , , lemma2 , lemma1 x xs , lemma2 [x] xs:

lemma2 acc (x :: xs) = let rec1 = lemma2 (x :: acc) xs in
                       let rec2 = lemma2 [x] xs in
                       rewrite rec1 in
                       rewrite rec2 in ?wut1

--------------------------------------
wut1 : revOnto [] xs ++ x :: acc = (revOnto [] xs ++ [x]) ++ acc

, :

lemma2 : (acc, lst : List a) -> revOnto acc lst = revOnto [] lst ++ acc
lemma2 acc [] = Refl
lemma2 acc (x :: xs) = let rec1 = lemma2 (x :: acc) xs in
                       let rec2 = lemma2 [x] xs in
                       rewrite rec1 in
                       rewrite rec2 in 
                       rewrite sym $ appendAssociative (revOnto [] xs) [x] acc in Refl

— , lemma1 , , lemma2 lemma. , , , :

lemma : (acc, lst : List a) -> revOnto acc lst = revOnto [] lst ++ acc
lemma acc [] = Refl
lemma acc (x :: xs) = let rec1 = lemma (x :: acc) xs in
                      let rec2 = lemma [x] xs in
                      rewrite rec1 in
                      rewrite rec2 in 
                      rewrite sym $ appendAssociative (revOnto [] xs) [x] acc in Refl

revsEq : (xs : List a) -> revAcc xs = revDumb xs
revsEq [] = Refl
revsEq (x :: xs) = let rec = revsEq xs in
                   rewrite sym rec in lemma [x] xs

15, - , .

— , , - .

— , , . ! , ? ?!

— ! , ! , , ? « »? : xs — , xs' «» , , . !

revCorrect : (xs : List a) ->
             (f : b -> a -> b) ->
             (init : b) ->
             foldl f init (revDumb xs) = foldr (flip f) init xs

— , revDumb revAcc ( forall xs. revDumb xs = revAcc xs, , , , ), , , revDumb.

revCorrect : (xs : List a) ->
             (f : b -> a -> b) ->
             (init : b) ->
             foldl f init (revDumb xs) = foldr (flip f) init xs
revCorrect [] f init = Refl
revCorrect (x :: xs) f init = let rec = revCorrect xs f init in ?wut

  rec : foldl f init (revDumb xs) = foldr (flip f) init xs
--------------------------------------
wut : foldl f init (revDumb xs ++ [x]) = f (foldr (flip f) init xs) x

— :

revCorrect (x :: xs) f init = let rec = revCorrect xs f init in
                              rewrite sym rec in ?wut

--------------------------------------
wut : foldl f init (revDumb xs ++ [x]) = f (foldl f init (revDumb xs)) x

— revDumb xs . : f f, . :

foldlRhs : (f : b -> a -> b) ->
           (init : b) ->
           (x : a) ->
           (xs : List a) ->
           foldl f init (xs ++ [x]) = f (foldl f init xs) x

— , . :

foldlRhs : (f : b -> a -> b) ->
           (init : b) ->
           (x : a) ->
           (xs : List a) ->
           foldl f init (xs ++ [x]) = f (foldl f init xs) x
foldlRhs f init x [] = Refl
foldlRhs f init x (y :: xs) = foldlRhs f (f init y) x xs

revCorrect : (xs : List a) ->
             (f : b -> a -> b) ->
             (init : b) ->
             foldl f init (revDumb xs) = foldr (flip f) init xs
revCorrect [] f init = Refl
revCorrect (x :: xs) f init = let rec = revCorrect xs f init in
                              rewrite sym rec in foldlRhs f init x (revDumb xs)

— - ?
— . , .
— … , , . , , , , .

, - .

एक गायन से जुड़े साक्षात्कार सूची को कैसे तैनात किया जाए

हम समस्या का समाधान करते हैं

More articles: