1.9 논리학과 컴퓨터과학의 관계

1.9 논리학과 컴퓨터과학의 관계

1. 절의 학술적 목표

본 절의 학술적 목표는 논리학(logic)과 컴퓨터 과학(computer science)이 학문 분과로서 맺어 온 관계를 학술적으로 정립하는 것이다. 학습자는 본 절을 통하여 두 학문의 결합이 단순한 응용 관계가 아니라 학문적으로 깊이 결합된 상호 정초 관계임을 표준적 학술 견해 수준에서 진술할 수 있어야 하며, 그 결합이 형성한 주요 분과들을 식별할 수 있어야 한다.

2. 컴퓨터 과학의 형성과 논리학적 토대

컴퓨터 과학은 20세기 중반 이후 형성된 학문 분과이며, 그 학술적 토대는 수리 논리학(mathematical logic)과 결정 가능성(decidability) 연구에서 마련되었다. 다비트 힐베르트(David Hilbert)의 ‘결정 문제(Entscheidungsproblem)’는 1928년에 제기되었으며, 이는 1차 술어 논리(first-order predicate logic)의 보편 타당성(validity)을 결정하는 일반적 알고리즘이 존재하는가를 묻는 문제였다. 이 문제에 대한 부정적 답변은 앨런 튜링(Alan M. Turing)의 「On Computable Numbers, with an Application to the Entscheidungsproblem」(1936)과 알론조 처치(Alonzo Church)의 「An Unsolvable Problem of Elementary Number Theory」(1936)에 의하여 독립적으로 제시되었다.

이 두 논문은 ‘계산 가능성(computability)’과 ‘알고리즘(algorithm)’의 형식적 정의를 제시하였으며, 그 결과로 튜링 기계(Turing machine)와 람다 계산(lambda calculus)이라는 두 가지 동치적 형식 체계가 도입되었다. 이러한 체계들은 이후 컴퓨터 과학 전체의 학술적 출발점이 되었다.

3. 디지털 회로와 명제 논리

조지 불(George Boole)의 『An Investigation of the Laws of Thought』(1854)에서 정초된 ‘불 대수(Boolean algebra)’는 명제 논리(propositional logic)의 대수적 표현이다. 클로드 섀넌(Claude E. Shannon)은 「A Symbolic Analysis of Relay and Switching Circuits」(1938)에서 불 대수가 전기 회로의 동작을 분석·설계하는 데 사용될 수 있음을 학술적으로 보였다. 이 결과는 디지털 회로 설계의 학술적 정초가 되었으며, 이후 모든 디지털 컴퓨터의 논리적 토대를 이루었다.

4. 형식 언어 이론과 자동기계 이론

형식 언어 이론(formal language theory)과 자동기계 이론(automata theory)은 형식 논리의 자원을 통해 발전된 컴퓨터 과학의 핵심 분과이다. 노엄 촘스키(Noam Chomsky)의 『Syntactic Structures』(1957)와 「On Certain Formal Properties of Grammars」(1959)에서 도입된 ‘촘스키 위계(Chomsky hierarchy)’는 형식 문법과 그 인식 자동기계의 종류를 분류하는 표준 도식이다. 존 홉크로프트(John E. Hopcroft)와 제프리 울먼(Jeffrey D. Ullman)의 『Introduction to Automata Theory, Languages, and Computation』(1979)은 이 분과의 표준 교과서로 사용되어 왔다.

5. 프로그램 검증과 형식 의미론

형식 논리는 프로그램의 정확성(correctness)을 학술적으로 검증하는 데 사용된다. 토니 호어(C. A. R. Hoare)의 「An Axiomatic Basis for Computer Programming」(1969)에서 정식화된 ‘호어 논리(Hoare logic)’는 사전 조건(precondition), 명령(command), 사후 조건(postcondition)의 삼항 관계를 통해 프로그램의 의미를 형식적으로 기술하는 체계이다. 에츠허르 데이크스트라(Edsger W. Dijkstra)의 『A Discipline of Programming』(1976)과 데이비드 그리스(David Gries)의 『The Science of Programming』(1981)은 이 흐름의 표준 저작에 속한다.

프로그램의 의미를 형식적으로 정의하는 ‘형식 의미론(formal semantics of programming languages)’은 다나 스콧(Dana S. Scott)과 크리스토퍼 스트레이치(Christopher Strachey)의 ‘지시 의미론(denotational semantics)’ 작업, 고든 플롯킨(Gordon D. Plotkin)의 ‘구조적 작동 의미론(structural operational semantics)’ 작업을 통해 발전하였다. 이 모든 흐름은 형식 논리의 자원에 기초한다.

6. 자동 정리 증명과 모형 검사

자동 정리 증명(automated theorem proving)은 형식 논리의 정리들을 컴퓨터 알고리즘으로 자동 증명하는 분과이다. 존 앨런 로빈슨(J. Alan Robinson)의 「A Machine-Oriented Logic Based on the Resolution Principle」(1965)에서 정식화된 ‘분해 원리(resolution principle)’는 이 분과의 학술적 출발점 가운데 하나이다. 모형 검사(model checking)는 시스템의 형식적 명세(specification)를 만족하는지를 자동으로 검증하는 분과이며, 에드먼드 클라크(Edmund M. Clarke), 앨런 에머슨(E. Allen Emerson), 조지프 시파키스(Joseph Sifakis)의 일련의 작업이 그 정초에 해당한다. 이 두 분과는 모두 형식 논리, 특히 시간 논리(temporal logic)와 같은 비고전 논리에 직접적으로 의존한다.

7. 논리 프로그래밍과 형식 체계

논리 프로그래밍(logic programming)은 형식 논리의 표현과 추론을 프로그래밍 언어의 의미적 토대로 직접 사용하는 패러다임이다. 로버트 코왈스키(Robert A. Kowalski)의 「Predicate Logic as Programming Language」(1974)와 알랭 콜메라우어(Alain Colmerauer)와 동료들의 ‘Prolog’ 언어 개발이 그 학술적 출발점이다. 이 분과는 형식 논리의 술어 논리(predicate logic) 부분, 특히 ‘혼절(Horn clause)’ 부분 집합을 알고리즘적 추론의 토대로 사용한다.

8. 타입 이론과 커리-하워드 대응

타입 이론(type theory)은 형식 논리와 컴퓨터 과학이 가장 깊이 결합된 분과 가운데 하나이다. 알론조 처치의 「A Formulation of the Simple Theory of Types」(1940)에서 정식화된 단순 타입 람다 계산(simply typed lambda calculus)은 이후 페어 마르틴-뢰프(Per Martin-Löf)의 『Intuitionistic Type Theory』(1984) 등으로 발전하였다. 커리-하워드 대응(Curry–Howard correspondence)은 직관주의 논리의 증명과 람다 계산의 항(term) 사이에 구조적 일치가 성립한다는 학술적 결과이며, 윌리엄 하워드(William A. Howard)의 「The Formulae-as-Types Notion of Construction」(1980)에서 정식화되었다. 이 대응은 형식 논리와 프로그래밍 언어 이론을 동일한 수학적 구조의 두 측면으로 이해할 수 있게 하는 학술적 토대가 된다.

9. 인공 지능과 지식 표현

인공 지능(artificial intelligence) 분야에서 형식 논리는 지식 표현(knowledge representation)과 자동 추론(automated reasoning)의 표준 도구로 사용되어 왔다. 존 매카시(John McCarthy)의 「Programs with Common Sense」(1959), 레이먼드 라이터(Raymond Reiter)의 비단조 논리(non-monotonic logic) 작업, 시맨틱 웹(Semantic Web)을 위한 기술 논리(description logic)와 OWL(Web Ontology Language) 표준의 정립은 이 흐름의 대표적 사례이다. 스튜어트 러셀(Stuart J. Russell)과 피터 노빅(Peter Norvig)의 『Artificial Intelligence: A Modern Approach』(현재 4판, 2020)는 이 분야의 표준 교과서이다.

10. 본 절의 결론적 정리

본 절은 다음과 같이 정리된다. 첫째, 컴퓨터 과학은 그 학술적 토대를 수리 논리학과 계산 가능성 이론에서 마련하였으며, 따라서 논리학과 컴퓨터 과학의 관계는 단순한 응용 관계가 아니라 상호 정초 관계이다. 둘째, 디지털 회로 설계, 형식 언어 이론, 프로그램 검증, 자동 정리 증명, 모형 검사, 논리 프로그래밍, 타입 이론, 인공 지능 등 컴퓨터 과학의 핵심 분과들은 모두 형식 논리의 자원에 직접적으로 의존한다. 셋째, 커리-하워드 대응은 두 학문이 동일한 형식적 구조의 두 표현임을 보여 주는 학술적 결과이다. 넷째, 두 학문의 결합은 20세기 중반 이래 지속적으로 심화되어 왔으며, 현대 학술 환경에서 두 학문을 분리하여 이해하는 것은 사실상 불가능하다.

11. 출처

  • Boole, G. (1854). An Investigation of the Laws of Thought. London: Walton and Maberly.
  • Hilbert, D., & Ackermann, W. (1928). Grundzüge der theoretischen Logik. Berlin: Springer.
  • Turing, A. M. (1936). On Computable Numbers, with an Application to the Entscheidungsproblem. Proceedings of the London Mathematical Society, 42(1), 230–265.
  • Church, A. (1936). An Unsolvable Problem of Elementary Number Theory. American Journal of Mathematics, 58(2), 345–363.
  • Shannon, C. E. (1938). A Symbolic Analysis of Relay and Switching Circuits. Transactions of the American Institute of Electrical Engineers, 57(12), 713–723.
  • Church, A. (1940). A Formulation of the Simple Theory of Types. Journal of Symbolic Logic, 5(2), 56–68.
  • McCarthy, J. (1959). Programs with Common Sense. In Proceedings of the Teddington Conference on the Mechanization of Thought Processes (pp. 75–91). London: HMSO.
  • Chomsky, N. (1959). On Certain Formal Properties of Grammars. Information and Control, 2(2), 137–167.
  • Robinson, J. A. (1965). A Machine-Oriented Logic Based on the Resolution Principle. Journal of the ACM, 12(1), 23–41.
  • Hoare, C. A. R. (1969). An Axiomatic Basis for Computer Programming. Communications of the ACM, 12(10), 576–580.
  • Kowalski, R. A. (1974). Predicate Logic as Programming Language. In Proceedings of IFIP Congress 74 (pp. 569–574). Amsterdam: North-Holland.
  • Dijkstra, E. W. (1976). A Discipline of Programming. Englewood Cliffs: Prentice-Hall.
  • Hopcroft, J. E., & Ullman, J. D. (1979). Introduction to Automata Theory, Languages, and Computation. Reading: Addison-Wesley.
  • Howard, W. A. (1980). The Formulae-as-Types Notion of Construction. In J. P. Seldin & J. R. Hindley (Eds.), To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism (pp. 479–490). London: Academic Press.
  • Gries, D. (1981). The Science of Programming. New York: Springer.
  • Martin-Löf, P. (1984). Intuitionistic Type Theory. Naples: Bibliopolis.
  • Russell, S. J., & Norvig, P. (2020). Artificial Intelligence: A Modern Approach (4th ed.). Hoboken: Pearson.

12. 버전

  • 문서 버전: 1.0
  • 작성 기준일: 2026-04-15