线性类型系统

Linear type system 把值视为资源：一个 linear value 必须恰好使用一次，或按语言规则显式转移、消耗。量子编程中，qubit 通常不可隐式复制，因此线性类型可在编译期阻止同一 qubit 被两个命令同时使用。一个抽象判断可以写成 $\Gamma,q:Qubit\vdash U(q):Qubit$；执行后原来的 $q$ 被消费，返回的新句柄继续出现在类型环境中。它与量子态与量子操作的 no-cloning 边界相呼应。

资源敏感的示例

设 q : Qubit，h q 的类型可理解为消耗 $q$ 并返回 $q'$，于是程序可写成 let q1 = h q，但不能把同一个线性绑定同时传给 measure q 和 x q。测量常把量子资源转换为 classical data，例如抽象类型为 $\mathrm{measure}:Qubit\to(Bit\times\mathbf{1})$；具体语言可能返回结果并销毁或重置 qubit。经典 Bit 若被标记为 unrestricted，则可以复制到多个变量。线性类型禁止的是程序层面的无记录资源复制，不是禁止复制测量后得到的经典 bit。

语义与边界

类型检查主要保证资源使用纪律；它不自动证明 unitary 的数学性质、测量统计正确，或程序满足某个 postcondition。类型系统还要处理 tensor product、ownership、别名、函数闭包和 classical control；不同语言的规则并不相同。有些系统采用 affine type，只要求资源至多使用一次，便于表达丢弃；另一些系统允许显式 discard，但必须说明其物理含义。与量子编程语言结合时，线性规则是静态保障的一层，仍需验证方法与工具检查更高层性质。

参考文献：

• Benton，A mixed linear and non-linear logic: Proofs, terms and models，Springer DOI。
• Selinger，Towards a quantum programming language，Cambridge DOI。