Linearity, Non-determinism and Solvability

• Autorzy: Pagani M. , Ronchi della Rocca S.
• Języki publikacji: EN

Abstrakty

EN

We study the notion of solvability in the resource calculus, an extension of the γ-calculus modelling resource consumption. Since this calculus is non-deterministic, two different notions of solvability arise, one optimistic (angelical, may) and one pessimistic (demoniac, must). We give a syntactical, operational and logical characterization for the may-solvability and only a partial characterization of the must-solvability. Finally, we discuss the open problem of a complete characterization of the must-solvability.

Słowa kluczowe

EN

gamma calculus; may solvability; must solvability

• Wydawca: Polskie Towarzystwo Matematyczne
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2010
• Tom: Vol. 103, nr 1-4
• Strony: 173--202
• Opis fizyczny: Bibliogr. 27 poz.

Twórcy

autor

Pagani M.

autor

Ronchi della Rocca S.

• Laboratoire d'Informatique de Paris-Nord - Université Paris 13, 99, avenue Jean-Baptiste Clément, 93430 Villetaneuse France,

Bibliografia

• [1] Henk Barendregt. The Lambda-Calculus, its Syntax and Semantics. Stud. Logic Found. Math., vol. 103. North-Holland, 1984.
• [2] Gerard Boudol, Pierre-Louis Curien, and Carolina Lavatelli. A Semantics for Lambda Calculi with Resources. MSCS, 9(5):437-482, 1999.
• [3] Antonio Bucciarelli, Thomas Ehrhard, and Giulio Manzonetto. Not Enough Points Is Enough. In CSL, volume 4646 of Lecture Notes in Comp. Sci., pages 298-312, 2007.
• [4] Antonio Bucciarelli, Thomas Ehrhard, and Giulio Mazonetto. A relational semantics for parallelism and non-determinism in a functional setting. Preprint, 2009.
• [5] Gérard Boudol. The Lambda-Calculus with Multiplicities. INRIA Report 2025, 1993.
• [6] Mario Coppo, Mariangiola Dezani-Ciancaglini, and Betti Venneri. Principal Type Schemes and Lambda-Calculus Semantics. In To H. B. Curry. Essays on Combinatory Logic, Lambda-calculus and Formalism, pages 480-490. Accademic Press, 1980.
• [7] Mario Coppo, Mariangiola Dezani-Ciancaglini, and Betti Venneri. Functional Characters of Solvable Terms. Zeitschrift f¨ur Mathematische Logik, 27:45-58, 1981.
• [8] Daniel de Carvalho. Execution Time of _-Terms via Denotational Semantics and Intersection Types. Preprint, 2009.
• [9] Daniel de Carvalho, Michele Pagani, and Lorenzo Tortora de Falco. A Semantic Measure of the Execution Time in Linear Logic. Th. Comp. Sc., 2008. to appear.
• [10] Ugo de'Liguoro and Adolfo Piperno. Non Deterministic Extensions of Untyped Lambda-Calculus. Inf. Comput., 122(2):149-177, 1995.
• [11] Thomas Ehrhard and Laurent Regnier. The Differential Lambda-Calculus. Theor. Comput. Sci., 309(1):1-41, 2003.
• [12] Thomas Ehrhard and Laurent Regnier. Böhm trees, Krivine's Machine and the Taylor Expansion of Lambda-Terms. In CiE, volume 3988 of LNCS, pages 186-197, 2006.
• [13] Thomas Ehrhard and Laurent Regnier. Uniformity and the Taylor Expansion of Ordinary Lambda-Terms. Theor. Comput. Sci., 403(2-3):347-372, 2008.
• [14] J. Martin E. Hyland. A Syntactic Characterization of the Equality in Some Models of the Lambda Calculus. J. London Math. Soc., 2(12):361-370, 1976.
• [15] Assaf J. Kfoury. A Linearization of the Lambda-Calculus and Consequences. J. Logic Comp., 10(3):411-436, 2000.
• [16] Jean-Louis Krivine. Lambda-calculus, types and models. Ellis Horwood, 1993.
• [17] Peter M. Neergaard and Harry G. Mairson. Types, Potency, and Idempotency: why Nonlinearity and Amnesia Make a Type System Work. In Okasaki and Fisher, editors, 9th ACM SIGPLAN ICFP 2004, pages 138-149. ACM, 2004.
• [18] Luca Paolini and Simona Ronchi Della Rocca. The parametric parameter passing _-calculus. Information and Computation, 189(1):87-106, February 2004.
• [19] Michele Pagani and Simona Ronchi Della Rocca. Solvability in Resource Lambda-Calculus. In Luke Ong, editor, FOSSACS, volume 6014 of Lecture Notes in Comp. Sci., pages 358-373, 2010.
• [20] Michele Pagani and Paolo Tranquilli. Parallel Reduction in Resource Lambda-Calculus. In APLAS, volume 5904 of LNCS, pages 226-242, 2009.
• [21] Simona Ronchi Della Rocca and Luca Paolini. The Parametric λ-Calculus: a Metamodel for Computation. EATCS Series. Springer, Berlin, 2004.
• [22] Dana S. Scott. Data types as lattices. SIAM J. Comput., 5(3):522-587, 1976.
• [23] Paolo Tranquilli. Intuitionistic Differential Nets and Lambda-Calculus. Theor. Comput. Sci., 2008. to appear.
• [24] Paolo Tranquilli. Nets between Determinism and Nondeterminism. Ph.D. thesis, Universit`a Roma Tre/Université Paris Diderot (Paris 7), April 2009.
• [25] Silvio Valentini. An elementary proof of strong normalization for intersection types. Archive for Mathematical Logic, 40(7):475-488, October 2001.
• [26] Lionel Vaux. The algebraic lambda calculus. Math. Struct. Comp. Sci., 19(5):1029-1059, 2009.
• [27] J. B. Wells, Allyn Dimock, Robert Muller, and Franklyn Turbak. A Calculus with Polymorphic and Polyvariant Flow Types. J. Funct. Program., 12(3):183-227, 2002.