Web上で動作する型なし・型付きラムダ計算のインタプリタ。 TypeScript (5,000 LOC超) で書かれており、OSSとして公開されている。 早稲田大学情報理工学科において100名超が受講する必修科目である 「プログラミング言語」にて2018年度より継続して使用されている。

実験補助を担当

実験補助を担当

一般のグラフ構造は，代数的データ型（リストや木構造）よりも複雑な構造をもち，それ故に既存のプログラミング言語では安全かつ簡潔な表現が困難である．例えば，C言語のようなポインタを扱える言語であれば，ポインタの接続構造としてグラフを表現することができるが，依然として不正なポインタが発生する危険性がある．そこで，グラフを第一級オブジェクトとしてもち，それを書き換えることによって計算を表現する，グラフ書換え言語というパラダイムが提案されている．中でもLMNtalは，アトム（ノード）やルール（書換え規則）といった最小限の言語要素からなる言語である．LMNtalプログラムはwell-formedであるかぎり，不正なポインタを含まない．この意味で，LMNtalは言語仕様のレベルで不正なポインタを排除しており，ポインタ安全といえる．一方で，LMNtalには静的型の概念がないため，書換えの結果がプログラマの意図しないものとなることがある．グラフ書換え言語では，関数型言語で扱える代数的データ構造よりも広範な構造を扱えるため，計算対象となるグラフの型の定式化は自明でない．そこで我々は，グラフ文法に基づく型定義手法を提案し，ユーザー定義のグラフ型を用いてパターンマッチを記述できる拡張機能を導入することで書換え規則の表現力を向上するとともに，書換え規則の静的型検査手法を確立することを目的としている．2023年度は，まず局所的な接続関係の整合性に着目した型検査手法であるLMNtypeの定式化を行うとともに，既存の拡張言語であるCSLMNtalとの技術交流を行った．また，グラフ文法に基づくグラフ型検査にtoken passingの手法を用いることにより最適化する研究にも参画した．

グラフ書換え言語LMNtalは，複雑な接続構造とその安全な操作を簡潔に表現できる言語である．LMNtalの項は，そのプログラムに対応するグラフの図的表現と併記されることがあるが，グラフ理論ではなく，構文主導の意味論に基づいて定義されている．そのため，LMNtalの項とその図的表現との対応関係，特にLMNtal項上の構造合同関係と，図的表現の間のグラフ同型との対応関係は非自明な課題である．本研究では，まず証明対象となるデータ構造の定義と，証明の大まかな方針を定めた．また，その知見を活かし，データ構造としてハイパーグラフを採用し形式文法に基づいた型定義を行う関数型言語λGTの提案に参画した．