A category-like structure of computational paths for parallel reduction (Proof theory and related topics)

Abstract

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 pathoperators. 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 prove that the reduction graph is a plane graph, and unique path and universal common-reduct properties are established. Based on this, 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. Finally, path matrices are defined as block matrices of adjacency matrices to count reduction orbits.