SIGPRO133 Talk
小規模組込みシステム向けFRP言語のための再帰データ型
横山陽彦, 森口草介, 渡部卓雄
情報処理学会第133回プログラミング研究会(SIGPRO133), オンライン, 2021年3月16-17日．
概要
関数リアクティブプログラミング（FRP）は，時間と共に変化する値を表す時変値を宣言的に組み合わせて，GUIなどのリアクティブシステムを簡潔に記述するプログラミングパラダイムである． EmfrpはFRPを小規模な組み込みシステムの記述に使用できるように設計，開発されたドメイン特化言語である． Emfrpによって記述されたプログラムは時変値の更新処理の停止性が保証されていること，実行時のメモリ使用量が静的に決定されていることから，リソースの制限された環境でも安全にリアクティブな動作を続けることができる． しかしながら，これらの性質を維持するためにデータ構造や関数の再帰的な定義，使用が禁止されている． そのため，リストや木構造のような動的なデータ構造を自然な表現で扱うことが難しい． FRPは宣言的な記述を前提としているため，これらの機能制限により保守性に乏しいプログラムや記述の困難なプログラムが存在する． 本発表では，この制限を緩和するためにEmfrpを構造のサイズ情報を伴ったデータ型で拡張したEmfrpBCTを提案する． EmfrpBCTによって表現力が向上することを例題を通して説明した後，その構文，操作的意味論，型システムについて形式的定義を与え健全性を証明した． さらにEmfrpBCTからC言語へのトランスパイラを作成し，変換時間や実行時のオーバーヘッドを測定，評価した．
Recursive Data Types for an FRP language for Small-scale Embedded Systems
Akihiko Yokoyama, Sosuke Moriguchi, Takuo Watanabe
IPSJ 133th SIGPRO Workshop (SIGPRO133), Online, Mar. 16-17, 2021.
Abstract
We introduce a new type system to Emfrp, a functional reactive programming language designed for resource-constrained embedded systems. To ensure such property that the language can statically determine the amount of runtime memory and guarantee the termination of reactive actions, it disallows the use of recursive data types and functions. However, such restrictions often impose unnatural representations of data structures and algorithms used in various applications. The declarative manner of FRP and these restriction force us to write redundant code or not to write certain kinds of programs. In this presentation, we propose EmfrpBCT, extended Emfrp with size annotated recursive data types, to overcome this problem. It is more expressive than Emfrp yet keeps the static property mentioned above. We formalize EmfrpBCT, present the algorithm for statically computing the runtime memory bounds, and prove its soundness. Moreover, we implement a compiler from EmfrpBCT to C, measure translation time, and evaluate runtime overheads.