Hola Habr

El otro día, fui a una entrevista en una empresa seria, y allí me ofrecieron entregar una lista simplemente conectada. Desafortunadamente, esta tarea tomó toda la primera ronda de la entrevista, y al final de la entrevista, el entrevistador dijo que todos los demás estaban enfermos hoy y, por lo tanto, puedo irme a casa. Sin embargo, todo el proceso de resolución de este problema, incluidas un par de opciones para el algoritmo y su posterior discusión, así como discusiones sobre cuál es el giro de la lista, bajo el gato.

Resolvemos el problema

El entrevistador fue bastante amable y amigable:

- Bueno, primero solucionemos este problema: se proporciona una lista simplemente conectada, debe darle la vuelta.

- Lo haré ahora! ¿Y en qué idioma es mejor hacer esto?

- ¿Cuál es más conveniente para ti?

Entrevisté a un desarrollador de C ++, pero para describir los algoritmos en las listas, este no es el mejor lenguaje. Además, leí en alguna parte que en las entrevistas primero debes ofrecer una solución ineficaz y luego mejorarla secuencialmente, así que abrí la computadora portátil, inicié vim y el intérprete y dibujé este código:

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)

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

, - .