Qudit Quantum Programming with Projective Cliffords

TL;DR

This work introduces LambdaPC, a typed lambda-calculus that encodes projective Clifford unitaries as conjugation maps on the qudit Pauli group, extending naturally to arbitrary qudit dimensions. It builds a Curry–Howard correspondence using condensed encodings (μ, ψ) and provides a sound, complete calculus with both linear (λL) and Clifford (λPc) layers, supported by categorical semantics and a symplectic form that enforces well-formedness. A key contribution is the extension to qudits, including detailed encodings of Pauli and Clifford groups, two-layer type systems, and a pathway to compiling to Pauli tableaux and circuits. The paper also demonstrates the framework on stabilizer error-correcting codes, showing how encoders, logical operators, and syndrome preparation can be expressed as LambdaPC programs. Overall, LambdaPC offers a high-level, type-safe, algebraic approach to Clifford-based quantum programming with an eye toward universality via dimension polymorphism and hierarchical extensions.

Abstract

This paper introduces a novel abstraction for programming quantum operations, specifically projective Cliffords, as functions over the qudit Pauli group. Generalizing the idea behind Pauli tableaux, we introduce a type system and lambda calculus for projective Cliffords called LambdaPC, which captures well-formed Clifford operations via a Curry-Howard correspondence with a particular encoding of the Clifford and Pauli groups. Importantly, the language captures not just qubit operations, but qudit operations for any dimension $d$. Throughout the paper we explore what it means to program with projective Cliffords through a number of examples and a case study focusing on stabilizer error correcting codes.

Figures (12)

• Figure 1: Typing rules for $\mathcal{L}$-expressions.
• Figure 2: $\beta$-reduction rules for $\mathcal{L}$-expressions. The full call-by-value small-step operational semantics rules can be found in the supplementary material (\ref{['app:lambdaC-reduction-rules']}).
• Figure 3: Categorical semantics of $\mathcal{L}$-expressions $\Delta \vdash a : \alpha$ as ${\mathbb{Z}_{d'}} { \mathbb{Z}_d }$-linear maps $\left\llbracket a \right\rrbracket ^{\hbox{$\mathcal{L}$}} \in \mathcal{L}(\left\llbracket \Delta \right\rrbracket ^{\hbox{$\mathcal{L}$}},\left\llbracket \alpha \right\rrbracket ^{\hbox{$\mathcal{L}$}})$, up to isomorphism of $\left\llbracket \Delta \right\rrbracket ^{\hbox{$\mathcal{L}$}}$. For example, in the rule for $\text{let}~x = a~\text{in}~a'$ typed by $\Delta,\Delta'$ where $\Delta \vdash^{\hbox{$\mathcal{L}$}} a : \alpha$ and $\Delta',x:\alpha \vdash^{\hbox{$\mathcal{L}$}} a' : \alpha'$, we assume we have $s \in \left\llbracket \Delta \right\rrbracket ^{\hbox{$\mathcal{L}$}}$ and $s' \in \left\llbracket \Delta' \right\rrbracket ^{\hbox{$\mathcal{L}$}}$.
• Figure 4: Projecting out the non-phase component of a $\mathcal{P}_c$-expression to form a $\mathcal{L}$-expression.
• Figure 5: Linearity typing rules for $\lambda^{\mathcal{P}_c}$ expressions.

Theorems & Definitions (48)

• proposition 1
• definition 1: winnick2024condensed
• theorem 1: winnick2024condensed
• lemma 1
• lemma 2
• theorem 2: Progress
• lemma 3: Substitution
• theorem 3: Preservation
• theorem 4: Strong normalization, \ref{['app:strong-normalization']}
• definition 2: $\equiv$