그래서 SupGen이 다가오면서, 나는 멍청한 AI 컨텐츠가 아니기 때문에 실패할 기술 컨텐츠를 게시할 것입니다. 하지만 나는 그것을 어쨌든 하고 싶습니다. 전체성과 종결에 대한 몇 가지 생각은 다음과 같습니다. Agda(그리고 Lean?)에서는 종료가 "구조적 재귀"에 의해 보장됩니다. 즉, 인수가 "사전식 순서"로 감소할 수 있습니다. 무슨 뜻인지 아시겠어요? 네, 저도 이해 못 했습니다. 하지만 실제로는 꽤 간단합니다. 다음과 같은 절이 있다고 가정해 보겠습니다. foo : Nat → Nat foo (S a) (S b) (S c) (S d) = foo (S a) (S b) c (S (S (S d))) 푸 x = x 종료되나요? 종료되지 않나요? 어떻게 알 수 있나요? Agda에서는 다음과 같이 진행됩니다. 0단계: - LHS의 인수 0: (S a) - RHS의 인수 0: (S a) - 이것은 *동일*하므로 다음 인수를 확인하세요. (참고: LHS/RHS는 방정식의 왼쪽/오른쪽을 의미합니다) 1단계: - LHS의 인수 1: (S b) - RHS의 인수 1: (S b) - 이것은 *동일*하므로 다음 인수를 확인하세요. 2단계: - LHS에 대한 인수 2: (S c) - RHS의 인수 2: c - 이건 *더 작습니다*. 따라서 이 절은 종료됩니다! 그리고 우리는 끝났습니다. 간단히 말해서, 오른쪽에 재귀 호출이 있을 때마다 인수를 왼쪽의 해당 패턴과 하나씩 비교하여 더 작은 패턴이 나올 때까지 비교하면 됩니다. 간단하죠? (그렇게 설명할 수 있었으면 좋았을 텐데...) 이제 다음을 고려해 보세요. foo : 쌍 -> 쌍 foo (쌍 (S a) (S b)) = foo (P a (S (S (S b)))) 푸 x = x 이 함수는 종료되나요? 음, Agda에 따르면... 아닙니다! 하지만 같은 논리로 보면 분명히 그렇습니다. 첫 번째 구성 요소가 더 작으므로 두 번째 구성 요소가 더 큰 것은 중요하지 않습니다. Agda의 검사기는 인수를 청크 형태로 처리하도록 하드코딩된 것 같습니다. 따라서 이 절은 작성대로라면 종료되더라도 검사기를 통과하지 못합니다. 왜 이 이야기를 하는 걸까요? 그래서 SupGen의 재귀 생성기를 살펴보던 중, 몇 가지 변경을 통해 더 깔끔하고 *더* 빨라질 수 있다는 것을 깨달았습니다. 하지만 이러한 변경 사항이 타당한 것일까요? 테스트해 보니 놀랍게도 SupGen은 종료되지 않는 프로그램을 생성했습니다... Agda에 따르면 말이죠. 처음에는 제 접근 방식이 잘못되었다고 생각했지만, Agda는 틀렸습니다. 이제 당신은 새로운 지식을 얻었습니다. 이것이 결국 여러분에게 유용할 거라고 확신합니다!
SupGen이 종료 재귀 호출을 생성하는 데 사용하는 새로운 알고리즘은 훨씬 더 간단하고 *더* 일반적입니다!
