LPolyNC

Linear polynomial (over natural numbers) constraint solvability

Preliminaries

The definitions below are mechanized in Problems/LPolyNC.v.

Polynomials ℙ[ℕ](X) over natural numbers with indeterminate X are mechanized as list nat (list of coefficients, possibly with trailing zeroes).

A constraint has the shape either x ≐ 1, x ≐ y + z, or x ≐ X ⋅ y, where x ∈ 𝕍 ranges over multiset variables.

Constraints are mechanized as polyc, where 𝕍 is mechanized as nat.

A valuation φ : 𝕍 → ℙ[ℕ](X) satisfies a constraint c if either

• c is x ≐ 1 and φ(x) ≃ 1 ⋅ X⁰
• c is x ≐ y + z and φ(x) ≃ φ(y) + φ(z)
• c is x ≐ X ⋅ y and φ(x) ≃ (1 ⋅ X¹) ⋅ φ(y)

where ≃ denotes polynomial equality, mechanized as list equality up to trailing zeroes. The above is mechanized as polyc_sem, where ≃ is mechanized as poly_eq.

Problem instance (mechanized as LPolyNC_PROBLEM)

An instance of linear polynomial (over natural numbers) constraint solvability is a list of constraints.

Decision problem (mechanized as LPolyNC_SAT)

Given a list of constraints, is there a valuation that satisfies each constraint?

Reduction

Undecidability of linear polynomial (over natural numbers) constraint solvability is obtained by reduction from finite multiset constraint solvability (FMsetC_SAT in Problems/FMsetC.v). The reduction is mechanized in Reductions/FMsetC_to_LPolyNC.v as

Theorem FMsetC_to_LPolyNC : FMsetC_SAT ⪯ LPolyNC_SAT.

and

Theorem LPolyNC_undec : Halt ⪯ LPolyNC_SAT.

Key ideas

Linear ℙ[ℕ](X) constraints are closely related to AC1h unification. Polynomial addition is associative (A), commutative (C), and has 0 ⋅ X⁰ as identity element. Multiplication with the indeterminate X, i. e. the function h(p) = X ⋅ p, is homomorphic wrt. polynomial addition. Therefore, we can use finite multiset constraint solvability, which is form of AC1h unification (see FMsetC).

Relationship elementary Diophantine constraints solvability

There are two key differences between elementary Diophantine constraints and linear polynomial (over natural numbers) constraints. First, the underlying semirings are ℕ and ℙ[ℕ](X), respectively. Second, elementary Diophantine constraints require non-linear multiplication constraints, i.e. x ≐ y ⋅ z, as opposed to x ≐ X ⋅ y, where the polynomial X is constant.

Linear elementary Diophantine constraint solvability is decidable (related to integer linear programming). Interestingly, elementary Diophantine constraint solvability over integers is undecidable, whereas linear polynomial (over integers) constraint solvability is decidable.

References

[1] Paliath Narendran: Solving Linear Equations over Polynomial Semirings. LICS 1996: 466-472, doi: 10.1109/LICS.1996.561463