불리언 값과 논리적 명제를 혼동할 때 생기는 문제(‘불리언 맹목’)를 지적하고, 의미의 출처를 보존하는 데이터 표현과 패턴 매칭 같은 대안을 통해 코드와 추론을 개선할 수 있음을 논한다.
나는 불리언이 싫다! 하지만 모든 것이 “그냥 비트” 아닌가? 컴퓨터는 게이트로 만들어지지 않았나? 그리고 게이트는 논리 결합자와 다름없지 않나? 컴퓨터 과학자가 어떻게 불리언을 싫어할 수 있단 말인가?
Fritz Henglein이 내게 지적하길, 이론 컴퓨터 과학의 세계는 두 진영으로 나뉜다. 언어와 의미에 관심을 두는 논리학자들과 알고리즘과 복잡도에 관심을 두는 조합론자들이다. 논리학자들은 프로그램이 올바르게 동작함을 증명하는 걸 사랑하고, 조합론자들은 프로그램이 실행에 몇 단계가 드는지 세는 걸 사랑한다. 그런데 묘하게도 논리학자들은 불리언을 싫어하고 트리나 스트림 같은 추상을 사랑하며, 조합론자들은 비트를 사랑하고 추상을 싫어한다! (적어도 흔히 그렇게 보인다. 수사적 장치 하나쯤은 봐주길.)
내 요지는 이렇다. 불리언은 데이터의 한 가지, 그것도 유난히(혹은 이진적으로) 지루한 타입일 뿐이다. 불리언 값 b 는 true 또는 false 둘 중 하나일 뿐이다. 끝. 불리언은 그 값 이외의 _정보_를 전혀 담지 않는다. 바로 그게 문제다. Conor McBride의 말처럼, 불리언을 제대로 사용하려면 그 값의 _출처(provenance)_를 알아야 하고, 그래야 그 값이 무엇을 의미하는지 알 수 있다.
불리언은(컴퓨터 과학 논문과 교재에서 거의 예외 없이) _명제(proposition)_와 혼동된다. 명제는 어떤 주장이나 단언을 표현한다. 명제 p 가 _참(true)_이라는 것은 _증명(proof)_이 존재한다는 뜻이다. 왜 p 가 성립하는지에 대한 전달 가능한 합리적 논거가 있다는 뜻이다. 명제 p 가 _거짓(false)_이라는 것은 _반증(refutation)_이 존재한다는 뜻으로, p 가 성립하지 않음을 보여 주는 반례가 있다는 뜻이다.
여기서 언어는 섬세하다. 명제 p 가 참이라는 _판정(judgement)_은 p 가 true와 _같다_고 말하는 것과 절대 같지 않다. 마찬가지로 p 가 거짓이라는 판정은 p 가 false와 _같다_고 말하는 것과 같지 않다! 사실 “p 가 true와 같은가?”라고 묻는 것 자체가 말이 안 된다. 전자는 _명제(주장)_이고, 후자는 _불리언(데이터 값)_이기 때문이다. 그 둘은 _타입_부터가 다르다.
계산 가능성이 문제가 되지 않는 고전 수학에서는 불리언과 명제의 개념을 뒤섞어 세상에 true와 false 두 개의 명제만 있다고 보는 것이 가능하다. 증명의 역할은 주어진 명제가 **이 둘 중 하나(와 같다)**임을 보이는 일이다. 이것은, 무언가가 참인지 거짓인지 _계산_하는 데 관심이 없다면, 그럭저럭 괜찮다. 하지만 일단 계산하려 든다면, 참거짓을 결정할 수 없을 수 있는 일반적 명제와, 어느 쪽이든 계산으로 구할 수 있는 불리언 사이를 분명히 구분해야 한다. 그런데 그렇게 되면, 앞서 언급했듯이, 우리가 불리언과 _그 불리언이 의미하는 바_를 연결해 주어야 한다. 즉 그 값의 출처를 명시해야 한다. 그리고 그 순간 깨닫게 된다. 불리언은 아무런 특별한 지위를 갖지 않으며, 대개는 데이터 구조로도 형편없는 선택이라는 사실을. 왜냐하면 Dan Licata가 부른 _불리언 맹목(Boolean blindness)_을 낳기 때문이다.
좋은 예가 bool 타입의 동등성 검사 e=e’ 이다. 예전에 논의했듯이, 이 겉보기엔 순진무구한 함수는 특히 풍부한 타입 구조를 지닌 추상 언어에서 심각한 복잡성을 야기한다. 그리고 명제와 불리언을 혼동하는 전형적인 사례이기도 하다. 타입이 말해 주듯, 동등성 검사는 인자가(그들의 타입이 정한 의미에서) 같은지 여부에 따라 true 또는 false를 돌려주는 함수다. 표기가 혼동을 부르지만, 식 e=e’ 는 e 와 e’ 가 같다는 _명제_가 아니다! 그것은 두 형태 중 하나, true 또는 false인 _데이터 조각_일 뿐이다. 이 동등성 검사는 다음과 같은 성질을 갖는 함수일 따름이다. 곧, 만약 true를 돌려주면 인자들은 같다(연관된 동등성 명제가 참이다). 만약 false를 돌려주면 인자들은 같지 않다(연관된 동등성 명제가 거짓이다). 그리고 어떤 입력에 대해서도 반드시 true 혹은 false 중 하나를 돌려준다는 것이 보장된다. 머리카락을 가르는 구분처럼 보일지 모르지만, 결코 그렇지 않다! 우선, 동등성 검사는 다른 문법으로도 쓸 수 있다. 이를테면 e==e’ 라거나 (equal? e e’) 같은, 또는 그 밖의 숱한 표기가 있을 수 있다. 이는 함수와 연관된 명제 사이의 연결 고리가 다른 수단으로 명시적으로 제공되어야 함을, 그러니까 함수와 명제는 다른 것임을 분명히 해 준다. 더 흥미롭게도, 같은 기능을 여러 방식으로 표현할 수 있다. 예컨대 부분 순서가 있는 타입이라면 e<=e’ andalso e'<=e 같은 식으로 쓸 수 있는데, 순진한 “등호” 함수와 동일한 명세를 만족한다. 이런 경우 연결은 훨씬 느슨해지고, 당신이 직접 만들어 볼 수 있는 수많은 변형들에서는 더더욱 느슨해진다.
이런 혼동이 무슨 해를 끼칠까? 아마 가장 큰 해악은 근본적인 구분을 흐린다는 점이고, 그 결과는 온갖 좋지 않은 것으로 이어진다. 예컨대 학생이 이렇게 묻는 것은 지극히 합리적이다. 왜 함수에 대해 동등성이 정의되어 있지 않죠? 며칠 전에 한 증명에서는, 내가 구조적 귀납법으로 두 함수가 같음을 아주 세심하게 보였잖아요. 그런데 이제 와서 함수에 대한 동등성이 정의되어 있지 않다고요? 이게 무슨 소리죠? 적절한 구분을 하면 아무 문제도 없다. 물론 두 함수가 수학적으로 같다는 개념은 잘 정의되어 있다. 일반적으로는 증명이 필요할 뿐이다. 하지만 (이를테면 정수에서 정수로 가는) 두 함수가 같으면 true, 아니면 false를 돌려주는 잘 정의된 계산 가능한 함수는 존재하지 않는다. 따라서 = : (int->int) x (int->int) -> prop 은 동등성을 표현하지만, = : (int->int)->(int->int)->bool 은 방금 제시한 명세를 만족시킬 수 없다. 달리 말하면, 당신은 명제의 동등성을 _테스트_할 수 없다! (그래야만 한다.)
또 다른 해악은 앞서 언급한 불리언 맹목의 상태다. e=e’ 를 평가해 e 와 e’ 가 같은지 시험한다고 하자. 내 손에 든 것은 비트 하나다. 그 비트 자체에는 본래적 의미가 없다. 그 비트에 의미를 부여하려면 그 비트의 _출처_를 연결해 주어야 한다. “이 비트가 true라는 건 e 와 e’ 가 같다는 뜻이고, 저 다른 비트가 false라는 건 다른 어떤 두 식이 같지 않다는 뜻이다.” 이런 정보를 계속 추적(혹은 갖가지 프로그램 분석 기법으로 나중에 복구)하는 일은 악명 높게 어렵다. 비트로 할 수 있는 유일한 일은 분기하는 것뿐이고, 금세 if-then-else의 덤불 속에서 길을 잃는다. 무엇이 무엇인지 헷갈리기 시작한다. 프로그램을 조금만 진화시켜도 곧바로 바다 한가운데로 떠밀려 가고, 대체 무슨 일이 벌어지는지 알아내려면 SAT 솔버가 필요해진다.
하지만 이것 역시 또 하나의 의인성(iatrogenic) 장애의 예다! 문제는 애초에 그 비트를 계산해 버리는 데 있다. 그렇게 해 버린 순간, 손에 쥔 정보를 비트 하나로 줄여 스스로 눈을 멀게 하고, 나중에 그 비트의 출처를 기억해 정보를 다시 복구하려 든다. 이에 대한 예시는 내가 동등성 글에서 다룬 바 있다:
fun plus x y = if x=Z then y else S(plus (pred x) y)
여기서는 우리가 x 에 대해 가지고 있던 정보를 비트 하나로 으깨 버린 다음 그 값으로 분기했고, 이어서 pred 호출을 정당화하기 위해 잃어버린 정보를 복구할 수밖에 없게 된다. 보통은 인자가 0이 아님을 사실대로 되살리지 못하므로, 확실히 하려고 다시 검사해야 한다. 정말 엉망진창이다! 대신 이렇게 써야 한다.
fun plus x y = case x of Z => y | S(x’) => S(plus x’ y).
불리언은 전혀 필요 없고, 코드도 더 좋아진다! 특히, 전진하면서(en passant) 자연스럽게 전자를 얻고, 어떤 비트의 출처를 추적할 필요도 없다.
[업데이트: 마지막 문단을 삭제함.]