F-대수와 fold: 재귀와 귀납의 범주론(Initial algebras and folds)

목록 [3, 1, 4, 1, 5]의 합을 재귀로 적으면 두 줄입니다. 빈 목록의 합은 0이고, 맨 앞 원소⁠(element)⁠ a와 나머지 r로 된 목록의 합은 a + (r의 합)입니다. 목록을 '맨 앞 원소를 나머지 앞에 붙이는' 연산 ∷로 적으면 [3, 1, 4, 1, 5] = 3 ∷ (1 ∷ (4 ∷ (1 ∷ (5 ∷ []))))이고, 합을 구하는 일은 이 식에서 ∷를 +로, []를 0으로 바꿔 쓴 것과 같습니다. 3 + (1 + (4 + (1 + (5 + 0)))) = 14. 곱은 ∷를 ×로, []를 1로 바꾸고, 길이는 ∷를 '1 +'로, []를 0으로 바꿉니다. 자연수도 마찬가지입니다. 5는 0에 '다음 수' S를 다섯 번 붙인 S(S(S(S(S(0)))))이고, $2^5$은 0을 1로, S를 '2 ×'로 바꾼 2 × (2 × (2 × (2 × (2 × 1)))) = 32입니다. 이렇게 생성자(값을 짓는 연산: [], ∷, 0, S)를 다른 값과 연산으로 바꿔 끼워 계산하는 일을 fold(접기)라 합니다.

바꿔 끼울 것: , 자연수일 때 n = .

이 계산이 늘 같은 모양이라는 것을 범주론⁠(category theory)⁠으로 적으면 이렇습니다. 자연수의 생성자는 '원소 하나(0)'와 '함수⁠(function)⁠ 하나(S)'입니다. 이 둘을 한데 묶으면 함수 $[0, S]: 1 + \mathbb N\to\mathbb N$ 하나가 됩니다. 여기서 1은 원소가 하나인 집합⁠(set)⁠이고 +는 서로소 합집합⁠(disjoint union)⁠이라, 1 + ℕ에서 나가는 함수는 '1의 원소가 갈 곳'과 'ℕ에서 나가는 함수'의 쌍입니다. 일반적으로 집합에서 집합으로 가는 함자⁠(functor)⁠ F가 있을 때, 집합 X와 함수 $\alpha: F(X)\to X$의 쌍을 F-대수(F-algebra)라 합니다. $F(X) = 1 + X$이면 F-대수는 '원소 하나와 X → X 함수 하나를 가진 집합'이고, $F(X) = 1 + A\times X$이면 '원소 하나와 A × X → X 함수 하나를 가진 집합'입니다. (ℕ, 0, S)와 (A의 목록 전체, [], ∷)가 각각의 예입니다. A가 정수⁠(integer)⁠일 때 (정수, 0, +)도 목록 쪽 F-대수이고, (정수, 1, 2 ×)는 자연수 쪽 F-대수입니다.

두 F-대수 사이의 준동형은 구조를 지키는 함수입니다. $h: (X, \alpha)\to(Y, \beta)$가 준동형이라는 것은 $h\circ\alpha = \beta\circ F(h)$, 곧 '먼저 X에서 짓고 h로 옮기든, 먼저 h로 옮기고 Y에서 짓든 같다'는 뜻입니다. Y의 구조가 원소 $y_0$와 함수 t라 하면, 자연수 쪽에서는 이 식이 두 등식 $h(0) = y_0$, $h(S\,n) = t(h(n))$로 풀립니다. 재귀 정의의 두 줄 그대로입니다. 목록 쪽이면 $h([\,]) = y_0$, $h(a \mathbin{::} r) = t(a, h(r))$입니다. 합은 (목록, [], ∷)에서 (정수, 0, +)로 가는 준동형이고, $2^n$은 (ℕ, 0, S)에서 (정수, 1, 2 ×)로 가는 준동형입니다. F-대수와 준동형은 다시 범주⁠(category)⁠를 이룹니다.

그 범주의 시작 대상⁠(initial object)⁠, 곧 다른 모든 F-대수로 가는 준동형이 정확히 하나씩 있는 대수를 시작 대수(initial algebra)라 하고 $\mu F$로 적습니다(보편 성질⁠, universal property⁠). 그 하나뿐인 준동형이 fold이고, 카타모피즘(catamorphism)이라고도 부릅니다. (ℕ, 0, S)가 $1 + X$의 시작 대수라는 것을 풀어 쓰면, 아무 집합 Y와 원소 $y_0$, 함수 $t: Y\to Y$가 주어져도 $h(0) = y_0$, $h(n+1) = t(h(n))$인 함수 $h: \mathbb N\to Y$가 있고, 하나뿐이라는 문장입니다. '있다'는 재귀로 함수를 정의해도 된다는 보증입니다. 당연해 보이지만 증명이 필요한 사실이라, 데데킨트가 1888년 『수란 무엇이며 무엇이어야 하는가』에서 이 재귀 정리⁠(recursion theorem)⁠를 따로 증명했습니다. '하나뿐'은 수학적 귀납법입니다. 두 함수 h, h′이 모두 두 등식을 만족하면, 두 함수가 같은 값을 주는 n들의 집합은 0을 포함하고 n을 포함하면 n + 1도 포함하므로 모든 자연수입니다.

거꾸로 유일성에서 귀납법이 나옵니다. 0을 포함하고 S로 닫힌 부분집합⁠(subset)⁠ P ⊆ ℕ가 있다고 합시다. P는 (P, 0, S) 자체로 F-대수입니다. 시작 대수에서 P로 가는 준동형을 따라간 뒤 P를 ℕ에 넣으면 ℕ에서 ℕ으로 가는 준동형이 되는데, 항등 함수도 그런 준동형이므로 유일성에 따라 둘은 같습니다. 그러면 모든 n이 P를 거쳐 가니 P = ℕ입니다. 곧 수학적 귀납법은 시작 대수의 '하나뿐'이 하는 말이고, 재귀로 정의하는 것은 시작 대수의 '있다'가 하는 말입니다. 목록에 대해서도 같은 논증으로 '빈 목록에서 성립하고, r에서 성립하면 a ∷ r에서도 성립하면 모든 목록에서 성립한다'는 구조적 귀납법⁠(structural induction)⁠이 나옵니다.

유일성은 계산에 쓸모 있는 법칙을 공짜로 줍니다. 첫째, 생성자를 생성자 그대로 바꿔 끼운 fold는 항등 함수입니다. 그림에서 '생성자 그대로'를 골라 보세요. 항등 함수도 두 등식을 만족하고, 그런 함수는 하나뿐이기 때문입니다. 둘째, 융합 법칙(fusion law)입니다. 대수 (Y, y₀, t)에서 (Z, z₀, u)로 가는 준동형 k가 있으면 $k\circ\mathrm{fold}(y_0, t) = \mathrm{fold}(z_0, u)$입니다. 왼쪽도 시작 대수에서 Z로 가는 준동형이라 오른쪽과 같을 수밖에 없습니다. 예를 들어 k(s) = 2s는 (정수, 0, +)에서 (정수, 0, (a, s) ↦ 2a + s)로 가는 준동형이므로(2(a + s) = 2a + 2s), '합을 구한 뒤 두 배'는 '원소마다 두 배 해서 더하기'와 같습니다. [3, 1, 4, 1, 5]라면 둘 다 28입니다. 목록을 한 번만 훑고 중간 결과를 만들지 않는 이런 변환을 컴파일러⁠(compiler)⁠가 자동으로 합니다. 1993년 앤디 길, 존 런치베리, 사이먼 페이턴 존스가 Haskell 컴파일러 GHC에 넣은 foldr/build 융합이 그 예입니다.

모든 재귀가 곧바로 한 칸짜리 fold인 것은 아닙니다. 피보나치 수 $F(n+1) = F(n) + F(n-1)$은 앞의 값 두 개가 필요합니다. 이때는 값을 쌍으로 들고 다니면 됩니다. 쌍 (F(n), F(n + 1))을 (F(n + 1), F(n) + F(n + 1))로 미는 함수를 S 자리에 끼우면 fold가 됩니다(그림의 '피보나치 쌍'). 같은 방법으로, h(n + 1)이 h(n)뿐 아니라 n에도 기대는 원시 재귀는 (n, h(n))의 쌍으로 접는 fold로 적힙니다. 값이 함수인 fold를 허용하면 더 멀리 갑니다. 1928년 빌헬름 아커만이 제시한, 원시 재귀로는 적을 수 없는 아커만 함수도 'ℕ에서 ℕ으로 가는 함수'를 값으로 삼는 fold로 적힙니다(괴델의 체계 T가 이런 언어입니다). 반면 '1에 닿을 때까지 n이 짝수면 반으로, 홀수면 3n + 1로'처럼 입력의 구조를 따라 줄어들지 않는 되부름은 fold가 아니고, 이 경우 모든 n에서 끝나는지는 아직 아무도 모릅니다(콜라츠 추측). fold는 유한한 값의 구조를 따라 한 칸씩 내려가므로, 바꿔 끼운 연산들이 끝나기만 하면 언제나 끝납니다. 증명 보조기⁠(proof assistant)⁠가 구조적 재귀만 그대로 받아들이는 까닭이 이것입니다.

시작 대수에는 놀라운 성질이 하나 더 있습니다. 1968년 요아힘 람벡이 증명한 람벡 보조정리(Lambek's lemma)에 따르면, 시작 대수의 구조 사상 $\alpha: F(\mu F)\to\mu F$는 동형 사상입니다. $\mathbb N\cong 1 + \mathbb N$, $\mathrm{List}\,A\cong 1 + A\times\mathrm{List}\,A$, 곧 모든 자연수는 0이거나 어떤 수의 다음 수이고, 모든 목록은 비어 있거나 맨 앞 원소와 나머지로 정확히 한 가지 방법으로 나뉩니다. 프로그래밍의 패턴 매칭⁠(matching)⁠이 이 역사상 $\alpha^{-1}$입니다. 증명의 뼈대는 이렇습니다. $F(\mu F)$도 $F(\alpha)$를 구조로 삼는 F-대수이므로 준동형 $\beta: \mu F\to F(\mu F)$가 하나 있고, $\alpha\circ\beta$는 $\mu F$에서 자기 자신으로 가는 준동형이라 항등입니다. 그러면 $\beta\circ\alpha = F(\alpha)\circ F(\beta) = F(\alpha\circ\beta) = \mathrm{id}$입니다. 곧 시작 대수는 방정식 $X\cong F(X)$의 해, F의 고정점⁠(fixed point)⁠이고, 유한한 값만 모은 가장 작은 고정점입니다. 목록이라면 $\varnothing\subseteq F(\varnothing)\subseteq F(F(\varnothing))\subseteq\cdots$, 곧 길이 0 이하, 1 이하, 2 이하인 목록들을 차례로 모아 합치면 얻어집니다(1974년 이르지 아다메크가 이 구성이 통하는 조건을 정리했습니다). 가장 작은 고정점을 이렇게 되풀이로 찾는 일은 영역 이론⁠(domain theory)⁠에서 가장 작은 고정점을 찾는 클리니 반복과 같은 모양입니다.

람벡 보조정리⁠(lemma)⁠는 '없다'는 판정에도 쓰입니다. 집합을 멱집합⁠(power set)⁠으로 보내는 함자 P에는 시작 대수가 없습니다. 있다면 $X\cong P(X)$일 텐데, 칸토어의 대각선 논법⁠(Cantor's diagonal argument)⁠에 따르면 어떤 집합도 자기 멱집합과 크기가 같지 않기 때문입니다. 반대로 상수, +, ×로 지은 함자(다항식⁠(polynomial)⁠ 함자)에는 늘 시작 대수가 있고, 그래서 대수적 자료형⁠(algebraic data type)⁠으로 정의한 타입마다 fold가 하나씩 따라옵니다. 방향을 모두 뒤집은 짝도 있습니다. 무한히 이어지는 수열(스트림)은 $X\mapsto A\times X$의 '끝 쌍대 대수⁠(terminal coalgebra)⁠'로, 여기서는 시작 대수의 fold 대신 값을 한 칸씩 펼쳐 내는 unfold가, 귀납법 대신 쌍대 귀납(coinduction)이 일합니다.

개수를 세는 생성함수⁠(generating function)⁠도 람벡의 동형⁠(isomorphism)⁠에서 나옵니다. 이진 나무는 잎⁠(leaf)⁠ 하나이거나 마디 하나에 나무 두 그루를 단 것이므로 $T\cong 1 + T\times T$입니다. 이 전단사⁠(bijective)⁠는 마디 수를 지키므로(오른쪽의 마디 수는 두 그루의 마디 수에 1을 더한 것), 마디가 n개인 나무의 수 $t_n$을 계수로 삼은 급수⁠(series)⁠ $T(x) = \sum t_n x^n$은 $T(x) = 1 + x\,T(x)^2$을 만족합니다. 여기서 동형은 집합 사이의 글자 그대로의 사실이고, 급수의 등식은 그 전단사가 크기를 지킨다는 데서 나온 결과입니다. 풀면 계수가 1, 1, 2, 5, 14, …인 카탈랑 수⁠(Catalan number)⁠가 나옵니다. 자연수 위의 fold $h(n+1) = t(h(n))$은 한 단계짜리 점화식⁠(recurrence relation)⁠이기도 합니다. 점화식의 해가 하나로 정해진다는 것이 곧 시작 대수의 유일성입니다.

이 관점은 1970년대에 대수적 명세 연구(조지프 고겐 등, 1977)에서 '시작 대수 의미론'으로 자리 잡았고, 1990년 무렵 그랜트 맬컴, 에릭 메이어, 마르턴 포킹아, 로스 패터슨이 프로그램 변환의 도구로 다듬었습니다. 메이어 등의 1991년 논문 제목 「바나나, 렌즈, 봉투, 가시철사로 하는 함수형 프로그래밍」의 '바나나'가 fold를 적는 괄호입니다. 증명 보조기 Lean과 Rocq(옛 이름 Coq)에서는 귀납적으로 정의한 타입마다 '재귀자⁠(recursor)⁠'가 자동으로 생기는데, 그 타입이 바로 귀납법의 명제입니다. 결과의 타입이 입력에 따라 달라지도록 fold를 넓힌 것이 귀납법이라는 뜻이고, 커리–하워드 대응⁠(Curry–Howard correspondence)⁠으로 읽으면 '재귀로 정의한 프로그램'과 '귀납법으로 한 증명'이 같은 것입니다.

이어지는 곳. 목록과 나무를 합과 곱으로 짓는 방법은 대수적 자료형에서, 시작 대상과 '하나뿐인 화살표'의 뜻은 보편 성질에서 볼 수 있습니다. fold는 재귀를 한 가지 틀로 모으고, 그 틀의 유일성이 수학적 귀납법이며, 한 단계짜리 점화식과 피보나치 수열⁠(Fibonacci sequence)⁠이 그 가장 작은 예입니다. 가장 작은 고정점을 되풀이로 찾는 방법은 영역 이론에서 끝나지 않는 재귀의 뜻을 정할 때 다시 나오고, 멱집합 함자에 시작 대수가 없다는 것은 대각선 논법⁠(diagonal argument)⁠의 또 다른 얼굴입니다. 동형 $T\cong 1 + T^2$에서 개수를 읽는 법은 생성함수와 카탈랑 수로 이어집니다. 목록 위의 fold가 모노이드⁠(monoid)⁠ 준동형이 되는 경우는 모노이드의 foldMap에서, 재귀자의 타입이 귀납법이라는 것은 의존 타입⁠(dependent type)⁠과 증명 보조기에서 이어집니다.