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

Привет.

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

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

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

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

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

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

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

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

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

Автор: 0xd34df00d

Источник