Programs routinely create temporary data, retain state and revisit earlier results. Negative and fractional types benefit those activities in a type-resolved account of computation. Negative values redirect evaluation. Fractional values introduce value-specific auxiliary data and discharge it after a computation restores the required value. We develop both as first-class computational forms in our Clef design, using Chen and Sabry's directed, value-indexed calculus and distinguishing James and Sabry's logic-variable search interpretation. Our Program Semantic Graph retains their value identities and resource uses, enabling Composer to preserve their behavior through MLIR operations and native realization. In this paper, a negative-type counter and a fractional workspace calculation demonstrate the two constructions. Local proofs establish preservation of matching and independent resource discharge. Dimensional inference and proof terms supply premises through our four verification tiers. The applications connect deferred reverse computation to gradient calculations without an activation tape, and checked inverse steps to in-memory event recovery. A finite reconstruction horizon governs the exchange between storage and recomputation. We derive its error recurrence and show where Urschel's elimination-growth bounds can support a realized inverse step. Bayesian updates and quantum circuits supply further computational cases, including temporary workspace, measurement and a worked adiabatic schedule. Exact matching, bounded reconstruction and physical realization retain their respective contracts. The resulting architecture makes the information needed to run, reverse or complete a computation available to the compiler. Libraries can expose these operations through familiar interfaces while their retained structure supports unboxed execution and differential compilation across targets.

翻译：暂无翻译