왜 Lean 인가🔗

Reynolds의 각 장은 대체로 같은 세 작업을 반복한다. 대상 언어의 구문을 정하고, 구문을 의미 공간으로 보내는 함수를 정의하고, 그 함수가 만족해야 할 성질을 증명한다. Lean에서는 구문 데이터, 실행 가능한 예제, 정리와 증명을 서로 참조하는 한 소스 트리에 둘 수 있다.

§1.1의 추상 구문부터 차이가 보인다. Reynolds는 생성자의 단사성, 같은 반송자로 가는 생성자 치역의 서로소성, 모든 구가 유한하게 생성된다는 조건을 명시한다. Lean의 inductive 선언은 이에 대응하는 no-confusion 원리와 재귀·귀납 원리를 함께 만든다.

inductive IntExp (V : Type u) where
  /-- 정수 상수. Reynolds의 `c₀, c₁, c₂, …`를 음의 정수까지 일반화했다. -/
  | num : Int → IntExp V
  /-- 변수. Reynolds의 `c_var` — 변수를 정수 식으로 넣어 주는 생성자다.
      §1.4 명제 1.2(b)에서 이것이 "항등 치환"으로 작동한다는 사실이 쓰인다. -/
  | var : V → IntExp V
  /-- 단항 마이너스 `- e`. -/
  | neg : IntExp V → IntExp V
  /-- 이항 연산 `e₀ op e₁`. -/
  | bin : IntOp → IntExp V → IntExp V → IntExp V
  deriving DecidableEq, Repr

위 코드 블록은 손으로 옮겨 적은 것이 아니다. 저장소의 Reynolds/Answers/Ch01/Syntax.lean 에서 그대로 인용한 것이고, 소스가 바뀌면 이 문서의 빌드가 실패한다.