Initial Algebra Semantics and Continuous Algebras

ABSTRACT

Many apparently divergent approaches to specifying formal semantics of programming languages are applications of initial algebra semantics. In this paper an overview of initial algebra semantics is provided. The major technical feature is an initial continuous algebra which permits unified algebraic treatment of iterative and recursive semantic features in the same framework as more basic operations.

REFERENCES

• 1: AHo. A V . AND ULLMAN, J D Properties of syntax directed translations J Computer and Syst, Scts. 3 (1969), 319-334
• 2: Ano, A B , AND ULLMAN, J D Translations of a context-free grammar Inform and Contr 19 (1971), 439-475
• 3: BAKER, B S Tree transductlons and families of tree languages Tech Rep TR9-73, Center for Research m Computing Technology, Harvard U , Cambridge, Mass , 1973
• 4: BEKI,~, H Definable operations in general algebra and the theory of automata and flowcharts Research Rep, IBM Laboratory, Vienna, Austria, 1969
• 5: B~NABOU, J Structures algGbrlques dans les catGgorles Th~se, fac scl , Unlverslt6 de Pans, March 1966 Also, Cahters de Topologze et G~om~trte Dtff~renuelle 10 (1968), 1-126
• 6: BII~KHOFF, G Structure of abstract algebras Proc Cambrtdge Phd Soc 31 (1938), 433-454
• 7: BIRKHOFF, G , AND LIeSON. J D Heterogeneous algebras J Combmatonal Theory 8 (1970), 115-133
• 8: BLIKLE, A Equational languages Inform and Contr 21 (1972). 134-147
• 9: BLOOM, S L , AND ELGOr, C C The existence and construction of free iteratlve theortes. Research Rep RC-4937, IBM Thomas J Watson Research Center, Yorktown Heights, N Y, 1974
• 10: BURSXALL, R M , ANO LANOIN, P J Programs and their proofs An algebraic approach Machine Intelhgence, Vol 4, B Meltzer and D Mlchie, Eds , Edinburgh U Press, Edinburgh, Scotland, 1969, pp 17- 43
• 11: Rod M. Burstall , James W. Thatcher, The algebraic theory of recursive program schemes, Proceedings of the Proceedings of the First International Symposium on Category Theory Applied to Computation and Control, p.126-131, February 25-26, 1974
• 12: Ashok K. Chandra, Degrees of translatability and canonical forms in program schemas: Part I, Proceedings of the sixth annual ACM symposium on Theory of computing, p.1-12, April 30-May 02, 1974, Seattle, Washington, United States [doi>10.1145/800119.803879]
• 13: COVlN, P M Unwersal Algebra Harper and Row. New York, 1965
• 14: B. Courcelle , J. Vuillemin, Semantics and axiomatics of a simple recursive language., Proceedings of the sixth annual ACM symposium on Theory of computing, p.13-26, April 30-May 02, 1974, Seattle, Washington, United States [doi>10.1145/800119.803880]
• 15: DONER, J E Tree acceptors and some of their applications J Computer and Syst Scts 4 (1970), 406- 451
• 16: EILENBERG. S , AND WRIGHT, J B Automata in general algebras Inform and Control 11 (1967), 452- 470
• 17: ELGOT, C C Monadlc computation and ~teratwe algebraic theories Research Rep. RC-4564, IBM Thomas J Watson Research Center, Yorktown Heights, N Y, 1973, also Proc Logic Colloqmum '73, Bristol, England, North-Holland Pub Co , Amsterdam, 1975, pp 175-230
• 18: ENGELFRIET, J , AND SCHMIDT, E M IO and Ol Dataloglsk Afdehng Rep, DAIM1 PB-47, Aarhus U , Aarhus, Denmark, July 1975
• 19: Seymour Ginsburg, The Mathematical Theory of Context-Free Languages, McGraw-Hill, Inc., New York, NY, 1966
• 20: GOGUEN, j A On homomorphlsms, correctness, terminahon, unfoldments and eqmvalence of flow diagram programs Proc 13th Ann IEEE Symp on Sw~tchlng and Automata Theory, 1972, pp 52-60 A portion of this paper appears m expanded form in J Computer and Syst Scls 8 (1974), 333-365
• 21: Joseph A. Goguen, Semantics of computation, Proceedings of the Proceedings of the First International Symposium on Category Theory Applied to Computation and Control, p.151-163, February 25-26, 1974
• 22: GOGUEN, J A , AND TI-IATC~ER. I W lmttal algebra semantics Extended Abstract, Research Rep RC- 4865, IBM Thomas J Watson Research Center, Yorktown Heights, N Y, May 1974, also, Proc 15th Ann IEEE Symp on Switching and Automata Theory, 1974, pp 63-77
• 23: GoouEN, I A, TnA'rCHER, J W , WAGNER, E G, ANO WRIGHT, J B A junction between computer science and category theory, I Basic definitions and examples Pt 1, Research Rep RC-4526, Pt 2, Research Rep RC-5908, IBM Thomas J Watson Research Center, Yorktown Heights, N Y , 1973, 1976
• 24: GO~trEN, J A , THATCHER, J W. WAGNER, E G, AND WRIGHT, J B Abstract data-types as lmtlal algebras and correctness of data representations Proc. Conference on Computer Graphics, Pattern Recognmon and Data Structure. May 1975, pp 89-93
• 25: GO~UEN, J A , THATCHER, J W, WAGNER, E G , ANn WmGnT, J B. Programs In categories (summary), in preparation
• 26: GORDON, M Models of pure LISP Ph D Th , Edinburgh U , Edinburgh, Scotland, 1973
• 27: GRAETZER, G UntversalAlgebra Van Nostrand, Princeton, N J , 1968
• 28: HIo~ISS, P J Algebras with a schema of operators Math Nachr 27 (1963), 115-132
• 29: Edgar T. Irons, A syntax directed compiler for ALGOL 60, Communications of the ACM, v.4 n.1, p.51-55, Jan. 1961 [doi>10.1145/366062.366083]
• 30: KNUTH, D E Semantics of context-free languages Math Syst Theory 2 (1968), 127-145
• 31: LANDIN, P J A program machme symmetric automata theory Machlne Intelhgence 5, B Meltzer and D MlcMe, Eds, Edinburgh U. Press, Edinburgh, Scotland, 1970, pp 99-120.
• 32: LAWVnRE, F W Functorlal semantics of algebraic theories. Proc. Nat Acad Sct. 50 (1963), 869-872.
• 33: C. H. Lewis , B. K. Rosen, Recursively defined data types: part 1, Proceedings of the 1st annual ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.125-138, October 01-03, 1973, Boston, Massachusetts [doi>10.1145/512927.512939]
• 34: P. M. Lewis, II , R. E. Stearns, Syntax-Directed Transduction, Journal of the ACM (JACM), v.15 n.3, p.465-488, July 1968 [doi>10.1145/321466.321477]
• 35: LUCAS, P, LAUER, P, AND STIGLEITNER. H Method and notation for the formal definition of programmmg languages Tech Rep TR 25 087, IBM Laboratory, Vienna, Austria, 1968
• 36: McCARTHY. J Towards a mathematical science of computation Proc IFIP Cong. North-Holland Pub Co, Amsterdam, 1962, pp 21-28
• 37: MCCARTHY, J A formal description of a subset of ALGOL In "Formal Language Description Languages for Computer Programming," Proc IFIP Working Conf 1964, T B Steel, Jr, Ed , North-Holland Pub Co , Amsterdam, 1966, pp 1-12
• 38: MCCARTHY, J , AND PAINTER, J Correctness of a compiler for arithmetic expressions In "Mathematical Aspects of Computer Science," Proc of Symposia In Applied Mathematics, Vol 19, J T Schwartz, Ed , Amer Math Soc, Providence, R I , 1967, pp 33-41
• 39: MACLANE, S Category Theory for the Worklng Mathematician Springer, New York, 1971
• 40: MAGIDOR, i , AND MORGAN, G Finite automata over finite trees Tech Rep 30, Hebrew U , Jerusalem, Israel, 1969
• 41: MAiBAUM, T S E The characterization of the derivation trees of context-free sets of terms as regular sets Proc 13th Ann IEEE Symp on Switching and Automata Theory, 1972, pp. 224-230
• 42: MAIBAUM, T S E Generalized grammars and homomorphic images of regular sets Research Rep CS-73- 30, U of Waterloo, Waterloo, Ontario, Canada, 1973
• 43: Zohar Manna, Properties of Programs and the First-Order Predicate Calculus, Journal of the ACM (JACM), v.16 n.2, p.244-255, April 1969 [doi>10.1145/321510.321516]
• 44: MARKOWSKY, G Chain-complete posets and directed sets with applications Research Rep RC-5024, IBM Thomas J Watson Research Center, Yorktown Heights, N Y, Aug 1974
• 45: MEZEI, J , AND WRIGHT, J B Algebraic automata and context-free sets Inform and Contr 11 (1967), 3- 29
• 46: Francis Lockwood Morris, Correctness of translations of programming languages--an algebraic approach, 1972
• 47: F. Lockwood Morris, Advice on structuring compilers and proving them correct, Proceedings of the 1st annual ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.144-152, October 01-03, 1973, Boston, Massachusetts [doi>10.1145/512927.512941]
• 48: NWAT, M Languages algGbralc sur le magna hbre et sGmantique des schdmas de programme In Automata, Languages and Programming, M Nlvat (Ed), North-Holland Pub Co , Amsterdam, 1972, pp 293-308
• 49: PARK, D F~xpomt induction and proofs of program properties Machine lntelhgence, Vol 5, B Meltzer and D Mlchie, Eds , Edinburgh U Press, Edmburgh, Scotland, 1970. pp 59-78 '
• 50: PETRONE, L Syntactic mappings of context-free languages Proc IFIP Cong 1965, Vol 2, North- Holland Pub Co, Amsterdam, pp 590-591
• 51: PorrENGER, R ARBOL, a system for defining functions on trees A I Memo 3, UCLA, 1976
• 52: RABIN, M P, AND SCOT, D Finite automata and their decision problems IBM J Res Develop 3 (1959), 114-125
• 53: John C. Reynolds, Definitional interpreters for higher-order programming languages, Proceedings of the ACM annual conference, p.717-740, August 01-01, 1972, Boston, Massachusetts, United States [doi>10.1145/800194.805852]
• 54: John C. Reynolds, On the Relation between Direct and Continuation Semantics, Proceedings of the 2nd Colloquium on Automata, Languages and Programming, p.141-156, July 29-August 02, 1974
• 55: REYNOLDS, J C. Semantics of the lattice of flow diagrams. Manuscript, Syracuse U , Syracuse, N Y , submitted for publication, July 1975
• 56: ROSEN, B K Program equivalence and context-free grammars Proc 13th Ann IEEE Symp on Switching and Automata Theory, 1972, pp 7-18, revised as Research Rep RC-4822, IBM Thomas J Watson Research Center, Yorktown Heights. N Y, 1974
• 57: ROUNDS, W C Mappings and grammars on trees Math Syst Theory 4 (1970), 256-287
• 58: SCHUTZENBERGER, M P Context-free languages and push down automata Inform and Contr 6 (1963), 246-264
• 59: SCHWARTZ, J T Semantic defmmon methods In Formal Semantics of Programmmg Languages, R Rustm, Ed , Prentice-Hall, Englewood Cliffs, N J , 1972, pp 1-23
• 60: SCOTT, D Outline of a mathematical theory of computation Proc 4th Ann Princeton Conf on Information Sciences and Systems, 1970, pp 169-176
• 61: Scoyr, D The lattice of flow diagrams Tech Monograph PRG 3, Oxford U Computing Lab , Oxford U , Oxford, England, also, Lecture Notes tn Mathematics, Vol 182 Semantics of Algortthmtc Languages, E Engeler. Ed , Springer. Berlin, 1971, pp 311-366
• 62: ScoTt, D Continuous lattices Tech. Monograph PRG 7, Oxford U Computing Lab, Oxford U, Oxford, England, 1971, also, Lecture Notes m Mathemattcs, Vol 274, Springer, Berhn, 1971, pp 97-136
• 63: Scorr, D Data types as lattices Unpubhshed notes, Amsterdam, 1972
• 64: ScoTT, D Data types as latUces Unpubhshed notes, Oxford, 1974
• 65: Scott, D AND SXRACHEV, C Towards a mathematacal semantics for computer languages Tech Monograph PRG 6, Oxford U. Computing Lab., Oxford U., Oxford, England, 1971, also, Computers and Automata, J Fox, Ed , Wdey, New York, 1971, pp 19-46
• 66: STRACHEV, C, ANO WADSWORTH, C P Contmuatlons-A mathematical semantics for handhng full jumps Tech Monograph PRG-11, Programming Research Group, Oxford U Computing Lab, Oxford, England, 1974
• 67: THATCHER, J.W. Characterizing derwat~on trees of context free grammars through a generahzatlon of fimte automata theory J Computer and Syst Scts 1 (1967), 317-322
• 68: THATCrIER, J W Generahzed~- sequential machines J Computer and Syst. Scts 4 (1970), 339-367
• 69: THATCHER, J W Tree automata' An informal survey In Currents tn Computing, A V, Aho, Ed, Prentice-Hall, Englewood Chffs, N J , 1973, 143-172
• 70: THATCHER, J W., AND WRIGHT, J B. Generahzed flmte automata theory with an application to a decision problem of second-order logic Math Systems Theory 2 (1968), 57-81
• 71: TURNE~, R Doctoral Dlss, U of London, London, England, 1973
• 72: VUILLEMIN, J Syntaxe, S6mant~que et Axlomat~que d'un Langage de Programmation Simple These d'Etat, Umverslt6 Pans 6, France, 1974
• 73: Eric G. Wagner, An algebraic theory of recursive definitions and recursive languages, Proceedings of the third annual ACM symposium on Theory of computing, p.12-23, May 03-05, 1971, Shaker Heights, Ohio, United States [doi>10.1145/800157.805034]
• 74: WA6NER, E G Languages for defining sets in arbitrary algebras. Proc llth Ann IEEE Syrup on Switching and Automata Theory, 1971, pp 191-201
• 75: WAND, M A concrete approach to abstract recurswe deflmt~ons inAutomata, Languages and Programmmg, M Ntvat, Ed , North-Holland Pub Co., Amsterdam, 1972, pp 331-341.
• 76: Mitchell Wand, An algebraic formulation of the Chomsky hierarchy, Proceedings of the Proceedings of the First International Symposium on Category Theory Applied to Computation and Control, p.209-213, February 25-26, 1974
• 77: VAN WIJNGAARDEN, A., Ed Report on the algonthmlc language ALGOL 68 Numer Math 14 (1969), 79-218

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.3 Formal Languages
          Subjects: Algebraic language theory

General Terms:
Languages, Theory, Verification