The conflict-free reduction geometry. (English) Zbl 1081.68039
Summary: We investigate mutual dependencies of subexpressions of computable expressions in orthogonal rewrite systems, and identify conditions for their independent concurrent computation. To this end, we introduce concepts familiar from ordinary Euclidean geometry (such as basis, projection, distance, etc.) for reduction spaces. We show how a basis at an expression can be constructed so that any reduction starting from that expression can be decomposed as the sum of its projections on the axes of the basis. To make the concepts computationally more relevant, we relativize them w.r.t. stable sets of results (such as the set of normal forms, head-normal forms, and weak-head-normal forms, in the \(\lambda\)-calculus), and show that an optimal concurrent computation of an expression w.r.t. \(S\) consists of optimal computations of its \(S\)-independent subexpressions. All these results are obtained in the framework of geterministic family structures, which are abstract reduction systems with axiomatized residual and family relations on redexes, that model all orthogonal rewrite systems.
MSC:
| 68Q42 | Grammars and rewriting systems |
Keywords:
Conflict-free rewrite systems; Concurrent computation; Euclidean geometry; Event structures; Relativized and optimal abstract rewritingReferences:
| [1] | Asperti, A.; Laneve, C., Interaction systems I: the theory of optimal reductions, Math. Struct. Comput. Sci., 11, 1-48 (1993) |
| [2] | Barendregt, H. P., The Lambda Calculus, its Syntax and Semantics (1984), North-Holland: North-Holland Amsterdam · Zbl 0551.03007 |
| [3] | Courcelle, B., Recursive applicative program schemes, (van Leeuwen, J., Handbook of Theoretical Computer Science, Vol. B (1990), Elsevier: Elsevier Amsterdam), 459-492 · Zbl 0900.68095 |
| [4] | J.R.W. Glauert, J.R. Kennaway, Z. Khasidashvili, Stable results and relative normalization, J. Logic Comput. 10(3) (special issue), in: F. Kamareddine, J.W. Klop (Eds.), Type Theory and Term Rewriting, Oxford University Press, Oxford, 2000, pp. 323-348.; J.R.W. Glauert, J.R. Kennaway, Z. Khasidashvili, Stable results and relative normalization, J. Logic Comput. 10(3) (special issue), in: F. Kamareddine, J.W. Klop (Eds.), Type Theory and Term Rewriting, Oxford University Press, Oxford, 2000, pp. 323-348. · Zbl 0966.68090 |
| [5] | J.R.W. Glauert, Z. Khasidashvili, Relative normalization in orthogonal expression reduction systems, in: Proc. CTRS’94, Lecture Notes in Computer Science, Vol. 968, Springer, Berlin, 1994, pp. 144-165.; J.R.W. Glauert, Z. Khasidashvili, Relative normalization in orthogonal expression reduction systems, in: Proc. CTRS’94, Lecture Notes in Computer Science, Vol. 968, Springer, Berlin, 1994, pp. 144-165. |
| [6] | J.R.W. Glauert, Z. Khasidashvili, Relative normalization in deterministic residual structures, in: Proc. CAAP’96, Lecture Notes in Computer Science, Vol. 1059, Springer, Berlin, 1996, pp. 180-195.; J.R.W. Glauert, Z. Khasidashvili, Relative normalization in deterministic residual structures, in: Proc. CAAP’96, Lecture Notes in Computer Science, Vol. 1059, Springer, Berlin, 1996, pp. 180-195. · Zbl 1355.68139 |
| [7] | J.R.W. Glauert, Z. Khasidashvili, An abstract Böhm-normalization, in: Proc. of Second Internat. Workshop on Reduction Strategies in Rewriting and Programming, WRS’02, Electronic Notes in Computer Science, Elsevier Science BV, Amsterdam, 2002.; J.R.W. Glauert, Z. Khasidashvili, An abstract Böhm-normalization, in: Proc. of Second Internat. Workshop on Reduction Strategies in Rewriting and Programming, WRS’02, Electronic Notes in Computer Science, Elsevier Science BV, Amsterdam, 2002. · Zbl 1270.68066 |
| [8] | G. Gonthier, J.-J. Lévy, P.-A. Melliès, An abstract standardisation theorem, in: Proc. 7th IEEE Symp. on Logic in Computer Science, 1992, pp. 72-81.; G. Gonthier, J.-J. Lévy, P.-A. Melliès, An abstract standardisation theorem, in: Proc. 7th IEEE Symp. on Logic in Computer Science, 1992, pp. 72-81. |
| [9] | Huet, G.; Lévy, J.-J., Computations in orthogonal rewriting systems, (Lassez, J.-L.; Plotkin, G., Computational Logic Essays in Honor of Alan Robinson (1991), MIT Press: MIT Press Cambridge), 394-443 · Zbl 0793.03002 |
| [10] | V. Kathail, Optimal interpreters for lambda-calculus based functional languages, Ph.D. Thesis, MIT, 1990.; V. Kathail, Optimal interpreters for lambda-calculus based functional languages, Ph.D. Thesis, MIT, 1990. |
| [11] | J.R. Kennaway, Z. Khasidashvili, A. Piperno, Static analysis of modularity in the hyperbalanced \(\operatorname{\Lambda;} \); J.R. Kennaway, Z. Khasidashvili, A. Piperno, Static analysis of modularity in the hyperbalanced \(\operatorname{\Lambda;} \) · Zbl 1045.03018 |
| [12] | Kennaway, J. R.; Klop, J. W.; Sleep, M. R.; de Vries, F.-J., On the adequacy of graph rewriting for simulating term rewriting, ACM Transactions on Programming Languages and Systems, 16, 3, 493-523 (1994) |
| [13] | J.R. Kennaway, M.R. Sleep, Neededness is hypernormalizing in regular combinatory reduction systems, School of Information Systems, UEA Norwich, 1989, preprint.; J.R. Kennaway, M.R. Sleep, Neededness is hypernormalizing in regular combinatory reduction systems, School of Information Systems, UEA Norwich, 1989, preprint. |
| [14] | Z. Khasidashvili, \( \operatorname{Β;}\operatorname{Β;}\operatorname{\Lambda;} \); Z. Khasidashvili, \( \operatorname{Β;}\operatorname{Β;}\operatorname{\Lambda;} \) |
| [15] | Z. Khasidashvili, Optimal normalization in orthogonal term rewriting systems, in: Proc. RTA’93, Lecture Notes in Computer Science, Vol. 690, Springer, Berlin, 1993, pp. 243-258.; Z. Khasidashvili, Optimal normalization in orthogonal term rewriting systems, in: Proc. RTA’93, Lecture Notes in Computer Science, Vol. 690, Springer, Berlin, 1993, pp. 243-258. · Zbl 1508.68162 |
| [16] | Z. Khasidashvili, On higher order recursive program schemes, in: Proc. CAAP’94, Lecture Notes in Computer Science, Vol. 787, Springer, Berlin, 1994, pp. 172-186.; Z. Khasidashvili, On higher order recursive program schemes, in: Proc. CAAP’94, Lecture Notes in Computer Science, Vol. 787, Springer, Berlin, 1994, pp. 172-186. · Zbl 0938.68643 |
| [17] | Z. Khasidashvili, R.W. Glauert, Discrete normalization and standardization in deterministic residual structures, in: Proc. ALP’96, Lecture Notes in Computer Science, Vol. 1139, Springer, Berlin, 1996, pp. 135-149.; Z. Khasidashvili, R.W. Glauert, Discrete normalization and standardization in deterministic residual structures, in: Proc. ALP’96, Lecture Notes in Computer Science, Vol. 1139, Springer, Berlin, 1996, pp. 135-149. · Zbl 1355.68139 |
| [18] | Z. Khasidashvili, J.R.W. Glauert, The geometry of orthogonal reduction spaces, in: Proc. ICALP’97, Lecture Notes in Computer Science, Vol. 1256, Springer, Berlin, 1997, pp. 649-659.; Z. Khasidashvili, J.R.W. Glauert, The geometry of orthogonal reduction spaces, in: Proc. ICALP’97, Lecture Notes in Computer Science, Vol. 1256, Springer, Berlin, 1997, pp. 649-659. · Zbl 1401.68137 |
| [19] | Z. Khasidashvili, J.R.W. Glauert, Relating conflict-free stable transition and event models (extended abstract), in: Proc. MFCS’97, Lecture Notes in Computer Science, Vol. 1295, Springer, Berlin, 1997, pp. 269-278.; Z. Khasidashvili, J.R.W. Glauert, Relating conflict-free stable transition and event models (extended abstract), in: Proc. MFCS’97, Lecture Notes in Computer Science, Vol. 1295, Springer, Berlin, 1997, pp. 269-278. · Zbl 0942.68061 |
| [20] | Z. Khasidashvili, J.R.W. Glauert, The geometry of conflict-free reduction spaces, Technical Report SYS-C98-04, UEA, Norwich, 1998.; Z. Khasidashvili, J.R.W. Glauert, The geometry of conflict-free reduction spaces, Technical Report SYS-C98-04, UEA, Norwich, 1998. · Zbl 1081.68039 |
| [21] | Z. Khasidashvili, J.R.W. Glauert, Relating conflict-free stable transition and event models via redex families, Theoret. Comput. Sci. 286 (2002) 65-95, in: P. Ružička (Ed.), Special Issue Dedicated to MFCS’97 Conf.; Z. Khasidashvili, J.R.W. Glauert, Relating conflict-free stable transition and event models via redex families, Theoret. Comput. Sci. 286 (2002) 65-95, in: P. Ružička (Ed.), Special Issue Dedicated to MFCS’97 Conf. · Zbl 1016.68052 |
| [22] | Z. Khasidashvili, J.R.W. Glauert, An abstract concept of optimal implementation, in: Proc. Second International Workshop on Reduction Strategies in Rewriting and Programming, WRS’03, Electronic Notes in Computer Science, Vol. 86, No. 4, Elsevier Science BV, Amsterdam, 2003.; Z. Khasidashvili, J.R.W. Glauert, An abstract concept of optimal implementation, in: Proc. Second International Workshop on Reduction Strategies in Rewriting and Programming, WRS’03, Electronic Notes in Computer Science, Vol. 86, No. 4, Elsevier Science BV, Amsterdam, 2003. · Zbl 1270.68129 |
| [23] | Z. Khasidashvili, A. Piperno, Normalization of typable terms by superdevelopments, in: Proc. CSL’98, Lecture Notes in Computer Science, Vol. 1584, Springer, Berlin, 1999, pp. 260-282.; Z. Khasidashvili, A. Piperno, Normalization of typable terms by superdevelopments, in: Proc. CSL’98, Lecture Notes in Computer Science, Vol. 1584, Springer, Berlin, 1999, pp. 260-282. · Zbl 0933.03010 |
| [24] | Z. Khasidashvili, A. Piperno, A syntactical analysis of normalization, J. Logic Comput. 10(3) (special issue), in: F. Kamareddine, J.W. Klop (Eds.), Type Theory and Term Rewriting, Oxford University Press, Oxford, 2000, pp. 381-410.; Z. Khasidashvili, A. Piperno, A syntactical analysis of normalization, J. Logic Comput. 10(3) (special issue), in: F. Kamareddine, J.W. Klop (Eds.), Type Theory and Term Rewriting, Oxford University Press, Oxford, 2000, pp. 381-410. · Zbl 0953.03015 |
| [25] | J.W. Klop, Combinatory Reduction Systems, Vol. 127, Mathematical Centre Tracts, Amsterdam, 1980.; J.W. Klop, Combinatory Reduction Systems, Vol. 127, Mathematical Centre Tracts, Amsterdam, 1980. · Zbl 0466.03006 |
| [26] | J.W. Klop, Term rewriting systems, in: S. Abramsky, D. Gabbay, T. Maibaum (Eds.), Handbook of Logic in Computer Science, Vol. 2, Oxford University Press, Oxford, 1992, pp. 1-116.; J.W. Klop, Term rewriting systems, in: S. Abramsky, D. Gabbay, T. Maibaum (Eds.), Handbook of Logic in Computer Science, Vol. 2, Oxford University Press, Oxford, 1992, pp. 1-116. · Zbl 0806.68003 |
| [27] | J. Lamping, An algorithm for optimal lambda calculus reduction, in: Proc. 17th ACM Symp. on Principles of Programming Languages, 1990, pp. 6-30.; J. Lamping, An algorithm for optimal lambda calculus reduction, in: Proc. 17th ACM Symp. on Principles of Programming Languages, 1990, pp. 6-30. |
| [28] | Lévy, J.-J., An algebraic interpretation of the \(\lambda \beta \kappa \)-calculus and a labelled \(\lambda \)-calculus, Theoret. Comput. Sci., 2, 97-114 (1976) · Zbl 0335.02016 |
| [29] | J.-J. Lévy, Réductions correctes et optimales dans le lambda-calcul, Thèse de l’Université de Paris VII, 1978.; J.-J. Lévy, Réductions correctes et optimales dans le lambda-calcul, Thèse de l’Université de Paris VII, 1978. |
| [30] | Lévy, J.-J., Optimal reductions in the Lambda-calculus, (Hindley, J. R.; Seldin, J. P., To H.B. Curry: Essays on Combinatory Logic, Lambda-calculus and Formalism (1980), Academic Press: Academic Press New York), 159-192 · Zbl 0469.03006 |
| [31] | L. Maranget L. La stratégie paresseuse, Thèse de l’Université de Paris VII, 1992.; L. Maranget L. La stratégie paresseuse, Thèse de l’Université de Paris VII, 1992. |
| [32] | P.-A. Melliès, Description Abstraite des Systèmes de RéÉcriture, Thèse de l’Université Paris VII, 1996.; P.-A. Melliès, Description Abstraite des Systèmes de RéÉcriture, Thèse de l’Université Paris VII, 1996. |
| [33] | Milner, R., Functions as processes, Math. Struct. Comput. Sci., 2, 2, 119-141 (1992) · Zbl 0773.03012 |
| [34] | V. Van Oostrom, Higher order families, in: Proc. RTA’96, Lecture Notes in Computer Science, Vol. 1103, Springer, Berlin, 1996, pp. 392-407.; V. Van Oostrom, Higher order families, in: Proc. RTA’96, Lecture Notes in Computer Science, Vol. 1103, Springer, Berlin, 1996, pp. 392-407. · Zbl 1503.68164 |
| [35] | Rusinowitch, M., On termination of the direct sum of term rewriting systems, Inform. Process. Lett., 26, 65-70 (1987) · Zbl 0654.68030 |
| [36] | Stark, E. W., Concurrent transition systems, Theoret. Comput. Sci., 64, 3, 221-269 (1989) · Zbl 0671.68027 |
| [37] | G. Winskel, An introduction to event structures, in: Proc. Linear Time, Branching Time and Partial Order in Logics and Models of Concurrency, Lecture Notes in Computer Science, Vol. 354, Springer, Berlin, 1989, pp. 364-397.; G. Winskel, An introduction to event structures, in: Proc. Linear Time, Branching Time and Partial Order in Logics and Models of Concurrency, Lecture Notes in Computer Science, Vol. 354, Springer, Berlin, 1989, pp. 364-397. · Zbl 0683.68074 |
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.
