기술 요약: Granthi: 유니터리 와이어링을 통한 고차 양자 프로그래밍

1. 문제 정의

기존의 양자 프로그래밍 언어들은 일반적으로 고차 구조(함수, 제어 추상화, 프로그램 생성기)는 완전히 고전적 호스트 언어에 존재하고, 양자 계층은 큐비트와 레지스터에 대한 1차 연산으로 제한되는 분리된 아키텍처를 채택한다. 이러한 설계는 양자 프로그램 자체에 대한 추상화를 제한한다. 즉, 양자 값을 인자로 전달하거나, 결과로 반환하거나, 고차 구조 내에서 합성할 수 없게 만든다.

나아가, 고전적 데이터 추상화 메커니즘(패턴 매칭, 케이스 분석, 반복)은 사용되지 않는 대안을 검사하고 폐기하는 파괴적 검사에 의존하며, 이는 제어 흐름을 붕괴시킨다. 이러한 원칙들은 순수하게 유니터리한 양자 환경과 양립할 수 없다. 왜냐로 인해 데이터를 자유롭게 검사, 복사 또는 폐기할 수 없기 때문이다. 결과적으로, 순수 유니터리 의미론을 유지하면서 정적 회로로 컴파일될 수 있는 진정한 고차 일관적 제어(예: 퀀텀 스위치)를 지원하는 양자 프로그래히 랭귀지가 부족한 실정이다.

2. 방법론

본 논문은 세 가지 핵심 설계 약속을 기반으로 구축된 순수 유니터리 고차 양자 프로그래밍 언어인 Granthi를 제시한다:

1. 일급 양자 프로그램 (First-Class Quantum Programs): 양자 프로그램은 일급 값으로서 전달, 반환 및 일관적으로 합성될 수 있다.
2. 태그 보존 라우팅 (Tag-Preserving Routing): 가산 구조(Additive structure)는 관측적 분기가 아닌 태그 보존 라우팅으로 정의된다. 이를 통해 제어가 상태를 붕괴시키지 않고 중첩 상태로 유지될 수 있게 한다.
3. 유한 라벨 타입 (Finite Label Types): 명명된 가역 연산을 가진 프로그래머 대상의 유한 라벨 타입은 도메인 수준의 제어 공간을 제공하며, 이는 재귀적 타입이나 표현 숨김 없이 평면적인 $n$-항 합(n-ary sums)으로 정교화된다.

핵심 언어 및 의미론

• 선형 $\lambda$-계산법 기초: 핵심은 텐서($\otimes$), 일관적 합($\oplus$), 그리고 선형 함수 공간($\multimap$)을 갖춘 선형 $\lambda$-계산법이다. 기본 타입 $\mathbb{b}$는 1차원 시드이며, 유한 차원 시스템은 일관적 합(예: $QBool := \mathbb{b} \oplus \mathbb{b}$)으로 구축된다.
• 경계 유니터리성 (Boundary Unitarity): 핵심적인 의미론적 혁신은 "경계 뷰(boundary view)"이다. 타입 $A \multimap B$인 항(term)은 구조화된 인터페이스를 가진 열린 회로 파편으로 취급된다. 적용(Application)은 자원을 소비하는 리덕션 단계가 아니라 연결 구조(와이어링 인터페이스)로서 해석된다. 모든 잘 정의된 항은 그 경계 인터페이스 상의 유니터리 연산자를 나타낸다.
  간의 $\beta/\eta$-안정적 규율을 강제한다. 이 시스템은 모든 닫힌 잘 정의된 항이 정의적 동등성(definitional equality)까지 유일한 정규형을 가짐을 증명하여, 소스 수준의 재배열(정규화)이 컴파일된 유니터리 회로를 변경하지 않음을 보장한다.
• 양자 확장: 핵심은 인증된 인볼루션(self-inverse operators)과 행렬 지수 함수($e^{i\theta J}$)를 통해 연속적인 유니터리 패밀리를 생성하는 Exp 항 생성자로 풍부해진다. 이를 통해 측정이나 혼합 상태를 도입하지 않고도 위상 변화(phase shifts)와 제어 연산을 수행할 수 있다.

컴파일

Granthi 시스템은 엔드 투 엔드 컴파일러를 구현한다:

1. 정교화 (Elaboration): 표면 프로그램(OCaml DSL로 작성됨)은 바인더가 없는 핵심 IR로 정교화된다.
2. 회로 생성: 컴파일러는 pytket 백엔드를 사용하여 유니터리 경계의 와이어링을 물리적 큐비트 레이아웃 상의 정적 양자 회로로 구현한다.
3. 와이어 레이아웃: 컴파일러는 태그 레지스터와 공유 페이로드 번들을 포함하는 합 타입(sum types)에 대해 특정 와이어 인코딩을 사용한다. 구조적 동형성(결합법칙, 교환법칙, 분배법칙)은 게이트가 전혀 없는 순수 와이어 순열로 컴파일되며, 일관적 제어 구조(예: case)는 태그 레지스터에 작용하는 제어 게이트로 컴파일된다.

3. 주요 기여

• 고차 유니터리 의미론: Granthi는 고차 구조가 클래식 호스트에 국한되지 않고 양자 계층에 내재된 최초의 프로그래밍 언어적 설명을 제공한다. 이는 고차 가역성이 닫힌 데이터가 아닌 노출된 인터페이스로 이동된 일반적인 유니터리성임을 입증한다.
• 합성에 대한 일관적 제어: 이 언어는 **퀀텀 스위치(Quantum Switch)**를 정의 가능한 항으로 지원한다. 두 연산의 합성 순서를 중첩 상태에 두는 스위치는 정적 회로로 컴파일되며, 이는 이러한 고차 효과가 프로그래밍 가능하며 물리적으로 실현 가능하다는 것을 증명한다.
• 제어 흐름에 대한 간섭: 언어는 제어 흐름 이력에 대한 간섭(예: 위상 마킹을 포함한 가역적 단락 논리곱)을 지원한다. 이는 명시적인 증인(witness) 와이어를 스레딩하고 관찰 없이 특정 브랜치에 위상을 적용함으로써, 고전적 대응물이 없는 현상을 구현한다.
• 유한 제어 데이터 타입: 시스템은 명명된 가역 연산을 가진 프로그래머 대상의 유한 라벨 타입(예: 순환 군 $\mathbb{Z}_5$)을 도입한다. 이는 핵심의 합 및 와이어링 메커니즘으로 정교화되어, 도메인 특화 제어 공간(예: 군-일관적 패턴 매칭)이 효율적으로 컴파일되도록 한다(예: $n$-항 합에 대해 $O(\log n)$ 게이트).
• 형식적 보증: 논문은 정규화, 결정성, 경계 유니터리성 정리를 확립한다. 컴파일된 회로가 레이아웃 동형성을 통해 전달된 의미론적 유니터리와 동일함을 증명한다(백엔드 프리미티브의 정확성을 가정할 때).

4. 결과

저자들은 Granthi를 pytket을 타겟팅하는 Python 컴파일러를 갖춘 OCaml DSL로 구현했다. 프로토타입은 다음과 같은 여러 예제로 검증되었다:

• 퀀텀 스위치: 실행 예제는 인과적 순서의 중첩을 실현하는 8-큐비트 정적 회로로 컴파일된다.
• 제어 연산: 균일 제어 적용 및 $n$-항 제어 디스패치(예: SELECT 조합자)가 구현되었으며, 효율적인 게이트 수(예: $n$-항 합에 대한 $O(\log n)$ 태그 플립)를 입증했다.
• 표준 알고리즘: 시스템은 Deutsch–Jozsa, Hidden Subgroup, Simon, Bell, GHZ 상태를 포함한 표준 알고리즘을 성공적으로 컴파일하고 검증했다.
• 게이트 비용 분석: 구현을 통해 곱셈 및 구조적 연산은 게이트가 거의 없는(순수 와이어링) 반면, 양자 프리미티브와 일관적 제어 구조는 필요한 게이트를 도입함을 확인했다. 예를 들어, 퀀텀 스위치는 $2 + 2(|f| + |g|)$ 개의 게이트로 컴파일된다.

5. 의의 및 범위

본 논문은 Granthi를 측정 및 고전적 피드백과 무관하게, 순수 유니터리 프레임워크 내에서 고차 추상화를 연구하기 위한 절제된 유니터리 코어로 포지셔닝한다.

• 범위: 언어는 의도적으로 측정, 혼합 상태, 고전적 피드백, 재귀적 타입을 제외한다. 이러한 제외는 모든 잘 정의된 항이 경계 유니터리를 나타내고 정적 회로로 컴파일된다는 불변성을 유지하기 위해 필요하다.
• 위치 선정: Granthi는 고차 구조를 호스트가 아닌 객체 언어에 배치한다는 점에서 기존 언어(Quipper, Q# 등)와 다르다. 또한 일반적인 직교성 판단에 의존하는 Qunity와 달리, 직교성을 가산 타입 구조에 내장하고 있다.
• 향후 방향: 저자들은 완전한 양자 프로그래밍 시스템을 위해서는 측정, 혼합 상태 의미론, 더 풍부한 데이터 추상성을 포함하도록 코어를 확장해야 한다고 인정한다. Granthi는 하드웨어 제약과 측정 효과가 도입되기 전, 양자 프로그램이 어떻게 구조화되어야 하는지를 이해하기 위한 기초적인 단계로 제공된다.

요약하자면, Granthi는 고차 양자 제어가 순수 유니터리 프레임워크 내에서 물리적으로 유의미하며 프로그래밍 가능하다는 것을 보여주며, 제어 흐름 자체가 간섭에 참여할 수 있는 양자 프로그램을 위한 형식적이고 실행 가능한 토대를 제공한다.