Result: Comparaison et équivalence de sémantiques pour les schémas de programmes non déterministes. (Comparison and equivalence of semantics for non-deterministic program schemes)
Further Information
We discuss three different definitions of the semantics of a non- deterministic recursive program scheme in Herbrand's universe: - the operational semantics based on the terminating computations [first introduced by \textit{G. Boudol}, Lect. Notes Comput. Sci. 112, 147-161 (1981; Zbl 0485.68020); Algebraic methods in semantics, Semin. Fontainbleau/France 1982, 169-232 (1985; Zbl 0611.68007)]; - the denotational semantics defined by a greatest fixed point method [\textit{A. Arnold} and \textit{M. Nivat}, Fundam. Inf. 3, 445-475 (1980; Zbl 0453.68021); Math. Syst. Theory 13, 219-236 (1980; Zbl 0441.68044); Theor. Comput. Sci. 11, 181-205 (1980; Zbl 0427.68022)]; - the so-called algebraic semantics which is obtained in two steps: first we consider the scheme as being a deterministic one, by hiding all non-deterministic choice symbols (`or') in a tree, and computing all rewriting sequences of that tree, second, we interpret in the resulting finite or infinite trees the `or' symbols as union of sets of trees. We study those three sets of trees; we show that in the general case they are naturally embedded, and equal in the case of Greibach schemes. Making notice of the fact that a set of mappings can be canonically interpreted as a multivalued-mapping, we define an equivalence relation on sets of trees, and we show that modulo this relation, the three semantics are indistinguishable.