ABSTRACT
According to folklore, Algol is an “orthogonal” extension of a simple imperative programming language with a call-by-name functional language. The former contains assignments, branching constructs, and compound statements; the latter is based on the typed λ-calculus. In an attempt to formalize the claim of “orthogonality”, we define a simple version of Algol and an extended λ-calculus. The calculus includes the full β-rule and rules for the reduction of assignment statements and commands. It has the usual properties, e.g., it satisfies a Church-Rosser and Strong Normalization Theorem. In support of the claim that the imperative and functional components are orthogonal to each other, we show that the proofs of these theorems are combinations of separate Church-Rosser and Strong Normalization theorems for each sublanguage.
An acclaimed consequence of Algol's orthogonal design is the idea that the evaluation of a program has two distinct phases. The first phase corresponds to an unrolling of the program according to the usual β and fixpoint reductions, which provide the formal counterpart to Algol's famous copy rule. The result of this phase is essentially an imperative program. The second phase executes the output of the first phase in the imperative fashion of a stack machine. Given our calculus, we can prove a Postponement Theorem and can thus formalize this phase separation.
- 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.]]Google Scholar
- 2.CRANK, E. AND M. FELLEISEN. Parameterpassing and the lambda-cMculus. In Proc. 18th A CM Symposium on Principles of Programming Languages, 1991,233-245.]] Google ScholarDigital Library
- 3.DAALEN VAN, D. The Language Theory of A UTOMATH. Ph.D. Dissertation, Eindhoven University, 1980.]]Google Scholar
- 4.DEMERS, A. AND J. DONAHUE. Making variables abstract: an equational theory for Russell. In Proc. l Oth A CM Symposium on Principles of Programming Languages, 1983, 59-72.]] Google ScholarDigital Library
- 5.FELLEISEN, M. The Calculi of Lambda-v-CS- Conversion: A Syntactic Theory of Control and State in Imperative Higher-Order Programming Languages. Ph.D. dissertation, Indiana University, 1987.]] Google ScholarDigital Library
- 6.FELLEISEN, M. On the expressive power of programming languages. Science of Computer Programming 17, 1991, 35-75. Preliminary version in: Proc. 3rd European Symposium on Programming. Nell Jones, Ed. Lecture Notes in Computer Science, 432. Springer Verlag, Berlin, 1990, 134-151.]] Google ScholarDigital Library
- 7.FELLEISEN~ M. AND D.P. FRIEDMAN. Control operators, the SECD-machine, and the A- calculus. In Formal Description of Programming Concepts III, edited by M. Wirsing. Elsevier Science Publishers B.V. (North-Holland), Amsterdam, 1986, 193-217.]]Google Scholar
- 8.FELLEISEN, M. AND D.P. FRIEDMAN. A syntactic theory of sequentiM state. Theor. Cornput. Sci. 69(3), 1989, 243-287. Preliminary version in: Proc. 14th A CM Symposium on Principles of Programming Languages, 1987, b314-325.]] Google ScholarDigital Library
- 9.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. 102~ 1992.]] Google ScholarDigital Library
- 10.GUZM.~N, J.C. AND P. HUDAK. Singlethreaded polymorphic lambda-calculus. In Proc. Symposium on Logic in Computer Science, 1990, 333-345.]]Google Scholar
- 11.LENT, A. F. The Category of Functors from State Shapes to Bottomless CPOs is Adequate for Block Structure. Master's thesis, MIT, 1992.]]Google Scholar
- 12.MASON, I.A. AND C. TALCOTT. Equivalence in functional programming languages with effects. Journal of Functional Programming 1 (3), July 1991, 287-327. Preliminary version in: Proc. International Conference on Automata, Languages and Programming. Springer Lecture Notes in Computer Science, Vol. 372, Berlin, 1989, 574-588.]] Google ScholarDigital Library
- 13.MASON, I.A. AND C. TALCOTT. Inferring the equivalence of functional programs that mutate data. Theor. Comput. Sci. 105(2), 1992, 167- 215. Preliminary version in: Proc. Symposium on Logic in Computer Science. Computer Society Press, Washington, D.C., 1989, 284-293.]] Google ScholarDigital Library
- 14.NAUR, P. (Ed.). Revised report on the algorithmic language ALGOL 60. Comm. A CM 6(1), 1963, 1- 7.]] Google ScholarDigital Library
- 15.PLOTKIN, G.D. Call-by-name, call-by-value, and the )~-calculus. Theor. Comput. Sci. 1, 1975, 125-159.]]Google ScholarCross Ref
- 16.REDDY, U.S., V. SWAttUP, AND E. IRELAND. Assignments for applicative languages, in Proc. Conference on Functional Programming and Computer Architecture. Lecture Notes in Computer Science~ Vol. 523. Springer Verlag, Berlin, 1991, 192-214.]] Google ScholarDigital Library
- 17.REYNOLDS, J.C. Replacing complexity with generality: The programming language Forsythe. Unpublished manuscript, Carnegie Mellon University, Computer Science Department, 1991.]]Google Scholar
- 18.REYNOLDS, J.C. The essence of Algol. In Algorithmic Languages, edited by de Bakker and van Vliet. North-Holland, Amsterdam, 1981, 345-372.]]Google Scholar
- 19.REYNOLDS, J.C. Preliminary Design of the Programming Language Forsythe. Technical Report CMU-CS-88-159, Carnegie Mellon University, Computer Science Department, 1988.]]Google Scholar
- 20.S~INDERGAttD, H. AND P. SESTOFT. Referentim transparency, definiteness and unfoldability. Acta Informatica 27, 1990, 505-517.]] Google ScholarDigital Library
- 21.WADLER, P. Comprehending monads. In Proc. 1990 A CM Conference on Lisp and Functional Programming, 1990, 61-78.]] Google ScholarDigital Library
- 22.WRIGHT, A. AND l~/I. FELLEISEN. A syntactic approach to type soundness. Technical Report 160. Rice University, 1991. Information and Computation, 1992, to appear.]]Google Scholar
Index Terms
- On the orthogonality of assignments and procedures in Algol
Recommendations
On the machine conversion of B5500 Algol to CDC 6000 Algol
ACM '71: Proceedings of the 1971 26th annual conferenceThis paper describes the machine conversion of Algol for the Burroughs B5500 to Algol for the CDC 6000 series. CDC Algol is essentially Algol 60 and is a subset of Burroughs Algol which is the primary language for the B5500. Burroughs Algol implements ...
Dynamic Logic of Propositional Assignments: A Well-Behaved Variant of PDL
LICS '13: Proceedings of the 2013 28th Annual ACM/IEEE Symposium on Logic in Computer ScienceWe study a version of Propositional Dynamic Logic (PDL) that we call Dynamic Logic of Propositional Assignments (DL-PA). The atomic programs of DL-PA are assignments of propositional variables to true or to false. We show that DL-PA behaves better than ...
Does LISP differ from ALGOL essentially?
A fare spread opinion is that LISP and ALGOL belong to different "families" of programming languages. In our current activities concerning LISP, we are trying to characterise pure LISP as an ALGOL-like programming language in the sense of ALGOL 60 resp. ...
Comments