An array is a map TAT_A from an element of type TIT_I (index type) to an element of type TET_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 atomIatom_I and atomEatom_E denote an atom in the index logic and element logic, respectively, and let termIterm_I and termEterm_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} $

termE:termA[termI]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 TA=T_A^=

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

  2. function symbols:

    • a[i]a[i] is a binary function representing the read of array a at index ii;
    • a⟨i ▹ v⟩ is a ternary function representing the write of value vv to index ii of array aa, it returns a new array aa' s.t. a[i]=e,a'[i] = e, and a[j]=a[j]a'[j] = a[j] at all other jij \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