Module Value.ProductSource

Reduced product of value abstractions.

This combiner implements a reduced product between 𝑚 value abstractions 𝒱₁, ..., 𝒱ₘ. Each abstraction 𝒱ᵢ represent values of types 𝐓ᵢ, such that: ∀ j ≠ i: 𝐓ᵢ ∩ 𝐓ⱼ ≠ ∅. The types represented by the combiner is 𝐓₁ ∩ ... ∩ 𝐓ₘ.

The reduced is represented with a cartesian product. The concretization of a product of values is the intersection of the concretizations: γ(v₁,...,vₘ) = γ₁(v₁) ∩ ... ∩ γₘ(vₘ).

The reduced product is parameterized by a set of reduction rules ρ₁, ..., ρₖ. Each reduction rule is applied after each transfer function. Note that reduction rules can access to all abstractions and can reduce many values at the same time.