ガード付き型システムの圏論的解明

保护类型系统的范畴论阐释

• 批准号: 21K11762
• 负责人: 星野 直彦
• 金额: $ 1.66万
• 依托单位: Sojo University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (C)
• 财政年份: 2021
• 资助国家: 日本
• 起止时间: 2021-04-01 至 2024-03-31
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-21K11762/
• 关键词: ガード付き不動点演算子; トレース演算子; プログラミング言語; 意味論; 圏論

まず、昨年度の「今後の研究の推進方針」の「圏MetCpo上のトレース演算子およびガード付き不動点演算子の関係の調査」について述べる。圏MetCpoはプログラミングでの繰り返し処理を捉える数学的構造とプログラムが入力に対しどの程度の依存度を持っているかを測る「距離」と呼ばれる尺度を兼ね備えた数学的対象である。この圏上には繰り返し処理を捉えるための数学的構造から得られるトレース演算子という繰り返し処理に相当する数学的構造が入る。トレース演算子は直感的には繰り返し処理に相当しているが、技術的にはトレース演算子では直接forループのような繰り返し処理を捉えられない。そこで気になる点が昨年度の「今後の研究の推進方針」の中で述べた「(1)この『ガード付きの不動点演算子』は圏MetCpoのスケーリング関手に対する余クライスリ圏上の演算子としてガード付きの不動点演算子になっていないかを調べる。」である。つまり、圏MetCpoの上には、プログラムが入力に対しどの程度の依存度を持っているのかを測る「距離」の目盛りを拡大・縮小する演算子があり、この演算子を経由して圏MetCpoのトレース演算子から繰り返し処理を捉える数学的構造（ガード付きの不動点演算子）が得られないかということである。研究結果として「距離」の目盛りがコンウェイ半環と呼ばれる数学的構造で与えられている場合には繰り返し処理を捉える数学的構造（コンウェイ半環を指標に持つガード付き不動点演算子と呼ぶべき構造）が得られることがわかった。次に、圏MetCpo上のトレース演算子の調査について述べる。Int構成と呼ばれる手法を経由して得られる線形ラムダ計算（ある種のプログラミング言語）のプログラムの間の距離の研究を行った。具体的には線形ラムダ計算上の距離として他に3種類を構成し、それらの距離の関係を明らかにした。

This article is part of the "Investigation of the Relationship between the Fixed Point Calculator and the Fixed Point Calculator on the MetCpo" section of "Future Research Promotion Policy" published last year. MetCpo is a mathematical construct, a mathematical construct, a mathematical The mathematical structure of the algorithm is equivalent to the mathematical structure of the algorithm. The algorithm is directly related to the processing of the data. The following points are mentioned in the "Policy for Promoting Future Research" of last year: "(1) The fixed-point algorithm of the system MetCpo has been adjusted to the fixed-point algorithm of the system."である。MetCpo's top, bottom, top, bottom, bottom The results of this study show that the mathematical structure of the distance semirings and the mathematical structure of the fixed point operators in the case of the inverse processing are obtained. Next, the investigation of the algorithm on MetCpo will be carried out. Int formation and communication techniques are studied by calculating the distance between the two groups. The distance between the three kinds of concrete line shapes is calculated, and the distance between them is clearly defined.

项目成果

On the Lattice of Program Metrics

关于计划指标的格子

• 发表时间: 2023
• 作者: Ugo Dal Lago;Naohiko Hoshino;Paolo Pistone
• 通讯作者: Paolo Pistone