An array is a map $T_A$ from an element of type $T_I$ (index type) to an element of type $T_E$.

Two kinds of array logic:

• Extensional theories require that if two arrays store the same value at index i, for each index i, then the arrays must be the same.
• Non-extensional theories do not make this requirement.

Definition (array logic). The syntax of a formula in array logic is defined by extending the syntactic rules for the index logic and the element logic. Let $atom_I$ and $atom_E$ denote an atom in the index logic and element logic, respectively, and let $term_I$ and $term_E$ denote a term in the index and element logic, respectively:

atom: atom_I\ |\ atom_E\ |\ ¬atom\ |\ atom ∧ atom\ |\ ∀ array-identifier . atom

$term_A : array\ identifier\ |\ term_A {term_I ← term_E}$

$term_E :term_A[term_I]$

Observe that equality between arrays is not permitted by the grammar. Equality between arrays a1 and a2 can be written as ∀i. a1[i] = a2[i], assuming equality is permitted by the element theory.

Extensional Theory of Arrays $T_A^=$

1. $Σ_A : {·[·], ·⟨·▹·⟩, =}$

2. function symbols:

• $a[i]$ is a binary function representing the read of array a at index $i$;
• a⟨i ▹ v⟩ is a ternary function representing the write of value $v$ to index $i$ of array $a$, it returns a new array $a'$ s.t. $a'[i] = e,$ and $a'[j] = a[j]$ at all other $j \neq i$ ;
3. predicate

• $=$ is a binary predicate.

decidability

1. full: undecidable (even without extensionality)
encode FOL

2. Quantier-free: decidable

• Without extensionality: [McCarthy, 62]
• With extensionality paper