Nyan101 Blog

얼마 전 코드포스에서 흥미로운 문제를 접했다. 대회 당시에는 풀지 못했는데, 에디토리얼을 읽어보던 중 뫼비우스 함수(Möbius function)에 대한 언급이 있어 이에 대해 좀더 자세히 알아보았다. Möbius function의 정의 뫼비우스 함수(Möbius function)는 자연수 n에 대해 다음과 같이 정의된다. (\(p\)는 소수) \[\mu(n) = \begin{cases} (-1)^k & \mathrm{if\,\,\,\,} n=p_1p_2\cdots p_k \, (p_i \neq p_j)\\...

코드잼이 새로운 시스템으로 바뀌었다. 사실 메인 코드잼에선 작년에 도입된 시스템이 올해 킥스타트까지 적용된 거라고 하는데 작년 코드잼은 국방부 전직퀘스트를 해야 했어서 개인적인 사정으로 참가를 못했으니 이번이 새로운 시스템을 경험하는 첫 대회였다. 결론부터 말하면 다소 삐걱거리는 출발이었다. 시작 직후 한동안 문제 로딩이 안 되면서 몇 분 후에야 문제를 볼 수 있었고,...

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를...

코드포스(http://codeforces.com/) Master 등급(a.k.a. 오렌지)을 달성했다. 그전까지 Candidate Master에서 거의 2년간 머무르다가 올해 들어 적극적으로 대회를 참가하기 시작했고, 그 덕분인지 최근 한 달(1.22 ~ 2.24) 동안 rating +241이라는 나름 의미있는 성과를 거두면서 승급에 성공했다. 이제 박제해야지 최근 대회를 진행하면서 느꼈던 건 (당연한 소리겠지만) 풀 수 있어야 하는 문제를 못 푸는 일은...

Polymorphic Lists 이전 장에서 natlist, 다시 말해 nat으로 이루어진 리스트에 대해 다뤘다. 마찬가지 방법으로 문자열 리스트, bool 리스트, 리스트의 리스트 등 다양한 리스트를 정의할 수 있다. 예를 들어 bool 리스트는 Inductive boollist : Type := | bool_nil | bool_cons (b : bool) (l : boollist). 로 정의된다. 그런데 매번 새로운...

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)...

본 챕터에서는 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' =>...

이제 Coq를 이용해 간단한 증명을 직접 작성해보자. Notation 본론을 시작하기에 앞서 전에 만들었던 plus, mult 에 infix notation을 정의하자. Notation "x + y" := (plus x y) (at level 50, left associativity) : nat_scope. Notation "x * y" := (mult x y) (at level 40, left associativity) : nat_scope. 이전에...

Define Numbers 이전 글에서는 day, bool, color 와 같이 원소의 개수가 유한한 타입, 다시 말해 타입 \(T\)에 대해 \(\{x | x \mathrm{\,has\,type\,}T\} \)가 유한집합인 경우만을 다뤘다. 무한한 원소를 가지는 타입을 정의하려면 어떻게 해야 할까? 집합론에서와 마찬가지로 자연수에서 시작해보자. 페아노 공리계(Peano axioms)에서 필요한 부분을 빌려오자. 크게 중요하지 않은 공리들은 생략했다 1....