Как развернуть односвязный список на собеседовании +146


Привет, Хабр.


Я тут на днях сходил на собеседование в одну серьёзную фирму, и там мне предложили перевернуть односвязный список. К сожалению, эта задача заняла весь первый раунд собеседования, а по окончанию интервьювер сказал, что все остальные сегодня заболели, и поэтому я могу идти домой. Тем не менее, весь процесс решения этой задачи, включая пару вариантов алгоритма и последующее их обсуждение, а также рассуждения о том, что вообще такое переворачивание списка, под катом.


image


Решаем задачу


Интервьювер был довольно приятным и дружелюбным:


Ну, давайте для начала решим такую задачу: дан односвязный список, нужно его обратить.


— Сейчас сделаю! А на каком языке лучше это сделать?


На каком вам удобнее.


Я собеседовался на 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)

Так а тесты-то где?
— А они не нужны. Мы же формально доказали, что мы обращаем список.
… Хм, похоже, время вышло. Ну, спасибо за то, что пришли к нам на интервью, всего доброго, мы вам перезвоним.


Правда, почему-то до сих пор не перезвонили.




К сожалению, не доступен сервер mySQL