A Formalization of Abstract Rewriting in Agda

이 논문은 Agda 증명 보조기를 사용하여 재귀적 추상 재작성 시스템 (ARS) 을 구성주의적으로 형식화하고, 고전 논리의 사용을 최소화하면서 종료성과 합류성에 대한 표준 결과를 정교화하고 일반화하며, 이를 람다 계산 형식화 예시를 통해 입증합니다.

핵심

1. 배경: 미로 찾기 게임 (추상적 재작성 시스템)

컴퓨터 과학에서 '재작성 (Rewriting)'이란 복잡한 식이나 문장을 더 간단한 형태로 바꾸는 과정을 말합니다. 예를 들어, (2 + 2) * 3을 12로 바꾸는 것처럼요.

이 논문에서 다루는 **ARS(추상적 재작성 시스템)**는 이 과정을 거대한 미로로 비유할 수 있습니다.

• 입구: 복잡한 식 (시작점)
• 길: 식을 바꾸는 규칙들 (재작성 규칙)
• 출구: 더 이상 바꿀 수 없는 가장 간단한 형태 (정상형, Normal Form)

이 미로에서 우리는 두 가지 중요한 질문을 던집니다.

1. 종료 (Termination): 이 미로를 따라가면 결국 출구에 도달할까, 아니면 영원히 빙글빙글 돌게 될까? (무한 루프 방지)
2. 합류 (Confluence): 시작점이 같다면, 어떤 길을 가든 결국 같은 출구 (정답) 에 도달할까? (결과가 일관적인가?)

2. 문제: 고전적인 지도는 '마법'에 의존했다

기존의 수학 이론 (고전 논리) 은 이 미로 문제를 풀 때 **"만약 출구가 없다면, 그건 존재하지 않는 거야"**라고 가정하는 **마법 같은 추론 (고전 논리)**을 많이 사용했습니다.

하지만 이 연구팀은 **"그건 마법이 아니야. 실제로 길을 찾아내는 구체적인 지도 (코드) 를 보여줘야 해"**라고 주장합니다.

• 구체적인 목표: 증명하는 과정이 단순히 "옳다/틀리다"를 확인하는 것을 넘어, **실제로 정답을 찾아주는 프로그램 (코드)**이 되어야 합니다.
• 아그다 (Agda) 의 역할: 아그다는 증명과 프로그램이 하나인 언어입니다. 여기서 증명하면, 그 증명 자체가 "어떻게 정답을 찾을지" 알려주는 실행 가능한 코드가 됩니다.

3. 주요 발견: 더 나은 지도와 새로운 규칙들

연구팀은 고전적인 지도를 다시 그려보면서 다음과 같은 발견을 했습니다.

A. "약한" 조건으로도 충분하다 (뉴먼의 보조정리 개선)

기존에는 "미로가 아주 짧게만 이어져야 (강한 종료성) 정답이 하나로 정해진다"고 믿었습니다. 하지만 연구팀은 **"미로가 조금 길어지더라도, 특정 조건 (약한 합류성) 을 만족하면 정답은 여전히 하나로 정해진다"**는 것을 증명했습니다.

• 비유: "미로가 아무리 복잡해도, 분기점에서 항상 다시 합쳐지는 길이 있다면, 결국 같은 출구에 도달한다"는 것을 더 넓은 조건에서 증명해낸 것입니다.

B. '정상형 (Normal Form)'의 새로운 정의

기존에는 "더 이상 바꿀 수 없는 상태"로만 정의했지만, 연구팀은 **"최소한의 형태 (Minimal Form)"**라는 새로운 개념을 도입했습니다.

• 비유: 요리할 때 "완성된 요리"만 보는 게 아니라, "더 이상 재료를 덜어낼 수 없는 최소한의 상태"를 기준으로 삼으면, 요리 과정 (계산) 을 더 효율적으로 분석할 수 있다는 것입니다.

C. 고전 논리 없이도 가능한가?

가장 중요한 점은, 대부분의 경우 고전적인 '마법 (고전 논리)' 없이도 이 미로 문제를 해결할 수 있다는 것입니다.

• 예외: 아주 기괴하고 복잡한 미로 (예: 무한히 갈라지는 길) 에서는 고전 논리가 필요할 수 있지만, 우리가 일상에서 쓰는 대부분의 프로그래밍 언어 (람다 계산법 등) 에서는 **구체적인 계산 (코드)**만으로 모든 것을 증명할 수 있습니다.

4. 왜 이것이 중요한가? (실생활 예시)

이 연구가 왜 유용할까요?

1. 안전한 소프트웨어: 이 이론을 적용하면, "이 프로그램이 영원히 멈추지 않는다"거나 "이 계산 결과는 항상 일정하다"는 것을 자동으로 검증할 수 있습니다.
2. 효율적인 증명: 수학자가 손으로 증명하는 대신, 컴퓨터가 자동으로 증명하고 그 증명 과정을 실행 가능한 코드로 만들어줍니다.
3. 새로운 도구: 연구팀은 이 이론을 바탕으로 **람다 계산법 (함수형 프로그래밍의 기초)**을 아그다로 완벽하게 구현했습니다. 이는 향후 더 복잡한 프로그래밍 언어 이론을 개발할 때 기초 공사 (부트스트래핑) 역할을 합니다.

5. 결론: 마법 대신 공학

이 논문은 **"수학적 진리는 마법처럼 증명되는 것이 아니라, 구체적인 공학적인 과정으로 증명되어야 한다"**는 메시지를 전달합니다.

• 과거: "출구가 있을 거야. 왜냐하면 없으면 안 되니까." (고전 논리)
• 이제: "출구가 여기 있어. 이 코드를 실행하면 바로 갈 수 있어." (구체적 증명)

연구팀은 아그다라는 도구를 이용해, 추상적인 수학 이론을 실제로 작동하는 소프트웨어로 변환하는 방법을 정립했습니다. 이는 앞으로 더 안전하고 신뢰할 수 있는 프로그래밍 언어와 시스템을 만드는 데 큰 발판이 될 것입니다.

---

한 줄 요약:

"이 논문은 복잡한 컴퓨터 계산의 '미로'를 해결하는 고전적인 수학 이론을, 마법 없이 실제로 작동하는 구체적인 코드로 다시 작성하여, 더 안전하고 효율적인 소프트웨어 개발의 기초를 닦았습니다."

기술 요약

논문 요약: Agda 를 통한 추상 재작성 시스템 (ARS) 의 형식화

이 논문은 Appalachian State University 의 Samuel Arkle 와 Andrew Polonsky 에 의해 작성되었으며, Agda 증명 보조도구를 사용하여 **추상 재작성 시스템 (Abstract Rewriting Systems, ARS)**의 기본 이론을 **구축적 (constructive)**으로 형식화한 내용을 다루고 있습니다. 저자들은 Terese [8] 책에 제시된 표준 ARS 이론을 바탕으로, 고전 논리의 사용을 최소화하고 구성적 증명 (constructive proofs) 을 통해 계산 가능한 알고리즘을 도출하는 것을 목표로 했습니다.

1. 문제 제기 (Problem)

• 고전 논리의 의존성: 재작성 이론의 많은 표준 결과 (예: 뉴먼의 보조정리, 정상화 성질 등) 는 고전 논리 (배중률, 선택 공리 등) 에 의존하여 증명됩니다. 그러나 Agda 와 같은 구성적 증명 보조도구에서는 이러한 고전적 가정이 유효하지 않거나, 증명된 결과가 실제 계산 (실행 가능한 코드) 으로 이어지지 않을 수 있습니다.
• 형식화의 필요성: 프로그래밍 언어 이론 (PL) 의 메타이론을 형식화할 때, 재작성 시스템의 기본 사실들을 신뢰할 수 있는 인프라로 구축해야 합니다. 특히, 타입 이론 기반의 형식화에서는 증명 자체가 프로그램이 되어야 하므로 (Curry-Howard 동형사상), 고전 논리를 배제한 순수한 구성적 형식화가 필수적입니다.
• 결정 가능성의 부재: 많은 ARS 결과들은 관계의 결정 가능성 (decidability) 이나 유한 분기성 (finite branching) 같은 추가 가정이 없으면 구성적으로 증명하기 어렵습니다.

2. 방법론 (Methodology)

저자들은 Agda 를 사용하여 ARS 이론을 재구축하며 다음과 같은 원칙을 준수했습니다.

• 구성적 증명 (Constructive Proofs): 배중률 (Excluded Middle), 함수 확장성 (Function Extensionality), 유일성 공리 (Uniqueness of Identity Proofs), Univalence 등 모든 고전적 공리나 가정을 배제했습니다.
• 명시적 결정성 가정: 고전 논리가 필수적인 경우, 해당 결정성 가정 (예: 관계의 결정 가능성 $Rxy \lor \neg Rxy$) 을 명시적으로 명시했습니다.
• Terese [8] 기반의 형식화: 표준 텍스트인 Terese 의 정의를 따르되, 구성적 맥락에 맞게 수정하거나 일반화했습니다.
  • 정상화 (Normalization): 무한 감소 수열의 부재가 아닌, 접근성 (Accessibility) 개념을 통해 강한 정상화 (Strong Normalization, SN) 를 정의했습니다.
  • 충분 조건 일반화: '증가 함수 (Inc)'와 같은 강한 조건 대신, 더 약하고 일반적인 재귀성 (Recurrence, RP) 속성을 도입하여 정리를 일반화했습니다.
• 형식적 검증: 모든 증명과 정의는 Agda 코드로 구현되었으며, 이는 검증된 알고리즘으로 직접 실행 가능합니다.

3. 주요 기여 (Key Contributions)

3.1 ARS 속성의 계층 구조 및 새로운 개념 정의

저자들은 종료성 (Termination) 과 합류성 (Confluence) 속성 간의 논리적 관계를 체계화하고 새로운 개념을 정의했습니다.

• 새로운 속성 정의:
  • 최소 형식 (Minimal Form, MF): $a \to^* b \implies b \to^* a$를 만족하는 형식.
  • 약한/강한 최소화 (Weakly/Strongly Minimalizing, WM/SM): MF 와 관련된 속성.
  • 재귀적 속성 (RP, RP-): Terese 의 '증가 (Inc)' 속성을 대체하는 더 일반적인 개념.
• 계층 구조 분석: SN, WN, CR, WCR, NP, UN 등 다양한 속성 간의 함의 관계를 분석했습니다. 특히, 고전 논리 없이 증명 가능한 관계와 고전적 가정이 필요한 관계를 명확히 구분했습니다.

3.2 뉴먼의 보조정리 (Newman's Lemma) 의 일반화

• 기존: $SN \land WCR \implies CR$ (강한 정상화 + 약한 합류성 $\implies$ 합류성).
• 일반화: $SM \land WCR \implies CR$.
  • 저자들은 $SN$ 대신 더 약한 조건인 **강한 최소화 (Strongly Minimalizing, SM)**를 사용하여 뉴먼의 보조정리를 일반화했습니다. 이는 무한 감소가 존재하더라도 (SN 이 실패하더라도) 합류성을 보장할 수 있는 새로운 조건을 제시합니다.

3.3 잘 정의된 관계 (Well-foundedness) 에 대한 분석

• 다양한 정의 비교: 접근성 (Accessibility), 귀납성 (Inductive), 코귀납성 (Coreductive), 최소성 (Minimality) 등 다양한 '잘 정의됨'의 정의를 구성적 맥락에서 비교했습니다.
• 논리적 관계 매핑: 이 정의들 간의 함의 관계를 고전적 가정 (예: 결정 가능성, 유한 분기성, 배중률) 하에서 어떻게 연결되는지 논리 다이어그램으로 시각화했습니다.
• 결정 가능성의 중요성: $SN \implies WN$ (강한 정상화 $\implies$ 약한 정상화) 임의가 고전 논리 없이 증명 불가능함을 보였으며, 이는 관계가 **결정 가능 (decidable)**하고 **유한 분기 (finitely branching)**일 때만 성립함을 규명했습니다.

3.4 람다 계산 (Lambda Calculus) 에의 적용

• 형식화된 ARS 라이브러리를 **비정형 람다 계산 (Untyped Lambda Calculus)**에 적용하여 표준 결과 (정규화, Church-Rosser 성질 등) 를 유도했습니다.
• 중첩 타입 (nested types) 인코딩을 사용한 람다 항의 표현이 ARS 이론과 어떻게 호환되는지 보여주었습니다.

4. 결과 (Results)

1. 효과적인 형식화: 대부분의 ARS 기본 결과들을 고전 논리 없이, 즉 완전히 **효과적 (effective)**으로 형식화할 수 있음을 입증했습니다. 이는 Agda 에서 증명된 결과가 실제 계산 가능한 함수로 변환됨을 의미합니다.
2. 조건 완화: 기존 정리들의 가정을 완화했습니다. 예를 들어, Terese 의 '증가 (Inc)' 조건을 '재귀성 (RP)'으로 대체하여 더 넓은 범위의 시스템에 적용 가능하게 했습니다.
3. 고전적 가정의 식별: 어떤 정리가 성립하기 위해 어떤 고전적 원리 (예: 배중률, 결정 가능성) 가 필요한지 정밀하게 식별했습니다. 특히, $SN \implies WN$이 일반적인 관계에서는 성립하지 않으나, 유한 분기적이고 결정 가능한 관계 (예: 1 차 TRS, 람다 계산) 에서는 성립함을 보였습니다.
4. 새로운 함의 관계 발견: $SM \land WCR \implies CR$과 같은 새로운 일반화 정리를 도출했습니다.

5. 의의 (Significance)

• 프로그래밍 언어 이론의 인프라 구축: 이 작업은 Appalachian State University 의 형식화된 PL 라이브러리 개발의 '부트스트래핑 (bootstrapping)' 단계로, 향후 더 복잡한 형식화 작업의 기초를 제공합니다.
• 구현 가능한 증명: Agda 의 특성상, 이 논문에서 증명된 모든 정리는 실행 가능한 코드로 변환됩니다. 예를 들어, Church-Rosser 성질을 증명하는 것은 두 항의 공통 축소항을 계산하는 함수를 생성하는 것을 의미합니다.
• 이론적 명확성: 재작성 이론의 다양한 개념 (정상화, 합류성, 잘 정의됨) 간의 미묘한 논리적 차이를 구성적 관점에서 명확히 구분함으로써, 이론의 구조에 대한 더 깊은 이해를 제공했습니다.
• 실용성: 1 차 Term Rewriting Systems(TRS) 와 람다 계산과 같은 실제 프로그래밍 언어 이론에서 자주 접하는 시스템에 대해서는 대부분의 결과가 효과적으로 적용 가능함을 보여주었습니다.

요약하자면, 이 논문은 추상 재작성 시스템 이론을 구현 가능한 계산으로 변환하기 위해 고전 논리를 배제한 엄격한 구성적 형식화를 수행하고, 이를 통해 기존 이론의 가정을 완화하고 새로운 관계를 발견한 중요한 연구입니다.