Bidirectional Transformation Description Bound

Abstract

Two inverse compilers bound both description costs and their distance.

Theorem 1.1 (Two described transformations bound both endpoint complexities).

$$\begin{array}{c}\forall Object,Transformation,ObjectCode,TransformationCode:\mathrm{Type},\\ \forall objects:\mathrm{DescriptionSystem}\left(Object,ObjectCode\right),\\ \forall transformations:\mathrm{DescriptionSystem}\left(Transformation,TransformationCode\right),\\ \forall applies:Transformation\to Object\to Object\to \mathrm{Prop},\\ \forall forwardOverhead,reverseOverhead:\mathbb{N},\\ \forall forwardCompiler:\mathrm{TransformationCompiler}\left(objects,transformations,objects,applies,forwardOverhead\right),\\ \forall reverseCompiler:\mathrm{TransformationCompiler}\left(objects,transformations,objects,applies,reverseOverhead\right),\\ \forall u,v:Transformation,\\ \forall x,y:Object,\\ (applies(u,x,y)\wedge applies(v,y,x))\Rightarrow \\ (K_{objects}(y)\le K_{objects}(x)+K_{transformations}(u)+forwardOverhead)\wedge \\ (K_{objects}(x)\le K_{objects}(y)+K_{transformations}(v)+reverseOverhead)\wedge \\ \mathrm{dist}\left(K_{objects}(x),K_{objects}(y)\right)\le \max \left(K_{transformations}(u),K_{transformations}(v)\right)+\max \left(forwardOverhead,reverseOverhead\right).\end{array}$$

Proof. Machine-checked in Lean as D5/S0/Computability/DescriptionComplexity/BidirectionalTransformationDescriptionBound.bidirectional_transformation_description_bounds (✓ std3). ∎

Source. Repository-derived.

Commentary.

Objects and transformations use the canonical description-system family. One application relation records both directions, and each compiler combines an endpoint description with a transformation description.

The two application premises state that the forward transformation sends x to y and the reverse transformation sends y to x. Applying the frozen one-way compiler theorem in each direction gives the first two public inequalities.

A case split on the ordering of the two endpoint complexities turns their natural-number distance into one subtraction. The corresponding directional bound is then enlarged by the maxima of the transformation costs and fixed compiler overheads.

Pinned Mathlib was searched for natural-distance lemmas and supplies Nat.dist_eq_sub_of_le and Nat.dist_eq_sub_of_le_right. The repository-wide description-complexity search found only the imported one-way predecessor; no theorem containing all three public clauses was present.

References

• Truth anchor: D5/S0/Computability/DescriptionComplexity/BidirectionalTransformationDescriptionBound.bidirectional_transformation_description_bounds
• Dependency: D5/S0/Computability/DescriptionComplexity/TransformationDescriptionBound