-
[BOJ] 1413 : 박스 안의 열쇠
1413 : 박스 안의 열쇠 풀이 모든 열쇠를 얻으러면, 열쇠들 사이에 사이클이 생겨야한다. 우리에겐 k개의 폭탄이 있기 때문에, 이 열쇠들을 k개의 집합으로 나눠서 사이클을 만드는 경우의 수를 세면 된다. n개의 원소를 k개의 원순열로 분할하기 위해, 제1종 스털링 수라는 걸 사용해보자. s(n, k) = s(n-1, k-1) + (n-1)*s(n-1, k)라는 점화식이 나온다. gcd로 최대공약수를 구하고, 합으로 나눠주면 끝! 코드 #include <stdio.h> typedef long long ll; int n, m, i, j; ll dp[21][21] = { 1 }, div;...
-
SIGPL Winter School 2017 3일차 정리
SIGPL Winter School 2017 3일차 정리 마지막 날 Type Check Val/Computation.Inductive/Fuction 4가지 룰이랑 Eval만 사용해서 체크함 logical한 step 4개의 룰만 있으면 거의 모든 증명을 할 수 있음 나머지 불가능한 것도 axiom? 추가하면 가능 프로그램 식을 그대로 읽으면 증명하는 거랑 똑같음 ->은 non dependent function forall은 dependent function ==forall, ->, =, P -> false, True, False, /|, |/, exists== 이것만 가지고 모든 set을 만들 수 있음 set이 바로 proposition (coq에서, m zigler set은 set prop는 prop)...
-
SIGPL Winter School 2017 2일차 정리
SIGPL Winter School 2017 2일차 정리 Martin Ziegler Logic 강의 tautology - always true satisfiability - true but not always inconsistency - false emptyset : false -> true 추후에 추가 예정 다시 Coq 강의 istrue = predicate type check 동시에 evaluate P -> Q P ------------ Q 증명 불가능한 함수는 짤 수 없다 1+(n:nat)를 짤 수는 없지만 1+(n:nat)->false 는 가능 evaluation은 증명을 단순화 시키는 것, simplify type checking 할 때 evaluation 해도 안전함 eval termination...
-
SIGPL Winter School 2017 1일차 정리
SIGPL Winter School 2017 1일차 정리 주어가 명시되지 않은 문장은 대부분 Coq가 그렇다는 의미로 받아들이면 대부분 알아들을 수 있을 것이다. Coq는 실제 계산할 때 퍼포먼스 때문에 nat에서 다른 타입으로 계산을 허용한다고 한다. Coq로 짠 코드를 실행하다가 오버플로우 등의 현실적인 에러가 발생할 수 있지만, 애초에 Coq는 Theorem을 증명하는 데에 목적을 두기 때문에 Coq에 대해 문제를 제기할 필요는 없다. 문제 없이 Type Check를 통과하면 안전하다고 보장된다. 이의를 제기할 필요는 없다. Type Check를 통과하면 안전하다는 사실이 이미 다...
-
SIGPL Winter School 2017
SIGPL Winter School 2017 SIGPL Winter School 2017에 참여하여 보고, 듣고, 배우고, 느낀점을 정리한 글입니다. 관련 자료가 여기(슬라이드)와 여기(책) 있으니 필요하신 분은 참고하시기 바랍니다!