💻 computer science

Well-Scoped Locally Nameless Representation of Syntax

본 논문은 Plotkin 스타일 바인딩 시그니처를 매개변수로 하는 Agda 를 위한 일반적이고 잘 정의된 로컬 네임리스 구문 표현을 제시하며, 이를 통해 단순한 네임풀 구문에 대한 알파-변환 modulo 적절성을 증명하고 예시를 통해 그 유용성을 입증한다.

원저자: Andrew M. Pitts

게시일 2026-05-12

📖 4 분 읽기☕ 가벼운 읽기

CC BY 4.0

원저자: Andrew M. Pitts

원본 논문은 CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) 라이선스로 제공됩니다. ✨ 이것은 아래 논문에 대한 AI 생성 설명입니다. 저자가 작성하거나 승인한 것이 아닙니다. 기술적 정확성을 위해서는 원본 논문을 참조하세요. 전체 면책 조항 읽기

당신이 책들 안에 다른 책들을 참조할 수 있는 거대하고 혼란스러운 도서관을 정리하려는 사서라고 상상해 보십시오. 어떤 책들은 표지에 제목이 적혀 있습니다 (예: "위대한 개츠비"). 반면 다른 책들은 특정 섹션 안의 번호가 매겨진 선반들일 뿐입니다 (예: "3 번 선반, 2 번째 줄").

앤드루 피츠 (Andrew Pitts) 가 쓴 이 논문은 컴퓨터 (특히 Agda 와 같은 "대화형 정리 증명기") 가 혼란스러워하거나 실수 없이 도서관의 규칙을 검증할 수 있도록, 이 도서관을 정리하는 새롭고 더 지능적인 방법에 관한 것입니다.

다음은 간단한 비유를 사용하여 이 논문의 아이디어를 분해한 것입니다:

1. 문제: "이름 없는" 대 "이름 있는" 딜레마

컴퓨터 과학자들이 컴퓨터에게 언어 (프로그래밍 언어나 논리 등) 를 가르치려 할 때, 변수를 처리해야 합니다.

"이름 있는" 방식: 모든 변수에 x, y, z 와 같은 이름을 부여합니다. 이는 인간이 읽기 쉽지만, 이름을 서로 바꾸면 컴퓨터가 혼란을 겪습니다 (이를 "알파 변환" 문제라고 합니다). 이름을 바꾸면 x 와 y 가 같은 것일까요?
"이름 없는" 방식 (드 브루인 인덱스): 이름을 전혀 사용하지 않습니다. 대신 "1 번째 변수", "2 번째 변수"라고 말하며 안쪽에서 바깥쪽으로 세어 나갑니다. 이는 컴퓨터에게는 훌륭하지만, 숫자 뒤죽박죽처럼 보이므로 인간에게는 끔찍합니다.

2. 구식 해결책: "지역적 이름 있는" 방식

몇 년 전, 연구자들은 지역적 이름 있는 (Locally Nameless) 이라는 하이브리드 아이디어를 고안해냈습니다.

자유 변수 (루프나 함수 내부에 묶이지 않은 것) 는 이름 (예: x) 을 유지합니다.
바인딩된 변수 (루프 내부의 것) 는 숫자 (예: 0, 1) 를 사용합니다.

주의할 점: 이 시스템에는 "함정"이 있습니다. 범위에 맞지 않는 숫자를 가진 "고장 난" 항을 만들 수 있게 허용합니다. 마치 "5 번 선반으로 가라"고 적힌 책이 있지만, 현재 있는 방에는 선반이 3 개뿐인 상황을 상상해 보십시오. 컴퓨터는 항이 "지역적으로 닫혀 있는지 (유효한지)"를 끊임없이 확인해야 합니다. 이는 사서가 누군가 책을 빌려주기 전에 책이 올바른 복도에 있는지 끊임없이 확인해야 하는 것과 같은 추가적인 증명 작업이 필요합니다.

3. 새로운 해결책: "잘 범위가 지정된 지역적 이름 있는" 방식

이 논문은 더 나은 방법을 제안합니다: 잘 범위가 지정된 지역적 이름 있는 (Well-Scoped Locally Nameless).

단순히 숫자를 사용하는 대신, 컴퓨터는 규칙을 강제하기 위해 타입을 사용합니다.

도서관을 서로 다른 "방"으로 생각하십시오.
방 0에 있으면, 0부터 0까지 번호가 매겨진 선반만 볼 수 있습니다 (즉, 선반은 없고 자유 이름만 있는 것).
방 1에 있으면, 0과 1 번 선반을 볼 수 있습니다.
방 5에 있으면, 0부터 5까지의 선반을 볼 수 있습니다.

마법 같은 점: 이 시스템에서는 고장 난 책을 만들 수 literally 없습니다. 방 2에 서 있는 상태에서 "10 번 선반으로 가라"고 쓰려고 하면, 컴퓨터의 타입 시스템이 "아니요, 불가능합니다. 그 문장조차 쓸 수 없습니다"라고 말합니다.

이 논문은 이 접근 방식이 다음과 같다고 주장합니다:

"함정" 제거: 항이 유효한지 확인하기 위한 추가 증명을 작성할 필요가 없습니다. 항이 존재한다는 사실 자체가 그것이 유효함을 증명합니다.
투명성: 여전히 인간이 익숙한 "이름 있는" 방식과 거의 비슷하게 보이므로, 순수한 "이름 없는" 방식만큼 혼란스럽지 않습니다.
범용성: 저자들은 조건부 바인딩 규칙 (예: if 문이나 lambda 함수가 작동하는 방식) 을 표준 템플릿을 사용하여 설명하기만 하면, 정의하려는 모든 언어에 작동하는 "도서관" (도구 세트) 을 구축했습니다.

4. 작동 원리 ("열기"와 "닫기")

이 논문은 방 사이를 이동하는 것과 같은 두 가지 주요 연산을 설명합니다:

추상화 (닫기): 자유 이름 (예: x) 을 가져와 바인딩된 인덱스 (예: 0) 로 변환합니다. 이는 책을 선반에서 꺼내 새로운 방의 특정 번호가 매겨진 슬롯에 넣는 것과 같습니다.
구체화 (열기): 바인딩된 인덱스를 가져와 특정 책 (항) 으로 대체합니다. 이는 슬롯에서 책을 꺼내 실제 책을 그 자리에 넣는 것과 같습니다.

저자들은 그들의 "잘 범위가 지정된" 수학이 완벽하게 작동함을 증명했습니다. 그들은 새로운 시스템이 기존의 "이름 있는" 시스템과 수학적으로 동등함을 보여주었습니다. 즉, 동일한 개념을 나타내지만 더 안전하게 조직화되었다는 것입니다.

5. 실제 사례

이 논문은 이론만 이야기하는 것이 아닙니다. 그들은 그들의 "도서관"을 세 가지 다른 유형의 언어에 테스트했습니다:

피-계산 (Pi-Calculus): 컴퓨터 프로그램이 서로 어떻게 통신하는지 (전화 통화와 같은) 기술하는 데 사용되는 언어입니다. 여기서는 이름이 통신을 위한 "채널"입니다.
마틴 - 뢰프 타입 이론: 수학적 증명을 위한 복잡한 시스템입니다. 그들은 이름의 "신선함"에 빠지지 않고 자연수와 타입에 대한 규칙을 작성하는 방법을 보여주었습니다.
괴델의 시스템 T: 계산이 결국 종료됨 (결정 가능성) 을 증명하는 시스템입니다. 그들은 특정 알고리즘이 올바르게 작동함을 증명하기 위해 그들의 방법을 사용했습니다.

결론

이 논문은 다음과 같이 말합니다: "변수가 올바른 위치에 있는지 수동으로 확인하는 것을 멈추십시오. 컴퓨터의 타입 시스템이 대신 무거운 작업을 하도록 하십시오."

의존 타입 (Agda 프로그래밍 언어의 기능) 을 사용하여, 그들은 잘못된 구문을 작성하는 것이 불가능한 시스템을 만들었습니다. 이는 "예, 이 변수는 범위 내에 있습니다"라고 말하기 위해 연구자들이 지루한 증명 코드 수천 줄을 작성하는 것을 절약해 줍니다. 이는 형식적 검증 (소프트웨어가 버그가 없음을 증명하는 것) 을 더 쉽고, 안전하며, 인간이 언어를 자연스럽게 생각하는 방식에 가깝게 만듭니다.

기술 요약: 잘 스코프된 로컬 네임리스 구문 표현

문제 제기
종속 타입 이론에 기반한 상호작용형 정리 증명기 (Agda, Lean, Rocq 등) 에서 바인딩 구조 (예: $\lambda$ -칼큘러스, 타입 시스템) 를 형식화할 때, 변수 바인딩과 $\alpha$ -동치성을 관리하는 것이 핵심적인 과제입니다. 자유 변수는 명시적인 이름으로, 바인딩된 변수는 드 브루인 인덱스로 표현하는 '로컬 네임리스' 접근법은 낮은 인프라 오버헤드, 투명성, 진입 용이성 측면에서 PoplMark 기준을 충족하는 것으로 입증되었습니다. 그러나 표준 로컬 네임리스 표현은 중요한 결함을 안고 있습니다: 즉, 항의 귀납적 정의가 현재 스코프를 초과하는 '떨어진' (dangling) 인덱스를 허용한다는 점입니다. 정확성을 보장하기 위해서는 '로컬 클로즈드' (locally closed) 항의 부분집합으로 도메인을 제한해야 합니다. 이는 치환과 같은 연산이 로컬 클로즈드를 보존함을 증명하기 위한 반복적이고 수동적인 증명을 필요로 하게 하여, 형식적 개발에서 상당한 부담과 잠재적 오류의 원인이 됩니다.

방법론
본 논문은 Agda 의 종속 타입 시스템을 활용하여 로컬 클로즈드를 별도의 술어로 하는 것이 아니라 본질적으로 강제하는 '잘 스코프된' (well-scoped) 로컬 네임리스 표현 변형을 제안합니다.

인덱스화된 귀납 타입: 단일 항 타입 대신, 자연수 $n$ 으로 인덱싱된 타입 계열 Trm[n]을 정의합니다. $n$ -항은 모든 드 브루인 인덱스가 유한 타입 Fin n ( $n$ 보다 작은 자연수) 에서 추출된 항입니다.
0-항으로서의 로컬 클로즈드 항: 이 프레임워크에서 '로컬 클로즈드' 항 (떨어진 인덱스가 없는 항) 은 정확히 Trm[0]에 해당합니다. 자유 변수를 가진 항은 스코프 내 자유 변수의 수에 해당하는 $n$ 에 대해 Trm[n]으로 표현됩니다.
바인딩 시그니처에 의한 매개변수화: 라이브러리는 범용적이며, Plotkin 스타일의 바인딩 시그니처에 의해 매개변수화됩니다. 이를 통해 연산자, 그들의 아리티, 그리고 각 인자 위치에서 바인딩되는 이름의 수를 정의할 수 있습니다.
종속 타입을 통한 연산:
- 스코프 약화 (Scope Weakening): 인덱스를 주입하고 더 큰 스코프로 이동할 때 필요한 시프트를 처리하는 함수 Trm[m] -> Trm[n] ( $m \le n$ ).
- 구체화 (Concretion, Opening): $(1+n)$ -항의 인덱스 $i$ 를 0-항으로 대체하여 $n$ -항을 생성합니다. 이는 $i$ 보다 큰 인덱스들을 1 만큼 아래로 시프트하는 과정을 포함합니다.
- 추상화 (Abstraction, Closing): $n$ -항의 자유 이름을 인덱스로 대체하여 $(1+n)$ -항을 생성합니다. 이는 인덱스들을 위로 시프트하는 과정을 포함합니다.
- 치환: 구조적으로 정의됩니다. 치환 함수가 이름을 0-항 (Trm) 으로 매핑하므로, '로컬 클로즈드' 조건은 타입 시스템에 의해 자동으로 강제됩니다. $n$ -항에 대한 치환은 또 다른 $n$ -항을 산출합니다.

주요 기여

WSLN 라이브러리: 잘 스코프된 로컬 네임리스 항을 구현한 범용 Agda 라이브러리입니다. Plotkin 바인딩 시그니처로 지정된 모든 언어에 대해 구문, 연산 (약화, 치환, 추상화, 구체화), 그리고 추론 원리를 정의하기 위한 인프라를 제공합니다.
형식적 적절성 증명: 논문은 다음 두 가지 사이의 전단사 (bijection) 를 확립하는 엄밀한 증명을 제공합니다:
1. 잘 스코프된 로컬 네임리스 0-항 (Trm[0]) 의 타입.
2. 자유 변수와 바인딩된 변수 모두에 대해 명시적인 이름을 가진 '네임풀' 항의 $\alpha$ -동치성 클래스.
  이 전단사는 잘 스코프된 표현이 포획을 피하는 치환과 $\alpha$ -동치성의 의미를 올바르게 포착함을 보여줍니다.
로컬 클로즈드 증명의 제거: 타입 인덱스에 스코프 제약을 인코딩함으로써, 명시적인 '로컬 클로즈드' 술어와 관련된 증명 의무 (예: 치환이 로컬 클로즈드를 보존함을 증명) 를 제거합니다. 이러한 속성들은 타입 규칙의 결과물이 됩니다.
신선도 (Freshness) 처리: 라이브러리는 명목 기법 (nominal techniques) 과 통합되어, 자연수 형태의 '유한히 무한한' (finitely inexhaustible) 원자 집합을 사용하여 여집합 양화를 통해 신선한 이름을 생성함으로써, 신선도 조건이 체계적으로 처리되도록 합니다.

결과
논문은 Agda 로 구현된 세 가지 명확한 예시를 통해 접근법을 검증합니다:

$\pi$ -칼큘러스: $\lambda$ -칼큘러스를 넘어 프로세스 표현과 채널 이름을 처리함으로써 라이브러리의 적용 가능성을 보여줍니다. 라이브러리가 바인딩 구조를 처리하지만, 채널이 기대된 곳에서 사용되는지 확인하는 것과 같은 잘 형성됨 (well-formedness) 에 대한 타입 체킹은 여전히 별도의 사용자 정의 판단임을 강조합니다.
마틴 - 뢰프 타입 이론 (MLTT): 라이브러리가 타입 규칙의 정의를 어떻게 용이하게 하는지 보여줍니다. 명시적인 신선도 가정을 요구하는 '존재 - 신선 (exists-fresh)' 규칙과 신선도가 암묵적인 '여집합 양화' 규칙을 대비시켜, 잘 스코프된 표현이 후자를 지원하여 더 깔끔하고 투명한 형식화를 가능하게 함을 입증합니다.
괴델의 시스템 T (평가에 의한 정규화): $\beta\eta$ -변환의 결정 가능성을 증명하는 상당한 개발입니다. 이 예시는 잘 스코프된 표현이 추상화의 의미론과 복잡한 의미론적 구성 (setoid 값 프리시브) 에서의 신선도 처리를 어떻게 단순화하며, 유한 지지 의미론적 객체의 필요성을 피하는지 보여줍니다.

의의와 주장
본 논문은 잘 스코프된 로컬 네임리스 표현이 전통적인 로컬 네임리스 접근법에서 발견되는 '떨어진 인덱스'의 함정에 대한 '직관적'이면서도 강력한 해결책을 제공한다고 주장합니다. 그 주요한 의의는 스코프 정확성을 보장하는 부담을 사용자 (수동 증명을 통해) 에서 정리 증명기의 타입 체커 (종속 타입을 통해) 로 이전하는 데 있습니다.

저자들은 이 접근법이 PoplMark 기준이 요구하는 투명성을 유지한다고 강조합니다: 형식적 정의는 비형식적 관례와 밀접하게 대응하며, '인덱스 요가' (드 브루인 인덱스의 조작) 는 라이브러리의 연산 내에 캡슐화됩니다. 구현은 유한 순서수 (Fin n) 와 인덱스 시프트에 대한 신중한 처리가 필요하지만, 라이브러리는 이러한 복잡성을 매개변수화하여 사용자가 저수준 스코프 메커니즘을 관리하지 않고도 언어를 정의하고 속성을 증명할 수 있게 합니다. 논문은 현재 바인딩 시그니처가 정렬되지 않았고 단순한 바인딩 스코프를 모델링하지만, 시스템 T 개발에서 입증된 바와 같이 이 접근법이 복잡한 타입 시스템과 의미론적 증명을 처리하기에 충분히 견고하다고 겸손하게 언급합니다.