(theory Arrays
:written_by {Silvio Ranise and Cesare Tinelli}
:date {08/04/05}
:sorts (Index Element Array)
:funs ((select Array Index Element) (store Array Index Element Array))
:definition
"This is a theory of functional arrays without extensionality.
It is formally and completely defined by the axioms below.
"
:axioms
(
(forall (?a Array) (?i Index) (?e Element)
(= (select (store ?a ?i ?e) ?i) ?e))
(forall (?a Array) (?i Index) (?j Index) (?e Element)
(or (= ?i ?j)
(= (select (store ?a ?i ?e) ?j)
(select ?a ?j))))
)
:notes
"It is not difficult to prove that the two axioms above are logically
equivalent to the following \"McCarthy axiom\":
(forall (?a Array) (?i Index) (?j Index) (?e Element)
(= (select (store ?a ?i ?e) ?j)
(ite (= ?i ?j) ?e (select ?a ?j))))
Such an axiom appeared in the following paper:
Correctness of a Compiler for Arithmetic Expressions,
by John McCarthy and James Painter,
available at http://www-formal.stanford.edu/jmc/mcpain.html.
"
)