Affine Logic

2026.09.23 18:44

아핀 논리(Affine Logic)는 구조 규칙 중 축약(contraction)을 버린 부분구조 논리(substructural logic)이다. 한 줄로 요약하면 “약화를 허용하는 선형 논리”이고, 가정을 많아야 한 번 쓸 수 있는 논리이다.

Structural Rules

보통의 고전 논리는 시퀀트 Γ ⊢ B를 다룰 때 세 가지 구조 규칙을 당연하게 쓴다. 이 규칙들은 논리 연결사(∧, ∨, →)와 무관하게 가정 목록 Γ 자체를 조작한다.

교환(exchange): 가정의 순서는 상관없다
```
Γ, A, B, Δ ⊢ C
Γ, B, A, Δ ⊢ C
```
약화(weakening): 가정은 안 써도 된다 (버려도 된다)
```
Γ ⊢ B
Γ, A ⊢ B
```
축약(contraction): 가정은 몇 번이든 쓸 수 있다 (복제해도 된다)
```
Γ, A, A ⊢ B
Γ, A ⊢ B
```

일상적인 증명에서 이 규칙들은 눈에 띄지도 않는다. “A를 가정했으니 A를 두 번 쓴다”는 것이 문제라고 생각하지 않기 때문이다. 부분구조 논리는 바로 이 지점을 의심한다. 가정을 자원(resource)으로 보면, 복제와 폐기는 공짜가 아니다.

어떤 규칙을 빼느냐에 따라 다른 논리가 된다.

논리	교환	약화	축약	가정을 쓰는 횟수
고전/직관주의 논리	O	O	O	0번 이상
아핀 논리	O	O	X	많아야 1번
관련 논리(relevance logic)	O	X	O	적어도 1번
선형 논리(linear logic)	O	X	X	정확히 1번
순서 논리(ordered logic)	X	X	X	정확히 1번, 순서까지 고정

아핀 논리는 복제만 금지한다. 쓰지 않고 버리는 것은 허용한다.

Relation to Linear Logic

아핀 논리는 선형 논리 안에 그대로 끼워 넣을 수 있다. 아핀 함의 A → B를 선형 논리의 언어로 다음과 같이 다시 쓰면 된다.

A → B  ≡  A ⊸ B ⊗ ⊤

⊤는 선형 논리에서 “무엇이든 흡수하는” 가법적 참이다. 남는 자원을 ⊤가 삼켜주기 때문에, 선형 논리 위에서 약화를 흉내 낼 수 있다.

이름은 지라르(Jean-Yves Girard)가 선형 논리의 상호작용 기하학(geometry of interaction) 의미론을 다루며 붙였다. 선형 대수의 아핀 변환에서 따온 것이다. 선형 변환이 원점을 고정한다면 아핀 변환은 평행이동을 허용하듯, 선형 논리의 “정확히 한 번”을 “많아야 한 번”으로 느슨하게 푼 체계라는 비유이다.

다만 체계 자체는 선형 논리보다 앞선다. 그리신(V. N. Grishin)이 1974년에 이미 이 논리를 썼다. 집합론에서 축약 규칙을 빼면 무제한 내포 공리(unrestricted comprehension)를 넣어도 러셀의 역설이 유도되지 않는다는 것을 발견했기 때문이다.

Russell’s Paradox and Contraction

R = { x | x ∉ x }로 두면 R ∈ R ↔ R ∉ R을 얻는다. 여기서 모순을 뽑아내는 과정을 자세히 보면 R ∈ R이라는 가정을 두 번 쓴다. 한 번은 ↔의 왼쪽에 넣어 R ∉ R을 끌어내는 데, 또 한 번은 그 R ∉ R과 부딪혀 모순을 만드는 데 쓴다.

축약이 없으면 이 복제가 막힌다. 가정은 한 번만 소비되므로 역설을 완주할 수 없다. 그리신이 본 것이 이것이고, 순진한 집합론이 축약 없는 논리 위에서는 무너지지 않는 이유이다.

Decidability

빼는 것이 손해만은 아니다. 선형 논리는 명제 수준에서도 결정 불가능하다(Lincoln, Mitchell, Scedrov, Shankar, 1992). 지수 연산자 !가 자원을 무한히 복제할 수 있어서 계산을 시뮬레이션해버리기 때문이다.

반면 지수 연산자를 포함한 명제 아핀 논리는 결정 가능하다(Kopylov, 1995). 축약이 없으니 증명 탐색에서 같은 가정이 무한히 불어나는 가지가 생기지 않고, 탐색이 끝난다. 아핀 논리를 바탕으로 만든 술어 논리의 결정 가능한 조각을 직접 논리(Direct Logic)라 부른다(Ketonen & Weyhrauch, 1984; Ketonen & Bellin, 1989).

지라르의 루디쿠스(ludics), 즉 증명과 계산을 상호작용으로 보는 접근도 아핀 논리를 토대로 한다.

Affine Type System

커리-하워드 대응(증명 = 프로그램, 명제 = 타입)을 따라가면 아핀 논리는 아핀 타입 시스템이 된다. 값을 많아야 한 번 쓸 수 있다는 규칙이다.

축약이 없다 = 값을 복제할 수 없다 → 이동(move)만 가능하고, 이동한 값은 다시 쓸 수 없다
약화가 있다 = 값을 쓰지 않고 버려도 된다 → 스코프를 벗어나면 그냥 폐기된다

러스트의 소유권이 정확히 이 모양이다.

let s = String::from("hi");
let t = s;          // 이동: s의 소유권이 t로 넘어간다
// println!("{s}"); // 컴파일 에러 — s는 이미 소비되었다 (축약 없음)
                    // t를 쓰지 않아도 아무 문제 없다 — 스코프 끝에서 drop (약화 있음)

t를 한 번도 쓰지 않고 함수가 끝나도 컴파일러는 불평하지 않는다. 그냥 Drop이 호출되고 끝이다. 이 “안 써도 된다”는 점이 러스트를 선형(linear)이 아니라 아핀(affine)으로 만든다. 선형 타입 시스템이라면 모든 값을 반드시 명시적으로 소비해야 하고, 쓰지 않은 값은 에러가 된다.

실제로 선형 타입이 필요한 경우가 있다. 파일 핸들을 반드시 닫아야 한다거나, 트랜잭션을 반드시 커밋 또는 롤백해야 하는 경우이다. 러스트에서 이것을 흉내 내려면 Drop을 구현하지 않고 소비 메서드만 제공한 뒤, 타입이 드롭되면 패닉을 내는 식의 우회가 필요하다. 타입 시스템이 강제해주지는 못한다.

Copy 트레이트는 이 그림에서 예외에 해당한다. i32처럼 Copy인 타입은 복제가 허용되므로 축약이 되살아난 것이고, 그래서 아핀 제약을 받지 않는다.