[{"_1":2,"_35":-5,"_36":-5},"loaderData",{"_3":4},"routes/tape",{"_5":6,"_24":22,"_25":26},"initialTree",[7,15,18,21],{"_8":9,"_10":9,"_11":12,"_13":14},"name","+.00-Preface.tape","path","type","file","title","서문",{"_8":16,"_10":16,"_11":12,"_13":17},"+.01-Advance-for-the-Readers.tape","독자를 위한 조언",{"_8":19,"_10":19,"_11":12,"_13":20},"00.01-Starting-Out.tape","0. 시작하기",{"_8":22,"_10":22,"_11":12,"_13":23},"1-type-theory.tape","1. 타입 이론","initialFilePath","initialFile",{"_13":23,"_27":28},"cells",[29],{"_30":31,"_11":32,"_33":34},"id","05295dd9-4452-4d6f-a9b0-1eb2bbb2bec4","prose","content","

신뢰 가능한 소프트웨어를 구성하는 일은 어렵다. 현대 소프트웨어는 거대해졌고, 이해관계자는 늘었으며, 요구사항은 변한다. 올바른 프로그램을 만드는 것은 거의 불가능하다. 컴퓨터 과학자와 소프트웨어 공학자는 이 문제를 해결하는 다양한 방책을 떠올렸고, 이는 팀을 관리하는 방법론 (애자일 등), 라이브러리 설계 (Pub-Sub 등), 그리고 더 나은 프로그래밍 언어를 향한 소망까지도 드러냈다. 우리는 버그가 살 수조차 없는 세계를 소망하며 마지막 논제에 집중하겠다.

버그는 프로그램이 원치 않는 성질을 갖는 것이다. 그렇다면, 프로그램의 성질을 기술하고 검증할 수 있게 된다면, 우리는 버그로부터 해방될 수 있다. 우리는 그러한 성질의 기술을 명제(Proposition)라고 부르며, 그 검증을 증명(Proof)이라고 부른다. 특히 우리는 이러한 논리 전개 과정에서 빠짐 없이 모든 성질을 증명할 수 있도록 증명 보조기(Proof Assistant)를 사용한다.

그러한 명제와 증명을 기술할 때, 우리는 불변속성(Invariant)을 바탕으로 추론하는 함수형 프로그래밍(Functional Programming) 관행을 따르며 논리 흐름을 전개할 것이다. 곧 배우겠지만, 코드를 구성하는 일은 증명을 만드는 일과 크게 다르지 않다. 특히 우리는 귀납적(Inductive) 정의를 활용해 다양한 명제를 증명해볼 것이다.

본 책은 Narya를 모티브로 개발한 프로그래밍 언어 Edhit을 사용해 다양한 증명을 다룬다. 원한다면 Rocq (전 Coq), Lean, Agda, Arend 등 다양한 대안 언어를 사용해도 좋다. 시작하자.

1차 술어 논리

프로그램의 성질을 기술할 때, 다르게 해석할 여지가 있으면 까다롭다. 내 검증이 과연 올바른 성질을 따진 것인지 알 수 없기 때문이다. 그렇기에 우리는 하나의 통일언어가 필요하다. 그리고 그 근간이 바로, 1차 술어 논리(1st Order Predicate Logic)다.

우리는 \"사람들 중 왕이 존재한다\"고 하지 않고, 기호를 써서 \"\"라고 한다. 은 for all, 는 exists라고 읽는다. 이렇게 작성한 언어는 더이상 모호하지 않다.

그렇다면 다음 질문이 떠오른다. 어떻게 해석(Interpret)할 것인가? 전통적으로 수학은 집합론(Set Theory)을 기초로 삼았다. 집합론은 존재를 선택(Choice)하는 데에 강력하다. 하지만 존재 그 자체가 값을 구성(Construct)하지 않는다.

반면 구성주의 수학의 생각은 다르다. 존재와 구성 가능성은 다른 개념이 아니다. 존재한다면 그 값에 도달할 수 있어야 한다. 증명은 단순히 논리적 타당성을 주장하는 게 아니라 값을 구하는 과정을 제시한다. 다시 말해, 증명은 알고리즘이고, 버그 없는 프로그램을 향한 도약이다.

타입은 증명을 알고리즘으로 다루는 좋은 도구다. 특히 값의 동등성을 논증하는 데에 있어 호모토피 타입 이론(Homotopy Type Theory; HoTT)는 매우 강력한 도구다. 하지만 강력한 도구에 앞서, 먼저 기초 타입 이론 지식을 다지고, 타입이 왜 증명을 다루는 좋은 도구인지 알아보겠다.

타입 이론과 집합론

집합론에서 1차 술어 논리는 명제를 서술하는 도구이고, 대상을 분류할 땐 집합의 원소 관계(Membership Relation)를 사용한다. 그 대상 사이 관계(Relation)는 순서쌍으로 나타내고, 이를 사용해 함수를 표현할 수 있다. 하지만 그렇게 정의한 함수는 알고리즘적 본질을 노출하지 않는다. 반면 타입 이론은 집합의 포함 관계 를 판단 로, 함수는 계산 가능한 -항으로 바꾼다.

","actionData","errors"]