§1.1 추상 구문🔗

프로그램을 글자 열과 그 글자 열이 가리키는 대상으로 나눠 생각할 필요가 있다. 1 + 2 * 3은 전자이고, 연산자와 피연산자로 이루어진 트리는 후자다.

글자 열이라고 하면 곤란해진다. 1 + 2 * 3과 1 + (2 * 3)은 다른 글자 열인데 같은 것을 말한다. 반대로 1 + 2 * 3 하나가 곱셈을 먼저 하는 트리와 덧셈을 먼저 하는 트리 둘 다로 읽힐 수도 있다. 우선순위 규칙이 그 애매함을 없애 주지만, 그건 읽는 방법에 관한 규칙이지 프로그램 자체에 관한 것이 아니다.

Reynolds는 그래서 둘을 나눈다.

구체 구문(concrete syntax): 사람이 쓰고 읽는 글자 열. 우선순위, 괄호, 공백이 여기 산다.
추상 구문(abstract syntax): 그 글자 열이 가리키는 트리. 1 + 2 * 3의 추상 구문은 뿌리가 +이고 오른쪽 가지가 * 인 트리 하나다. 우선순위는 이미 소진되어 사라졌다.

의미를 주고 성질을 증명하는 일은 전부 추상 구문 위에서 한다. 구체 구문은 §1.1의 Notation.lean에서 DSL 로 따로 다룬다.

트리를 트리답게 만드는 세 조건🔗

"트리" 라고 말만 해서는 부족하다. 트리들의 집합이 어떤 집합이어야 하는지를 못박아야 구조적 귀납법 같은 도구를 쓸 수 있다. Reynolds가 손으로 부과하는 조건이 셋이다.

생성자(constructor)가 단사(injective)다. e₀ + e₁과 e₀' + e₁'이 같은 트리면 e₀ = e₀'이고 e₁ = e₁'이다. 이것이 없으면 트리를 보고 부분식을 되찾을 수 없다.
서로 다른 생성자의 치역(range)이 서로소(disjoint)다. 어떤 트리도 "덧셈이면서 동시에 변수" 일 수 없다. 이것이 없으면 경우를 나누는 정의가 서지 않는다.
모든 원소가 유한 번의 생성자 적용으로 만들어진다. 생성자로 도달할 수 없는 정체불명의 원소가 없다는 뜻이다. 이것이 없으면 구조적 귀납법이 거짓말이 된다 — 모든 생성자 경우를 증명해도 남는 원소가 있을 수 있으니까.

1과 2를 합쳐 no confusion, 3을 no junk라고 부르기도 한다. 이것은 구문 반송자의 생성 원리를 설명하는 말이다. 임의의 목표 대수로 가는 준동형이 유일하다는 초기성의 보편 성질은 여기서 한 단계 더 나아간 명제이며, Depth/Algebra.lean에서 따로 증명한다.

Lean에서는 선언 한 번이 이 셋을 준다🔗

inductive로 타입을 선언하면 위 셋이 자동으로 성립한다. 별도로 공리를 놓지 않는다. 확인해 보면 이렇다.

/-- 조건 1. 생성자는 단사다. `injection`이 바로 처리한다. -/
example : Function.Injective (IntExp.var (V := V)) := fun _ _ h => byV:Type un:ℤv:Vx✝¹:Vx✝:Vh:IntExp.var x✝¹ = IntExp.var x✝⊢ x✝¹ = x✝ injection hAll goals completed! 🐙

/-- 조건 2. 서로 다른 생성자의 치역은 서로소다. -/
example : IntExp.num (V := V) n ≠ IntExp.var v := byV:Type un:ℤv:V⊢ IntExp.num n ≠ IntExp.var v nofunAll goals completed! 🐙

-- 조건 3. 모든 정수 식은 유한 번의 생성자 적용으로 만들어진다.
-- 별도의 `True` 증명이 아니라, Lean이 생성한 재귀자 자체가 유한 구성을 따라가는 원리다.
Reynolds.Answers.Ch01.IntExp.rec.{u_1, u} {V : Type u} {motive : IntExp V → Sort u_1}
  (num : (a : ℤ) → motive (IntExp.num a)) (var : (a : V) → motive (IntExp.var a))
  (neg : (a : IntExp V) → motive a → motive a.neg)
  (bin : (a : IntOp) → (a_1 a_2 : IntExp V) → motive a_1 → motive a_2 → motive (IntExp.bin a a_1 a_2)) (t : IntExp V) :
  motive t#check IntExp.rec

세 번째 조건이 구조적 귀납법(structural induction)을 정당하게 만든다. 1장의 증명은 거의 전부 구조적 귀납법이므로, 이 조건이 빠지면 손에 남는 것이 없다. 조건 3은 별도의 명제를 증명한 것이 아니라 IntExp.rec라는 재귀자의 타입으로 확인한다. induction e with …를 쓸 때마다 그 재귀자를 부르고 있다.

한 가지 더 짚을 것이 있다. 위 IntExp 선언에는 (V : Type u) 라는 매개변수가 붙어 있다. 변수 이름의 타입을 문자열로 고정하지 않고 열어 둔 것이다. Reynolds는 ⟨var⟩를 "표현이 지정되지 않은 가산 무한 집합"이라고 두지만, 구문·의미·일치 정리에는 가산성이 필요하지 않아 여기서는 임의의 V로 일반화했다. 따라서 유한 타입도 허용한다. 포획 회피 치환에서만 유한 집합 밖의 이름을 고르는 HasFresh V를 요구한다. 이 조건은 무한성은 주지만 가산성까지 요구하지 않는다. 예제에서는 V = String으로 읽으면 된다.

단언(assertion)의 구문은 이렇게 생겼다.

inductive Assert (V : Type u) where
  /-- 참 `true`. -/
  | tru
  /-- 거짓 `false`. -/
  | fls
  /-- 정수 비교 `e₀ ∼ e₁`. -/
  | cmp : Cmp → IntExp V → IntExp V → Assert V
  /-- 부정 `¬p`. -/
  | not : Assert V → Assert V
  /-- 이항 논리 연산 `p₀ ∘ p₁`. -/
  | bin : LogOp → Assert V → Assert V → Assert V
  /-- 양화 `∀v. p` / `∃v. p`. **결합 구성자**. -/
  | quant : Quant → V → Assert V → Assert V
  deriving DecidableEq, Repr

마지막 절이 이 장에서 유일하게 새로운 것이다. quant는 변수를 묶는다. 정수 식(integer expression)에는 결합자(binder)가 없어서 자유·속박 구분이 생기지 않았는데, 여기서 생긴다.

종이에서는 "이런 조건을 만족하는 집합이 있다고 하자" 로 시작해서 그 집합을 끝까지 만들지 않는다. Lean에서는 선언 한 번이 그 집합을 실제로 만든다.

범주론 렌즈로 보면🔗

Reynolds의 세 조건을 범주론의 말로 다시 쓰면, 구문 반송자는 초기 대수다 — 모든 목표 대수로 가는 준동형이 꼭 하나 있다는 뜻이다. inductive 선언 한 번이 그 대수를 즉시 만들어 준다. 책이 식 (1.2)에서 층별로 쌓아 올리는 구성은 그 초기 대수를 짓는 표준적인 방법 하나이고, 초기성 자체에서 구조적 귀납법과 유일한 "접기(fold)"가 둘 다 따라 나온다. 범주론 어휘를 몰라도 본문은 이 문단 없이 완결된다. 자세한 증명은 선택 심화에 있다.