# zbMATH — the first resource for mathematics

Positive models and abstract data types. (Russian) Zbl 0693.68011
Let $$\sum$$ be any abstract type. Theory GES is a many-sorted theory over a type (cons, head, tail, nil, $$\in$$, $$\subseteq$$, $$\sum)$$ with a new sort of lists over the sort defined by $$\sum$$, and with natural axioms binding cons, head, tail and nil. Axiom of induction has the following form (parametrized by n) $(\Phi (nil)\wedge (\forall \alpha)(\forall y)(\Phi (\alpha)\to \Phi (cons(\alpha,y)))\to (\forall \alpha)\Phi (\alpha))$ where $$\Phi$$ has a prefix with no more than n-1 changing quantifier beginning with an existential one (for $$n=0$$ it must be quantifier-free formula). Theory $$GES_ 1$$ is GES with induction axiom for $$n=1$$. By a standard method it is shown that all primitive recursive functions are strongly represented in $$GES_ 1$$ by $$\sum$$-formulas. Similarly it is proved that $$GES_ 1$$ has non-standard models, i.e. such that $$tail^ k(a)\neq nil$$ for certain element a. The main theorem of the paper shows that if ((M,S),$$\nu)$$ is a positive model of $$GES_ 1$$, where M is the sort of elements, S is the sort of lists and $$\nu$$ is an enumeration of M, then $$S=HW(M)$$ and $$\nu$$ is unique up to autoequivalence positive enumeration.
Reviewer: A.Kreczmar
##### MSC:
 68P05 Data structures 03C70 Logic on admissible sets 68Q65 Abstract data types; algebraic specification