∃BV_{[n]}-Solvability

An Undecidable Problem

Oliver Möller October, 7th 1996 SRI, Menlo Park, CA

The Problem ∃BV_{[n]}-Solvability

Consider the theory of bitvectors with nonzero size and the operations . ⊗. (composition) and .ˆ (i,j) (extraction). i and j are allowed to be cardinal variables. Also, there exist constants of arbitrary but fixed length c, further denoted as 0_{[c]} and 1_{[c]}. Additional, there exists one special cardinal variable n, on which the terms can be dependent on, t.i. the

cardinal variables can be indexed from 1 through to n and we allow an operation ⨂_{i=1}^{n}, which is a composition

of n arguments. (Note that in the following ⨂_{i=1}^{m} is not really a new operation, for m will be a fixed number.)

Let t_{n} and u_{n} be bitvector-terms dependent on n. The problem to decide whether there exists a sollution to the equation ∃n : t_{n} = u_{n} is called ∃BV_{[n]}-Solvability.

Claim

∃BV_{[n]}-Solvability is undecidable.

Proof: (Reduction Post’s correspondence problem ≤ ∃BV_{[n]}-Solvability)

Let P = {(a_{1}, b_{1}), ..., (a_{m}, b_{m})}, m ≥ 1 be an instance of Post’s correspondence problem, a_{i}, b_{i} ∈ Σ^{+}. Basi-

cally, we will construct two ⨂_{i=1}^{n}-compositions which match if (and only if) there is a corresponding sequence

i_{1}, ..., i_{n} that solves the correspondence problem (t.i. a_{i_{1}}a_{i_{2}} ⋯ a_{i_{n}} = b_{i_{1}}b_{i_{2}} ⋯ b_{i_{n}}). Let σ Σ → Σ′ = {0, 1}^{ν} be a mapping from the basic alphabet into an artifical one, where ν := max(3, ⌈log_{2} ∥Σ∥⌉). σ^{∗} : Σ^{∗} → Σ′ ^{∗} is defined according to this. Let ω := max{|σ^{∗}(a_{i})| : i = 1, .., m} ∪ {|σ^{∗}(b_{i})| : i = 1, .., m}. Let μ := ⌈log_{2} m⌉, the binary length needed to store the information, which pair (a_{i}, b_{i}) is chosen. Thus let τ : {1, ... , m} → {0_{[1]}, 1_{[1]}}^{μ} be the binary encoding of these numbers, represented in compositions of bitvector constants. We introduce the following abbreviations:

A_{0}  := ⨂_{i=1}^{m}( 1_{[1]} ⊗ 0_{[|σ^{∗}(a_{i})|−2]} ⊗ 1_{[1]} ⊗ 1_{[μ]})
A_{CHOOSE} := ⨂_{i=1}^{m}(  σ^{∗}(a_{i})  ⊗ τ(i))
B_{0}  := ⨂_{i=1}^{m}( 1_{[1]} ⊗ 0_{[|σ^{∗}(b_{i})|−2]} ⊗ 1_{[1]} ⊗ 1_{[μ]})
B_{CHOOSE} := ⨂_{i=1}^{m}(  σ^{∗}(b_{i})  ⊗ τ(i))
Ω  := ⨂_{i=1}^{m} 0_{[max(|σ^{∗}(a_{i})|,|σ^{∗}(b_{i})|)+μ]}

We also need some (indexed) integer variables to express which pair is chosen. l_{i} and r_{i} will be the marker for the first argument (a), l′_{i} and r′_{i} accordingly to the second one. Also, we introduce some ’puffers’, namely c_{i}, d_{i}, e_{i} and c′_{i}, d′_{i}, e′_{i} to avoid arithmetic operations. It will yield that for every i ∈ {1, .., n} :

\begin{matrix}c_{i} = l_{i} − r_{i} & d_{i} = r_{i} − 1 & e_{i} = r_{i} − μ \\ c′_{i} = l′_{i} − r′_{i} & d′_{i} = r′_{i} − 1 & e′_{i} = r′_{i} − μ \end{matrix} \} (∗)

To make sure, that l_{i}, r_{i} always extract a valid pair-component out of A_{CHOOSE}(respectively l′_{i}, r′_{i} from B_{CHOOSE}), we define:

\begin{aligned}Φ_{n} & := & ⨂_{i=1}^{n} & A_{0}ˆ (l_{i}, r_{i}) & Φ′_{n} & := & ⨂_{i=1}^{n} & B_{0}ˆ (l′_{i}, r′_{i}) \\ Ψ_{n} & := & ⨂_{i=1}^{n} & (1_{[1]} ⊗ 0_{[ω]}ˆ (c_{i}, 0) ⊗ 1_{[1]}) & Ψ′_{n} & := & ⨂_{i=1}^{n} & (1_{[1]} ⊗ 0_{[ω]}ˆ (c′_{i}, 2) ⊗ 1_{[1]}) \end{aligned}

To enforce the ’right order’ of the segments, we will match

Δ_{n}^{A} := ⨂_{i=1}^{n} A_{CHOOSE}ˆ (d_{i}, e_{i})  and  Δ_{n}^{B} := ⨂_{i=1}^{n} B_{CHOOSE}ˆ (d′_{i}, e′_{i})

To make shure that (∗) yields, we introduce

Γ_{n} := ⨂_{i=1}^{n}(Ωˆ (l_{i}, r_{i}) ⊗ 1_{[1]} ⊗ Ω(r_{i}, d_{i}) ⊗ 1_{[1]} ⊗ Ωˆ (d_{i}, e_{i}) ⊗ 1_{[1]})
Λ_{n} := ⨂_{i=1}^{n}(Ωˆ (c_{i}, 0) ⊗ 1_{[1]} ⊗  0_{[2]}  ⊗ 1_{[1]} ⊗  0_{[ν]}  ⊗ 1_{[1]})
Γ′_{n} := ⨂_{i=1}^{n}(Ωˆ (l′_{i}, r′_{i}) ⊗ 1_{[1]} ⊗ Ω(r′_{i}, d′_{i}) ⊗ 1_{[1]} ⊗ Ωˆ (d′_{i}, e′_{i}) ⊗ 1_{[1]})
Λ′_{n} := ⨂_{i=1}^{n}(Ωˆ (c′_{i}, 0) ⊗ 1_{[1]} ⊗  0_{[2]}  ⊗ 1_{[1]} ⊗  0_{[ν]}  ⊗ 1_{[1]})

Now define the reduction f as follows:

f(P) := \{ \begin{matrix}Γ_{n} & ⊗ & Γ′_{n} & ⊗ & Φ_{n} & ⊗ & Φ′_{n} & ⊗ & Δ_{n}^{A} & ⊗ & ⨂_{i=1}^{n}A_{CHOOSE}ˆ (l_{i}, r_{i}) \\ Λ_{n} & ⊗ & Λ′_{n} & ⊗ & Ψ_{n} & ⊗ & Ψ′_{n} & ⊗ & Δ_{n}^{B} & ⊗ & ⨂_{i=1}^{n}B_{CHOOSE}ˆ (l′_{i}, r′_{i}) \end{matrix} =^{!}

It is obvious, that P has a sollution, if (and only if) f(P) is solvable.

Q.E.D