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])
하지만 리스트 꼬리의 합을 계산하려면 프로그램은 먼저 그 꼬리가 비어 있는지 확인해야 합니다. 꼬리는 비어 있지 않습니다. 꼬리 자체가 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.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 루프를 사용하는 것처럼, 이런 종류의 순회에는 보통 재귀 함수를 사용합니다. 이 함수는 누산기 전달 스타일을 사용하여 꼬리 재귀 함수로 간단히 다시 작성할 수 없습니다. 적어도 이 책에서 소개하는 기법으로는 불가능합니다.
일반적으로 재귀 단계마다 둘 이상의 재귀 호출이 필요하다면 누산기 전달 스타일을 사용하기 어렵습니다. 이 어려움은 재귀 함수를 루프와 명시적인 자료 구조를 사용하도록 다시 작성할 때의 어려움과 비슷하며, 여기에 함수가 종료된다는 것을 Lean에게 납득시켜야 하는 복잡함이 더해집니다. 하지만 BinTree.mirror의 경우처럼, 여러 번의 재귀 호출은 자기 자신이 재귀적으로 여러 번 나타나는 생성자를 가진 자료 구조를 의미하는 경우가 많습니다. 이러한 경우 구조의 깊이는 전체 크기에 대해 로그 수준인 경우가 많으므로 스택과 힙 사이의 트레이드오프가 덜 극명해집니다. 연속 전달 스타일과 탈함수화를 사용하는 것처럼 이러한 함수를 꼬리 재귀로 만드는 체계적인 기법이 있지만, 이는 이 책의 범위를 벗어납니다.
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