Formally Verified Linear-Time Invertible Lexing

Each language version is independently generated for its own context, not a direct translation.

1. 문제 상황: "레고 블록을 다시 조립할 수 있을까?"

컴퓨터가 텍스트를 읽을 때, 이를 레고 블록에 비유해 볼 수 있습니다.

원문 (Input): 긴 레고 벽돌 줄입니다.
분석 (Lexing): 컴퓨터가 이 벽돌들을 잘게 나누어 "이것은 '문자' 블록, 저것은 '숫자' 블록"이라고 분류하는 작업입니다.
출력 (Printing): 분류된 블록들을 다시 원래대로 조립하여 텍스트를 만드는 작업입니다.

기존의 문제점:
기존의 컴퓨터 분석기들은 "이 블록이 '문자'다"라고 분류하는 데는 능숙했지만, 분류된 블록을 다시 조립했을 때 원래 텍스트와 정확히 똑같은지를 보장하지 못했습니다.

예시: "val x = 1"이라는 문장이 있습니다. 분석기가 공백을 무시하고 "val", "x", "=", "1"로 나눕니다.
만약 개발자가 이 블록들을 다시 조립할 때 공백을 잘못 넣으면 "val x=1"이 됩니다.
이걸 다시 분석하면, 컴퓨터는 "x="를 하나의 이름으로 잘못 인식할 수 있습니다. 정보를 잃어버린 (되돌릴 수 없는) 상태가 된 것입니다.

2. ZipLex 의 해결책: "완벽한 거울"

ZipLex 는 이 문제를 해결하기 위해 두 가지 핵심 아이디어를 사용합니다.

A. "되돌릴 수 있는" 분석 (Invertibility)

ZipLex 는 단순히 텍스트를 분류하는 것을 넘어, 분류된 블록을 다시 조립하면 반드시 원래 텍스트가 나오도록 설계되었습니다.

비유: 마치 거울을 보는 것과 같습니다. 거울에 비친 모습 (분류된 토큰) 을 다시 거울에 비추면 (다시 텍스트로 변환), 원래의 내 얼굴 (원래 텍스트) 과 100% 똑같아야 합니다.
이를 위해 ZipLex 는 "이 블록은 원래 이 글자에서 왔어"라는 정보를 잃지 않고 저장합니다.

B. "부드러운" 연결 (Separability)

가장 어려운 점은 인접한 블록을 합칠 때입니다.

비유: "cat"과 "dog"라는 블록이 있다고 칩시다. 그냥 붙이면 "catdog"이 됩니다. 하지만 "ca"와 "t"를 붙이면 "cat"이 되고, "t"와 "a"를 붙이면 "ta"가 되어 의미가 달라질 수 있습니다.
ZipLex 는 블록들이 서로 붙었을 때 혼동되지 않도록 미리 규칙을 정해둡니다. (예: "cat" 다음에 "dog"가 오면 안전하지만, "ca" 다음에 "t"가 오면 위험할 수 있으니 미리 체크합니다.)
이 규칙을 **R-Path(경로)**라고 부르는데, 마치 레고 블록의 연결 부위가 서로 딱 맞아야만 (Separable) 조립이 가능하다는 안전장치와 같습니다.

3. 속도 문제: "기억력 좋은 비서" (Memoization)

보통 "정확한 것"과 "빠른 것"은 상충됩니다. ZipLex 는 메모이제이션 (Memoization) 기술을 써서 이 딜레마를 해결했습니다.

비유: ZipLex 는 아주 똑똑한 비서입니다. 이전에 "이런 패턴을 분석했더니 이 결과가 나왔어"라고 계산한 적이 있다면, 그 결과를 메모장에 적어둡니다.
나중에 똑같은 패턴이 나오면, 처음부터 다시 계산하지 않고 메모장에서 바로 가져옵니다.
덕분에 ZipLex 는 텍스트 길이에 비례해서 선형적으로 (Linear) 매우 빠르게 작동합니다. (기존의 정밀한 분석 도구들은 텍스트가 길어지면 속도가 급격히 느려지는 '이차 함수' 형태였는데, ZipLex 는 직선처럼 일정하게 빠릅니다.)

4. 왜 이것이 중요한가요? (실제 효과)

이 논문은 ZipLex 가 실제로 얼마나 강력한지 증명했습니다.

정확성 보장: 수학적으로 증명된 (Formally Verified) 코드이므로, "이 토큰을 다시 조립하면 원래 글자가 나온다"는 것을 100% 확신할 수 있습니다.
압도적인 속도: 기존에 검증된 도구들 (Verbatim++, Coqlex 등) 보다 100 배 (두 자릿수) 이상 빠릅니다.
- 비유: 다른 검증된 도구들이 "정밀한 수작업"을 하느라 느리다면, ZipLex 는 "정밀한 수작업의 원리를 알고 있는 로봇"처럼 빠릅니다.
실용성: JSON 파일 정렬이나 프로그래밍 언어 분석 같은 실제 업무에서도 잘 작동하며, 텍스트 길이가 아무리 길어져도 속도가 떨어지지 않습니다.

요약

ZipLex는 "컴퓨터가 텍스트를 분석할 때, 실수하지 않고 (정확성), 다시 원상복구도 가능하게 (되돌림), 그리고 아주 빠르게 (선형 속도)" 처리해주는 새로운 도구입니다.

마치 완벽한 레고 조립 키트처럼, 한 번 분해한 블록을 다시 조립하면 절대 모양이 변하지 않고, 그 과정이 매우 효율적으로 이루어지도록 만든 것입니다. 이는 미래의 안전한 소프트웨어와 컴파일러를 만드는 데 큰 발걸음이 될 것입니다.

Each language version is independently generated for its own context, not a direct translation.

이 논문은 ZipLex이라는 이름의 형식적으로 검증된 (Formally Verified) 가역적 (Invertible) 선형 시간 어휘 분석 (Lexing) 프레임워크를 제안합니다. 저자들은 EPFL 소속으로, Scala 와 Stainless 증명 도구를 사용하여 이 시스템을 구현하고 검증했습니다.

다음은 논문의 주요 내용을 기술적으로 요약한 것입니다.

1. 문제 정의 (Problem)

기존의 어휘 분석기 (Lexer) 는 주로 정규식과 '최대 매칭 (Longest Match/Maximal Munch)' semantics 를 만족하는지 검증하는 데 초점을 맞추었습니다. 그러나 많은 실제 응용 프로그램 (IDE 리팩토링, 프로그램 합성, 직렬화/역직렬화 등) 에서는 어휘 분석 (Lexing) 과 텍스트 출력 (Printing) 이 서로 역함수 (Inverse) 관계를 이루어야 합니다.

가역성 (Invertibility) 문제: 토큰 시퀀스를 텍스트로 출력한 후 다시 어휘 분석을 수행했을 때, 원래의 토큰 시퀀스와 정확히 일치해야 합니다.
실제 사례: val x = 1과 같은 코드에서 공백을 제거하여 val x=1로 만들면, x_와 같은 식별자 규칙이 있는 경우 x_=1로 해석되어 원래 토큰 시퀀스 (val, x_, =, 1) 와 달라지는 문제가 발생합니다.
기존 한계: 기존 검증된 어휘 분석기 (Coqlex, Verbatim++ 등) 는 가역성을 보장하지 않거나, 성능이 선형 시간이 아닌 이차 시간 ( $O(n^2)$ ) 을 보이는 경우가 많았습니다.

2. 방법론 (Methodology)

ZipLex 는 가역성과 선형 시간 복잡도를 동시에 달성하기 위해 다음과 같은 핵심 기법들을 결합했습니다.

A. 분리 가능성 (Separability) 및 R-Path 조건

가역성을 보장하기 위해 토큰 시퀀스가 '분리 가능 (Separable)'해야 함을 정의했습니다.

R-Path 조건: 인접한 두 토큰 $t_1, t_2$ 가 결합되었을 때, $t_1$ 이 $t_2$ 의 첫 번째 문자와 결합되어 더 긴 토큰으로 잘못 인식되지 않도록 하는 조건을 정의합니다.
구체적 정의: $sep(t_1, t_2)$ 는 $t_1$ 과 $t_2$ 의 첫 글자가 결합된 문자열이 어떤 규칙에도 매칭되지 않음을 의미합니다.
PrintableTokens: 이 조건을 만족하는 토큰 시퀀스를 감싸는 추상 타입을 제공하여, 슬라이싱 (Slicing) 과 연결 (Concatenation) 시 분리 가능성 불변량을 효율적으로 유지합니다. 연결 시에는 경계에서만 상수 시간 ( $O(1)$ ) 의 확인이 필요합니다.

B. 정규식 엔진 및 최적화

Brzozowski 의 Derivatives: 정규식 매칭의 기초로 사용되며, 입력 문자열을 한 번만 순회하며 매칭을 수행합니다.
Huet 의 Zippers: 정규식을 '컨텍스트 (Context)'의 집합으로 표현하는 Zippers 를 도입하여, Derivative 연산 시 발생하는 표현식의 폭발 (Expression blow-up) 을 방지하고 메모이제이션을 효율적으로 적용할 수 있게 했습니다.
Tail Recursion: JVM 의 스택 오버플로우를 방지하기 위해 모든 재귀 함수를 꼬리 재귀 (Tail-recursive) 형태로 구현하고, 이를 증명과 실행 코드 간에 연결했습니다.

C. 검증된 메모이제이션 (Verified Memoization)

선형 시간 ( $O(n)$ ) 복잡도를 달성하기 위해 메모이제이션을 적용했습니다.

검증된 해시 테이블: Scala 의 LongMap을 기반으로 한 검증된 가변 해시 테이블을 사용하여, 메모이제이션 캐시를 효율적으로 관리합니다.
최장 매칭 알고리즘: 단순 재귀 대신 인덱스를 기반으로 한 꼬리 재귀 알고리즘을 설계하고, 명시적인 스택을 통해 캐시를 업데이트하여 $O(n)$ 시간 복잡도를 보장합니다. 이는 기존 검증된 어휘 분석기들이 $O(n \log n)$ 또는 $O(n^2)$ 을 보이는 것과 대조적입니다.

3. 주요 기여 (Key Contributions)

가역성 정의 및 검증: 토큰 시퀀스에 대한 분리 가능성 (Separability) 조건을 정의하고, 이를 효율적으로 체크하고 유지하는 메커니즘을 설계했습니다.
ZipLex 프레임워크:
- 정규식 기반 토큰 정의
- 최대 매칭 (Longest Match) semantics
- 가역적 출력 (Invertible Printing)
- 메모이제이션을 통한 선형 시간 어휘 분석
  를 모두 포함하는 검증된 프레임워크를 구현했습니다.
성능 및 검증: Stainless 증명 도구를 사용하여 전체 시스템을 검증했으며, JSON 처리 및 프로그래밍 언어 어휘 분석 등 실제 응용 사례에서 높은 성능을 입증했습니다.

4. 결과 (Results)

실험 환경 (AMD EPYC 서버) 에서 ZipLex 를 평가한 결과는 다음과 같습니다.

시간 복잡도:
- 적대적인 문법 (예: a 와 a*b 규칙) 에 대해 ZipLex 는 **선형 시간 ( $O(n)$ )**을 보입니다.
- 반면, Flex 와 Coqlex 는 이차 시간 ( $O(n^2)$ ) 을 보였고, Verbatim++ 은 큰 입력에서 스택 오버플로우가 발생하거나 $O(n \log n)$ 의 성능을 보였습니다.
성능 비교:
- ZipLex 는 검증된 어휘 분석기인 Verbatim++ 보다 약 100 배 (2 차수) 빠릅니다.
- 검증되지 않은 OCamllex 보다 느리지만, 가역성과 형식적 검증이라는 추가적인 보장을 제공합니다. Coqlex 보다 약 8 배 느리지만, Coqlex 는 가역성을 지원하지 않습니다.
실용성: JSON 객체 정렬 애플리케이션 등에서 PrintableTokens를 사용한 슬라이싱과 재결합이 매우 효율적임을 보여주었습니다.

5. 의의 (Significance)

이 연구는 **형식적 검증 (Formal Verification)**과 **실용적인 성능 (Performance)**을 동시에 달성한 최초의 사례 중 하나입니다.

가역성 보장: 토큰 시퀀스를 출력하고 다시 분석할 때 정보 손실이 없음을 수학적으로 증명했습니다. 이는 리팩토링 도구, 프로그램 합성, 검증된 컴파일러 파이프라인 등에 필수적입니다.
선형 시간 검증: 메모이제이션을 포함한 최적화 기법까지 형식적으로 검증하여, 검증된 소프트웨어가 실제 대규모 입력에서도 효율적으로 작동할 수 있음을 보였습니다.
확장성: 임의의 알파벳 (ASCII, UTF-8, 바이너리 등) 을 지원하며, 검증된 해시 테이블과 Zippers 같은 데이터 구조를 활용하여 검증된 시스템의 성능 한계를 극복했습니다.

결론적으로 ZipLex 는 신뢰할 수 있는 컴파일러 및 데이터 처리 도구를 구축하기 위한 강력한 기반을 제공하며, 검증된 소프트웨어가 단순히 '올바른 것'을 넘어 '실용적으로 빠른 것'도 될 수 있음을 입증했습니다.