Reversible computation requires that intermediate data be explicitly undone rather than discarded. In quantum programming, this principle appears as uncomputation, usually treated as a technical cleanup mechanism. We instead present uncomputation as a semantic foundation. In the Qutes language, we introduce a formal model of \emph{Scope-Bounded Liveness-Guided Uncomputation}, where lexical scope bounds variable lifetime and static liveness and entanglement analysis determine the earliest safe reclamation point. We define semantic lifetime and a Restoration Invariant ensuring that temporary quantum information disappears once it becomes semantically irrelevant. We prove compositional correctness under nested scopes and show that early reclamation can reduce circuit depth by avoiding critical-path overhead and can bound peak live qubits through disciplined ancilla reuse. Finally, we show that parameter passing semantics emerges from the same lifetime discipline, with pass-by-value and pass-by-reference corresponding to different lifetime boundaries, and we characterize the constraints (irreversibility, persistent entanglement, and aliasing) under which automatic uncomputation must be restricted.

翻译：可逆计算要求中间数据被显式地撤销而非丢弃。在量子编程中，这一原则表现为逆计算，通常被视为一种技术性的清理机制。相反，我们将逆计算作为一种语义基础来呈现。在Qutes语言中，我们引入了一种**作用域限定的活跃性引导逆计算**的形式化模型，其中词法作用域限定变量的生命周期，静态活跃性与纠缠分析共同确定最早的安全回收点。我们定义了语义生命周期和一个**恢复不变性**，确保临时量子信息一旦在语义上变得无关便消失。我们证明了嵌套作用域下的组合正确性，并表明早期回收可以通过避免关键路径开销来减少电路深度，并通过规范化的辅助比特重用限制峰值存活量子比特数。最后，我们展示了参数传递语义源于相同的生命周期规则，其中按值传递和按引用传递对应不同的生命周期边界，并且我们刻画了自动逆计算必须受到限制的约束条件（不可逆性、持久纠缠和别名）。