مرحبا يا هبر.

في اليوم الآخر ، ذهبت إلى مقابلة في إحدى الشركات الجادة ، وعرضوا عليها أن أقوم بتسليم قائمة متصلة ببساطة. لسوء الحظ ، استغرقت هذه المهمة الجولة الأولى بأكملها من المقابلة ، وفي نهاية المقابلة ، قال المحاور إن كل شخص كان مريضًا اليوم ، وبالتالي يمكنني العودة إلى المنزل. ومع ذلك ، فإن العملية برمتها من حل هذه المشكلة ، بما في ذلك اثنين من الخيارات للخوارزمية ومناقشتها اللاحقة ، فضلا عن المناقشات حول ما تحول القائمة ، تحت القط.

نحن نحل المشكلة

كان المحاور لطيفًا وودودًا للغاية:

- حسنًا ، دعنا أولاً نحل هذه المشكلة: يتم توفير قائمة متصلة ببساطة ، تحتاج إلى قلبها.

- سأفعل ذلك الآن! وبأي لغة من الأفضل القيام بذلك؟

- أيهما أكثر ملاءمة لك؟

لقد أجريت مقابلة مع أحد مطوري C ++ ، لكن لوصف الخوارزميات في القوائم ، فهذه ليست هي أفضل لغة. بالإضافة إلى ذلك ، قرأت في مكان ما أنه في المقابلات الأولى تحتاج إلى تقديم حل غير فعال ، ومن ثم تحسينه بشكل متتابع ، لذلك فتحت الكمبيوتر المحمول ، وأطلقت vim والمترجم الفوري ورسمت هذا الرمز:

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)

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

, - .