How to deploy a singly-linked interview list
Hi, Habr.
The other day, I went to an interview in one serious company, and there they offered me to turn over a simply connected list. Unfortunately, this task took the entire first round of the interview, and at the end of the interview, the interviewer said that everyone else was sick today, and therefore I can go home. Nevertheless, the whole process of solving this problem, including a couple of options for the algorithm and their subsequent discussion, as well as discussions about what the list turning is, under the cat.
We solve the problem
The interviewer was pretty nice and friendly:
- Well, let's first solve this problem: a singly connected list is given, you need to reverse it.
- I'll do it now! And in what language is it better to do this?
- Which one is more convenient for you?
I interviewed a C ++ developer, but to describe the algorithms on lists, this is not the best language. In addition, I read somewhere that at the interviews you first need to offer an ineffective solution, and then improve it sequentially, so I opened the laptop, launched vim and the interpreter and sketched this code:
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)
— - ?
— . , .
— … , , . , , , , .
, - .
All Articles