Undecidable, Soundness, Completeness

 계산 가능한 문제는 크게 Decidable한지 Undecidable한지로 나뉠 수 있다. 일반적으로 개발하면서 마주치고 해결하는 문제들은 decidable한 문제로, P 클래스와 NP 클래스의 문제들이 이 영역에 속한다. 그래서 대부분 알고리즘 구현을 한다던지 어떤 문제를 마주했을 때 해결하고자 하는 문제들은 다 decidable한 문제이고, 그렇기 때문에 Soundness나 Completeness에 대해 크게 고민해보지 않았을 것이다. 이번에는 Undecidable한 문제들에 대해서 다뤄볼 예정이다.
 Undecidable한 문제의 정의부터 해야하는데, 정의는 문제에 대한 정답이 맞는지 틀리는지 항상 도출해내는 알고리즘을 설계하는게 불가능한 문제를 의미한다. 말로 설명해서는 이해가 힘들 수 있지만, 대표적인 예시로 halting problem이라는 것이 존재한다. 컴퓨터 과학분야에서 가장 유명한 문제 중 하나로 어떤 프로그램이 종료할지 혹은 아닐지(무한 루프)에 대해서 결정하는 것이 불가능 하다는 내용이다. 이는 이미 증명이 된 내용으로, contradiction을 통해 증명하는데 자료가 많으니 궁금하면 쉽게 검색해서 찾아볼 수 있다.
 이런 문제들이 언제 나타날까 싶은 생각이 들겠지만, 실제로 종종 이런 문제들을 만나게 된다. 특히 프로그램 성질에 대해서 정적인 시간 (컴파일 타임)에 알아내는 문제를 해결할 때 많이 나타난다. 최근에 사람들이 많이 쓰고 있고 대부분의 언어에서 지원하고 있는 lambda관련 higher-order function들과 함께 Static Type System을 사용하게 되면 문제가 나타난다. 고차원 함수에 대해서 Type을 완벽하게 정확한 추론을 해내는게 불가능하다. 또한 컴파일러 최적화 및 Warning 메세지를 띄워주는 과정에서도 정적인 시간에 런타임을 예측하는 부분인데 이 때도 완벽한 예측이 불가능하기 때문에 일부분 포기하는 과정이 생긴다.
 
 A. Soundness
  Soundness는 안전하다는 의미인데, 어떤 검증기가 존재할 때 이 검증기가 모든 가능한 경우에 대한 검증을 진행하는 것을 의미한다. 쉽게 설명하자면 내가 만약에 A라는 오류가 있는지에 대한 검증을 하는 검증기를 만들었을 때 Sound한 검증기는 다음과 같다:
  A오류를 가지고 있는 모든 프로그램을 찾아내는 검증기
 하지만 Sound하다는게 완벽한 것을 의미하는 것은 아닌데, 검증기가 찾아낸 프로그램이 항상 A오류를 포함하고 있다라는 의미는 다른 것이다. 조금 더 와닿는 예시로 Halting Problem을 Sound하게 풀어내는 검증기를 만든다고 생각해보자. 이 검증기는 무한루프에 빠지는 프로그램들을 찾아내는 검증기라고 하자. 그렇다면 가장 쉬운 검증기로 프로그램에 loop이 있으면 무한루프에 빠진다고 판단하는 검증기를 만들 수 있을 것이다. 이 검증기의 Soundness를 확인해보면, 무한루프 프로그램은 loop이 있을 수 밖에 없기 때문에 항상 검증기는 무한루프를 찾아낼 것이다. 즉, 모든 무한루프 프로그램은 해당 검증기를 통해 검증이 된다. 하지만 유한한 루프를 가진 프로그램도 검증기에 걸리게 되는데, 이는 soundness와 상관없다.
 
 B. Completeness 
  Completeness는 완전성을 의미하는데, 어떤 검증기가 검증을 해서 결과를 내면, 그 검증이 항상 올바른 검증을 한다는 의미이다. 위의 Soundness와 비교를 해보면, Soundness는 모든 경우에 대한 검증을 한다는건 보장하지만 그 결과가 항상 참이라는 것을 보장하지 않는다. Completeness는 검증을 해서 나온 결과는 항상 신뢰가능하지만 검증하지 못한 경우들도 존재할 수 있음을 의미한다. Halting Problem예시로 들어볼 때, 검증기를 loop의 인자가 true인 경우에 무한루프로 판단하는 검증기를 만든다고 해보자. 검증기가 무한루프라고 판단한 경우에는 항상 무한루프임이 맞다. 하지만 발산하면서 무한루프를 생성하는 경우에 해당 검증기가 찾아낼 수 없다.
  
 C. Program Analyzer
  프로그램 검증기를 만들 때는 Soundness와 Completeness를 둘 다 얻을 수 없다. Undecidable한 문제에 대해서는 halting problem과 같은 난이도의 문제를 해결해야하는 것이고 이미 불가능하다고 증명이 됐다. 그렇기 때문에 일반적으로 검증기에서는 둘 중 하나를 보장하는 방식으로 사용되고 있다. 예를 들어 Type System에서는 검증기가 illegal한 type을 가진 프로그램을 통과시키면 안되기 때문에 Soundness를 보장하는 방식으로 동작하고 컴파일러 최적화 단계에서는 확실한 최적화 기법만 사용해야하기 때문에 Complete한 검증에 대해서만 최적화를 시키게 된다.
  이 검증 분야에서는 그래서 최대한 sound하면서 complete한 분석기를 만들어 내는거에 초점이 있다.
  
 요약.
  문제를 구분할 때 크게 decidability로 구분할 수 있는데, 우리가 흔히 마주치는 문제들인 P 영역, NP영역의 계산 가능한 문제들은 complete하고 sound한 해결책이 존재한다. 하지만 undecidable한 문제는 완벽한 해결책을 만들어 내는 것이 불가능하고 상황에 맞게 sound한 해결책 혹은 complete한 해결책을 적용시킨다.