Observable sequentiality and full abstraction

ABSTRACT

One of the major challenges in denotational semantics is the construction of fully abstract models for sequential programming languages. For the past fifteen years, research on this problem has focused on developing models for PCF, an idealized functional programming language based on the typed lambda calculus. Unlike most practical languages, PCF has no facilities for observing and exploiting the evaluation order of arguments in procedures. Since we believe that such facilities are crucial for understanding the nature of sequential computation, this paper focuses on a sequential extension of PCF (called SPCF) that includes two classes of control operators: error generators enable us to construct a fully abstract model for SPCF that interprets higher types as sets of error-sensitive functions instead of continuous functions. The error-sensitve functions form a Scott domain that is isomorphic to a domain of decision trees. We believe that the same construction will yield fully abstract models for functional languages with different control operators for observing the order of evaluation.

REFERENCES

• 1: BARENDREGT, H.P. The Lambda Calculus: Its Syntax and Semantics. Revised Edition. Studies in Logic and the Foundations of Mathematics 103. North-Holland, Amsterdam, 1984.
• 2: BERRY, G. ModUles compl~tement addquafs et stables des lambda-calculus typd. Ph.D. dissertation, Universit~ Paris VII, 1979.
• 3: BERRY, G. AND P-L. CURIEN. Sequential algorithms on concrete data structures. Theor. Comput. Sci. 20, 1982, 265-321.
• 4: G Berry , P L Curien, Theory and practice of sequential algorithms: the kernel of the applicative language CDS, Algebraic methods in semantics, Cambridge University Press, New York, NY, 1986
• 5: BEnnY, G., P-L. CUaIEN, AND P.-P. L~.vY. Fullabstraction of sequential languages: the state of the art. In Algebraic Methods in Semantics, edited by :}. Reynolds and M.Nivat. Cambridge University Press. London, 1985, 89-131.
• 6: CAR.TWRIGHT, R. AND i. DEMERS. The topology of program termination. In Proc. Symposium on Logic in Computer Science, 1988, 296-308.
• 7: CARTWRIGHT, R.S. AND M. FELLEISEN. Observable sequentiality and full abstraction. Technical Report TR91-167. Rice University Department of Computer Science, 1991.
• 8: Currien, Categorical Combinators, Sequential Algorithms and Funtional Programming, Halsted Press, New York, NY, 1986
• 9: M. Felleisen, The theory and practice of first-class prompts, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.180-190, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73576]
• 10: FELLEISEN, M. AND R. HIEB. The revised report on the syntactic theories of sequential control and state. Technical Report 100, Rice University, June 1989. Theor. Comput. Sci., 1991, to appear.
• 11: M. Felleisen , D. P. Friedman , E. Kohlbecker , B. Duba, A syntactic theory of sequential control, Theoretical Computer Science, v.52 n.3, p.205-237, June 1987 [doi>10.1016/0304-3975(87)90109-5]
• 12: KAHN, G. AND G. PLOTKIN. Structures des donnds concretes. INRIA Report 336. 1978.
• 13: A. R. Meyer , K. Sieber, Towards fully abstract semantics for local variables, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.191-203, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73577]
• 14: MILNER, R. Fully abstract models of typed A- calculi. Theor. Comput. Sci. 4, 1977, 1-22.
• 15: Ketan Mulmuley, Full abstraction and semantic equivalence, MIT Press, Cambridge, MA, 1987
• 16: I:)LOTKIN, G.D. LCF considered as a programming language. Theor. Comput. Sci. 5, 1977, 223-255.
• 17: RosE, J.R. AND G.L. STEELE JR. C*: An extended C language for data parallel programming. In Proc. Second International Conference on Supercomputing. International Supercomputing Institute, Inc. (Santa Clara, 1987) Volume iI, 2-16. Also available as: Technical Report No. PL87-5, Thinking Machines Corporation, 1987.
• 18: Dana S. Scott, Domains for Denotational Semantics, Proceedings of the 9th Colloquium on Automata, Languages and Programming, p.577-613, July 12-16, 1982
• 19: SCOTT, D.S. Lectures on a Mathematical Theory of Computation. Techn. Monograph PRG-19, Oxford University Computing Laboratory, Programming Research Group, 1981.
• 20: Dorai Sitaram , Matthias Felleisen, Reasoning with continuations II: full abstraction for models of control, Proceedings of the 1990 ACM conference on LISP and functional programming, p.161-175, June 27-29, 1990, Nice, France [doi>10.1145/91556.91626]
• 21: Guy L. Steele, Jr., Common LISP: the language, Digital Press, Newton, MA, 1984
• 22: STEELE, G.L., Ja. AND G.J. SUSSMAN. The revised report on Scheme, a dialect of Lisp. Memo 452, MIT AI-Lab, 1978.
• 23: Allen Stoughton, Fully abstract models of programming languages, Pitman Publishing, Inc., Marshfield, MA, 1988

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Denotational semantics

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

  G. Mathematics of Computing
  G.2 DISCRETE MATHEMATICS
      G.2.2 Graph Theory
          Subjects: Trees

General Terms:
Languages, Theory