変換系と翻訳の理論と応用

转换系统与翻译的理论与应用

基本信息

批准号：
09780244
负责人：
赤間陽二
金额：
$ 1.47万
依托单位：
The University of Tokyo
依托单位国家：
日本
项目类别：
Grant-in-Aid for Encouragement of Young Scientists (A)
财政年份：
1997
资助国家：
日本
起止时间：
1997 至 1998
项目状态：
已结题

项目摘要

BerryとBoudolが導入したCHAMは並行計算を記述するための項の書き換え系で、並行計算を化学反応になぞらえて得られた論点は以下の2点である。1. 計算論的な抽象的な資源の移り変わり。項(“分子")を資源として扱うために項の多重集合(“溶液")もまた項とされ、多重集合のなかの各項に書き換え(“化学反応")が独立に起きる。2. カプセル化された計算。書き換えの及ぶ範囲が定められているため、や、ネットワークの動的な変化が記述できる。Girardの線形論理は、推論過程における論理的な資源の移り変わりを記述できるのだが、線形論理により、CHAMの上記1点目のことが記述できる考える。また、線形論理の証明図の表現の一つであるGirardのproof netは、boxと呼ばれる入れ子構造を持つのだが、対応してCHAMでは複数の計算主体が単一のものとみなされることがある。私は、CHAMの一種でAbramskyが導入したlinear chemical abstract machine(LCHAM)をまず取り扱い、そこにおける計算資源の移り変わりが機械的に推論するできること(主型定理)を証明した。また、関数型プログラミング言語の中間言語の一つである線形λ計算からLCHAMへの翻訳を導入した。線形λ計算の項のその翻訳による結果は、入出力ポートが原始的であるような計算単位となる。また、この翻訳により、線形λ計算における1ステップの計算はLCHAMにおける1ステップの計算に対応することが明らかになった。

Berry和Boudol引入的CHAM是一个用于描述并行计算的重写系统，以及通过将并行计算与化学反应进行比较而获得的以下两个问题。 1。抽象资源的计算。为了将术语（“分子”）视为资源，本节的多组（“解决方案”）也称为术语，并且在每个多组中的每个集合中都独立发生重写（“化学反应”）。 2。封装计算。由于定义了重写的范围，因此可以描述网络的动态变化。 Girard的线性逻辑可以描述推理过程中逻辑资源的变化，但可以用线性逻辑描述CHAM的第一点。此外，吉拉德（Girard）的证明网是线性逻辑认证的表达式之一，具有称为盒子的嵌套结构，但在相应的cham中，可以将多个计算视为单个计算。我首先处理了艾布拉姆斯基（Abramsky）在某种CHAM中引入的线性化学抽象机（LCHAM），并证明可以机械推断计算资源的过渡（主要定理）。另外，从线性λ计算（是功能编程语言的中间语言之一）到LCHAM的翻译。线性λ计算段落中翻译的结果是一个计算单元，其中输入 /输出端口是原始的。此外，该翻译表明，线性λ计算中一个步骤的计算对应于LCHAM中一个步骤的计算。