AI가 수학의 정리를 증명하는 시대가 시작되고 있습니다.

Google DeepMind의 AlphaProof나 중국에서 발매된 DeepSeek-Prover와 같이, 대규모 언어 모델(Large Language Model)이 증명의 후보를 작성하고, 그것을 기계가 엄격하게 검사한다는 연구가 급속도로 늘어나고 있습니다.

머신러닝(Machine Learning)에 익숙한 분이라면, 여기에 흥미로운 대비가 있다는 것을 눈치챌 것입니다.

뉴럴 네트워크(Neural Network)의 출력은 "아마도 맞을 것이다"라고밖에 말할 수 없습니다.

하지만 기계의 검사를 통과한 수학의 증명은 "틀림없이 맞다"라고 단언할 수 있습니다.

모호함을 허용하지 않는 검사를 통과하고 있기 때문입니다.

이 "기계가 증명을 검사하거나 탐색하는 세계"의 무대 뒤에서, 일본에서는 거의 알려지지 않은 하나의 프로그래밍 언어가 작동하고 있습니다.

증명의 합격 여부를 최종 판정하는 검사 장치 그 자체로서가 아닙니다.

그 앞단에서, 밀려드는 증명 후보를 검사하고, 정돈하고, 처리해 나가는 계층

── 검사 장치가 최종 면접이라면, 서류 심사에 해당하는 계층

── 을 작성하기 위한 언어로서, 세계적인 정리 증명계(Theorem Prover)의 내부에서 가동되고 있습니다.

그 언어의 이름은 λProlog(람다 프로로그라고 읽습니다). 본 기사의 주인공입니다.

본 기사는 논리 프로그래밍(Logic Programming)도 함수형 프로그래밍(Functional Programming)도 논리학(Logic)도 배운 적이 없는 독자를 상정하고 있습니다.

전문 용어는 처음 등장할 때마다 그 자리에서 설명하겠습니다.

전제 지식은 Python 경험만으로 충분합니다.

본 기사는 상당히 긴 글입니다.

길을 잃지 않도록, 먼저 결론과 지도를 보여드리겠습니다.

λProlog는 Prolog를 고차 논리(Higher-order Logic)와 단순 타입 지정 람다 계산(Simply Typed Lambda Calculus)으로 확장한 논리형 프로그래밍 언어입니다.

λProlog의 프로그램을 실제로 구동하는 소프트웨어 ── 이를 "구현(Implementation)"이라고 부릅니다 ── 가 ELPI이며, 이 ELPI는 세계적인 정리 증명계 Rocq(구 Coq)의 공식 확장 언어인 Coq-Elpi로서 실무에서 가동되고 있습니다.

그리고 AI가 수학의 증명을 쓰는 시대 속에서, "AI의 출력을 받아들여 엄격하게 검증하며 정리 증명계로 연결하는" 가교 역할로서 그 가치를 더욱 높여갈 것입니다 ── 이것이 본 기사의 결론입니다.

오해가 없도록, 이 "가교"의 의미를 보충해 두겠습니다.

Rocq가 AI의 출력을 받기 위해서 반드시 ELPI의 검증을 거쳐야 한다는 의미는 아닙니다.

증명의 올바름을 최종적으로 보증하는 것은 어디까지나 Rocq 본체의 검사 장치(커널(Kernel)이라고 부릅니다)입니다.

그렇다면 ELPI 계층은 무엇을 검증할까요?

회사의 채용에 비유하자면, 커널이 최종 면접이고 ELPI는 서류 심사에 해당합니다.

최종 면접만으로도 합격 여부는 결정할 수 있습니다.

하지만 AI가 대량의 후보 ── 그 중 상당수는 형식이 갖춰지지 않은 불합격품 ── 를 차례차례 보내오는 시대에는, 앞단에서 후보를 검사하여 걸러내고, 정돈하고, 순차적으로 시도해 나가는 접수 계층이 필수적입니다.

이 접수 업무 ── "후보의 타입(Type)이나 형태가 요건에 맞는지에 대한 사전 검사", "불합격품에 대한 알기 쉬운 에러 반환", "후보의 변환과 재시도" ── 를 작성하기 위한 언어가 바로 ELPI입니다.

(이 메커니즘은 제5절(AI와의 접점)에서 실제 코드와 함께 확인합니다)

여기에 등장한 용어는 모두 본문에서 하나씩 설명하므로, 지금 시점에서 몰라도 괜찮습니다.

제1부(기초편) ── 전제 지식 제로 상태에서 다음 4단계로 토대를 만듭니다.

• 먼저 "논리 프로그래밍"이란 무엇인가, 그 대표 격인 Prolog란 무엇인가를 알기
• 다음으로, Prolog를 확장한 언어인 λProlog를 알기
• 그리고 "정리 증명계" ── 수학의 증명을 기계가 뒷받침하는 구조 ── 를 알기
• 마지막으로, λProlog의 구현체인 ELPI가 정리 증명계 내부에서 어떻게 작동하는지 알기

제2부(본편) ── 이 4단계를 토대로 λProlog의 역사, 기술의 핵심, 실무에서의 사용법, AI와의 접점을 깊이 있게 파고듭니다. 본편이 답하는 것은 다음 5가지 질문입니다.

• λProlog란 무엇인가?
• λProlog는 컴퓨터 사이언스(Computer Science) 전체 중에서 어디에 위치하는 언어인가?
• λProlog가 설계·개발된 동기와 목적은 무엇인가?
• Prolog와 무엇이 다른가? 채택된 고차 추상 구문(HOAS, Higher-Order Abstract Syntax)이란 무엇인가?
• Rocq의 확장인 Coq-Elpi나 Abella 등에서 어떻게 사용되며, AI·정리 증명과 어떤 접점을 갖는가?

제3부 (응용편) ── 마무리로서, λProlog를 지탱하는 8가지 개념의 정리, 코드 실례, 실무에서 위력을 발휘하는 유스케이스 (Use Case), 다른 정리 증명계와의 구분 사용법, 일본과 세계에서의 인지도, 학습 리소스, 대화편, 요약으로 이어집니다.

본문의 각 소제목에는 「기초편」 「절 1~5」 「응용편」 라벨이 붙어 있으므로, 현재 어느 부를 읽고 있는지 소제목을 통해 언제든 확인할 수 있습니다.

또한 본 기사는 λProlog의 문법을 세부적으로 해설하는 기사가 아닙니다. 문법의 상세한 내용은 기사 종반의 「학습 리소스」 절에서 소개할 1차 정보에 맡기겠습니다.

본 기사는 단독으로 읽을 수 있습니다.

전제로 읽어두어야 할 기사는 없습니다.

관련 기사는 다음과 같습니다.

• 선행 기사 ── 논리 프로그래밍은 끝나지 않았다 ── 제5세대 컴퓨터에서 LLM / AI Agent / MCP Solver까지. Prolog와 현대 클라우드 기술의 관계를 다루고 있으며, 본 기사의 배경 이해를 깊게 해줍니다.

• 자매 기사 ── F* (F Star)란 무엇인가 ── Firefox · Linux · WireGuard에서 동작하는 「증명된 코드 (Proven Code)」를 작성할 수 있는 프로그래밍 언어 입문. 「증명된 코드를 실무 시스템에 직접 통합한다」는, λProlog와는 다른 관점의 언어를 소개합니다.

• 속편 (공개 예정) ── 구현체인 ELPI와 Coq-Elpi의 메타프로그래밍 (Metaprogramming) 실무를 깊이 파고드는 자매 기사를 본 기사 다음에 공개할 예정입니다.

• 지금까지 프로그래밍 언어는 Python만을 사용해 온 엔지니어

• 논리형 프로그래밍 (Logic Programming), 고차 논리 (Higher-Order Logic), 단순 타입 지정 람다 계산 (Simply Typed Lambda Calculus)을 배울 기회가 없었던 분

• Prolog라는 이름은 들어본 적이 있지만, 자세히 접할 기회가 없었던 분

• 정리 증명계 (Rocq, Lean 4, Isabelle, Agda 등)를 학습한 적이 없는 분

• AI와 정리 증명계의 접점에 관심이 있는 분

• 메타프로그래밍 (프로그램을 조작하는 프로그램)의 세계에 관심이 있는 분

사전 지식은 필요하지 않습니다. 논리형 프로그래밍, 고차 논리, 고차 추상 구문 (HOAS, Higher-Order Abstract Syntax), 제약 조건 처리 규칙 (CHR, Constraint Handling Rules), 메타프로그래밍과 같은 개념은 등장할 때마다 본문 속에서 설명합니다.

• Prolog와 λProlog가 무엇이 다른지 알 수 있게 됩니다.
• 고차 추상 구문 (HOAS)이란 무엇인지, 이 기법으로 무엇을 할 수 있게 되는지 알 수 있게 됩니다.
• λProlog의 구현체인 ELPI가 Rocq의 Coq-Elpi, mathcomp의 Hierarchy Builder, 대화형 정리 증명계 Abella, 프로그래밍 언어 이론의 Makam 등에서 어떻게 사용되는지 알 수 있게 됩니다.
• AI 시대에서의 λProlog의 위치와, AI × 정리 증명의 이미지를 가질 수 있게 됩니다.
• 왜 λProlog가 탄생했는지, 그 역사적 경위와 학술적 동기를 알 수 있게 됩니다.
• 세계 각국의 λProlog 존재감 (유럽·미국, 중국, 러시아, 한국, 인도, 이스라엘, 일본)의 전체상을 파악할 수 있게 됩니다.

(이 절에 등장하는 전문 용어는 모두 본문 속에서 설명합니다. 여기서는 전체상만 파악해 주세요.)

• λProlog는 1987년에 Dale Miller과 Gopalan Nadathur가 발표한, Prolog를 고차 논리와 단순 타입 지정 람다 계산으로 확장한 논리형 프로그래밍 언어입니다. 「고차 추상 구문 (HOAS, Higher-Order Abstract Syntax)을 통한 바인딩 변수 (Bound Variable)의 자연스러운 처리」와 「타입 시스템 (Type System)의 도입」이 Prolog와의 근본적인 차이점입니다.

• λProlog가 탄생한 동기는 「프로그래밍 언어나 논리 체계의 의미론 (Semantics, 프로그램이나 논리식이 무엇을 의미하는지에 대한 엄밀한 정의)을 기계적으로 다룰 수 있는 프로그래밍 언어를 만들자」는 것이었습니다. 프로그래밍 언어의 타입 검사, 컴파일러의 중간 표현, 증명 보조계의 내부 데이터 구조 ── 이들은 모두 「변수의 바인딩을 포함하는 구문 트리 (Syntax Tree, 프로그램의 구조를 트리 형태로 나타낸 데이터)」를 기계적으로 조작해야 하는데, Prolog에서는 이 바인딩 처리가 부자연스러웠습니다. λProlog는 이 난제를 올바르고 자연스럽게 해결하는 언어로 설계되었습니다.

• λProlog의 주요 구현체인 ELPI는 2015년에 Cvetan Dunchev, Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi가 발표했습니다. OCaml로 작성되었으며, 다른 애플리케이션에 임베드(embed)하는 것을 목적으로 설계되었고, λProlog 표준에 제약 처리 규칙(Constraint Handling Rules, CHR)을 추가한 방언입니다.

• λProlog/ELPI의 주요 실무 용도는 Rocq(구 Coq)의 확장 언어인 Coq-Elpi입니다. Rocq의 택틱(tactic), 명령(command), 그리고 대수 구조의 계층(mathcomp를 뒷받침하는 Hierarchy Builder)과 같은 Rocq 자체의 메타프로그래밍이 ELPI로 작성되어 있습니다. 이 외에도 프로그래밍 언어 의미론(semantics)의 증명계인 Abella(Miller, Nadathur, Gacek 등), 프로그래밍 언어 이론 구현을 위한 Makam(Antonis Stampoulis) 등의 활용 사례가 있습니다.

• AI 시대에 λProlog의 학습 가치는 높다고 생각됩니다. Coq-Elpi는 Rocq와 AI를 연결하는 "택틱 기술 언어"로서 기능합니다. AI가 생성하는 코드나 택틱을 λProlog의 타입 시스템(type system)과 고차 논리(higher-order logic)의 힘으로 엄격하게 검증하는 장면에서, λProlog는 독보적인 강점을 발휘합니다.

λProlog에 관한 1차 정보는 다음 장소에서 공개되어 있습니다.

• 공식 사이트 ── https://www.lix.polytechnique.fr/Labo/Dale.Miller/lProlog/ (Dale Miller 氏가 관리)

• 주요 구현체인 ELPI의 GitHub 리포지토리 ── https://github.com/LPCIC/elpi (최신 버전 v3.7은 2026년 4월 24일에 출시)

• 또 다른 주요 구현체인 Teyjus(테이주스)의 GitHub 리포지토리 ── https://github.com/teyjus/teyjus (최신 버전 v2.1.1은 2023년 2월 8일에 출시. Gopalan Nadathur 氏가 주도, 미네소타 대학교, OCaml로 구현)

• Rocq 플러그인 Coq-Elpi의 GitHub 리포지토리 ── https://github.com/LPCIC/coq-elpi

• Abella(아벨라) 공식 사이트 ── https://abella-prover.org/

• Makam(마캄) 공식 사이트 ── https://astampoulis.github.io/makam/

• 공식 서적 "Programming with Higher-Order Logic" (Dale Miller, Gopalan Nadathur 공저, 2012년, Cambridge University Press) ── λProlog의 이론과 구현의 결정판

• Dale Miller 氏의 홈페이지 ── https://www.lix.polytechnique.fr/Labo/Dale.Miller/

• λProlog 영어 Wikipedia ── https://en.wikipedia.org/wiki/%CE%9BProlog

• 주요 학술 논문 ──
  "A logic programming approach to manipulating formulas and programs" (Miller・Nadathur, 1987년), "Uniform Proofs as a Foundation for Logic Programming" (Miller・Nadathur・Pfenning・Scedrov, ICLP 1988), "ELPI: fast, Embeddable, λProlog Interpreter" (LPAR 2015), "Elpi: an extension language for Coq" (Tassi, 2018년), "Hierarchy Builder" (Cohen・Sakaguchi・Tassi, FSCD 2020)

Python으로 프로그램을 작성할 때는 컴퓨터가 수행하기를 원하는 절차를 하나씩 지시합니다. "이 값을 받는다. 계산한다. 결과를 반환한다"라는 절차의 연속이 프로그램입니다.

논리 프로그래밍은 발상이 완전히 다릅니다. 절차를 쓰지 않습니다.

작성하는 것은 다음 두 가지뿐입니다.

사실과 규칙── 「무엇이 성립하는가」 -
질문── 「무엇을 알고 싶은가"

답을 찾는 일은 컴퓨터에 맡깁니다.

구체적인 예로 살펴보겠습니다.

다음의 두 가지 사실과 한 가지 규칙을 가정합니다.

사실 1: 지로는 타로의 아버지이다 -
사실 2: 사브로는 지로의 아버지이다 -
규칙: $X$가 $Y$의 아버지이고, $Y$가 $Z$의 아버지라면, $X$는 $Z$의 할아버지이다

여기서 "타로의 할아버지는 누구인가?"라고 질문하면, 컴퓨터는 사실과 규칙을 자동으로 조합하여 "사브로입니다"라고 답해줍니다.

작성자는 찾는 방법을 단 한 줄도 쓰지 않았습니다. 이것이 논리 프로그래밍 (Logic Programming)입니다.

이 발상을 처음으로 형태화한 언어가 Prolog (프롤로그)입니다.

1972년 프랑스 마르세유 대학교에서 Alain Colmerauer와 Philippe Roussel이 개발했습니다.

이름은 Programming in Logic (논리에 의한 프로그래밍)에서 유래했습니다.

앞서 말한 가계도 예시는 Prolog에서 다음과 같이 작성합니다.

father(jiro, taro). % 지로는 타로의 아버지이다 (사실)
father(saburo, jiro). % 사브로는 지로의 아버지이다 (사실)
% X가 Y의 아버지이고, Y가 Z의 아버지라면, X는 Z의 할아버지이다 (규칙)
...

그리고 질문을 던집니다.

?- grandfather(G, taro). % 타로의 할아버지 G는 누구인가?
G = saburo. % 답: 사브로

여기서 father나 grandfather와 같은 부품을 **"술어 (Predicate)"**라고 부릅니다.

이 용어는 본 기사를 관통하는 가장 중요한 용어이므로, 확실히 설명해 두겠습니다.

국어 시간에 배웠던 "주어와 술어"를 떠올려 보세요.

"타로는 학생이다"라는 문장에서 "──는 학생이다" 부분이 술어였습니다.

논리학의 술어도 이와 같은 발상으로, 한마디로 말하면 **"빈칸이 있는 문장"**입니다.

• "** ext{ extunderscore extunderscore}**는 짝수이다" ── 빈칸이 하나인 술어. 빈칸에 $4$를 넣으면 참(True), $7$을 넣으면 거짓(False)이 됩니다.
• "** ext{ extunderscore extunderscore}**는 ** ext{ extunderscore extunderscore}**의 아버지이다" ── 빈칸이 두 개인 술어. (지로, 타로) 순으로 넣으면 참, (타로, 지로) 순이면 거짓이 됩니다.

빈칸을 모두 채우면 참인지 거짓인지 결정되는 문장이 됩니다 ── 이것이 술어입니다.

Python으로 치면 def is_even(x): return x % 2 == 0과 같이 참/거짓을 반환하는 함수가 정확히 술어에 해당하며, 함수의 인자(Argument)가 "빈칸"에 대응합니다.

앞서 본 코드의 father(jiro, taro)는 " ext{ extunderscore extunderscore}는 ext{ extunderscore extunderscore}의 아버지이다"라는 빈칸 두 개인 술어에 지로와 타로를 넣은 문장이었던 셈입니다.

또한 grandfather(X, Z) :- father(X, Y), father(Y, Z).와 같이 "$A$ 이고 $B$ 가 성립한다면 $C$ 가 성립한다"라는 형태의 식을 **"Horn 절 (Horn Clause)"**라고 부릅니다.

미국의 논리학자 Alfred Horn (1918-2001, UCLA)이 1951년에 제안한 형식입니다.

Prolog의 프로그램이란, 결국 Horn 절의 집합입니다.

Prolog가 무엇을 대신 처리해 주고 있는지 실감하기 위해, 동일한 "할아버지 찾기"를 Python으로 작성해 보겠습니다.

facts = {("jiro", "taro"), ("saburo", "jiro")} # (아버지, 아들)의 집합
def grandfather(z):
    """z의 할아버지를 찾는다"""
    ...

Python에서는 "사실의 집합을 이중 루프(Double Loop)로 전수 조사하고, 연결 고리(y1 == y2)를 직접 대조한다"라는 탐색 절차를 작성자가 전부 작성합니다.

Prolog 버전으로 작성한 것은 규칙 한 줄뿐이었습니다.

탐색도 대조도 언어 측의 업무였던 것입니다.

또 다른 큰 차이점이 있습니다.

Python의 grandfather(z)는 "손자를 전달하면 할아버지가 반환되는" 일방향 함수입니다.

반면 Prolog의 grandfather(X, Z)는 관계 (Relation)이므로, 동일한 한 줄 그대로 역방향으로도 사용할 수 있습니다.

?- grandfather(saburo, W). % Saburo의 손주 W는 누구인가? (방금 전과 반대 방향의 질문)
W = taro.

Python에서는 역방향이 필요해지면 함수를 하나 더 작성해야 할 것입니다.

관계를 작성하면 질문의 방향은 자유롭다 ── 이것이 논리 프로그래밍 (Logical Programming)의 즐거움입니다.

Prolog는 ISO 표준으로 표준화되어 있으며, SWI-Prolog, GNU Prolog, SICStus Prolog 등의 구현체가 있습니다.

1980년대에는 일본의 국가 프로젝트인 「제5세대 컴퓨터」의 핵심 언어로도 선정되었습니다.

Prolog와 현대 클라우드 기술(AWS Cedar, Neo4j Cypher, Datalog 등)과의 관계는, 「논리 프로그래밍은 끝나지 않았다 ── 제5세대 컴퓨터에서 LLM / AI Agent / MCP Solver로」(2026년 5월 19일 공개)에서 논하였습니다.

괜찮으시다면 함께 확인해 보시기 바랍니다.

**Prolog의 추론 엔진 (Inference Engine)**은 두 가지 기본 조작을 조합하여 답을 찾습니다.

첫 번째는 **「단일화 (Unification)」**입니다.

두 식의 형태를 맞추어 보며, 아직 결정되지 않은 변수에 들어갈 값을 찾아내는 조작입니다.

예를 들어 grandfather(G, taro)

라는 질문과 규칙의 헤드(Head) grandfather(X, Z)

를 맞추어 보면, 「G와 X는 같은 것, Z는 taro」라는 대응을 찾을 수 있습니다.

Python의 딕셔너리(Dictionary)로 말하자면 {"name": "太郎", "age": 30}

와 {"name": X, "age": 30}

을 비교하여 X = "太郎"

라고 결정하는 것과 같습니다.

두 번째는 **「백트래킹 (Backtracking)」**입니다.

어떤 선택에서 막히게 되면, 직전의 갈림길까지 돌아가서 다른 선택을 시도하는 움직임입니다.

미로를 풀 때, 막다른 길에 다다르면 분기점까지 되돌아가는 것과 같은 발상입니다 (알고리즘에서 말하는 깊이 우선 탐색 (Depth-First Search)에 해당합니다).

「단일화로 식을 대조하고, 실패하면 백트래킹으로 돌아간다」

── 이 반복이 논리 프로그래밍의 심장부입니다.

실제로, 앞서 언급한 「타로의 할아버지는 누구인가?」에 대해 Prolog가 답하기까지의 움직임을 단계별로 따라가 보겠습니다.

질문: grandfather(G, taro)
단계 1: 규칙의 헤드 grandfather(X, Z)와 질문을 단일화
→ X = G, Z = taro로 결정됨
...

「가령 결정하며 나아가고, 막히면 돌아가서 다른 후보를 시도한다」

── 컴퓨터가 이 시행착오를 자동으로 수행해주므로, 작성자는 사실과 규칙만을 작성하면 됩니다.

Prolog에 대해 알게 되었으니, 본 기사의 주인공으로 넘어가겠습니다.

λProlog는 1987년에 Dale Miller (당시 University of Pennsylvania, 현재 INRIA & LIX/École polytechnique)와 Gopalan Nadathur (당시 Duke University, 현재 University of Minnesota)가 발표한 언어입니다.

읽는 법은 「람다 프로로그」, 영어로는 Lambda Prolog입니다.

한마디로 말하면, λProlog는 **「Prolog를 고차 논리 (Higher-order Logic)와 단순 타입 람다 계산 (Simply Typed Lambda Calculus)이라는 두 가지 수학적 도구로 강화한 언어」**입니다.

이 두 가지 도구를 차례로 설명하겠습니다.

먼저, Prolog의 절(Clause)에서 설명한 「술어 (Predicate) = 빈칸이 있는 문장」을 떠올려 보십시오.

「 extunderscore 는 짝수이다」, 「 extunderscore 는 extunderscore 의 아버지이다」와 같이, 빈칸을 모두 채우면 참/거짓이 결정되는 문장이 술어였습니다.

논리의 세계에는 빈칸을 하나씩 값으로 채우는 대신, 「모든 ~에 대하여, …가 성립한다」, 「어떤 ~가 존재하여, …가 성립한다」라고 한꺼번에 서술하는 방식이 있습니다.

이를 **「양화 (Quantification)」**라고 부르며, 「모든」, 「어떤」을 나타내는 기호를 **「양화사 (Quantifier)」**라고 부릅니다.

여기서부터가 본론입니다.

1차와 고차를 나누는 것은 단 하나의 질문입니다.

── 빈칸에 넣어도 되는 것, 「모든」이라고 말해도 되는 것은 무엇인가?

1차 논리 (First-order Logic)의 답은 「사물뿐」입니다.

사람, 수치, 문자열과 같은 구체적인 대상만이 빈칸에 들어갈 수 있으며, 양화(quantification)의 대상이 될 수 있습니다.

• 「모든 정수 $x$에 대하여, $x + 0 = x$가 성립한다」 ── $x$는 사물(수). 1차 논리로 쓸 수 있음
• 「모든 사람 $p$에 대하여, $p$에게는 아버지가 있다」 ── $p$는 사물(사람). 1차 논리로 쓸 수 있음
• 「어떤 정수 $x$가 존재하여, $x \times x = 4$가 성립한다」 ── 이것도 1차 논리로 쓸 수 있음

Prolog가 다룰 수 있는 것은 바로 이 1차 논리(First-order Logic)입니다.

**고차 논리 (Higher-order Logic)**의 답은 **「술어(predicate)나 함수(function) 그 자체도 넣어도 된다」**입니다.

그러면, 문에 대한 문, 성질에 대한 문을 쓸 수 있게 됩니다.

구체적인 예시를 두 가지 살펴보겠습니다.

예 1 ── 「대칭적이다」라는 술어

「friend(친구) 라는 관계는 대칭적이다.

$A$가 $B$의 친구라면 $B$도 $A$의 친구이기 때문이다.

하지만 father(아버지) 라는 관계는 대칭적이지 않다」

── 우리는 일상에서도 이런 문장을 사용합니다.

자세히 보면, 이 문장의 주어는 사람이 아니라, friend나 father라는 관계 그 자체입니다.

제대로 풀어 쓰면 다음과 같습니다.

「관계 $R$이 대칭적이라는 것은, 모든 $x$와 $y$에 대하여, $R(x, y)$라면 $R(y, x)$가 성립하는 것」

빈칸 $R$에 들어가 있는 것은 술어입니다.

즉 「대칭적이다」는 술어를 빈칸으로 취하는 술어 ── 한 단계 높은 술어입니다.

1차 논리에는 $R$을 양화할 수단이 없기 때문에, 이 정의 자체를 쓸 수 없습니다.

예 2 ── 수학적 귀납법

「어떤 성질 $P$에 대해서도, $P$가 $0$에서 성립하고, 『$n$에서 성립한다면 $n + 1$에서도 성립한다』라고 말할 수 있다면, $P$는 모든 자연수에 대해 성립한다」

이것은 수학적 증명의 근간을 이루는 귀납법의 원리입니다.

도입부가 「어떤 성질 $P$에 대해서도」 ── 성질(술어)에 대한 양화 ── 로 시작한다는 점에 주목해 주세요.

귀납법의 원리는 본래 고차 문장이며, 1차 논리로는 하나의 문장으로 풀어 쓸 수 없습니다.

정리 증명(theorem proving)의 세계에서 고차 논리가 필요로 하는 이유가 벌써 여기서 드러나고 있습니다.

λProlog가 다룰 수 있는 것은 바로 이 고차 논리입니다.

「고차(higher-order)」라는 말은 익숙할지도 모릅니다.

Python에서는 함수를 인자로 받는 함수나, 함수를 반환값으로 반환하는 함수를 「고차 함수 (higher-order function)」라고 부릅니다.

sorted(["banana", "apple", "fig"], key=len) # 함수 len을 인자로 전달
map(str.upper, ["a", "b"]) # 함수 str.upper를 인자로 전달
def make_adder(n): # 함수를 반환값으로 반환하는 함수
...

고차 함수란 「함수를 수치나 리스트와 같은 값으로서 주고받을 수 있는 함수」를 말했습니다.

고차 논리는 그 논리 버전으로, 「술어나 함수를 사물과 같은 취급으로 빈칸에 넣거나 양화할 수 있는 논리」입니다.

대응 관계를 표로 나타내면 다음과 같습니다.

두 경우 모두 「고차」의 의미는 같으며, 「한 단계 높은 것까지 대상으로 삼을 수 있다」는 뜻입니다.

「계층 (order)」은 말하고자 하는 대상의 단계를 나타냅니다.

사물에 대해 말하는 것이 1차, "사물에 대해 말하는 술어"에 대해 말하는 것이 2차

── 2차 이상을 통칭하여 고차라고 부릅니다.

서적에 따라서는 「1차 술어 논리」라는 표기도 보이지만, 「1차 논리」와 같은 것입니다 (술어와 양화를 갖춘 논리를 「술어 논리」라고 부르며, 그 1차 버전·고차 버전이라는 의미입니다).

마찬가지로 「고차 술어 논리」와 「고차 논리」도 같은 개념을 가리킵니다.

본 기사에서는 짧게 「1차 논리」, 「고차 논리」로 통일하겠습니다.

또 다른 도구는 「단순 타입 람다 계산 (simply typed lambda calculus)」입니다. 1940년에 Alonzo Church (미국 Princeton 대학. 컴퓨터 과학의 이론적 기초를 쌓은 수학자 중 한 명)가 제안한 체계로, 한마디로 말하면 「타입이 지정된 함수를 수학적으로 엄밀하게 다루기 위한 체계」입니다.

용어를 분해해 봅시다.

「람다 (Lambda)」란, 이름을 붙이지 않고 그 자리에서 함수를 작성하는 표기법을 말합니다. Python의 lambda x: x + 1에서 lambda는 바로 이 체계에서 유래되었습니다. 수학적 표기법으로는 $\lambda x. x + 1$이라고 쓰며, 이를 「람다 추상 (Lambda Abstraction)」이라고 부릅니다.

「타입 (Type)」이란, 값의 종류에 대한 약속입니다. Python의 타입 힌트(Type Hint)인 def add(x: int, y: int) -> int:가 나타내는 「정수 2개를 받아 정수를 반환한다」라는 약속이 바로 타입입니다.

즉, 단순 타입 지정 람다 계산 (Simply Typed Lambda Calculus)이란 「람다 식과 타입 힌트의 세계를 수학으로서 정립한 것」입니다. Haskell이나 OCaml과 같은 「함수형 프로그래밍 언어 (Functional Programming Language)」── 계산을 함수의 조합으로 기술하는 방식의 언어군 ── 의 타입 이론은 모두 이 체계를 근원으로 합니다.

Prolog에는 실무에서 사용할수록 뼈저리게 느껴지는 두 가지 약점이 있었습니다.

이 약점을 코드로 살펴보겠습니다.

Prolog에서는 다음과 같이 명백히 이상한 사실도 아무런 불평 없이 받아들여집니다.

father(jiro, taro).
father(42, taro). % 「42는 타로의 아버지」!? Prolog는 그냥 통과시킨다

숫자 $42$가 사람의 이름이 들어갈 자리에 섞여 들어와도, Prolog는 아무런 경고를 하지 않습니다.

버그는 실행 시점에 이상한 결과가 나올 때까지 잠복합니다.

이는 Python에서 타입 힌트나 검사 없이 코드를 작성하고 있을 때와 같은 상황입니다.

같은 내용을 $\lambda$Prolog (ELPI 구문)로 작성하면, 타입 선언이 추가됩니다.