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

機関リポジトリ (HANDLE) オープンアクセス

この論文をさがす

説明

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.

収録刊行物

詳細情報 詳細情報について

  • CRID
    1050567175332610560
  • NII書誌ID
    AN00061013
  • ISSN
    18802818
  • HANDLE
    2433/255053
  • 本文言語コード
    en
  • 資料種別
    departmental bulletin paper
  • データソース種別
    • IRDB

問題の指摘

ページトップへ