Extending the loop language with higher-order procedural variables

ABSTRACT

We extend Meyer and Ritchie's Loop language with higher-order procedures and procedural variables and we show that the resulting programming language (called Loop^ω) is a natural imperative counterpart of Gödel System T. The argument is two-fold:

(1) we define a translation of the Loop^ω language into System T and we prove that this translation actually provides a lock-step simulation,

(2) using a converse translation, we show that Loop^ω is expressive enough to encode any term of System T.

Moreover, we define the “iteration rank” of a Loop^ω program, which corresponds to the classical notion of “recursion rank” in System T, and we show that both translations preserve ranks. Two applications of these results in the area of implicit complexity are described.

REFERENCES

• 1: Andrew W. Appel, Modern Compiler Implementation: In ML, Cambridge University Press, New York, NY, 1998
• 2: Avigad, J. and Feferman, S. 1998. Gödel's functional (“dialectica”) interpretation. In Handbook of Proof Theory, S. R. Buss, Ed. Elsevier Science Publishers, 337--405.
• 3: Beckmann, A. and Weiermann, A. 2000. Characterizing the elementary recursive functions by a fragment of Gödel's T. Archive Math. Logic 39, 475--491.
• 4: Cristian Calude, Theories of computational complexity, Elsevier Science Inc., New York, NY, 1988
• 5: Loïc Colson, About primitive recursive algorithms, Theoretical Computer Science, v.83 n.1, p.57-69, June 21, 1991
• 6: Loïc Colson , Daniel Fredholm, System T, call-by-value and the minimum problem, Theoretical Computer Science, v.206 n.1-2, p.301-315, Oct. 6, 1998 [doi>10.1016/S0304-3975(98)00011-5]
• 7: Tristan Crolard , Samuel Lacas , Pierre Valarcher, On the expressive power of the loop language, Nordic Journal of Computing, v.13 n.1, p.46-57, June 2006
• 8: Martin D. Davis , Ron Sigal , Elaine J. Weyuker, Computability, complexity, and languages (2nd ed.): fundamentals of theoretical computer science, Academic Press Professional, Inc., San Diego, CA, 1994
• 9: DOD. 1980. The Programming Language Ada. Reference Manual. Springer.
• 10: Donahue, J. E. 1977. Locations considered unnecessary. Acta Inf. 8, 221--242.
• 11: Mattias Felleisen , D. P. Friedman, A calculus for assignments in higher-order languages, Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.314, January 21-23, 1987, Munich, West Germany [doi>10.1145/41625.41654]
• 12: Andrzej Filinski, Representing monads, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.446-457, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.178047]
• 13: Jean-Christophe Filliâtre, Verification of non-functional programs using interpretations in type theory, Journal of Functional Programming, v.13 n.4, p.709-745, July 2003 [doi>10.1017/S095679680200446X]
• 14: Filliâtre, J.-C. and Marché, C. 2004. Multi-prover verification of C programs. In Proceedings of the Formal Methods and Software Engineering, 6th International Conference on Formal Engineering Methods, (ICFEM'04). Lecture Notes in Computer Science, vol. 3308. Springer-Verlag, 15--29.
• 15: Wolfgang Gellerich , Erhard Plödereder, Parameter-Induced Aliasing in Ada, Proceedings of the 6th Ade-Europe International Conference Leuven on Reliable Software Technologies, p.88-99, May 14-18, 2001
• 16: David K. Gifford , John M. Lucassen, Integrating functional and imperative programming, Proceedings of the 1986 ACM conference on LISP and functional programming, p.28-38, August 1986, Cambridge, Massachusetts, United States [doi>10.1145/319838.319848]
• 17: Jean-Yves Girard , Paul Taylor , Yves Lafont, Proofs and types, Cambridge University Press, New York, NY, 1989
• 18: Gödel, K. 1958. Über eine bisher noch nicht benützteerweiterung des finiten standpunktes. Dialectica 12, 280--287.
• 19: Gödel, K. 1990. Collected Works vol. 2. Oxford University Press, Oxford, UK.
• 20: John Hatcliff , Olivier Danvy, Thunks and the λ-calculus, Journal of Functional Programming, v.7 n.3, p.303-319, May 1997 [doi>10.1017/S0956796897002748]
• 21: Anders Hejlsberg , Scott Wiltamuth , Peter Golde, C# Language Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2003
• 22: Neil D. Jones, Computability and complexity: from a programming perspective, MIT Press, Cambridge, MA, 1997
• 23: Gilles Kahn, Natural Semantics, Proceedings of the 4th Annual Symposium on Theoretical Aspects of Computer Science, p.22-39, February 19-21, 1987
• 24: H. Abelson , R. K. Dybvig , C. T. Haynes , G. J. Rozas , N. I. Adams Iv , D. P. Friedman , E. Kohlbecker , G. L. Steele, Jr. , D. H. Bartley , R. Halstead , D. Oxley , G. J. Sussman , G. Brooks , C. Hanson , K. M. Pitman , M. Wand, Revised Report on the Algorithmic Language Scheme, Higher-Order and Symbolic Computation, v.11 n.1, p.7-105, August 1998 [doi>10.1023/A:1010051815785]
• 25: Kreisel, G. 1951. On the interpretation of non-finitist proofs—part I. J. Symb. Log 16, 4, 241--267.
• 26: Landin, P. J. 1964. The mechanical evaluation of expressions. Comput. J. 6, 308--320.
• 27: John McCarthy, Recursive functions of symbolic expressions and their computation by machine, Part I, Communications of the ACM, v.3 n.4, p.184-195, April 1960 [doi>10.1145/367177.367199]
• 28: Meyer, A. R. and Ritchie, D. M. 1976. The complexity of loop programs. In Proceedings of the ACM Natural Meeting.
• 29: Robin Milner , Mads Tofte , David Macqueen, The Definition of Standard ML, MIT Press, Cambridge, MA, 1997
• 30: Eugenio Moggi, Notions of computation and monads, Information and Computation, v.93 n.1, p.55-92, July 1991 [doi>10.1016/0890-5401(91)90052-4]
• 31: Peter O'Hearn , Robert D. Tennent, ALGOL-like languages (v.2), Birkhauser Boston Inc., Cambridge, MA, 1996
• 32: Peter, R. 1968. Recursive Functions. Academic Press.
• 33: Plotkin, G. 1981. A structural approach to operational semantics. Tech. rep. DAIMI FN-19, Aarhus University.
• 34: John C. Reynolds, Syntactic control of interference, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.39-46, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512766]
• 35: Reynolds, J. C. 1981. The essence of Algol. In Algorithmic Languages, de Bakker and van Vliet, Eds. IFIP, North-Holland, Amsterdam, 345--372.
• 36: John C. Reynolds, Theories of programming languages, Cambridge University Press, New York, NY, 1999
• 37: David A. Schmidt, The structure of typed programming languages, MIT Press, Cambridge, MA, 1994
• 38: Schütte, K. 1967. Proof Theory. Addison Wesley.
• 39: Joseph E. Stoy, Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory, MIT Press, Cambridge, MA, 1977
• 40: Jean-Pierre Talpin , Pierre Jouvelot, The type and effect discipline, Information and Computation, v.111 n.2, p.245-296, June 1994 [doi>10.1006/inco.1994.1046]
• 41: Turner, D. A. 2004. Total functional programming. J. Unin. Comput. Sci. 10, 7, 751--768.
• 42: Philip Wadler, Comprehending monads, Proceedings of the 1990 ACM conference on LISP and functional programming, p.61-78, June 27-29, 1990, Nice, France [doi>10.1145/91556.91592]
• 43: Philip Wadler, The marriage of effects and monads, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.63-74, September 26-29, 1998, Baltimore, Maryland, United States

INDEX TERMS

General Terms:
Theory, Verification

Keywords:
Gödel System T, Loop language, higher-order procedures, procedural variables