On the definition of classes of interpretations

  • Bruno Courcelle
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 52)


A class C of interpretations is algebraic if, roughly speaking, for every two recursive program schemes ø and ø', the equivalence of ø and ø' with respect to C can be proved by an induction on the length of computation [9] if it holds. Classes of interpretations can be defined by logical, and/or order theoretical conditions. We examine several cases of algebraicity (for classes defined by first-order conditions) and non-algebraicity.


Function Symbol Relational Class Predicate Symbol Structural Induction Induction Principle 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. [0]
    E. Aschroft, Z. Manna, A. Pnueli, "Decidable properties of monadic functional schemas", JACM Vol. 20 (1973) pp. 489–499.Google Scholar
  2. [1]
    G. Berry, B. Courcelle, "Program Equivalence and Canonical forms in stable discrete interpretations", Proc. of 3rd colloqium on Automata, Languages and Programming, Edinburgh, (1976). pp. 168–188.Google Scholar
  3. [2]
    R. Burstall, "Proving properties of programs by structural induction", Comp. Journal (12) pp. 41–48.Google Scholar
  4. [3]
    R. Burstall, J. Darlington, "A system which automatically improves programs", Proc. of 3rd Int. joint conf. artif. intelligence, S.R.I. (1973) pp. 537–542.Google Scholar
  5. [4]
    B. Courcelle, M. Nivat, "Algebraic Families of interpretations", 17th symp. on F.O.C.S., Houston (1976) (also available as Laboria Report no 189).Google Scholar
  6. [5]
    S.A. Greibach, "Theory of program Structures: Schemes, Semantics, Verifications" Lecture Notes in Computer Science Vol 36 (1975) Springer Verlag.Google Scholar
  7. [6]
    I. Guessarian, "Semantic equivalence of program schemes", Proc. of 3rd coll. on Aut., Languages and Programming, Edinburgh (1976), pp. 189–200.Google Scholar
  8. [7]
    J. Kfoury, D. Park, "On termination of program schemas" Inf. and Control Vol 29 (1975) pp. 243–251.Google Scholar
  9. [8]
    R. Milner, "Models of LCF", Memo stanford. AIM-184 (1973).Google Scholar
  10. [9]
    J.H. Morris, "Another Recursion Induction Principle", CACM Vol 14, no5 (1971).Google Scholar
  11. [10]
    M. Nivat, "On the interpretation of polyadic recursive schemes", symp. Mathematica Vol 15, Academic Press (1975).Google Scholar
  12. [11]
    D. Park, "Finiteness is μ-ineffable", Report no3, Warwick University (1974).Google Scholar
  13. [12]
    J.R. Schoenfield, "Mathematical Logic", Addison-Wesley (1967).Google Scholar
  14. [13]
    B. Courcelle, I. Guessarian, M. Nivat, "The algebraic semantics of recursive program schemes", submitted for publication.Google Scholar
  15. [14]
    A. Chandra, "Generalized program schemas" SIAM J. on computing Vol 5 (1976) pp. 402–413.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1977

Authors and Affiliations

  • Bruno Courcelle
    • 1
  1. 1.IRIA, RocquencourtLe ChesnayFrance

Personalised recommendations