×

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
PDF BibTeX XML Cite