종료 검사
종료 검사 (Termination Checking)
모든 재귀 함수가 허용되는 것은 아니에요. Agda는 기계적으로 종료함을 증명할 수 있는 재귀 스킴만 받아들여요.
원시 재귀 (Primitive recursion)
가장 단순한 경우, 주어진 인자가 각 재귀 호출에서 정확히 하나의 생성자만큼 작아야 해요. 이 스킴을 원시 재귀(primitive recursion)라고 불러요. 몇 가지 올바른 예:
plus : Nat → Nat → Nat
plus zero m = m
plus (suc n) m = suc (plus n m)
natEq : Nat → Nat → Bool
natEq zero zero = true
natEq zero (suc m) = false
natEq (suc n) zero = false
natEq (suc n) (suc m) = natEq n m
plus와 natEq는 둘 다 원시 재귀로 정의돼요.
plus의 재귀 호출은 n이 suc n의 부분 표현식이므로(n이 suc n보다 구조적으로 작으므로) OK예요. 따라서 plus가 재귀적으로 호출될 때마다 첫 번째 인자가 점점 작아져요. 자연수는 유한한 개수의 suc 생성자만 가질 수 있으므로 plus는 항상 종료한다는 것을 압니다.
natEq도 같은 이유로 종료하지만, 이 경우 natEq의 첫 번째와 두 번째 인자 모두가 감소한다고 말할 수 있어요.
구조 재귀 (Structural recursion)
Agda의 종료 검사기는 원시 재귀만이 아니라 구조 재귀(structural recursion)도 허용해요.
이는 재귀 호출이 인자의 (엄격한) 부분 표현식에 있어야 함을 의미해요 (아래 fib 참고) — 이것은 한 번에 하나의 생성자를 빼는 것보다 더 일반적이에요.
fib : Nat → Nat
fib zero = zero
fib (suc zero) = suc zero
fib (suc (suc n)) = plus (fib n) (fib (suc n))
또한 인자가 사전식(lexicographic) 순서로 감소할 수 있음을 의미해요 — 이것은 중첩된 원시 재귀로 생각할 수 있어요 (아래 ack 참고).
ack : Nat → Nat → Nat
ack zero m = suc m
ack (suc n) zero = ack n (suc zero)
ack (suc n) (suc m) = ack n (ack (suc n) m)
ack에서 첫 번째 인자가 감소하거나, 같게 유지되고 두 번째 인자가 감소해요. 이것은 사전식 순서와 같아요.
with-함수 (With-functions)
프래그마와 옵션 (Pragmas and Options)
NON_TERMINATING 프래그마
이것은 영향을 받는 함수를 종료하는 것으로 취급하지 않는 TERMINATING의 더 안전한 버전이에요.
이는 NON_TERMINATING 함수가 타입 체킹 중에 축약되지 않는다는 뜻이에요. 물론 런타임과 C-u C-c C-n으로 대화형으로 호출할 때는 축약돼요.
이 프래그마는 Agda 2.4.2에서 추가됐어요.
TERMINATING 프래그마
개별 함수 정의와 상호 블록에 대해 종료 검사기를 꺼서 그것들을 종료하는 것으로 표시해요. Agda 2.4.2.1부터 NO_TERMINATION_CHECK 프래그마를 대체했어요.
프래그마는 함수 정의 또는 상호 블록 앞에 와야 해요. 프래그마는 --safe 모드에서 사용할 수 없어요.
예:
단일 정의 건너뛰기: 타입 시그니처 앞:
{-# TERMINATING #-}
a : A
a = a
단일 정의 건너뛰기: 첫 번째 절 앞:
b : A
{-# TERMINATING #-}
b = b
옛 스타일 상호 블록 건너뛰기: mutual 키워드 앞:
{-# TERMINATING #-}
mutual
c : A
c = d
d : A
d = c
옛 스타일 상호 블록 건너뛰기: 타입 시그니처나 첫 번째 함수 절 앞의 상호 블록 어딘가:
mutual
{-# TERMINATING #-}
e : A
e = f
f : A
f = e
새 스타일 상호 블록 건너뛰기: 블록 안의 타입 시그니처나 첫 번째 함수 절 앞 어디든:
g : A
h : A
g = h
{-# TERMINATING #-}
h = g
--termination-depth로 최대 분석 깊이 늘리기
다음 상호 함수들은 종료 검사기가 받아들이도록 종료 깊이(termination depth) 2가 필요해요:
mutual
f : Nat → Nat
f zero = zero
f (suc zero) = suc zero
f (suc (suc x)) = g x
g : Nat → Nat
g y = f (suc y)
종료 깊이 1로는 종료 검사기가 f에서 g로의 호출이 인자를 감소시키고 g에서 f로의 호출이 인자를 증가시킨다는 것만 등록할 뿐 얼마나 되는지는 등록하지 않아요.
따라서 호출 순서 f → g → f가 인자를 감소시킨다는 증거가 없어요.
종료 깊이 2로는 f → g 호출이 2만큼 감소하고 g → f 호출은 단지 1만큼만 증가한다는 것을 볼 수 있어서, f → g → f의 전체 감소는 여전히 1이에요.
일반적으로 종료 깊이 N은 감소를 최대 N까지, 증가를 최대 N-1까지 추적할 수 있어요.
Agda는 먼저 종료 깊이 1로 종료 검사를 하고, 종료 검사가 성공하거나 최대 종료 깊이에 도달할 때까지 이 값을 증가시켜요. 최대 깊이는 기본적으로 3(Agda 2.9.0부터)이고 --termination-depth로 설정할 수 있어요.
실제로는 최대 종료 깊이를 늘릴 필요가 없어야 해요. 깊이 2를 사용하는 예도 이미 드물기 때문이에요.
높은 종료 깊이는 종료 검사기를 느리고 메모리 많이 사용하게 만들 수 있어요. 종료 깊이를 늘리는 대신 함수를 구조 재귀적, 즉 한 레벨만 깊게 매칭하도록 재구성해야 해요.
참고 문헌 (References)
Andreas Abel, Foetus – termination checker for simple functional programs