Type definitions with parameters

ABSTRACT

It has long been known that recursively defined types in a highly typed language such as Algol 68 or Pascal may be tested for structural equivalence by the same algorithm that compares finite automata [5,11]. Several authors (for example, [3,8,9,16]) have proposed that classes of types be simultaneously defined by the use of parameterized type definitions, such asType list(x) = record val:x; next:↑list(x) end .This paper shows that unless the use of such parameterized definitions is restricted, new (unparameterized) types may be defined which more closely resemble deterministic context-free languages. In fact, the equivalence problem for such types becomes as hard as the (currently unsolved) deterministic pushdown automaton equivalence problem. Several restrictions on type definitions are considered which allow known equivalence algorithms to be applied.

REFERENCES

• 1: Alfred V. Aho , Jeffrey D. Ullman, Theory of Parsing, Translation and Compiling, Prentice Hall Professional Technical Reference, 1973
• 2: Goguen, J. A. and Thatcher, J. W. Initial algebra semantics. IEEE Symposium on Switching and Automata Theory, v. 15, 1974, 63-77.
• 3: Peter Naur, IFIP WG2.1: Report of Subcommittee on Data Processing and Transput, ALGOL Bulletin [doi>10.1145/1061589.1061595]
• 4: Kathleen Jensen , Niklaus Wirth, Pascal-User Manual and Report, Springer-Verlag New York, Inc., Secaucus, NJ, 1975
• 5: J. Kral, The Equivalence of Modes and the Equivalence of Finite Automata, ALGOL Bulletin [doi>10.1145/1061623.1061632]
• 6: B. W. Lampson , J. J. Horning , R. L. London , J. G. Mitchell , G. J. Popek, Report on the programming language Euclid, ACM SIGPLAN Notices, v.12 n.2, p.1-79, February 1977 [doi>10.1145/954666.971189]
• 7: 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]
• 8: C. H. Lindsey, Modals, ALGOL Bulletin [doi>10.1145/1061646.1061652]
• 9: Liskov, B., et al. Abstraction Mechanisms in CLU. M.I.T. Computation Structures Group Memo 144-1. January, 1977.
• 10: Rosen, B. K. and Lewis, C. H. Recursively defined datatypes, part II. Report RC 4713, IBM T. J. Watson Research Center, Yorktown Heights, N. Y., 1974.
• 11: Marvin Solomon, Modes, values and expressions, Proceedings of the 2nd ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.149-159, January 20-22, 1975, Palo Alto, California [doi>10.1145/512976.512992]
• 12: Marvin Harry Solomon, Theoretical issues in the implementation of programming languages., 1977
• 13: Stearns, R. E. A regularity test for pushdown machines. Inf. and Control 11, 3 (September, 1967), 323-340.
• 14: Valient, L. B. The equivalence problem for deterministic finite-turn pushdown automata. Inf. and Control 25, 2 (June, 1974), 123-133.
• 15: Wijngaarden, A. van et al. Revised report on the algorithmic language ALGOL 68. Acta Informatica 5 (1975), 1-236.
• 16: Wulf, W. A., London, R. L., and Shaw, M. Abstraction and verification in Alphard: introduction to language and methodology. Technical report, Carnegie-Mellon University, June 14, 1976.