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

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

• 批准号: 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種類を構成し、それらの距離の関係を明らかにした。

首先，我们将讨论去年“未来研究促进政策”中包含的“MetCpo 类别中追踪算子与受保护定点算子之间关系的调查”。 MetCpo 类别是一个数学对象，它既具有捕获编程中重复处理的数学结构，又具有称为“距离”的度量，用于测量程序对输入的依赖程度。在这个类别中，存在一种与重复处理相对应的数学结构，称为跟踪算子，该数学结构是从用于捕获重复处理的数学结构获得的。直观上，trace算子对应的是重复处理，但从技术上来说，trace算子无法直接捕获for循环等重复处理。我关心的一点是，我在去年的《未来研究促进政策》中提到，“（1）这个“受保护的定点算子”是缩放函子的 co-Creisli 类别上的算子检查它是否是带有守卫的定点运算符。换句话说，在 MetCpo 类别之上，有一个运算符可以扩大或缩小“距离”尺度，衡量程序对输入的依赖程度，通过这个运算符，MetCpo 类别的问题是是否存在一个数学结构（a捕获重复处理的受保护定点运算符）可以从跟踪运算符获得。研究的结果是，当“距离”的尺度由一个称为康威半年的数学结构给出时，这种捕获重复处理的数学结构（应该称为以康威半年为索引的保护定点算子的结构） ) ) 被发现获得。接下来，我们将讨论对 MetCpo 类别的跟踪算子的调查。我研究了通过称为 Int 构造的技术获得的线性 lambda 演算（一种编程语言）中的程序之间的距离。具体来说，我们在线性 lambda 计算中构造了其他三种类型的距离，并阐明了这些距离之间的关系。

项目成果

On the Lattice of Program Metrics

关于计划指标的格子

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

On the Lattice of Program Metrics

关于计划指标的格子

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