8.1. 꼬리 재귀
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])
하지만 목록의 나머지 부분(tail)의 합을 계산하려면 프로그램은 그것이 비어 있는지 확인해야 합니다. 그렇지 않습니다—꼬리는 그 자체로 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.sumHelper의 중간 호출들이 재귀 호출의 결과를 수정 없이 그대로 반환할 뿐이기 때문에 제어를 곧바로 Tail.sum으로 돌려줄 수 있습니다. 다시 말해, Tail.sumHelper의 각 재귀 호출마다 동일한 스택 프레임을 재사용할 수 있습니다. 꼬리 호출 제거(tail-call elimination)는 바로 이러한 스택 프레임의 재사용을 말하며, Tail.sumHelper는 꼬리 재귀 함수라고 불립니다.
Tail.sumHelper의 첫 번째 인자는 그렇지 않으면 호출 스택에서 추적해야 했을 모든 정보, 즉 지금까지 마주친 숫자들의 합을 담고 있습니다. 각 재귀 호출에서 이 인자는 호출 스택에 새로운 정보를 추가하는 대신 새로운 정보로 갱신됩니다. soFar처럼 호출 스택의 정보를 대신하는 인자를 누산기라고 부릅니다.
이 글을 쓰는 시점, 저자의 컴퓨터에서 NonTail.sum은 216,856개 이상의 항목을 가진 리스트를 전달받으면 스택 오버플로로 중단됩니다. 반면 Tail.sum은 스택 오버플로 없이 1억 개의 원소로 이루어진 리스트를 합산할 수 있습니다. Tail.sum을 실행하는 동안 새로운 스택 프레임을 푸시할 필요가 없으므로, 이는 현재 리스트를 담는 가변 변수를 사용하는 while 루프와 완전히 동등합니다. 각 재귀 호출마다, 스택에 있는 함수 인자는 단순히 리스트의 다음 노드로 대체됩니다.
8.1.1. 꼬리 위치와 비꼬리 위치
Tail.sumHelper가 꼬리 재귀인 이유는 재귀 호출이 꼬리 위치에 있기 때문입니다. 비형식적으로 말하자면, 함수 호출은 호출자가 반환된 값을 어떤 식으로든 수정할 필요 없이 그대로 곧바로 반환하는 경우에 꼬리 위치에 있다고 합니다. 좀 더 형식적으로, 꼬리 위치는 표현식에 대해 명시적으로 정의될 수 있습니다.
match-표현식이 꼬리 위치에 있다면, 그 각 분기 역시 꼬리 위치에 있습니다. match가 분기를 선택하면, 제어는 즉시 해당 분기로 넘어갑니다. 마찬가지로, if-표현식 자체가 꼬리 위치에 있다면 if-표현식의 두 분기 모두 꼬리 위치에 있습니다. 마지막으로, let-표현식이 꼬리 위치에 있다면, 그 본문 또한 꼬리 위치에 있는 것입니다.
그 외의 모든 위치는 꼬리 위치가 아닙니다. 함수나 생성자의 인자는 꼬리 위치에 있지 않습니다. 이는 평가 과정에서 인자의 값에 적용될 함수나 생성자를 계속 추적해야 하기 때문입니다. 내부 함수의 본문은 제어가 아예 전달되지 않을 수도 있기 때문에 꼬리 위치에 있지 않습니다. 함수 본문은 함수가 호출되기 전까지는 평가되지 않습니다. 마찬가지로, 함수 타입의 본문은 꼬리 위치에 있지 않습니다. (x : α) → E에서 E를 평가하려면, 결과 타입에 (x : α) → ...가 감싸져야 한다는 것을 추적해야 합니다.
NonTail.sum에서는 재귀 호출이 +의 인자이기 때문에 꼬리 위치에 있지 않습니다. Tail.sumHelper에서 재귀 호출은 함수 본문 자체인 패턴 매칭 바로 아래에 있기 때문에 꼬리 위치에 있습니다.
이 글을 쓰는 시점에서, Lean은 재귀 함수 내의 직접적인 꼬리 호출만 제거합니다. 이는 f의 정의 안에 있는 f에 대한 꼬리 호출은 제거되지만, 다른 함수 g에 대한 꼬리 호출은 제거되지 않는다는 것을 의미합니다. 다른 함수로의 꼬리 호출을 제거하여 스택 프레임을 절약하는 것은 분명히 가능하지만, 이는 아직 Lean에 구현되어 있지 않습니다.
8.1.2. 리스트 뒤집기
함수 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로 계산하는 동안 각 스택 프레임에 저장된 컨텍스트가 기저 사례부터 시작하여 적용되기 때문입니다. "기억된" 각 컨텍스트 조각은 후입선출(last-in, first-out) 순서로 실행됩니다. 반면, 누산기를 전달하는 버전은 다음의 축약 단계들에서 볼 수 있듯이, 원래의 기저 사례가 아니라 목록의 첫 번째 항목부터 시작하여 누산기를 수정합니다.
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. 여러 개의 재귀 호출
BinTree.mirror의 정의에는 두 개의 재귀 호출이 있습니다:
def BinTree.mirror : BinTree α → BinTree α
| .leaf => .leaf
| .branch l x r => .branch (mirror r) x (mirror l)
명령형 언어에서 reverse나 sum과 같은 함수에 일반적으로 while 루프를 사용하는 것처럼, 이런 종류의 순회에는 일반적으로 재귀 함수를 사용합니다. 이 함수는 누산기 전달 방식(accumulator-passing style)을 사용하여 꼬리 재귀로 간단히 다시 작성할 수 없습니다. 적어도 이 책에서 소개한 기법으로는 그렇게 할 수 없습니다.
일반적으로 각 재귀 단계마다 둘 이상의 재귀 호출이 필요한 경우, 누산기 전달 방식을 사용하기 어렵습니다. 이 어려움은 재귀 함수를 루프와 명시적 자료 구조를 사용하도록 다시 작성하는 것의 어려움과 유사하며, 여기에 해당 함수가 종료함을 Lean에게 납득시켜야 한다는 복잡함이 추가됩니다. 하지만 BinTree.mirror에서처럼, 여러 개의 재귀 호출은 종종 자기 자신에 대한 재귀적 출현이 여러 번 있는 생성자를 가진 데이터 구조를 나타냅니다. 이러한 경우 구조의 깊이는 전체 크기에 대해 로그 함수 형태를 띠는 경우가 많으며, 이 때문에 스택과 힙 사이의 트레이드오프가 덜 극명해집니다. 연속 전달 스타일(continuation-passing style)과 탈함수화(defunctionalization)를 사용하는 것과 같이 이러한 함수들을 꼬리 재귀로 만드는 체계적인 기법들이 있지만, 이는 이 책의 범위를 벗어납니다.
8.1.4. 연습문제
다음의 꼬리 재귀가 아닌 각 함수를 누산기를 전달하는 꼬리 재귀 함수로 변환하십시오:
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