(*
Autor(s):
Andrej Dudenhefner (1)
Affiliation(s):
(1) Saarland University, Saarbrücken, Germany
*)
Autor(s):
Andrej Dudenhefner (1)
Affiliation(s):
(1) Saarland University, Saarbrücken, Germany
*)
(*
Problem:
Finite Multiset Constraint Solvability (FMsetC_SAT)
Finite multisets with one constant 0 and one unary constructor h.
A finite multiset A is represented by a list of its elements.
The element (h^n 0) is represented by the natural number n.
Constraints are of shape:
x ≐ 0
x ≐ y ⊍ z
x ≐ h (y)
Constraint semantics:
φ(y ⊍ z) = φ(y) ++ φ(z)
φ(h (y)) = map h (φ(y))
FMsetC:
Given a list of constraints,
is there a valuation φ : nat -> list nat such that
for each constraint c we have
if c is x ≐ 0, then φ(x) ≡ 0
if c is x ≐ y ⊍ z, then φ(x) ≡ φ(y) ++ φ(z)
if c is x ≐ h (y), then φ(x) ≡ map S (φ(y))
where ≡ is equality up to permutation?
References:
1 Paliath Narendran: Solving Linear Equations over Polynomial Semirings.
LICS 1996: 466-472, doi: 10.1109/LICS.1996.561463
*)
Require Import PeanoNat List.
Import ListNotations.
(* list equality up to permutation *)
Definition mset_eq (A B: list nat) : Prop :=
forall c, count_occ Nat.eq_dec A c = count_occ Nat.eq_dec B c.
Local Notation "A ≡ B" := (mset_eq A B) (at level 65).
(* constraints *)
Inductive msetc : Set :=
| msetc_zero : nat -> msetc
| msetc_sum : nat -> nat -> nat -> msetc
| msetc_h : nat -> nat -> msetc.
(* constraint semantics *)
Definition msetc_sem (φ: nat -> list nat) (c: msetc) :=
match c with
| msetc_zero x => φ x ≡ [0]
| msetc_sum x y z => φ x ≡ (φ y) ++ (φ z)
| msetc_h x y => φ x ≡ map S (φ y)
end.
(* given a list l of constraints,
is there a valuation φ satisfying each constraint? *)
Definition FMsetC_SAT (l : list msetc) := exists φ, forall c, In c l -> msetc_sem φ c.