8.1. Tail Recursion
Lean의 do 표기법으로 for와 while 같은 전통적인 루프 문법을 사용할 수 있지만, 이 구성은 내부적으로 재귀 함수 호출로 변환된다.
대부분의 프로그래밍 언어에서 재귀 함수는 루프에 비해 중요한 단점이 있다. 루프는 스택 공간을 사용하지 않지만 재귀 함수는 재귀 호출 수에 비례하는 스택 공간을 사용한다.
스택 공간은 보통 제한되어 있으므로 재귀 함수로 자연스럽게 표현되는 알고리즘을 명시적인 가변 힙 스택과 함께 루프로 다시 써야 하는 경우가 많다.
함수형 프로그래밍에서는 대체로 반대다. 가변 루프로 자연스럽게 표현되는 프로그램이 스택 공간을 사용할 수 있지만 이를 재귀 함수로 다시 쓰면 빠르게 실행할 수 있다. 이는 함수형 언어의 핵심 특성인 꼬리 호출 제거 때문이다. 꼬리 호출은 새 스택 프레임을 쌓지 않고 현재 프레임을 바꾸는 일반 점프로 컴파일할 수 있는 함수 호출이며, 꼬리 호출 제거는 이 변환을 구현하는 과정이다.
꼬리 호출 제거는 단순한 선택적 최적화가 아니다. 효율적인 함수형 코드를 작성하려면 꼬리 호출 제거가 반드시 필요하다. 유용하려면 신뢰할 수 있어야 한다. 프로그래머는 꼬리 호출을 확실히 식별할 수 있어야 하고 컴파일러가 이를 제거한다고 믿을 수 있어야 한다.
NonTail.sum 함수는 Nat 리스트의 원소를 더한다:
def NonTail.sum : List Nat → Nat
| [] => 0
| x :: xs => x + sum xs
이 함수를 리스트 [1, 2, 3]에 적용하면 다음 평가 단계가 나온다:
NonTail.sum [1, 2, 3]1 + (NonTail.sum [2, 3])1 + (2 + (NonTail.sum [3]))1 + (2 + (3 + (NonTail.sum [])))1 + (2 + (3 + 0))1 + (2 + 3)1 + 56
평가 단계에서 괄호는 NonTail.sum에 대한 재귀 호출을 나타낸다.
즉 세 수를 더하려면 먼저 리스트가 비어 있지 않은지 확인해야 한다.
리스트의 머리(1)를 꼬리의 합에 더하려면 먼저 꼬리의 합을 계산해야 한다:
1 + (NonTail.sum [2, 3])
그러나 리스트 꼬리의 합을 계산하려면 비어 있는지 확인해야 한다.
비어 있지 않다. 꼬리 자체가 머리에 2를 가진 리스트다.
그 다음 단계는 NonTail.sum [3]의 반환을 기다린다:
1 + (2 + (NonTail.sum [3]))
실행 시점 호출 스택의 목적은 값 1, 2, 3과 이를 재귀 호출 결과에 더하라는 명령을 추적하는 것이다.
재귀 호출이 끝나면 제어가 호출을 만든 스택 프레임으로 돌아가므로 덧셈의 각 단계를 수행한다.
리스트의 머리와 이를 더하라는 명령을 저장하는 데는 비용이 든다. 리스트 길이에 비례하는 공간이 필요하다.
Tail.sum 함수도 Nat 리스트의 원소를 더한다:
def Tail.sumHelper (soFar : Nat) : List Nat → Nat
| [] => soFar
| x :: xs => sumHelper (x + soFar) xs
def Tail.sum (xs : List Nat) : Nat :=
Tail.sumHelper 0 xs
이를 리스트 [1, 2, 3]에 적용하면 다음 평가 단계가 나온다:
Tail.sum [1, 2, 3]Tail.sumHelper 0 [1, 2, 3]Tail.sumHelper (0 + 1) [2, 3]Tail.sumHelper 1 [2, 3]Tail.sumHelper (1 + 2) [3]Tail.sumHelper 3 [3]Tail.sumHelper (3 + 3) []Tail.sumHelper 6 []6
내부 도우미 함수는 자신을 재귀 호출하지만 최종 결과를 계산하기 위해 기억할 것이 없는 방식으로 호출한다.
Tail.sumHelper가 기저 사례에 도달하면 제어를 Tail.sum으로 바로 반환할 수 있다. 중간의 Tail.sumHelper 호출은 재귀 호출 결과를 수정하지 않고 그대로 반환하기 때문이다.
즉 Tail.sumHelper의 각 재귀 호출에 스택 프레임 하나를 재사용할 수 있다.
꼬리 호출 제거가 바로 이 스택 프레임 재사용이며 Tail.sumHelper를 꼬리 재귀 함수라고 한다.
Tail.sumHelper의 첫 번째 인자에는 호출 스택이 추적해야 할 모든 정보, 즉 지금까지 만난 수의 합이 들어 있다.
각 재귀 호출에서 호출 스택에 새 정보를 추가하는 대신 이 인자를 새 정보로 갱신한다.
호출 스택의 정보를 대신하는 soFar 같은 인자를 누산기라고 한다.
집필 시점 저자의 컴퓨터에서 NonTail.sum은 원소가 216,856개 이상인 리스트를 받으면 스택 오버플로로 중단된다.
반면 Tail.sum은 스택 오버플로 없이 100,000,000개 원소의 리스트를 합할 수 있다.
Tail.sum 실행 중 새 스택 프레임을 쌓을 필요가 없으므로 현재 리스트를 보유한 가변 변수의 while 루프와 완전히 같다.
각 재귀 호출에서 스택의 함수 인자를 리스트의 다음 노드로 바꾼다.
8.1.1. Tail and Non-Tail Positions
Tail.sumHelper가 꼬리 재귀인 이유는 재귀 호출이 꼬리 위치에 있기 때문이다.
비공식적으로 함수 호출은 호출자가 반환값을 어떤 방식으로도 수정하지 않고 그대로 반환할 때 꼬리 위치에 있다.
더 형식적으로는 표현식에 대해 꼬리 위치를 명시적으로 정의할 수 있다.
match 표현식이 꼬리 위치에 있으면 각 분기도 꼬리 위치에 있다.
match가 분기를 고르면 제어는 즉시 그 분기로 진행한다.
마찬가지로 if 표현식의 두 분기는 if 표현식 자체가 꼬리 위치에 있으면 꼬리 위치에 있다.
마지막으로 let 표현식이 꼬리 위치에 있으면 그 본문도 꼬리 위치에 있다.
그 밖의 위치는 꼬리 위치가 아니다.
함수나 생성자의 인자는 꼬리 위치가 아니다. 평가할 때 인자 값에 적용할 함수나 생성자를 추적해야 하기 때문이다.
내부 함수의 본문도 꼬리 위치가 아니다. 제어가 그 함수로 넘어가지 않을 수도 있으며 함수 본문은 호출될 때까지 평가되지 않기 때문이다.
함수 타입의 본문도 마찬가지로 꼬리 위치가 아니다.
(x : α) → E에서 E를 평가하려면 결과 타입이 (x : α) → ...로 감싸져야 함을 추적해야 한다.
NonTail.sum에서는 재귀 호출이 +의 인자이므로 꼬리 위치가 아니다.
Tail.sumHelper에서는 재귀 호출이 함수 본문인 패턴 매칭 바로 아래에 있으므로 꼬리 위치에 있다.
현재 Lean은 재귀 함수의 직접 꼬리 호출만 제거한다.
즉 f의 정의에서 f에 대한 꼬리 호출은 제거하지만 다른 함수 g에 대한 꼬리 호출은 제거하지 않는다.
다른 함수의 꼬리 호출을 제거해 스택 프레임을 저장하는 일은 가능하지만 아직 Lean에 구현되지 않았다.
8.1.2. Reversing Lists
NonTail.reverse 함수는 각 부분 리스트의 머리를 결과 끝에 덧붙여 리스트를 뒤집는다:
def NonTail.reverse : List α → List α
| [] => []
| x :: xs => reverse xs ++ [x]
이를 사용해 [1, 2, 3]을 뒤집으면 다음 단계가 나온다:
NonTail.reverse [1, 2, 3](NonTail.reverse [2, 3]) ++ [1]((NonTail.reverse [3]) ++ [2]) ++ [1](((NonTail.reverse []) ++ [3]) ++ [2]) ++ [1](([] ++ [3]) ++ [2]) ++ [1]([3] ++ [2]) ++ [1][3, 2] ++ [1][3, 2, 1]
꼬리 재귀 버전은 각 단계에서 누산기에 · ++ [x] 대신 x :: ·를 사용한다:
def Tail.reverseHelper (soFar : List α) : List α → List α
| [] => soFar
| x :: xs => reverseHelper (x :: soFar) xs
def Tail.reverse (xs : List α) : List α :=
Tail.reverseHelper [] xs
이는 NonTail.reverse를 계산할 때 각 스택 프레임에 저장한 문맥이 기저 사례부터 적용되기 때문이다.
각 “기억된” 문맥 조각은 후입선출 순서로 실행된다.
반면 누산기 전달 버전은 원래 기저 사례가 아니라 리스트의 첫 원소부터 누산기를 수정하며, 다음 축약 단계에서 볼 수 있다:
Tail.reverse [1, 2, 3]Tail.reverseHelper [] [1, 2, 3]Tail.reverseHelper [1] [2, 3]Tail.reverseHelper [2, 1] [3]Tail.reverseHelper [3, 2, 1] [][3, 2, 1]즉 비꼬리 재귀 버전은 기저 사례에서 시작하여 리스트를 오른쪽에서 왼쪽으로 지나며 재귀 결과를 수정한다. 리스트 원소는 선입선출 순서로 누산기에 영향을 준다. 누산기를 사용하는 꼬리 재귀 버전은 리스트 머리에서 시작하여 리스트를 왼쪽에서 오른쪽으로 지나며 초기 누산기 값을 수정한다.
덧셈은 교환법칙을 따르므로 Tail.sum에서는 이를 고려할 필요가 없었다.
리스트 덧붙이기는 교환법칙을 따르지 않으므로 반대 방향으로 실행해도 같은 효과를 내는 연산을 찾아야 한다.
NonTail.reverse에서 재귀 결과 뒤에 [x]를 덧붙이는 것은 결과를 반대 순서로 만들 때 리스트 앞에 x를 더하는 것과 같다.
8.1.3. Multiple Recursive Calls
BinTree.mirror의 정의에는 재귀 호출이 두 개 있다:
def BinTree.mirror : BinTree α → BinTree α
| .leaf => .leaf
| .branch l x r => .branch (mirror r) x (mirror l)
명령형 언어가 보통 reverse와 sum 같은 함수에 while 루프를 사용하듯 이런 순회에는 재귀 함수를 사용한다.
적어도 이 책에서 소개한 기법으로는 이 함수를 누산기 전달 방식의 꼬리 재귀로 간단히 다시 쓸 수 없다.
보통 각 재귀 단계에 재귀 호출이 하나보다 많이 필요하면 누산기 전달 방식을 사용하기 어렵다.
이는 재귀 함수를 루프와 명시적 자료구조로 다시 쓰는 어려움과 비슷하지만 함수가 종료함을 Lean에 납득시켜야 한다는 어려움이 추가된다.
그러나 BinTree.mirror처럼 재귀 호출이 여러 개라는 것은 생성자 안에 자기 자신이 여러 번 재귀적으로 나타나는 자료구조인 경우가 많다.
이런 경우 구조의 깊이는 전체 크기의 로그에 비례하는 경우가 많으므로 스택과 힙 사이의 절충이 덜 극단적이다.
이런 함수를 꼬리 재귀로 만드는 체계적인 기법으로는 연속 전달 방식(continuation-passing style, CPS)과 탈함수화(defunctionalization) 등이 있지만, 이 책의 범위를 벗어난다.
8.1.4. Exercises
다음 비꼬리 재귀 함수들을 누산기 전달 방식의 꼬리 재귀 함수로 바꾸라:
def NonTail.length : List α → Nat
| [] => 0
| _ :: xs => NonTail.length xs + 1def NonTail.factorial : Nat → Nat
| 0 => 1
| n + 1 => factorial n * (n + 1)
NonTail.filter를 변환한 프로그램은 꼬리 재귀를 통해 일정한 스택 공간을 사용하고 입력 리스트의 길이에 선형인 시간이 걸려야 한다.
원래 프로그램에 비해 상수 배수의 오버헤드는 허용한다.
def NonTail.filter (p : α → Bool) : List α → List α
| [] => []
| x :: xs =>
if p x then
x :: filter p xs
else
filter p xs