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.  
  2. Y. Andou, Church-Rosser property of a simple reduction for full first order classical natural deduction (submitted).  
  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.  
  5. H.P. Barendregt, The Lambda Calculus, Its Syntax and Semantics, Revised edition. North-Holland (1984).  
  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.  
  8. G. Barthe and M.H. Sørensen, Domain-Free Pure Type Systems, the revised version of [].  
  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).  
  13. R. Davies and F. Pfenning, A Modal Analysis of Staged Computation, Technical Report CMU-CS-99-153 (1999).  
  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.  
  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.  
  18. K. Fujita, Polymorphic Call-by-Value Calculus based on Classical Proofs. Springer, Lecture Notes in Artificial Intelligence 1476 (1998) 170-182.  
  19. K. Fujita, Explicitly Typed λµ-Calculus for Polymorphism and Call-by-Value. Springer, Lecture Notes in Comput. Sci. 1581 (1999) 162-176.  
  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.  
  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.  
  24. Ph. de Groote, A Simple Calculus of Exception Handling. Springer, Lecture Notes in Comput. Sci. 902 (1995) 201-215.  
  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.  
  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.  
  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).  
  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.  
  35. S. Kobayashi, Monads as modality. Theoret. Comput. Sci.175 (1997) 29-74.  
  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.  
  38. A. Meyer and M. Wand, Continuation Semantics in Typed Lambda-Calculi. Springer, Lecture Notes in Comput. Sci. 193 (1985) 219-224.  
  39. J.C. Mitchell, Polymorphic Type Inference and Containment. Inform. and Comput.76 (1988) 211-249.  
  40. R. Milner, A Theory of Type Polymorphism in Programming. J. Comput. System Sci.17 (1978) 348-375.  
  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.  
  42. E. Moggi, Notions of computation and monads. Inform. and Comput.93 (1991) 55-92.  
  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.  
  47. M. Parigot, Classical Proofs as Programs. Springer, Lecture Notes in Comput. Sci. 713 (1993) 263-276.  
  48. M. Parigot, Proofs of Strong Normalization for Second Order Classical Natural Deduction. J. Symbolic Logic62 (1997) 1461-1479.  
  49. G. Plotkin, Call-by-Name, Call-by-Value and the λ-Calculus. Theoret. Comput. Sci.1 (1975) 125-159.  
  50. D. Prawitz, Natural Deduction: A Proof-Theoretical Study. Almqvist & Wiksell (1965).  
  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.  
  52. N.J. Rehof and M.H. Sørensen, The λΔ-Calculus. Springer, Lecture Notes in Comput. Sci. 789 (1994) 516-542.  
  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).  
  56. M. Takahashi, Parallel Reductions in λ-Calculus. J. Symbolic Comput.7 (1989) 113-123.  
  57. J. Tiuryn, Type Inference Problems: A Survey. Springer, Lecture Notes in Comput. Sci. 452 (1990) 105-120.  
  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.