Hallo Habr.
Neulich ging ich zu einem Interview in einer seriösen Firma und dort wurde mir angeboten, eine einfach verbundene Liste umzudrehen. Leider dauerte diese Aufgabe die gesamte erste Runde des Interviews, und am Ende des Interviews sagte der Interviewer, dass alle anderen heute krank waren und ich daher nach Hause gehen kann. Der gesamte Prozess der Lösung dieses Problems, einschließlich einiger Optionen für den Algorithmus und der anschließenden Diskussion sowie Diskussionen darüber, wie die Liste umgedreht wird, unter der Katze.
Wir lösen das Problem
Der Interviewer war sehr nett und freundlich:
- Nun, lassen Sie uns zuerst dieses Problem lösen: Eine einfach verbundene Liste wird gegeben, Sie müssen sie umdrehen.
- Ich mache es jetzt! Und in welcher Sprache ist das besser?
- Welches ist fĂĽr Sie bequemer?
Ich habe einen C ++ - Entwickler interviewt, aber um die Algorithmen in Listen zu beschreiben, ist dies nicht die beste Sprache. Außerdem habe ich irgendwo gelesen, dass Sie bei den Interviews zuerst eine ineffektive Lösung anbieten und diese dann nacheinander verbessern müssen. Deshalb habe ich den Laptop geöffnet, vim und den Interpreter gestartet und diesen Code skizziert:
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)
— - ?
— . , .
— … , , . , , , , .
, - .