A formal system of reduction paths for parallel reduction.

*(English)*Zbl 1433.68190Summary: We introduce a formal system of reduction paths as a category-like structure induced from a digraph. Our motivation behind this work comes from a quantitative analysis of reduction systems based on the perspective of computational cost and computational orbit. From the perspective, we define a formal system of reduction paths for parallel reduction, wherein reduction paths are generated from a quiver by means of three path-operators. Next, we introduce an equational theory and reduction rules for the reduction paths, and show that the rules on paths are terminating and confluent so that normal paths are obtained. Following the notion of normal paths, a graphical representation of reduction paths is provided. Then we show that the reduction graph is a plane graph, and unique path and universal common-reduct properties are established. Finally, a set of transformation rules from a conversion sequence to a reduction path leading to the universal common-reduct is given under a certain strategy.

##### MSC:

68Q42 | Grammars and rewriting systems |

03B40 | Combinatory logic and lambda calculus |

68R10 | Graph theory (including graph drawing) in computer science |

##### Keywords:

Church-Rosser theorem; \( \lambda \)-calculus; parallel reduction; plane graph; quiver; Takahashi translation
Full Text:
DOI

##### References:

[1] | Assem, I.; Simson, D.; Skowroński, A., Elements of the Representation Theory of Associative Algebras, London Mathematical Society Student Texts, vol. 65 (2006), Cambridge University Press: Cambridge University Press Cambridge · Zbl 1092.16001 |

[2] | Baader, F.; Nipkow, T., Term Rewriting and All That (1998), Cambridge University Press |

[3] | Barendregt, H. P., The Lambda Calculus. Its Syntax and Semantics (1984), North-Holland · Zbl 0551.03007 |

[4] | Beckmann, A., Exact bound for lengths of reductions in typed λ-calculus, J. Symb. Log., 66, 1277-1285 (2001) · Zbl 1159.03305 |

[5] | Church, A.; Rosser, J. B., Some properties of conversion, Trans. Am. Math. Soc., 39, 3, 472-482 (1936) · JFM 62.0037.03 |

[6] | Dybjer, P.; Moeneclaey, Hugo, Finitary higher inductive types in the groupoid model, (Mathematical Foundations of Program Semantics, Ljubljana (June 2017)) |

[7] | Dehornoy, P.; van Oostrom, V., Z, proving confluence by monotonic single-step upper bound functions, (Logical Models of Reasoning and Computation, Moscow, Russia (May 2008)), 5-8 |

[8] | Fujita, K., On upper bounds on the Church-Rosser theorem, (Third International Workshop on Rewriting Techniques for Program Transformation and Evaluation. Third International Workshop on Rewriting Techniques for Program Transformation and Evaluation, Porto, Portugal, 23rd June 2016. Third International Workshop on Rewriting Techniques for Program Transformation and Evaluation. Third International Workshop on Rewriting Techniques for Program Transformation and Evaluation, Porto, Portugal, 23rd June 2016, Electron. Proc. Theor. Comput. Sci., vol. 235 (2017)), 16-31 |

[9] | Fujita, K., The Church-Rosser theorem and analysis of reduction length, Kyoto University RIMS Kôkyûroku, 2083, 124-136 (2018) |

[10] | Fujita, K., The Church-Rosser theorem and quantitative analysis of witnesses, Inf. Comput., 263, 52-56 (2018) · Zbl 1436.03104 |

[11] | Fujita, K., A category-like structure of computational paths for parallel reduction, Kyoto University RIMS Kôkyûroku (2020), 23 pages in press: |

[12] | Grzegorczyk, A., Some classes of recursive functions, Rozpraw. Mat., IV, 1-48 (1953) |

[13] | Hindley, J. R.; Seldin, J. P., Lambda-Calculus and Combinators, an Introduction (2008), Cambridge University Press: Cambridge University Press Cambridge · Zbl 1149.03016 |

[14] | Ketema, J.; Simonsen, J. G., Least upper bounds on the size of confluence and Church-Rosser diagrams in term rewriting and λ-calculus, ACM Trans. Comput. Log., 14, 4, 31:1-31:28 (2013) · Zbl 1354.68143 |

[15] | Kobayashi, Y., Complete rewriting systems and homology of monoid algebras, J. Pure Appl. Algebra, 65, 263-275 (1990) · Zbl 0711.20035 |

[16] | Komori, Y.; Matsuda, N.; Yamakawa, F., A simplified proof of the Church-Rosser theorem, Stud. Log., 102, 175-183 (2014) · Zbl 1338.03017 |

[17] | Lafont, Y., A new finiteness condition for monoids presented by complete rewriting systems (after Craig C. Squier), J. Pure Appl. Algebra, 98, 229-244 (1995) · Zbl 0832.20080 |

[18] | Nakazawa, K.; Fujita, K., Compositional Z: confluence proofs for permutative conversion, Stud. Log., 104, 1205-1224 (2016) · Zbl 1368.03020 |

[19] | Schwichtenberg, H., Complexity of normalization in the pure lambda-calculus, (Troelstra, A. S.; van Dalen, D., The L.E.J. Brouwer Centenary Symposium (1982)), 453-457 |

[20] | Sørensen, M. H.; Urzyczyn, P., Lectures on the Curry-Howard Isomorphism (2006), Elsevier · Zbl 1183.03004 |

[21] | Statman, R., The typed λ-calculus is not elementary recursive, Theor. Comput. Sci., 9, 73-81 (1979) · Zbl 0411.03050 |

[22] | Takahashi, M., Parallel reductions in λ-calculus, Inf. Comput., 118, 120-127 (1995) · Zbl 0827.68060 |

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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.