Lambda Friends is a web-based interpreter for untyped & simply typed lambda calculus. It's written in TypeScript (>5k Lines of Code), published as Open Source Software, and used for education in a required course on Programming Languages (>100 students) in the Department of Computer Science and Engineering, Waseda University.

As an Assistant of Experiments

As an Assistant of Experiments

本研究は、形式文法に基づいて複雑なグラフ構造を抽象化することにより、グラフ構造を扱う大規模なプログラムに関するプログラマの理解を助け、またプログラムの実行および安全性検証の効率化を図るものである。なお本研究は、学部および修士課程において行った、グラフ書換え言語LMNtalの形式文法に基づいた型検査手法LMNtal ShapeTypeに関する研究に端を発する。2024年度は、JSSST 2023にて発表した局所的な接続関係の整合性に着目した型検査手法であるLMNtypeの着想を基に、定式化を洗練させていった。その成果として、LMNtal上のグラフ文法であるLMNtalGGと、それに基づくグラフ型とその差分からなる差分グラフ型の概念を確立し、査読付き国際会議で発表した[1]。また、10月には同内容を国際ワークショップAPLAS-NIER 2024にて発表した。従来、LMNtal ShapeTypeやLMNtypeといった静的な型定義・検査手法と、書換え規則の発火条件としてユーザが定義したグラフ型による制約を課すことができる拡張言語であるCSLMNtalとは、双方ともにグラフ文法に基づいているため共通する部分が多いにもかかわらず、独立に研究が進められてきた。一方で、今回提案したLMNtalGGではその垣根を取り払い、相互の技術交流・融合を行うことを目指している。実際、論文[1]においてもLMNtalGGの主要な応用として上記の2点を挙げている。加えて、従来のLMNtal ShapeTypeでは、リスト型とその差分である差分リスト型とを独立に定義する必要があり、「差分リストにリストを繋いだものはリストである」といった一見自明な性質を示すのが困難であったが、今回のLMNtalGGに基づく差分グラフ型では、差分リスト型を既存のリスト型に基づいてその差分として定義することで、この問題を回避している。また、上記の成果および従来のLMNtal ShapeTypeに関する成果（2022年IEEE ACCESS論文）をもとに、博士論文を執筆・提出し、博士（工学）の学位を拝領した。

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

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