Minimality in a linear calculus with iteration. (English) Zbl 1279.68045
Giesl, J. (ed.), Proceedings of the 7th international workshop on reduction strategies in rewriting and programming (WRS 2007), Paris, France, June 25, 2007. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 204, 163-179 (2008).
Summary: System \(\mathcal{L}\) is a linear version of Gödel’s \(\mathcal{T}\), where the \(\lambda\)-calculus is replaced with a linear calculus; or alternatively a linear \(\lambda\)-calculus enriched with some constructs including an iterator. There is thus at the same time in this system a lot of freedom in reduction and a lot of information about resources, which makes it an ideal framework to start a fresh attempt at studying reduction strategies in \(\lambda\)-calculi. In particular, we show that call-by-need, the standard strategy of functional languages, can be defined directly and effectively in System \(\mathcal{L}\), and can be shown minimal among weak strategies.
For the entire collection see [Zbl 1276.68016].
For the entire collection see [Zbl 1276.68016].
MSC:
| 68N18 | Functional programming and lambda calculus |
| 03B40 | Combinatory logic and lambda calculus |
| 03F52 | Proof-theoretic aspects of linear logic and other substructural logics |
Keywords:
linearity; iteration; system \(\mathcal{T}\); strategies; efficiency; minimality; optimalityReferences:
| [1] | Alves, S.; Fernández, M.; Florido, M.; Mackie, I., The power of linear functions, (Ésik, Z., Proceedings of the 15th EACSL Conference on Computer Science Logic. Proceedings of the 15th EACSL Conference on Computer Science Logic, (CSL’06). Proceedings of the 15th EACSL Conference on Computer Science Logic. Proceedings of the 15th EACSL Conference on Computer Science Logic, (CSL’06), Lecture Notes in Computer Science, volume 4207 (2006), Springer-Verlag), 119-134 · Zbl 1225.03014 |
| [2] | Alves, S.; Fernández, M.; Florido, M.; Mackie, I., Iterator types, (Proceedings of Foundations of Software Science and Computation Structures. Proceedings of Foundations of Software Science and Computation Structures, (FOSSACS’07). Proceedings of Foundations of Software Science and Computation Structures. Proceedings of Foundations of Software Science and Computation Structures, (FOSSACS’07), LNCS, volume 4423 (2007), Springer-Verlag), 17-31 · Zbl 1195.03020 |
| [3] | Ariola, Z. M.; Felleisen, M., The call-by-need lambda calculus, Journal of Functional Programming, 7, 3, 265-301 (May 1997) · Zbl 0887.68007 |
| [4] | H. Barendregt, J.A. Bergstra, J.W. Klop, and H. Volken. Degrees, reductions and representability in the lambda-calculus. Technical report, University of Utrecht, Department of Mathematics, 1976; H. Barendregt, J.A. Bergstra, J.W. Klop, and H. Volken. Degrees, reductions and representability in the lambda-calculus. Technical report, University of Utrecht, Department of Mathematics, 1976 · Zbl 0399.03013 |
| [5] | Barendregt, H. P., The Lambda Calculus: Its Syntax and Semantics, Studies in Logic and the Foundations of Mathematics, volume 103 (1984), North-Holland Publishing Company · Zbl 0551.03007 |
| [6] | Blanc, T.; Lévy, J.-J.; Maranget, L., Sharing in the weak lambda-calculus, (Processes, Terms and Cycles. Processes, Terms and Cycles, Lecture Notes in Computer Science, volume 3838 (2005), Springer), 70-87 · Zbl 1171.03309 |
| [7] | Bruggink, H. J.S., Residuals in higher-order rewriting, (Nieuwenhuis, R., Proceedings of Rewriting Techniques and Applications. Proceedings of Rewriting Techniques and Applications, (RTA’03). Proceedings of Rewriting Techniques and Applications. Proceedings of Rewriting Techniques and Applications, (RTA’03), Lecture Notes in Computer Science, volume 2706 (June 2003), Springer), 123-137 · Zbl 1038.68071 |
| [8] | Colson, L.; Fredholm, D., System T, call-by-value and the minimum problem, Theor. Comput. Sci., 206, 1-2, 301-315 (1998) · Zbl 0912.68012 |
| [9] | Dal Lago, U.; Martini, S., An invariant cost model for the lambda calculus, (Beckmann, A.; Berger, U.; Löwe, B.; Tucker, J. V., Logical Approaches to Computational Barriers. Logical Approaches to Computational Barriers, Second Conference on Computability in Europe, CiE 2006. Logical Approaches to Computational Barriers. Logical Approaches to Computational Barriers, Second Conference on Computability in Europe, CiE 2006, Lecture Notes in Computer Science, volume 3988 (2006), Springer), 105-114, Proceedings · Zbl 1145.68375 |
| [10] | Engelfriet, J.; Schmidt, E., IO and OI, Journal of Computer and Systems Sciences, 15, 328-353 (1997) · Zbl 0366.68053 |
| [11] | Fernández, M.; Mackie, I.; Sinot, F.-R., Closed reduction: explicit substitutions without alpha conversion, Mathematical Structures in Computer Science, 15, 2, 343-381 (2005) · Zbl 1129.68409 |
| [12] | Field, J., On laziness and optimality in lambda interpreters: Tools for specification and analysis, (Conference Record of the 17th Annual ACM Symposium on Principles of Programming Languages. Conference Record of the 17th Annual ACM Symposium on Principles of Programming Languages, (POPL ’90) (Jan. 1990), ACM Press: ACM Press San Francisco, CA, USA), 1-15 |
| [13] | Fradet, P., Compilation of head and strong reduction, (ESOP. ESOP, Lecture Notes in Computer Science, volume 788 (1994)), 211-224 |
| [14] | Girard, J.-Y.; Lafont, Y.; Taylor, P., Proofs and Types, Cambridge Tracts in Theoretical Computer Science, volume 7 (1989), Cambridge University Press · Zbl 0671.68002 |
| [15] | Glauert, J. R.W.; Kennaway, R.; Khasidashvili, Z., Stable results and relative normalization, Journal of Logic and Computation, 10, 3, 323-348 (2000) · Zbl 0966.68090 |
| [16] | Khasidashvili, Z.; van Oostrom, V., Context-sensitive conditional expression reduction systems, Electronic Notes in Theoretical Computer Science, 2, 167-176 (1995) · Zbl 0910.68098 |
| [17] | Lamping, J., An algorithm for optimal lambda calculus reduction, (Proceedings of the 17th ACM Symposium on Principles of Programming Languages. Proceedings of the 17th ACM Symposium on Principles of Programming Languages, (POPL’90) (Jan. 1990), ACM Press), 16-30 |
| [18] | J. Launchbury. A natural semantics for lazy evaluation. In Conference Record of the Twentieth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages; J. Launchbury. A natural semantics for lazy evaluation. In Conference Record of the Twentieth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages |
| [19] | Lévy, J.-J., Optimal reductions in the lambda-calculus, (Seldin, J. P.; Hindley, J. R., To H. B. Curry: Essays on Combinatory Logic, Lambda-Calculus, and Formalism (1980), Academic Press, Inc.: Academic Press, Inc. New York, NY), 159-191 · Zbl 0469.03006 |
| [20] | Maraist, J.; Odersky, M.; Wadler, P., The call-by-need lambda calculus, Journal of Functional Programming, 8, 3, 275-317 (May 1998) · Zbl 0918.03019 |
| [21] | Maranget, L., Optimal derivations in orthogonal term rerwiting systems and in weak lambda calculi, (Proc. of the 1991 conference on Principles of Programming Languages (1991), ACM Press) |
| [22] | Parigot, M., On the representation of data in lambda-calculus, (CSL ’89: Proceedings of the third workshop on Computer science logic (1989), Springer-Verlag New York, Inc.: Springer-Verlag New York, Inc. New York, NY, USA), 309-321 · Zbl 0925.03149 |
| [23] | Peyton Jones, S. L., The Implementation of Functional Programming Languages (1987), Prentice Hall International · Zbl 0712.68017 |
| [24] | Spawski, Z.; Urzyczyn, P., Type fixpoints: iteration vs. recursion, (ICFP ’99: Proceedings of the fourth ACM SIGPLAN international conference on Functional programming (1999), ACM Press: ACM Press New York, NY, USA), 102-113 · Zbl 1343.03010 |
| [25] | Terese, Term Rewriting Systems, Cambridge Tracts in Theoretical Computer Science, volume 55 (2003), Cambridge University Press · Zbl 1030.68053 |
| [26] | van Oostrom, V., Random descent, (Proceedings of 18th Rewriting Techniques and Applications. Proceedings of 18th Rewriting Techniques and Applications, (RTA’07). Proceedings of 18th Rewriting Techniques and Applications. Proceedings of 18th Rewriting Techniques and Applications, (RTA’07), Lecture Notes in Computer Science, volume 4533 (2007), Springer-Verlag), 314-328 · Zbl 1203.68082 |
| [27] | C.P. Wadsworth. Semantics and Pragmatics of the Lambda-Calculus; C.P. Wadsworth. Semantics and Pragmatics of the Lambda-Calculus |
| [28] | Yoshida, N., Optimal reduction in weak lambda-calculus with shared environments, Journal of Computer Software, 11, 6, 3-18 (Nov. 1994) |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
