本研究の目的は、リダクション並列化を明快に議論するための理論的基盤となりうるラムダ計算体系の確立である。2018年度までに、このようなラムダ計算に必要な構成要素が代数的性質による式の単純化であることを突き止め、ラムダ計算の新たな変種を定義し、その操作的意味を与え、式の単純化が失敗する可能性を排除する型システムを与え、さらにこの体系が望ましい性質を満たすことを証明した。 2019年度は、前年度に与えたラムダ計算体系を元に、様々な具体例への適用可能性を検討した。その結果、この計算体系を用いることで、プログラムが満たす基本的な性質を用いた簡単な式変形によって、並列化を意識しないプログラムを並列プログラムへと変形できることが確認できた。しかも、この方法により、既存のリダクション並列化の文脈で議論されてきた例はもちろん、既存手法ではその扱いが困難であったような、例えば条件分岐を伴うジャンプを含んだループの並列化や、各部分構造毎の集約結果を求める複数の並列アルゴリズムの比較、木構造を複雑に巡回して結果を主役するプログラムの並列化などについても比較的明快に扱うことができることが確認された。以上のことから、この計算体系はリダクション並列化を論じる上での有用な基盤技術であると判断できる。 以上の成果は、プログラミング言語分野のトップ国際会議の一つであるICFP (ACM International Conference on Functional Programming)2019に採択されており、国際的にも高い評価を受けるに至った。
|