Domain-Free λµ-Calculus

Ken-Etsu Fujita

RAIRO - Theoretical Informatics and Applications (2010)

  • Volume: 34, Issue: 6, page 433-466
  • ISSN: 0988-3754

Abstract

top
We introduce a domain-free λµ-calculus of call-by-value as a short-hand for the second order Church-style. Our motivation comes from the observation that in Curry-style polymorphic calculi, control operators such as callcc-operators cannot, in general, handle correctly the terms placed on the control operator's left, so that the Curry-style system can fail to prove the subject reduction property. Following the continuation semantics, we also discuss the notion of values in classical system, and propose an extended form of values. It is proved that the CPS-translation is sound with respect to domain-free λ2 (second-order λ-calculus). As a by-product, we obtain the strong normalization property for the second-order λµ-calculus of call-by-value in domain-free style. We also study the problems of type inference, typability, and type checking for the call-by-value system. Finally, we give a brief comparison with standard ML plus callcc, and discuss a natural way to avoid the unsoundness of ML with callcc.

How to cite

top

Fujita, Ken-Etsu. "Domain-Free λµ-Calculus." RAIRO - Theoretical Informatics and Applications 34.6 (2010): 433-466. <http://eudml.org/doc/222038>.

@article{Fujita2010,
abstract = { We introduce a domain-free λµ-calculus of call-by-value as a short-hand for the second order Church-style. Our motivation comes from the observation that in Curry-style polymorphic calculi, control operators such as callcc-operators cannot, in general, handle correctly the terms placed on the control operator's left, so that the Curry-style system can fail to prove the subject reduction property. Following the continuation semantics, we also discuss the notion of values in classical system, and propose an extended form of values. It is proved that the CPS-translation is sound with respect to domain-free λ2 (second-order λ-calculus). As a by-product, we obtain the strong normalization property for the second-order λµ-calculus of call-by-value in domain-free style. We also study the problems of type inference, typability, and type checking for the call-by-value system. Finally, we give a brief comparison with standard ML plus callcc, and discuss a natural way to avoid the unsoundness of ML with callcc. },
author = {Fujita, Ken-Etsu},
journal = {RAIRO - Theoretical Informatics and Applications},
keywords = {λµ-calculus; domain-free style; call-by-value; polymorphism; subject reduction; CPS-translation; strong normalization; Church-Rosser; type inference; type checking.; domain-free -calculus},
language = {eng},
month = {3},
number = {6},
pages = {433-466},
publisher = {EDP Sciences},
title = {Domain-Free λµ-Calculus},
url = {http://eudml.org/doc/222038},
volume = {34},
year = {2010},
}

TY - JOUR
AU - Fujita, Ken-Etsu
TI - Domain-Free λµ-Calculus
JO - RAIRO - Theoretical Informatics and Applications
DA - 2010/3//
PB - EDP Sciences
VL - 34
IS - 6
SP - 433
EP - 466
AB - We introduce a domain-free λµ-calculus of call-by-value as a short-hand for the second order Church-style. Our motivation comes from the observation that in Curry-style polymorphic calculi, control operators such as callcc-operators cannot, in general, handle correctly the terms placed on the control operator's left, so that the Curry-style system can fail to prove the subject reduction property. Following the continuation semantics, we also discuss the notion of values in classical system, and propose an extended form of values. It is proved that the CPS-translation is sound with respect to domain-free λ2 (second-order λ-calculus). As a by-product, we obtain the strong normalization property for the second-order λµ-calculus of call-by-value in domain-free style. We also study the problems of type inference, typability, and type checking for the call-by-value system. Finally, we give a brief comparison with standard ML plus callcc, and discuss a natural way to avoid the unsoundness of ML with callcc.
LA - eng
KW - λµ-calculus; domain-free style; call-by-value; polymorphism; subject reduction; CPS-translation; strong normalization; Church-Rosser; type inference; type checking.; domain-free -calculus
UR - http://eudml.org/doc/222038
ER -

References

top
  1. Y. Andou, A Normalization-Procedure for the First Order Classical Natural Deduction with Full Logical Symbols, Tsukuba J. Math. 19 (1995) 153-162.  Zbl0835.03021
  2. Y. Andou, Church-Rosser property of a simple reduction for full first order classical natural deduction (submitted).  Zbl1016.03006
  3. Y. Andou, Strong normalization of classical natural deduction, Logic Colloquium 2000. Bull. Symbolic Logic (to appear).  
  4. F. Barbanera and S. Berardi, Extracting Constructive Context from Classical Logic via Control-like Reductions. Springer, Lecture Notes in Comput. Sci. 664 (1993) 45-59.  Zbl0788.68016
  5. H.P. Barendregt, The Lambda Calculus, Its Syntax and Semantics, Revised edition. North-Holland (1984).  Zbl0551.03007
  6. H.P. Barendregt, Lambda Calculi with Types. Oxford University Press, Handbook of Logic in Comput. Sci. 2 (1992) 117-309.  
  7. G. Barthe and M.H. Sørensen, Domain-Free Pure Type Systems. Springer, Lecture Notes in Comput. Sci. 1234 (1997) 9-20.  Zbl0887.03010
  8. G. Barthe and M.H. Sørensen, Domain-Free Pure Type Systems, the revised version of [].  Zbl0979.03013
  9. K. Baba, S. Hirokawa and K. Fujita, Parallel Reduction in Type-Free λµ-Calculus, in The 7th Asian Logic Conference (1999).  
  10. K. Baba, S. Hirokawa and K. Fujita, Parallel Reduction in Type-Free λµ-Calculus. Elsevier, Amsterdam, Electron. Notes Theoret. Comput. Sci. 42 (2001) 52-66.  
  11. L. Damas and R. Milner, Principal type-schemes for functional programs, in Proc. the 9th Annual ACM Symposium on Principles of Programming Languages (1982) 207-212.  
  12. R. Davies and F. Pfenning, A Modal Analysis of Staged Computation, in Proc. the 23rd Annual ACM Symposium of Principles of Programming Languages (1996).  Zbl1323.68107
  13. R. Davies and F. Pfenning, A Modal Analysis of Staged Computation, Technical Report CMU-CS-99-153 (1999).  Zbl1323.68107
  14. M. Felleisen, D.P. Friedman, E. Kohlbecker and B. Duba, Reasoning with Continuations, in Proc. the Annual IEEE Symposium on Logic in Computer Science (1986) 131-141.  
  15. P.C. Fischer, Turing Machines with Restricted Memory Access. Inform. and Control9 (1966) 364-379.  Zbl0145.24205
  16. K. Fujita, On embedding of Classical Substractural Logics, RIMS 918. Research Institute for Mathematical Sciences, Kyoto University (1995) 178-195.  
  17. K. Fujita, Calculus of Classical Proofs I. Springer, Lecture Notes in Comput. Sci. 1345 (1997) 321-335.  Zbl0890.03028
  18. K. Fujita, Polymorphic Call-by-Value Calculus based on Classical Proofs. Springer, Lecture Notes in Artificial Intelligence 1476 (1998) 170-182.  Zbl0914.03036
  19. K. Fujita, Explicitly Typed λµ-Calculus for Polymorphism and Call-by-Value. Springer, Lecture Notes in Comput. Sci. 1581 (1999) 162-176.  Zbl0933.03009
  20. K. Fujita, Type Inference for Domain-Free λ2, Technical Report in Computer Science and Systems Engineering CSSE-5. Kyushu Institute of Technology (1999).  
  21. K. Fujita and A. Schubert, Partially Typed Terms between Church-Style and Curry-Style. Springer, Lecture Notes in Comput. Sci. 1872 (2000) 505-520.  Zbl0998.03009
  22. T.G. Griffin, A Formulae-as-Types Notion of Control, in Proc. the 17th Annual ACM Symposium on Principles of Programming Languages (1990) 47-58.  
  23. Ph. de Groote, A CPS-Translation for the λµ-Calculus. Springer, Lecture Notes in Comput. Sci. 787 (1994) 85-99.  Zbl0938.03024
  24. Ph. de Groote, A Simple Calculus of Exception Handling. Springer, Lecture Notes in Comput. Sci. 902 (1995) 201-215.  Zbl1063.68565
  25. R. Harper, B.F. Duba and D. MacQueen, Typing First-Class Continuations in ML. J. Funct. Programming3 (1993) 465-484.  
  26. R. Harper and M. Lillibridge, ML with callcc is unsound. The Types Form, 8 July (1991).  
  27. R. Harper and M. Lillibridge, Explicit polymorphism and CPS conversion, in Proc. the 20th Annual ACM Symposium on Principles of Programming Languages (1993) 206-219.  
  28. R. Harper and M. Lillibridge, Polymorphic type assignment and CPS conversion. LISP and Symbolic Computation6 (1993) 361-380.  Zbl1058.68727
  29. R. Harper and J.C. Mitchell, On The Type Structure of Standard ML. ACM Trans. Programming Languages and Systems15 (1993) 210-252.  
  30. M. Hofmann, Sound and complete axiomatisations of call-by-value control operators. Math. Structures Comput. Sci.5 (1995) 461-482.  Zbl0846.68066
  31. M. Hofmann and T. Streicher, Continuation models are universal for λµ-calculus, in Proc. the 12th Annual IEEE Symposium on Logic in Computer Science (1997) 387-395.  
  32. J.E. Hopcroft and J.D. Ullman, Introduction to Automata Theory, Languages and Computation. Addison-Wesley (1979).  Zbl0426.68001
  33. W. Howard, The Formulae-as-Types Notion of Constructions, To H.B. Curry: Essays on combinatory logic, lambda-calculus, and formalism. Academic Press (1980) 479-490.  
  34. A.J. Kfoury, J. Tiuryn and P. Urzyczyn, An Analysis of ML Typability. J. Assoc. Comput. Mach.41 (1994) 368-398.  Zbl0806.68016
  35. S. Kobayashi, Monads as modality. Theoret. Comput. Sci.175 (1997) 29-74.  Zbl0895.03011
  36. X. Leroy, Polymorphism by name for references and continuations, in Proc. the 20th Annual ACM Symposium of Principles of Programming Languages (1993) 220-231.  
  37. S. Martini and A. Massini, A Computational Interpretation of Modal Proofs, Proof Theory of Modal Logic. Kluwer (1996) 213-241.  Zbl0867.03016
  38. A. Meyer and M. Wand, Continuation Semantics in Typed Lambda-Calculi. Springer, Lecture Notes in Comput. Sci. 193 (1985) 219-224.  Zbl0565.68028
  39. J.C. Mitchell, Polymorphic Type Inference and Containment. Inform. and Comput.76 (1988) 211-249.  Zbl0656.68023
  40. R. Milner, A Theory of Type Polymorphism in Programming. J. Comput. System Sci.17 (1978) 348-375.  Zbl0388.68003
  41. M.L. Minsky, Recursive Unsolvability of Post's Problem of ``TAG'' and Other Topics in Theory of Turing Machines. Ann. of Math.74 (1961) 437-455.  Zbl0105.00802
  42. E. Moggi, Notions of computation and monads. Inform. and Comput.93 (1991) 55-92.  Zbl0723.68073
  43. C.R. Murthy, An Evaluation Semantics for Classical Proofs, in Proc. the 6th Annual IEEE Symposium on Logic in Computer Science (1991) 96-107.  
  44. C.-H.L. Ong, A Semantic View of Classical Proofs: Type-Theoretic, Categorical, and Denotational Characterizations, Linear Logic '96 Tokyo Meeting (1996).  
  45. C.-H.L. Ong and C.A. Stewart, A Curry-Howard Foundation for Functional Computation with Control, in Proc. the 24th Annual ACM Symposium of Principles of Programming Languages (1997).  
  46. M. Parigot, λµ-Calculus: An Algorithmic Interpretation of Classical Natural Deduction. Springer, Lecture Notes in Comput. Sci. 624 (1992) 190-201.  Zbl0925.03092
  47. M. Parigot, Classical Proofs as Programs. Springer, Lecture Notes in Comput. Sci. 713 (1993) 263-276.  Zbl0805.03012
  48. M. Parigot, Proofs of Strong Normalization for Second Order Classical Natural Deduction. J. Symbolic Logic62 (1997) 1461-1479.  Zbl0941.03063
  49. G. Plotkin, Call-by-Name, Call-by-Value and the λ-Calculus. Theoret. Comput. Sci.1 (1975) 125-159.  Zbl0325.68006
  50. D. Prawitz, Natural Deduction: A Proof-Theoretical Study. Almqvist & Wiksell (1965).  Zbl0173.00205
  51. D. Prawitz, Ideas and Results in Proof Theory, in Proc. the 2nd Scandinavian Logic Symposium, edited by N.E. Fenstad. North-Holland (1971) 235-307.  Zbl0226.02031
  52. N.J. Rehof and M.H. Sørensen, The λΔ-Calculus. Springer, Lecture Notes in Comput. Sci. 789 (1994) 516-542.  Zbl0942.03512
  53. A. Schubert, Second-order unification and type inference for Church-style, Tech. Report TR 97-02 (239). Institute of Informatics, Warsaw University (1997).  
  54. A. Schubert, Second-order unification and type inference for Church-style, in Proc. the ACM Symposium on Principles of Programming Languages (1998) 279-288.  
  55. T. Streicher and B. Reus, Continuation semantics: Abstract machines and control operators. J. Funct. Programming (to appear).  Zbl0928.68074
  56. M. Takahashi, Parallel Reductions in λ-Calculus. J. Symbolic Comput.7 (1989) 113-123.  Zbl0661.03008
  57. J. Tiuryn, Type Inference Problems: A Survey. Springer, Lecture Notes in Comput. Sci. 452 (1990) 105-120.  Zbl0745.03013
  58. J.B. Wells, Typability and Type Checking in the Second-Order λ-Calculus Are Equivalent and Undecidable, in Proc. IEEE Symposium on Logic in Computer Science (1994) 176-185.  

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.