Call-by-value is dual to call-by-name

ABSTRACT

The rules of classical logic may be formulated in pairs corresponding to De Morgan duals: rules about & are dual to rules about V. A line of work, including that of Filinski (1989), Griffin (1990), Parigot (1992), Danos, Joinet, and Schellinx (1995), Selinger (1998,2001), and Curien and Herbelin (2000), has led to the startling conclusion that call-by-value is the de Morgan dual of call-by-name.This paper presents a dual calculus that corresponds to the classical sequent calculus of Gentzen (1935) in the same way that the lambda calculus of Church (1932,1940) corresponds to the intuitionistic natural deduction of Gentzen (1935). The paper includes crisp formulations of call-by-value and call-by-name that are obviously dual; no similar formulations appear in the literature. The paper gives a CPS translation and its inverse, and shows that the translation is both sound and complete, strengthening a result in Curien and Herbelin (2000).

REFERENCES

• 1: Zena Ariola and Hugo Herbelin (2003) Minimal classical logic and control operators. In 30'th International Colloquium on Automata, Languages and Programming, Eindhoven, The Netherlands.
• 2: Franco Barbanera , Stefano Berardi, A symmetric lambda calculus for classical program extraction, Information and Computation, v.125 n.2, p.103-117, March 15, 1996 [doi>10.1006/inco.1996.0025]
• 3: P. Bernays (1936) Review of "Some Properties of Conversion" by Alonzo Church and J. B. Rosser. Journal of Symbolic Logic, 1:74--75.
• 4: George Boole (1847) The mathematical analysis of logic. Macmillan, Barclay, and Macmillan, Cambridge.
• 5: Alonzo Church (1932) A set of postulates for the foundation of logic. Annals of Mathematics, II.33:346--366.
• 6: Alonzo Church (1940) A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56--68.
• 7: Pierre-Louis Curien , Hugo Herbelin, The duality of computation, Proceedings of the fifth ACM SIGPLAN international conference on Functional programming, p.233-243, September 2000
• 8: H. B. Curry and R. Feys (1958) Combinatory Logic. North-Holland (see Chapter 9, Section E).
• 9: Vincent Danos , Jean-Baptiste Joinet , Harold Schellinx, LKQ and LKT, Proceedings of the workshop on Advances in linear logic, p.211-224, June 1995
• 10: N. G. de Bruijn (1968) The mathematical language Automath, its usage, and some of its extensions. In Symposium on Automatic Demonstration, Versailles, 1968, pages 29--61. Springer-Verlag, Lecture Notes in Mathematics 125, 1970.
• 11: M. Felleisen, D. Friedman, E. Kohlbecker, and B. Duba (1986) Reasoning with continuations. In Proceedings of the First Symposium on Logic in Computer Science, pages 131--141, IEEE.
• 12: Andrzej Filinski (1989) Declarative continuations and categorical duality. Master's thesis, University of Copenhagen, Copenhagen, Denmark, August 1989. (DIKU Report 89/11.)
• 13: Gottlob Frege (1879) Begriffsschrift,a formula language, modeled upon that of arithmetic, for pure thought. Halle. Reprinted in Jan van Heijenoort, editor, From Frege to Gödel, A Sourcebook in Mathematical Logic, 1879--1931, Harvard University Press, 1967.
• 14: Jean Gallier. Constructive Logics. Part II: Linear Logic and Proof Nets. Technical Report, CIS Department, University of Pennsylvania.
• 15: Gerhard Gentzen (1935) Investigations into Logical Deduction. Mathematische Zeitschrift 39:176--210,405--431. Reprinted in M. E. Szabo, editor, The Collected Papers of Gerhard Gentzen, North-Holland, 1969.
• 16: Joseph Diaz Gergonne (1826) Annales de mathématique pures et appliquées, 16:209.
• 17: Timothy G. Griffin, A formulae-as-type notion of control, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.47-58, December 1989, San Francisco, California, United States [doi>10.1145/96709.96714]
• 18: Ivor Grattan Guinness (2000) The Search for Mathematical Roots 1870--1940. Princeton University Press.
• 19: Hugo Herbelin, A Lambda-Calculus Structure Isomorphic to Gentzen-Style Sequent Calculus Structure, Selected Papers from the 8th International Workshop on Computer Science Logic, p.61-75, September 25-30, 1994
• 20: Martin Hofmann , Thomas Streicher, Continuation models are universal for lambda-mu-calculus, Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science, p.387, June 29-July 02, 1997
• 21: Eugenio Moggi (1988) Computational lambda-calculus and monads. Technical Report ECS-LFCS-88-66, Edinburgh University, Department of Computer Science.
• 22: P. H. Nidditch (1969) The Development of Mathematical Logic. Thoemmes Press, Bristol (reprinted 1998).
• 23: C. -H. L. Ong, A semantic view of classical proofs: type-theoretic, categorical, and denotational characterizations, Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, p.230, July 27-30, 1996
• 24: C.-H. L. Ong , C. A. Stewart, A Curry-Howard foundation for functional computation with control, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.215-227, January 15-17, 1997, Paris, France [doi>10.1145/263699.263722]
• 25: Michel Parigot, Lambda-My-Calculus: An Algorithmic Interpretation of Classical Natural Deduction, Proceedings of the International Conference on Logic Programming and Automated Reasoning, p.190-201, July 15-20, 1992
• 26: G. D. Plotkin (1975) Call-by-name, call-by-value and the ?-calculus. In Theoretical Computer Science, 1:125--159.
• 27: Jean-Victor Poncelet (1818) Annales de mathématique pures et appliquées, 8:201.
• 28: Dag Prawitz (1965) Natural Deduction: A Proof-Theoretical Study. Almqvist and Wiksell, Stockholm.
• 29: John C. Reynolds, The discoveries of continuations, Lisp and Symbolic Computation, v.6 n.3-4, p.233-248, Nov. 1993 [doi>10.1007/BF01019459]
• 30: Amr Sabry , Matthias Felleisen, Reasoning about programs in continuation-passing style, Lisp and Symbolic Computation, v.6 n.3-4, p.289-360, Nov. 1993 [doi>10.1007/BF01019462]
• 31: Amr Sabry , Philip Wadler, A reflection on call-by-value, ACM Transactions on Programming Languages and Systems (TOPLAS), v.19 n.6, p.916-941, Nov. 1997 [doi>10.1145/267959.269968]
• 32: F. W. K. E. Schröder (1890) Vorlesungen über die Algebra der Logik (Teachings on the Algebra of Logic), Volume 1. Teubner Press, Leibzig.
• 33: Peter Selinger (1998) Control categories and duality: an axiomatic approach to the semantics of functional control. Talk presented at Mathematical Foundations of Programming Semantics, London, May 1998.
• 34: Peter Selinger, Control categories and duality: on the categorical semantics of the lambda-mu calculus, Mathematical Structures in Computer Science, v.11 n.2, p.207-260, April 2001 [doi>10.1017/S096012950000311X]
• 35: Gerald Jay Sussman and Guy Lewis Steele Jr. (1975) Scheme: an interpreter for extended lambda calculus. MIT AI Memo 319, December 1975.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic

General Terms:
Languages, Theory

Keywords:
Curry-Howard correspondence, De Morgan dual, lambda calculus, lambda mu calculus, logic, natural deduction, sequent calculus