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

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

基本信息

批准号：
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引入的线性化学抽象机（LCHAM）作为一种CHAM，并证明可以机械推断计算资源的变化（主要类型定理）。此外，从线性λ计算中转换为LCHAM，这是功能编程语言的中间语言之一。线性λ计算中术语翻译的结果是一个计算单元，因此输入/输出端口是原始的。该翻译还表明，线性λ计算中的一步计算对应于LCHAM中的一步计算。