FMsetC

Finite multiset constraint solvability

Preliminaries

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

Elements e are defined as e ∈ 𝔼 ::= 0 | h (e). 𝔼 is mechanized as nat.

A constraint has the shape either x ≐ [0], x ≐ y ⊍ z, or x ≐ h (y), where x ∈ 𝕍 ranges over multiset variables.

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

A valuation φ : 𝕍 → list 𝔼 satisfies a constraint c if either

• c is x ≐ [0] and φ(x) ≡ [0]
• c is x ≐ y ⊍ z and φ(x) ≡ φ(y) ++ φ(z)
• c is x ≐ h (y) and φ(x) ≡ map h φ(y)

where ≡ denotes equality up to permutation (multiset equality). The above is mechanized as msetc_sem, where ≡ is mechanized as mset_eq.

Problem instance (mechanized as FMsetC_PROBLEM)

An instance of finite multiset constraint solvability is a list of constraints.

Decision problem (mechanized as FMsetC_SAT)

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

Reduction

Undecidability of finite multiset constraint solvability is obtained by reduction from uniform Diophantine constraint solvability (H10UC_SAT in Problems/H10UC.v). The reduction is mechanized in Reductions/H10UC_to_FMsetC.v as

Theorem H10UC_to_FMsetC : H10UC_SAT ⪯ FMsetC_SAT.

and

Theorem FMsetC_undec : Halt ⪯ FMsetC_SAT.

Key ideas [1]

For n ∈ ℕ let repeat 0 n = [0, …, 0] of length n and seq 0 n = [0, h (0), …, h^(n-1) (0)].

A natural number n ∈ ℕ is encoded as the list repeat 0 n.

Natural number addition is encoded as list concatenation.

For natural number squaring we observe the following.

• For multisets A, B such that A ++ B ≡ [0] ++ (map h A) we necessarily have A ≡ seq 0 n and B ≡ [h^n (0)] for some n ∈ ℕ.
• For a multiset A such that (seq 0 n) ++ A ≡ (repeat 0 n) ++ (map h A) we necessarily have length A + length A = n * n - n.

Relationship with AC1h unification

AC1h unification is term unification modulo associativity (A), commutativity (C) of a binary symbol + having 0 as the identity element (1), and a homomorphism h such that h (t + u) = h(t) + h(u) and h(0) = 0. Finite multisets satisfy (A), (C), and (1), when considered as multiset sums of their elements with the empty multiset as identity. Therefore, finite multiset constraint solvability, including h that is interpreted as homomorphic wrt. multiset sum, is an equivalent presentation of AC1h unification.

References

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