Хабрахабр

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

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

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

image

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

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

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

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

Кроме того, я где-то читал, что на собеседованиях сначала надо предложить неэффективное решение, а потом последовательно его улучшать, так что я открыл ноутбук, запустил vim и интерпретатор и набросал такой код: Я собеседовался на C++-разработчика, но для описания алгоритмов на списках это не лучший язык.

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

При этом case split мы делаем по lst, а не по acc, так как revOnto рекурсивно определён по lst: Привычным движением заставляю IDE сделать всю грязную работу.

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 xs = revAcc xs, а равенство функций следует из экстенсиональности, которую мы, увы, не можем интернализировать), то нам неважно, какую из функций обращения списка рассматривать, так что мы для простоты возьмём revDumb. — Так как мы уже доказали, что revDumb равно revAcc (технически мы доказали forall 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 ?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

Нам достаточно сформулировать и доказать довольно очевидное свойство левых свёрток: свёртка всего списка с функцией f эквивалентна функции f, вызванной с результатом свёртки префикса списка и последнего элемента списка. — Начиная с этого момента revDumb xs нам не нужен. Или в коде:

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)

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

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

Теги
Показать больше

Похожие статьи

Добавить комментарий

Ваш e-mail не будет опубликован. Обязательные поля помечены *

Кнопка «Наверх»
Закрыть