지난 Round A에 이어 리뉴얼된 킥스타트에서 치르는 두번째 대회였다. 다행히 지난번과 같은 서버 문제는 없었지만 생각처럼 문제가 잘 풀리지는 않았다. A번을 제출하고 나니 딱히 풀이가 떠오르는 문제가 없어 결국 B, C 모두 Small까지만 통과할 수 있었다. 결과는 최종 115등으로 전체 문제는 여기에서 볼 수 있다.
Problem A. Building Palindromes 문자열이 주어지면 주어진 문자열의 l…r 구간에 포함된 글자들로 팰린드롬을 만들 수 있는지 판단해야 한다. 구간 [l, r]에 속한 글자들만으로 팰린드롬을 만들기 위해서는 홀수 번 등장하는 알파벳이 최대 하나여야 한다는 사실에 유의하면, 각 알파벳 등장 횟수의 prefix sum을 이용해 각 쿼리를 \(O(26)\)에 처리할 수 있다. 첫 제출에서 초기화에 쓴 fill 함수의 범위를 잘못 잡았다는 걸 깨달아 대회 도중 다시 제출했다. [[source](https://github.com/nyan101/algorithm_snippet/blob/master/CodeJam/Kickstart 2019 Round B/A.cpp)]
* 개인 페이스북 타임라인에 썼던 내용을 다듬어 업로드한 글입니다.
알고리즘(PS)을 공부하는 법 인터넷을 보면 종종 “알고리즘 잘 하는 법(or알고리즘 문제 잘 푸는 법)“에 대한 질문글이 올라오고, 많은 경우 “모르겠다고 답지를 보지 말고 혼자서 끝까지 고민해봐야 한다"라는 답변이 주를 이룬다.
얼마 전 코드포스에서 흥미로운 문제를 접했다. 대회 당시에는 풀지 못했는데, 에디토리얼을 읽어보던 중 뫼비우스 함수(Möbius function)에 대한 언급이 있어 이에 대해 좀더 자세히 알아보았다.
Möbius function의 정의 뫼비우스 함수(Möbius function)는 자연수 n에 대해 다음과 같이 정의된다. (\(p\)는 소수)
코드잼이 새로운 시스템으로 바뀌었다. 사실 메인 코드잼에선 작년에 도입된 시스템이 올해 킥스타트까지 적용된 거라고 하는데 작년 코드잼은 국방부 전직퀘스트를 해야 했어서 개인적인 사정으로 참가를 못했으니 이번이 새로운 시스템을 경험하는 첫 대회였다.
결론부터 말하면 다소 삐걱거리는 출발이었다. 시작 직후 한동안 문제 로딩이 안 되면서 몇 분 후에야 문제를 볼 수 있었고, 제출에서도 다소의 딜레이가 있었다. 거기에 더해 대회 막판에는 아예 제출버튼을 눌러도 코드 제출이 이루어지지 않아서 결국 끝까지 제출하지 못한 상태로 대회가 끝났다. 나름 지난 몇 차례의 킥스타트에서 꾸준히 10~20등 정도의 성적을 내다가 이번에 299등이라는 숫자를 보니 조금 억울하긴 하다(…)
High-Order Functions 다른 함수를 다룰 수 있는 함수를 고차 함수(higher-order function)라고 한다.
Definition do3times {X:Type} (f:X->X) (a:X) : X := f (f (f a)). >> Check @do3times : @do3times : forall X : Type, (X -> X) -> X -> X 이 do3times는 함수 f와 인자 a를 받아 a에 f를 3번 적용한 결과를 돌려준다. 함수를 인자로 제공한다는게 어떤 의미인지 살펴보자
>> Definition doubleMe (n:nat) : nat := n+n. >> Compute do3times doubleMe 3. : 24 : nat Filter 이제 좀더 유용한 고차 함수들에 대해 알아보자. filter는 X타입의 리스트(list X)와 원소 X에 대한 판정함수(predicate, \(f:X\rightarrow bool\))를 받아 주어진 predicate를 만족하는(i.e. true를 리턴하는) 원소들만을 남긴다.
코드포스(http://codeforces.com/) Master 등급(a.k.a. 오렌지)을 달성했다. 그전까지 Candidate Master에서 거의 2년간 머무르다가 올해 들어 적극적으로 대회를 참가하기 시작했고, 그 덕분인지 최근 한 달(1.22 ~ 2.24) 동안 rating +241이라는 나름 의미있는 성과를 거두면서 승급에 성공했다. 이제 박제해야지
최근 대회를 진행하면서 느꼈던 건 (당연한 소리겠지만) 풀 수 있어야 하는 문제를 못 푸는 일은 없어야 한다는 점이었다. 개인적으로는 Div.2 D,E (=Div.1 B,C) 정도를 기준으로 잡았다. 대바대(대회 by 대회)라고는 하지만 이 난이도에서는 대체로 “잘 알려진”, 혹은 규칙을 파악하면 코딩 자체는 어렵지 않은 문제들이 많다. 아이디어성 문제들은 어쩔 수 없다고 해도, 대회가 끝나고 나서 “이걸 왜 두시간동안 못 떠올렸지"라는 아쉬움을 없애자고 생각했다. 특히 최근 에듀코포 D에서 대회 종료 직전이 되어서야 풀이를 찾아내면서 이런 생각을 굳혔다. 다행히 지난 라운드에선 F의 밸런스 붕괴에 힘입어 그런 아쉬움 없이 28등으로 끝마칠 수 있었다.
Polymorphic Lists 이전 장에서 natlist, 다시 말해 nat으로 이루어진 리스트에 대해 다뤘다. 마찬가지 방법으로 문자열 리스트, bool 리스트, 리스트의 리스트 등 다양한 리스트를 정의할 수 있다. 예를 들어 bool 리스트는
Inductive boollist : Type := | bool_nil | bool_cons (b : bool) (l : boollist). 로 정의된다.
그런데 매번 새로운 타입의 리스트가 필요할 때마다 (거의) 동일한 정의를 다시 써주는 건 낭비일 것이다. 새로운 타입에 맞게 정의를 다시 쓴다는 말은 단순히 nil이나 cons의 문제가 아니라, length, reverse, append 등 앞서 natlist에서 정의했던 모든 함수를 전부 새로 작성해야 한다는 의미가 된다. 이런 불필요한 중복을 피하기 위해 Coq에서는 다형적(polymorphic) 타입을 지원한다.
Reasoning About Lists 리스트에 대한 간단한 정리를 증명해보자.
Theorem nil_app : forall l:natlist, [] ++ l = l. Proof. reflexivity. Qed. 대상이 natlist라는 점만 제외하면 이전의 forall n:nat, 0+n=n과 같은 형태이다. nat에서와 마찬가지로 natlist도 destruct를 통해 생성규칙에 따라 경우를 나눌 수 있다.
Theorem tl_length_pred : forall l:natlist, pred (length l) = length (tl l). Proof. intros l. destruct l as [| n l'] eqn:E. - (* l = [] *) reflexivity. - (* l = n::l' *) reflexivity. 마찬가지로 수학적 귀납법(induction tactic) 역시 적용 가능하다. nat에서의 귀납법과 마찬가지로 base step과 induction step으로 이루어져 있으며, 각각
본 챕터에서는 Structured Data, 그중에서도 List에 대해 다룬다.
Pairs of Numbers 지난번 nybble을 정의할 때 언급했듯이, Coq의 생성자(constructor)는 여러 개의 인자를 받을 수 있다.
Inductive natprod : Type := | pair (n1 n2 : nat). 이렇게 정의된 natprod에는 오직 하나의 생성규칙만 존재한다.(ex: pair 3 5)
Proof by Case Analysis 다뤄야 하는 대상이 복잡해지면 simpl이나 rewrite만으로는 충분하지 않은 경우가 있다. 잠시 예전 글에서 정의했던 is_equal을 가져오면서 여기에 새로운 Notation을 추가하자.
Fixpoint is_equal (n m : nat) : bool := match n with | O => match m with | O => true | S m' => false end | S n' => match m with | O => false | S m' => is_equal n' m' end end. Notation "x =? y" := (eqb x y) (at level 70) : nat_scope. 이제 거의 비슷하게 생긴 다음 두 명제를 증명해보자.
