Relative normalization in deterministic residual structures. (English) Zbl 1508.68155
Kirchner, Hélène (ed.), Trees in algebra and programming – CAAP ’96. 21st international colloqium, Linköping, Sweden, April 22–24, 1996. Proceedings. Berlin: Springer-Verlag. Lect. Notes Comput. Sci. 1059, 180-195 (1996).
Summary: This paper generalizes the Huet and Lévy theory of normalization by neededness to an abstract setting. We define Stable Deterministic Residual Structures (SDRS) and Deterministic Family Structures (DFS) by axiomatizing some properties of the residual relation and the family relation on redexes in an Abstract Rewriting System. We present two proofs of the Relative Normalization Theorem, one for SDRSs for regular stable sets, and another for DFSs for all stable sets of desirable ‘normal forms’. We further prove the Relative Optimality Theorem for DFSs. We extend this result to deterministic Computation Structures which are deterministic Event Structures with an extra relation expressing self-essentiality.
For the entire collection see [Zbl 1435.68032].
For the entire collection see [Zbl 1435.68032].
MSC:
| 68Q42 | Grammars and rewriting systems |
References:
| [1] | Antoy S., Echahed R., Hanus M. A needed narrowing strategy. In: Proc. of POPL’94, Portland, Oregon, 1994. |
| [2] | Antoy S. and Middeldorp A. A Sequential Reduction Strategy. In Proc. of the \(4^{th}\) International Conference on Algebraic and Logic Programming, ALP’94, Madrid, Springer LNCS. vol. 850, p. 168-185, 1994. · Zbl 0988.68554 |
| [3] | Ariola Z.M., Felleisen M., Maraist J., Odersky M., Wadler P. A Call-By-Need Lambda Calculus. In: Proc. POPL’95, 1995. |
| [4] | Asperti A., Laneve C. Interaction Systems I: The theory of optimal reductions. Mathematical Structures in Computer Science, vol. 11, Cambridge University Press, 1993, p. 1-48. |
| [5] | Barendregt H. P. The Lambda Calculus, its Syntax and Semantics. North-Holland, 1984. · Zbl 0551.03007 |
| [6] | Barendregt H. P., Kennaway J. R., Klop J. W., Sleep M. R. Needed Reduction and spine strategies for the lambda calculus. Information and Computation, v. 75, no. 3, 1987, p. 191-231. · Zbl 0635.03009 |
| [7] | Berry G. Modéles complétement adéquats et stables des \(λ\)-calculs typés. Thèse de l’Université de Paris VII, 1979. |
| [8] | Curry H. B., Feys R. Combinatory Logic. vol. 1, North-Holland, 1958. |
| [9] | Glauert J.R.W., Khasidashvili Z. Relative Normalization in Orthogonal Expression Reduction Systems. In: Proc. of the \(4^{th}\) International workshop on Conditional (and Typed) Term Rewriting Systems, CTRS’94, Springer LNCS, vol. 968, N. Dershowitz, ed. Jerusalem, 1994, p. 144-165. |
| [10] | Gonthier G., Lévy J.-J., Melliès P.-A. An abstract Standardisation theorem. In: Proc. LICS’92, Santa Cruz, California, 1992, p. 72-81. |
| [11] | Huet G., Lévy J.-J. Computations in Orthogonal Rewriting Systems. In: Computational Logic, Essays in Honor of Alan Robinson, J.-L. Lassez and G. Plotkin, eds. MIT Press, 1991. |
| [12] | Kennaway J.R. Sequential evaluation strategy for parallel-or and related reduction systems. Annals of Pure and Applied Logic 43, 1989, p.31-56. · Zbl 0684.68043 |
| [13] | Kennaway J. R., Sleep M. R. Neededness is hypernormalizing in regular combinatory reduction systems. Report. University of East Anglia, 1989. |
| [14] | Kennaway J. R., Klop J. W., Sleep M. R, de Vries F.-J. Event structures and orthogonal term graph rewriting. In: M. R. Sleep, M. J. Plasmeijer, and M. C. J. D. van Eekelen, eds. Term Graph Rewriting: Theory and Practice. John Wiley, 1993. · Zbl 0818.68099 |
| [15] | Kennaway J. R., Klop J. W., Sleep M. R, de Vries F.-J. Transfinite reductions in orthogonal term graph rewriting. Inf. and Comp., To appear. |
| [16] | Khasidashvili Z. \(Β\)-reductions and \(Β\)-developments of \(λ\)-terms with the least number of steps. In: Proc. of the International Conference on Computer Logic COLOG’88, Tallinn 1988, Springer LNCS, v. 417, P. Martin-Löf and G. Mints, eds. 1990, p. 105-111. · Zbl 0716.03004 |
| [17] | Khasidashvili Z. The Church-Rosser theorem in Orthogonal Combinatory Reduction Systems. Report 1825, INRIA Rocquencourt, 1992. |
| [18] | Khasidashvili Z. Optimal normalization in orthogonal term rewriting systems. In: Proc. RTA’93, Springer LNCS, vol. 690, C. Kirchner, ed. Montreal, 1993, p. 243-258. · Zbl 1508.68162 |
| [19] | Klop J. W. Combinatory Reduction Systems. Mathematical Centre Tracts n. 127, CWI, Amsterdam, 1980. |
| [20] | Klop J. W. Term Rewriting Systems. In: S. Abramsky, D. Gabbay, and T. Maibaum eds. Handbook of Logic in Computer Science, vol. II, Oxford University Press, 1992, p. 1-116. |
| [21] | Lévy J.-J. Réductions correctes et optimales dans le lambda-calcul, Thèse de l’Université de Paris VII, 1978. |
| [22] | Lévy J.-J. Optimal reductions in the Lambda-calculus. In: To H. B. Curry: Essays on Combinatory Logic, Lambda-calculus and Formalism, Hindley J. R., Seldin J. P. eds, Academic Press, 1980, p. 159-192. · Zbl 0469.03006 |
| [23] | Maranget L. Optimal derivations in weak \(λ\)-calculi and in orthogonal Term Rewriting Systems. In: Proc. POPL’91, p. 255-269. |
| [24] | Maranget L. La stratégie paresseuse. Thèse de l’Université de Paris VII, 1992. |
| [25] | Nipkow T. Orthogonal higher-order rewrite systems are confluent. In: Proc. of the \(1^{st}\) International Conference on Typed Lambda Calculus and Applications, TLCA’93, Springer LNCS, vol. 664, Bazem M., Groote J.F., eds. Utrecht, 1993, p. 306-317. · Zbl 0789.68081 |
| [26] | Nöcker E. Efficient Functional Programming. Compilation and Programming Techniques. Ph.D. Thesis, Catholic University of Nijmegen, 1994. |
| [27] | Van Oostrom V. Confluence for Abstract and Higher-Order Rewriting. Ph.D. Thesis, Free University of Amsterdam, 1994. |
| [28] | Van Oostrom V., van Raamsdonk F. Weak orthogonality implies confluence: the higher-order case. In: Proc. of the \(3^{rd}\) International Conference on Logical Foundations of Computer Science, LFCS’94, Springer LNCS, vol. 813, Narode A., Matiyasevich Yu. V. eds. St. Petersburg, 1994. p. 379-392. · Zbl 0964.68523 |
| [29] | Sekar R.C., Ramakrishnan I.V. Programming in Equational Logic: Beyond Strong Sequentiality. Proc. of the \(5^{th}\) IEEE Symposium on Logic in Computer Science, LICS’95, Philadelphia, 1990. p. 230-242. |
| [30] | Stark E. W. Concurrent transition systems. Theoretical Computer Science, vol. 64, 1989, p. 221-270. · Zbl 0671.68027 |
| [31] | Winskel G. Events in Computation. Ph.D. Thesis, Univ. Edinburgh, 1980. |
| [32] | Yoshida N. Optimal reduction in weak \(λ\)-calculus with shared environments. In Proc. of ACM Conference on Functional Programming Languages and Computer Architecture, FPCA’93, Copenhagen, 1993, p. 243-252. |
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.
