Abstract

In this thesis we investigate various equivalence relations between expressions in first order LISP. This fragment of LISP includes the destructive operations rplaca and rplacd. To define the semantics we introduce the notion of a memory structure. The equivalence relations are then defined within this model theoretic framework. ;A distinction is made between intensional relations and extensional relations. The former class turned out to have a much more managable theory than the latter. The principle intensional relation studied is strong isomorphism, its properties allow for elegant verification proofs in a style similar to that of pure Lisp. In particular the relation is preserved under many standard syntactic manipulations and transformations. In particular it satisfied a Substitution theorem; any program that is obtained from another by replacing a portion by another strongly isomorphic one is guaranteed to be strongly isomorphic to the original one. ;A plethora of verification proofs of both simple and complex programs was given using the intensional equivalence relation. All of these proofs were of the transformation plus induction variety. In contrast, we gave some verification proofs of programs, using the extensional relations. Because the Substitution Theorem fails for these extensional relations, the proofs were necessarily of the hand simulation variety. ;In a more theoretical light, we also proved that the equivalence relations introduced here are decidable, and used them to study the expressive powers of certain fragments of Lisp