定義のデータ化による証明木可視化システム Mikiβ の拡張
大石美緒, 浅井健一
お茶の水女子大学{oishi.mio, asai}@is.ocha.ac.jp
概要
Mikiβ とは GUI 上で証明木の構築や操作を行うシステムのことで、型推論等の証明木を用いた計算を行う際に利用されている。推論規則などの証明木に関する定義を与えると対応したグラフィカルな証明木が構築され、クリック操作によって計算を行うことができる。先行研究における Mikiβ では、ユーザが OCaml プログラミングで証明
木に関する定義を与えていたが、大きく 2 点の問題点が挙げられていた。1 点目が相互再帰をする型システムでは Mikiβ を利用できないという点、2 点目は機械的に導出できる関数もユーザが記述する必要がありプログラミング量が多いという点である。これらの問題点に対し、OCaml の型を用いて記述していた証明木に関する定義を、ユーザがデータとして定義するように変更することで解決した。また、web インターフェース上でグラフィカルな証明木の構築に必要な情報を入力できるように改善を加えたことで、ユーザは OCaml プログラミングをせずに Mikiβ を使ってグラフィカルな証明木を構築できるようになり、利便性が向上した。

1

はじめに

証明木を用いた計算は、プログラミング言語における型推論、論理学などで用いられている。手計算にて証明木を用いた計算を行うと、何度も項を書き写したり書き換えたりしながら進める必要があり、非常に手間がかかる。複雑な体系になればなるほど煩雑さは増し、実質的に手計算で型推論を行うには複雑すぎる型システムなども存在していた。
このような問題を解決するために、Mikiβ [7] を用いた計算が提案されていた。Mikiβ とは、GUI上で証明木の構築や操作を行うシステムのことで、ユーザが証明木に関する定義を OCaml プログ
ラミングで与えると、対応したグラフィカルな証明木が構築され、クリック操作などを用いて計算を行うことができる。GUI 上で証明木を構築するためには、通常ユーザに GUI 関連の知識が必要となるが、Mikiβ では GUI 構築に関する関数は全てライブラリとして提供しているため GUI に関する知識を必要としない。型定義や推論規則などの証明木に関する情報を OCaml プログラミングにて記述すると、対応したグラフィカルな証明木を構築することができる。
先行研究において、大きな問題点が 2 つ挙げられていた。1 点目は相互再帰で定義された型シス
テムでは Mikiβ を用いてグラフィカルな証明木を構築できない点、2 点目は機械的に導出できる関数もユーザが記述する必要があり、プログラミング量が多いという点である。これらの問題点は、
Mikiβ に与える証明木に関する定義を OCaml の型定義とその型上の関数で与えなくてはならない
ことに起因していた。本研究では、Mikiβ の中身の大枠は保ったまま、証明木に関する定義を単なるデータで表現するというとても単純なアイディアでこれらの問題を解決する。
１点目の問題点である相互再帰が扱えない問題は、相互再帰先が単なるデータで指定できるようになったため、定義の順番に関係なく相互再帰させることが可能となった。先行研究においては、内部で使用している Two-level Types [8] が相互再帰に対応していなかったため、その部分に手を入れない限り相互再帰を扱うことはできなかった。２点目の問題点であるプログラミング量が多い
問題は、与える情報が全てデータとなったため、そもそもプログラミングをする必要がなくなった。

1

これまでユーザがプログラムを作ることで実現していた関数群は、データを見ながら動きを模倣する関数群をあらかじめ作っておくことで対応した。
証明木に関する定義が全てデータになったことで、これまでプログラムで与えていた証明木に関する定義を web のフォームから入力することが可能になった。これにより証明木に関する定義の入力から証明木の構築までの全てを web 上で行うことができるようになった。Mikiβ は、実際にお茶の水女子大学の授業で使われるとともに、研究の上でも先進的な型システムの実装などにも使われている。
本稿の構成を以下に示す。2 節で先行研究における Mikiβ の構成や Two-level Types を用いた実装の概要を示し、複雑なユーザのプログラミングや、相互再帰で定義された型システムを導入する上での問題点も具体的に述べる。3 節で本研究における、データによって与える証明木の定義を示
し、相互再帰で定義された型システムの導入とユーザのプログラミング量の変化について述べる。4
節ではフォームを用いた画面上からの入力について述べる。5 節では本研究で新たに追加した、ファイルの保存や tex への出力などといった、諸機能の実装について述べる。6 節で関連研究について述べ、7 節でまとめる。
Mikiβ のデモは、http://pllab.is.ocha.ac.jp/~asai/jpapers/ppl/24/MikiBeta/ にて公開されている．

2

先行研究における Mikiβ の概要

先行研究における Mikiβ はライブラリとユーザファイルから構成されていた。ライブラリではGUI を構成するための関数を提供し、ユーザは GUI に関するプログラミングをせずに証明木を構築することができた。一方、ユーザファイルは推論規則に依存する『構文の定義・推論規則・出力
関数・単一化関数・lexer・parser』などから構成され、ユーザが OCaml プログラミングを行うことで作成する必要があった。ユーザファイルを作成しコンパイルをすると、ユーザファイルに記述した証明木の体系に特化したグラフィカルな証明木が構築される。
GUI に関するプログラムを意識せず、ユーザファイルでは証明木に関する定義のみを記述すればよい。これは、GUI に関する部分と型システムについての部分を独立した形で定義しているからである。GUI に関する関数と推論を行う型システムについての部分を独立させずに混在して定義してしまうと、型システムが変わるたびに GUI に関する部分も書き直す必要が生じてしまう。それを避けるため、次節で述べる Two-level Types [8] を用いることで GUI に関する部分を型システムに依存しない形で定義し、ユーザは型システムに関する関数のみを記述するように構成されている。

2.1

Two-level Types

Two-level Types を用いたプログラミングでは、再帰的な構造をしている一つのデータ型を、再帰的な構造を司る部分 (generic type) と、再帰以外の構造を表す部分 (speciﬁc type) の二つに分ける。
generic type と speciﬁc type は互いに依存せず独立して記述されるため generic type についての関数は speciﬁc type の内容を知らなくても記述できる。それを利用し、GUI に関する部分を generictype に対して記述しておき、ユーザが speciﬁc type のみを記述することで、GUI に関する部分を意識せずにプログラミングを行うことができる。
簡単な例として図 1. に示すような足し算言語の定義を用いて説明する。n は任意の数字（n と表記している）からなり、項 t は数字 n か、引数が二つとも t 型である足し算 t + t のどちらかである。次に推論規則について説明する。ここでは簡単のため推論規則として単純な formation 規則のみを扱っているが、型を導入した上で型規則を記述するのも全く同様に行うことができる。推論規則 TNum と TAdd はメタ変数を用いて記述されるが、ここでは t1 , t2 , n がメタ変数である。メタ変数とは、任意の具体的な構文に置き換えられる変数のことで、推論を進めていく中でメタ変数の値が
2

構文

n :=
t :=

n (TNum)
推論規則 t1 t2(TAdd)
t1 + t2nn | t + t

図 1. 足し算言語の定義

type num_t = N of int
type term_t = Val of num_t| Add of term_t * term_t

module NumS = structtype ’num_t t = N of int
end
module Num = Fix.F (NumS)
module TermS = structtype ’term_t t = Val of Num.fix_t| Add of ’term_t * ’term_t
endmodule Term = Fix.F (TermS)

図 2. OCaml による構文の定義

図 3. 型変数を用いた構文の定義確定すると、証明木中の同じメタ変数が同じ具体的な値に書き変わる。ここで n を t とは独立な構文としているのは、TNum で n がメタ変数として使われているためである。メタ変数として現れる
場合は独立した構文として定義する必要がある。
図 1. の構文を OCaml にして表現すると図 2. のようになる。直感的には、この OCaml の定義に
GUI の情報を追加していけば、簡単にグラフィカルな証明木を構築できそうである。しかしそうす
ると、プログラムの汎用性が失われてしまい、型システムが変わるたびに GUI に関する部分も書き直さなくてはならない。
それを避けるために Mikiβ では、図 2. のような構文定義に GUI の情報を付加することはせずに、
Two-level types を用いて、構文の定義は speciﬁc type として記述し、GUI に関する情報は generictype に付加するようにする。
Two-level Types を用いて構文を定義すると、再帰的に定義されている部分はパラメータ化され、図 3. のようになる。speciﬁc type はモジュール NumS、TermS の中で定義され、generic type はファンクタ Fix.F（後述）内で定義されている。モジュールにファンクタを適用することで Two-levelTypes を用いた定義が完成する。
詳しく説明すると、図 2. の型定義の末尾_t を S を置き換えたものをモジュール名とし、型名は全て t とする。図 2. における term_t は、図 3. において、TermS モジュール内で’term_t t として定義され、再帰部分は型変数 ’term_t に置き換わっている。’num_t t と’term_t t は Two-levelTypes における speciﬁc type であり、実際に Mikiβ で用いるためには、ファンクタ Fix.F 内に fix_t型として定義されている generic type を用いて、型変数を具体化する必要がある。ファンクタ Fix.F
は Mikiβ が提供するファンクタで、不動点オペレータである。
generic type として用いる fix_t 型の定義は以下のようになっている。fix_t 型の定義は、Fix
モジュールの F というファンクタで与えられる。STRUCTURE_SIG については次節で説明する。S はspeciﬁc type の定義を与えるもので、図 3. の NumS、TermS ようなモジュールが入る。

module F (S : STRUCTURE_SIG) = structtype fix_t = Fix of fix_t S.t| Meta of string * fix_t option ref3

end
fix_t はコンストラクタ Fix と Meta から構成される。それぞれについて説明する。
Meta はまだ具体化されていない項であることを表す。推論を進めるうちに単一化が起こり、 fix_t型の項に変化する可能性がある。1 つ目の引数はメタ変数の名前を示し、この名前が画面上に表示される。2 つ目の引数は fix_t 型のデータへのオプション参照を保持しており、同じ意味を持つメ
タ変数の参照先は同じになっている。このように generic type の部分にメタ変数の定義を入れることで speciﬁc type の部分はメタ変数を意識することなく定義できるようになっている。
一方、Fix は再帰以外の構造を表す speciﬁc type の部分を表す。ファンクタ Fix.F を適用すると、S.t の型変数が fix_t で具体化される。例えば、’term_t t の型変数’term_t は fix_t 型となり、Fix や Meta の値をとる。例を用いて説明する。図 2. のような Two-level Types を用いない
OCaml の定義の場合、再帰部分は term_t で表されており、そこには term_t 自身が入り再帰する。
このとき足し算 3 + 5 を表すと、Add (Val (N 3), Val (N 5)) のようになる。一方、Two-levelTypes を用いた定義では、’term_t t の再帰部分は型変数’term_t によって表されているが、それは fix_t で具体化され、’term_t と fix_t で相互再帰が起こる。Two-level Types において足し算
3 + 5 を表すと、以下のように表される。
let plus : Term.fix_t = Fix (Add (Fix (Val (Fix (N 3))), Fix (Val (Fix (N 5)))))
generic type である fix_t のコンストラクタ Fix と speciﬁc type のコンストラクタが交互に現れていることがわかる。このようなデータを本稿では Fix データと呼ぶ。
この複雑な定義を簡単に行うために「小文字でのコンストラクタ」を定義する。例えば NumS、
TermS について、次のようにして小文字のコンストラクタを定義する。
(* NumS の小文字のコンストラクタ *)let n num = Num.make_fix (NumS.N num)(* TermS の小文字のコンストラクタ *)let val n = Term.make_fix (TermS.Val (n))
let add t1 t2 = Term.make_fix (TermS.Add (t1, t2))関数 make_fix はファンクタ Fix.F 内に定義されている関数で、Fix データを生成する。小文字コン
ストラクタを用いて足し算 3 + 5 を記述すると add (val (n 3), val (n 5)) となり、Fix デー
タを簡単に定義できる。

2.2

ユーザ定義の関数

型変数を用いた’a t 以外にも、ファンクタ Fix.F に渡すモジュール内で定義しなければならない関数は 4 つある。map 関数は再帰部分に関数を適用するもの、unify 関数は単一化を行うもの、
search 関数はコンストラクタの各要素に真値 (true) があるかを調べるもの、draw 関数は描画方法を指定するものである。これらはユーザが定義する speciﬁc type である型’a t に依存するためユーザが記述しなければならない。ユーザが記述するモジュールのシグネチャは以下のようになっている。

module type STRUCTURE_SIG = sig
type ’a t (* データ型 *)val map : (’a -> ’b) -> ’a t -> ’b t
val unify : (’a -> ’a -> unit) -> ’a t -> ’a t -> unit
val search : bool t -> bool
val draw : id_t t -> id_t
end
4

4 つの関数の中で、map, unify, search はデータ型’a t から機械的に導出できる。一方 draw はユー
ザが定義したデータ型をどのように画面上に表示するかを表現する関数であり、データ型’a t から機械的に導出することはできない。
unify 関数と draw 関数を TermS モジュールを元に例として示す。
2.2.1

unify 関数unify 関数は、ユーザが定義した speciﬁc type の単一化を行う関数である。単一化されたらユニッ
トを返し、単一化できない場合には例外を起こすようになっている。この関数は speciﬁc type である’term_t t に対して記述されている。’term_t t の構造から機械的に導出できる関数だが、先行研究においてはユーザーが与える必要があった。
(* unify 関数の型 : (’a -> ’a -> unit) -> ’a t -> ’a t -> unit *)(* TermS 内の unify 関数 *)let unify f t1 t2 = match (t1, t2) with
| (Val (n1), Val (n2)) -> Num.unify n1 n2| (Add (n1, n2), Add (n3, n4)) -> f n1 n3; f n2 n4| _ -> raise (Unify_Error "of Term")
引数の関数 f を二つの項に適用させるため、二つの項のコンストラクタが同じでない場合には例外が発生する。このような speciﬁc type に対する unify 関数をユーザが定義すると、Fix.F に記述されている generic type の部分に関する unify 関数と合わせて、再帰的なデータに対する単一化を行えるようになっている。

2.2.2

draw 関数draw 関数はユーザが定義したデータ型を画面上の証明木にどのように表示するかを記述する関数である。Mikiβ では画面上に文字列を GUI オブジェクトとして配置することで証明木を描画している。id_t とは、画面上の各 GUI オブジェクトの持つ識別子である。この関数も speciﬁc type である’term_t t に対して記述されている。
(* draw 関数の型 : id_t t -> id_t *)(* TermS 内の draw 関数 *)let draw n = match n with
| Val (v) -> Num.draw v| Add (e1, e2) -> combineH [e1; create_str " + "; e2]create_str は文字列を生成し画面上に配置する関数、combineH は複数の GUI オブジェクトを水平に並べて配置する関数である。これらは draw 関数のために定義された、GUI オブジェクトを配置するための関数である。これらの関数を用いて画面上に GUI オブジェクトを配置する。型変数の入っていた部分には、既に生成された GUI オブジェクトが入っていると見なすことができる。

2.3

推論規則の定義

ユーザはファンクタ Fix.F に渡すモジュールの他に、推論規則の定義を記述する必要がある。これを OCaml で記述するためには、木構造を表すデータ構造’a tree_t を用いる。

type ’a tree_t = Axiom of ’a(* 公理 *)| Infer of ’a * ’a tree_t list (* 帰結 * 前提条件リスト *)5

足し算言語の例を考えると、’a は Term.fix_t で具体化される。Infer は帰結部分と、前提条件となる’a tree_t 型のリストから構成される。
推論規則はメタ変数を用いて記述される。ファンクタ Fix.F を適用すると、各データ型のメタ変数を生成する関数である make_meta 関数を得られる。文字列を引数とするが、メタ変数として表示する文字列を指定している。例えば、Term.meka_meta "e"は、画面上に “e”と描画する fix_t
Term.t 型のメタ変数を得る。これを用いて足し算の推論規則を記述すると以下のようになる。

let t_num () =let i = Num.make_meta "i" in
Axiom (n i)
let t_plus () =let e1 = Term.make_meta "e" inlet e2 = Term.make_meta "e" inInfer (add e1 e2, [Infer (e1, []); Infer (e2, [])])
推論規則内で用いるメタ変数を定義し、それを用いて推論規則を記述している。小文字で記述されている n や add、val は 2.1 節で説明した小文字のコンストラクタである。t_num は推論が終了したことを示す Axiom を用いて記述される。一方、t_plus は帰結部分と、前提条件のリストから構成されるが、前提条件のリストの Infer (e1, []) の部分は推論が終了していないため、Axiom ではなく前提が空である Infer で記述している。

2.4

Mikiβ 上で計算を行う項

ユーザファイルの定義ができたら、Mikiβ 上で型付けを行いたい項、つまり証明木の根となる項を文字列で入力し、lexer・ parser を用いて読み取ることで構文木に変換し、グラフィカルな証明木を用いた計算を開始していた。そのためユーザは lexer・ parser も記述する必要があった。

2.5

問題点

前節までに述べた方法でユーザファイルを定義する際には、以下のような問題点が挙げられていた。

1. OCaml に関する知識がなければ Mikiβ を利用できない点
2. OCaml で記述するコードの量が多く、複雑である点
3. 相互再帰する型をサポートできない点
4. 計算を行う項を文字列で入力する際に、間違いがあると項を認識しない点
3. について詳しく説明する。ユーザファイルで相互再帰する型を記述することができなかった理由は、ユーザが定義したモジュール外の型を参照するからである。例を用いて示す。図 4. のような型をモジュールを用いて表す場合、図 5. のように記述したくなる。
しかし、型’a_t t 内のコンストラクタ B の引数 B.fix_t は、モジュール B を定義前であるため使用できない。これを解決するためには、Fix.F の定義を変更してふたつの相互再帰する型を受け取ってきて、その不動点を取る形にする必要がある。しかし、このような変更はふたつの型が相互再帰している場合にしか使えない。３つの型が相互再帰する場合には、さらに別の Fix.F を定義する必要がある。加えて、このような定義を加えたとしても、ユーザが多くの OCaml プログラミン
グを行わなくてはならないという問題は変わらない。
続いて、4. について説明する。従来の Mikiβ では、実際に計算を行いたい項は文字列で入力し、ユーザが記述した lexer・parser を用いて字句解析・構文解析を行なった後に計算を開始していた。し6module AS = structtype ’a_t t = B of B.fix_t
end
module A = Fix.F (AS)type a_t = B of b_t
and b_t = A of a_t
図 4. 相互再帰をしている型の例

module BS = structtype ’b_t t = A of A.fix_t
end
module B = Fix.F (BS)図 5. 図 4. に対してモジュールを用いて記述した例

かし、lexer・parser に間違いがあった場合や、入力に間違いがあった際にはエラーが起き計算が開始できなかった。記号を用いた構文を入力する際などに、エラーが発生することが多く不便であった。
そこで本研究では、speciﬁc type を OCaml の型として与えるのではなく、単なるデータとして与えることで、これらの問題を解決した。次節で詳しく説明する。

3

データによるユーザの入力先行研究ではユーザは speciﬁc type として OCaml の型を用いてデータ型を定義していた。対して本研究では、型ではなくデータとして構文を定義する。これによりユーザによるモジュールを用いた型と関数の記述が必要なくなり、ファンクタは構造体となった。ユーザがモジュール内で型 tに対して記述していた諸関数を書く必要がなくなったことで、ユーザの OCaml プログラミングを必要としない、フォームを用いた web 上の入力からグラフィカルな証明木を構築することにつながった。ユーザが web ページから入力するのは「型定義・推論規則の定義・計算したい項の定義」の 3つである。本節では、先行研究における Mikiβ と比較してどのように変化したか述べる。

3.1

型定義

先行研究においては、ユーザが OCaml プログラミングで型変数をパラメータ化して型を定義していた。対して本研究では、ユーザが web のフォームから図 6. で示すレコード型を持つデータを入力し、それを Mikiβ 内部で 3.2.2 節で述べる図 10. のレコード型のデータに変換することで型を定義する。本節ではユーザの入力する図 6. で示すレコード型を持つデータについて述べる。
ユーザが定義するデータのレコード型を図 6. に示す。型、構成子、引数についてのレコード型をそれぞれ定義している。先行研究において OCaml にて’a t 型として与えていた型定義と draw関数の情報をデータとして保持している。詳しく見ていくと、type_t では型の名前と構成子の列、
constr_t では構成子の名前と引数の数と描画に関する情報、arg_t は引数の名前と型を指定している。引数の型は prim_t で指定していて、IntT、 StringT は OCaml における int 型と string 型
をそれぞれ表現している。RecT は再帰を表しており、type_t の type_name を文字列で引数として受け取り、格納する。
型定義を図 6. で示すレコード型を持つデータにしたことで、相互再帰する型も定義することが可能になった。モジュールを用いて定義していた際は、定義が終わっていない再帰先は記述することができなかったが、本研究では、文字列のデータとして与えるだけで再帰先の指定を行えるため、エラーが起きずに記述できる。

7

1
2
3

(* 描 画 指 定 用 の 型 *)type draw_t = Str of string| Arg of string(* 文 字 列 *)(* 引 数 を 指 定 *)(* 基 本 的 な 型
type prim_t =||(* 再 帰 *)

4
5
6
7
8

*)
IntT
StringT
RecT of string

9
10
11
12
13
14

(* 引 数 の 型 *)type arg_t = {arg_name : string ;arg_type : prim_t}(* 引 数 の 名 前 。 描 画 リ ス ト で 参 照 す る *)(* 引 数 の 型 *)

15
16
17
18
19
20
21

(* 構 成 子 ひ と つ の 型 *)type constr_t = {constr_name : string ;args : arg_t list ;draw : draw_t list ;}(* 構 成 子 の 名 前 *)(* 引 数 の 型 *)(* 描 画 指 定 リ ス ト *)

22
23
24
25
26
27

(* 型 の 型 *)type type_t = {type_name : string ;constrs : constr_t list ;}(* 型 の 名 前 *)(* 構 成 子 の 列 *)

28
29
30
31
32

type types_t = {name : string ;types : type_t list ;}(* メ イ ン の 型 の 名 前 *)(* 相 互 再 帰 す る 型 *)図 6. ユーザが型定義の入力画面から入力するデータのレコード型

先行研究では OCaml によって draw 関数を記述して描画に関する情報を与えていたが、本研究では構文を定義する際に描画に関する情報も同時に入力する。つまり、関数ではなく図 6. で示すレ
コード型を持つデータの中で描画に関する情報を与えている。draw_t について説明する。Str は引数の文字列をそのまま描画し、Arg は、arg_t の arg_name を引数とし、その引数を描画する。 例
えば足し算言語において、数字は、引数をそのまま文字列にして描画したいので、Arg "Num"とす
ると、引数がそのまま描画される。足し算は引数 t1, t2 と “＋ という文字列を表示したいので、[Arg "t1"; Str "+"; Arg "t2"] というリストになる。
図 6. のレコード型を持つ足し算言語についてのデータは図 7. のようになる。ユーザはこのようなデータを web のフォームを用いて画面上から入力する。

3.2

推論規則の定義

先行研究では推論規則の定義を OCaml プログラミングで記述していたが、本研究では図 8. のレ
コード型を持つデータとしてフォームを用いて画面上から入力し、そのデータを 2.3 節で述べた’atree_t に変換することで推論規則を定義する。

3.2.1

ユーザの入力ユーザが入力する推論規則のデータのレコード型の定義を図 8. に示す。rule_element_t で推論規則ひとつを表し、推論規則名を name、推論規則本体を rule のフィールドに格納する。rule_data_t
は規則が推論規則か公理かを表し、推論規則なら結論部と前提条件のリストからなる infer_t、公理なら前提のない axiom_t を引数とする。prim_data_t は推論規則データひとつを表す。prim_data_tにおける V が具体的な値やコンストラクタ、M がメタ変数である。

8

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17

let plus = {name = " term_t ";types = [{ type_name = " num_t ";constrs = [{ constr_name = " N ";args = [{ arg_name = " x1 "; arg_type = IntT }];draw = [ Arg " x1 "]}]};{ type_name = " term_t ";constrs = [{ constr_name = " Val ";args = [{ arg_name = " v1 "; arg_type = RecT " num_t "}];
draw = [ Arg " v1 "]};{ constr_name = " Add ";args = [{ arg_name = " e1 "; arg_type = RecT " term_t "};{ arg_name = " e2 "; arg_type = RecT " term_t "}];
draw = [ Arg " e1 "; Str "+"; Arg " e2 "]}]}]}

図 7. データとして定義した足し算言語の定義

実際に足し算言語の定義を図 8. のレコード型を持つデータにして例として示すと、図 9. のようになる。推論規則もフォームを用いて画面上から入力することで定義する。
1
2
3
4
5
6

(* 推 論 規 則 デ ー タ の 型 *)type prim_data_t = M of string* string| V of string* string* prim_data_t list

(*
(*
(*
(*
(*

メ タ 変 数 の 型 *)メ タ 変 数 の 名 前 *)構 成 子 の 型 *)構 成 子 の 名 前 *)構 成 子 の 引 数 列 *)

7
8
9
10
11

type infer_t = {conclusion : prim_data_t ;premises : prim_data_t list}(* 結 論 *)(* 前 提 の 列 *)type axiom_t = { axiom : prim_data_t }(* 公 理 *)type rule_data_t = I of infer_t| A of axiom_t(* 推 論 規 則 *)(* 公 理 *)

12
13
14
15
16
17
18
19
20
21
22

(* 推 論 規 則 ひ と つ の 型 *)type ru le_ele ment_ t = {name : string ;rule : rule_data_t}(* 推 論 規 則 の 名 前 *)(* 推 論 規 則 本 体 *)図 8. ユーザが推論規則の定義の入力画面から入力する推論規則のデータのレコード型

3.2.2

Two-level Types を用いた定義

推論規則は Mikiβ 内部では Two-level Types を用いた Fix データを用いて処理を行う。本研究における speciﬁc type と generic type について述べ、Mikiβ 内部で使用される Fix データを用いた推論規則の定義について説明する。まず、speciﬁc type について説明する。3.1 節で述べたユーザの入力した、図 6. に示したレコード型を持つ図 7. のようなデータを、図 10. で示す type_f に変換
し、speciﬁc type として用いる。type_f は図 6. の type_t に対応しており、再帰一段分の定義を表している。type_f は type_t と対応しているが、大きな違いが２点ある。１点目は、type_f が（speciﬁc type として使用するため）’a でパラメータ化されている点、２点目は描画に関する情報がなくなっている点である。１点目について説明する。2.1 節で述べたように、speciﬁc type は generictype と合わせて再帰を実現している。そのため speciﬁc type では再帰部分が ’a でパラメータ化

9

1
2
3
4
5
6
7
8
9
10
11
12
13

let infers = [{ name = " TNum ";rule =A ({ axiom =V (" term_t " , " Val " , [ V (" num_t " , " n " , [ V (" Int " , " n " , [])])])})};{ name = " TAdd " ,rule =I ({ conclusion =V (" term_t " , " Add " , [ M (" term_t " , " t1 "); M (" term_t " , " t2 ")]);
premises =[ V (" term_t " , " Val " , [ M (" num_t " , " n1 ")]);V (" term_t " , " Val " , [ M (" num_t " , " n2 ")])]})}]

図 9. データとして定義した足し算言語の推論規則
12
34(* 基 本 的 な 型 *)type ’a prim_f = IntF of int| StringF of string| RecF of string * ’a

5
6
7
8
9
10

(* 構 成 子 ひ と つ の 型 *)type ’a constr_f = {constr_name : string ;args : ’a prim_f list ;}(* 構 成 子 の 名 前 *)(* 引 数 の 型 *)

11
12
13
14
15
16

(* 型 の 型 *)type ’a type_f = {type_name : string ;constr : ’a constr_f ;}(* 型 の 名 前 *)(* 構 成 子 *)図 10. speciﬁc type として用いるデータのレコード型されており、この部分が後に generic type (fix_t) で具体化されることになる。２点目について説明する。証明木を構築するためには描画に関する情報が必要なため、type_t にはその情報が含まれる。しかし、証明木を表す内部データを構築する部分では描画情報は不要なため、type_f には
描画情報は含まれない。描画情報は、描画時に別途 type_t を参照することで取得する。（3.3.2 節参照。）
一方、generic type となる fix_t を以下のように定義し直す。

type fix_t = Fixof fix_t type_f* string| Meta of string* string* fix_t option ref(* 型名 *)(* メタ変数名 *)(* 型名 *)(* 実体へのポインタ *)先行研究における fix_t に比べて、コンストラクタ Fix における 2 つ目の引数とコンストラクタ
Meta における 2 つ目の引数が追加されている。これはどちらも type_name フィールドに格納されている文字列で、その項の型名を保持する。
type_f と fix_t を用いて、Fix データの足し算 3 + 5 と表すと図 11. の 32 行目の plus_3_5 のようになる。

3.2.3

Mikiβ 上で変換された推論規則

generic type と speciﬁc type を用いて Fix データを生成できたら、’a tree_t の引数部分に格納し、Mikiβ 内部で用いる推論規則とする。これで先行研究における推論規則の定義と同じ情報を生
10

1
2
3
4
5

let n_3 : fix_t type_f = {type_name = " num_t ";constr = { constr_name = " N ";args = [ IntF 3]}
}

6
7
8
9
10
11

let val_3 : fix_t type_f = {type_name = " term_t ";constr = { constr_name = " Val ";args = [ RecF (" num_t " , Fix ( n_3 , " num_t "))]}
}

12
13
14
15
16
17

let n_5 : fix_t type_f = {type_name = " num_t ";constr = { constr_name = " N ";args = [ IntF 5]}
}

18
19
20
21
22
23

let val_5 : fix_t type_f = {type_name = " term_t ";constr = { constr_name = " Val ";args = [ RecF (" num_t " , Fix ( n_5 , " num_t "))]}}

24

let plus_33 : fix_t type_f = {type_name = " term_t ";constr = { constr_name = " Add ";args = [ RecF (" term_t " , Fix ( val_3 , " term_t "));
RecF (" term_t " , Fix ( val_5 , " term_t "))]}

25
26
27
28
29
30

}

31
32

let plus_3_5 : fix_t = Fix ( plus_33 , " term_t ")図 11. 3 + 5 の Fix データの例

成できた。

3.3

ユーザ定義の関数

2 節で述べた関数である、unify 関数と draw 関数についてそれぞれの定義を述べる。先行研究ではユーザが定義していたが、本研究では Mikiβ が提供するためユーザは記述しない。
3.3.1

unify 関数unify 関数を含む諸関数は type_f に対して記述するように変更される。すると、型のコンストラ
クタについてパターンマッチを行っていたところが、type_f・constr_f・prim_f のレコードについてパターンマッチを行うようになった。すると、型定義が変更されても同じ関数で記述できるため、毎回ユーザが記述する必要がなくなった。
3.3.2

draw 関数

すでに述べた通り、draw 関数で表現していた画面上へどのように描画するかの情報は、データとして図 6. における constr_t の draw フィールドにリストとして保存している。Mikiβ は証明木を構築する際に、draw_t に格納されている情報を参照して GUI オブジェクトを作成し、画面上に配置する。そのため、draw 関数としてユーザが記述する必要がなくなった。

3.4

Mikiβ で計算を行う項

証明木の根となる項もフォームを用いて入力する。図 8. における prim_data_t 型の入力を受け取ったら Fix データに変換し、Mikiβ 上での計算を開始する。

11

4

フォームを用いた入力

3 節で述べた通り、データにより定義を与えることで、ユーザが OCaml プログラミングによって型や関数を記述する必要がなくなった。本研究では、証明木を構成するために必要な情報ををフォー
ムを用いて画面上から入力できるよう入力画面を実装した。前節でも述べた通り、ユーザが入力する情報は、構文・出力の定義、推論規則の定義・Mikiβ 上で計算を行う項である。本節では、それぞれの入力画面とフォーム上からの入力を足し算言語を例としながら述べる。

4.1

型定義

足し算言語の型定義の入力について述べる。図 7. で示したようなデータをフォームから入力する。実際に入力する画面は図 12. のようになっている。

図 13. 画面上からの推論規則の定義

図 12. 画面上からの型と定義の入力「drawbox」では、証明木の描画に関する情報を入力する。「drawbox の数」で数を選択するとdrawbox の数を調整することができ、引数を描画する際は arg を選択し、入力した引数から該当するものを選択する。「+」のような文字列を入力する際には String を選択して表示したい文字列を入力する。一番下には入力した内容が反映され、OCaml の型定義のような形で表示されている。
一つの型の入力ごとに、抽象構文木のような形で、文字列でユーザの入力を表示している。このように表示したことで、フォームを用いた入力がユーザの意図した通りになっているかを確認しやすくなっている。

12

また、型一つずつをドラッグ可能となるように実装した。これにより、型の順番を自由に入れ替えることができる。

4.2

推論規則の定義

推論規則の定義の入力について述べる。図 9. で示したデータを web 上から入力する。入力する
画面は図 13. のようになっている。推論規則の定義では、入力するのは「規則の名前・前提の数・結論・前提」の 4 項目である。「規則の名前」では規則名、「前提の数」では各規則の前提の数を入力する。次に「結論」と「前提」の入力について説明する。結論は conclusion、前提は premises に入力する。「前提の数」に応じて premises の入力欄の数が変動する。
前節で述べた通り、推論規則はメタ変数を用いて記述する。TAdd の場合、t1 、t2 がメタ変数となる。メタ変数を入力する際には、“meta : ”がはじめについている選択肢を選ぶと入力できる。
まず、結論の入力を説明する。根の型を term t にしたので、推論規則に現れる型は必ず term t型となる。TAdd の結論部は足し算の形をしているのでコンストラクタ Add を選択する。すると、前節で入力した term t の構成子 Add には引数が 2 つあったため、2 つの引数が表示される。項の定義で入力した内容を参照しながら選択肢が表示される。メタ変数を選択した場合、同じ文字列は同じ
メタ変数として認識されるようになっていることに注意しながらメタ変数の変数名を記述する。メタ変数以外を選択した場合、すなわち構成子を選んだ場合には前節の定義をもとに引数が自動的に表示される。
前提部分は、結論部分と同様に記述する。メタ変数は 1 つの規則の中で有効である。例えば、TAddの結論部で用いたメタ変数 t1 は結論だけでなく前提でも使用することができる。
推論規則は、構文にそって入力のフォームや入力ボックスが配置されるように工夫した。これにより、複雑な体系になってもそれぞれの項の引数が何かわかりやすくなっている。
また、型定義と同様に、入力内容が文字列で表示されるようになっている。この文字列は、型定義で入力した drawbox の内容を参照しながら表示されている。例えば、図 13. における TAdd の規則の結論部分 conclusion では、図 12. で示した型定義の入力の中の構成子 Add の drawbox を参照
して t1 + t2 と文字列を表示している。
型定義と同様に、推論規則一つずつをドラッグ可能となるように実装したため、順番を自由に入れ替えることができる。

4.3

Mikiβ 上で計算を行う項

最後に、Mikiβ 上で実際に計算を行いたい項を入力する。推論規則と同様に項を入力し、「go」ボタンをクリックすると計算を開始する。

4.4

lexer, parser について

web 上から入力できるようになり、ユーザは OCaml でプログラミングをせずに Mikiβ を利用してグラフィカルな証明木を構築できるようになった。今までは OCaml の型定義として構文を定義していたため、文字列での入力を読み取り構文解析していたが、本研究では画面上でセレクトボッ
クスを用いて入力するため、lexer・parser が必要なくなった。その結果入力ミスによる Syntax エ
ラーや、間違った構文を入力する事による型エラーも起きなくなった。
先行研究では型安全性が OCaml の型システムにより保たれていたが、本研究では、フォームを用いた web 上からの入力を実装し、型が間違っている入力はできなくなったため、型安全性は引き続き保たれている。

13

図 14. Mikiβ 上で構築した単純型付ラムダ計算の証明木

4.5

構築された証明木

型定義・推論規則の定義・Mikiβ 上で計算を行いたい項の 3 つを入力したら証明木を構築し計算を開始できる。単純型付ラムダ計算を例に構築された証明木を図 14. に示す。一番上の段には定義した推論規則のボタンが並んでいる。真ん中の段には Mikiβ 上で計算したい項が入力されている。
「開く」ボタンを押すと、入力画面が表示される。一番下には構築された証明木が表示されている。
証明木をクリックすると、そのノードに適用可能な規則のボタンが緑色に光るようになっている。
そのボタンをクリックすることで計算が進んでいく。

5

諸機能の実装5.1

xml ファイルへの入出力とダウンロード

入力した定義のダウンロード、アップロードを行う機能を実装した。ダウンロードを実行すると入力した定義を保存することができ、またそのファイルをアップロードすれば使用することができる。この機能は OCaml を JSON ファイルに出力、解析する yojson というライブラリを用いて実
装した。

5.2

これまでに実装した体系

本研究において使用した定義を使用できるように実装した。使用したい体系を選択し、『ok』のボタンをクリックすると Mikiβ 使用を開始できる。編集、ダウンロードなどの機能は変わらず利用できる。
使用できる論理体系は 8 つあり、「sk, sk_plus, nm, nm_plus, lambda_caluculus, shift_reset,
control_prompt, 4typeControlOperators」となっている。それぞれの体系について説明する。
まず、sk とは一階命題論理の体系 SK [9] を実装したもので、sk_plus とは、sk に諸規則を追加したものである。nm は自然演繹による最小論理の体系 N M を実装したものであり、nm_plus は
nm に諸規則を追加し N J や N K まで拡張したものである。lambda_caluculus は単純型付きラムダ計算を実装したものである。shift_reset は単純型付ラムダ計算に限定継続 shift/reset を加えたもの、control_prompt [2] は単純型付ラムダ計算に限定継続 control/prompt を実装したもの、
4typeControlOperators [3] は単純型付ラムダ計算に 4 種の限定継続、shift/reset・shift0/reset0・
control/prompt・control0/prompt0 を実装したものである。
本研究においては、先行研究でユーザが OCaml にて与えていた定義と同じ情報をデータで与えるようになったため、先行研究で定義することのできる体系は全て本研究においても定義すること
ができる。

14

5.3

tex への出力

利便性の向上のため、定義や完成した証明木の tex への出力を実装した。
『tex を download する』というボタンをクリックすると tex のファイルがダウンロードされる。ファイルは、項の定義・推論規則の定義・計算した証明木の３つから構成される。項の定義と推論規則の定義は新しいコマンドとして定義し、それを用いて計算した証明木を出力する。足し算言語の体系を例に示す。
項の定義のセクションの中身として、N、Val、Add の三つの定義は以下のように出力される。
\ newcommand \ MikiBetaN [1]{{#1}}\ newcommand \ MikiBetaVal [1]{{#1}}\ newcommand \ MikiBetaAdd [2]{{#1} + {#2}}1
2
3

これは、項の定義でユーザーが入力した drawbox を元に出力されている。次に、推論規則の定義のセクションの中身を例として示す。TNum と TAdd の推論規則は以下のように出力される。
\ newcommand \ M i k i B e t a R u l e N a m e [1]{(\ textsc {#1})}

1
2%推 論 規 則 の 定 義\ newcommand \ MikiBetaTNum{\ infer [\ Mi ki Be ta Ru le Na m e { TNum }]{{\ MikiBetaVal { n }}}{{}}}

3
4
5
6

\ newcommand \ MikiBetaTAdd{\ infer [\ Mi ki Be ta Ru le Na m e { TAdd }]{{\ MikiBetaAdd { t1 }{ t2 }}}{{{ t1 }}&{{ t2 }}&{}}}

7
8
9
10

1 行目では、規則名の表示の仕方、4 行目で TNum、7 行目で TAdd の定義を出力している。項の定義のセクションで作成したコマンドを使用して記述され、引数部分には、Mikiβ にユーザーが入力した文字列がそのまま出力されている。最後に、計算した証明木のセクションについて述べる。3+ 5 を計算した結果は以下のように出力される。
%計 算 し た 証 明 木\ newcommand \ M i k i B e t a P r o o f T r e e{\ infer [\ Mi ki Be ta Ru le Na m e { TAdd }]{\ MikiBetaAdd {\ MikiBetaVal {\ MikiBetan {3}}}{\ MikiBetaVal {\ MikiBetan {5}}}}{\ infer [\ Mi ki Be ta Ru le Na m e { TNum }]{\ MikiBetaVal {\ MikiBetan {3}}}{}&\ infer [\ Mi ki Be ta Ru le Na m e { TNum }]{\ MikiBetaVal {\ MikiBetan {5}}}{}
&{}}}

1
2
3
4
5
6
7

これを実際に LATEX 上で表示すると、以下のようになる。

3(TNum)(TNum)
5
3+5(TAdd)

証明木は上記で生成したコマンドを使って記述しているため、tex におけるスタイルを変更したい場合、項の定義や推論規則の定義のセクションで定義したコマンドを変更すれば簡単に可能である。

関連研究

6

自然演繹の学習支援システム [5] では、選択したレベルに応じて学習をサポートしながら、画面上で自然演繹の計算を行う。これは、自然演繹における証明木の構築・学習支援ができるものだが、本研究ではユーザが論理体系を自由に設定できる点で異なっている。
五十嵐は、教科書「プログラミング言語の基礎概念」[10] に出てくる体系の証明木をブラウザ上
で入力、チェックできる演習システム1 を開発している。教科書に出てくる色々な体系の証明木を試せるようになっているが、証明木の入力は GUI ではなくテキストである。また、新たな体系をユーザが加えることはできない。
1

https://www.fos.kuis.kyoto-u.ac.jp/~igarashi/CoPL/

15

Mikiβ は、公理や推論規則をユーザが与えるとそれに従った証明木を書くことができるようになる。これは、公理や推論規則を全て与え、その上に論理体系を構築している Coq [1] や Agda [6] といった定理証明系と近いととらえることができる。従って、同様の定義を記述すれば、原理的には
Mikiβ でも定理証明系と同じようなことができると考えられる。しかし、タクティクスや便利なコ
マンドは Mikiβ にはなく、あまり現実的ではないと考えられる。
Coq と連携して自動的に証明木を生成する TRaf [4] というツールがある。Proof General を介した対話的な証明を行う過程に対し、グラフィカルな証明木を生成し表示するが、GUI 上で証明を行うものではない。

7

まとめ

7.1

本研究の成果本研究における成果は大きく分けて 2 つある。1 つ目は、ユーザの入力と speciﬁc type をデータにしたことにより、相互再帰する型をサポートできるようになったことである。先行研究におけるモジュールを用いた手法では制約が多く定義できなかったが、本研究においてデータで記述したことで、再帰先を文字列で指定するだけで再帰の構造を記述できるようになり、型の表現の自由度が向上し利用できるようになった。
例えば control_prompt 付き単純型付ラムダ計算 [2] や 4 種の限定継続付き単純型付ラムダ計算 [3]は相互再帰を含む複雑な体系であり、手計算で型推論を行うことは非常に困難であった。compatible
や id cont type など、手計算では結果がわかりにくく複雑な規則を含むからである。しかし、Mikiβを用いてグラフィカルな証明木を構築できたことで、型推論の様子を (手動で) 観察できるようになった。
2 つ目は、ユーザが OCaml プログラミングをせずに、フォームを用いた web 上からの入力のみで証明木を構築できるようになったことである。これにより、OCaml の煩雑なプログラミングが必要なくなり、より使いやすくなった。Agda や Coq を用いて証明を行うためにはそれぞれ知識が必要になるが、Mikiβ を用いて計算を行えば、プログラミング言語に関する知識がなくても計算を行うことができる。また、画面上で入力した定義を参照しながら推論規則を入力するため、再帰先が間違っている項は入力できなくなり、複雑な体系でも利用しやすくなった。また、相互再帰における再帰先の指定も画面上から再帰可能な型から選択することにより行うので、間違った再帰を記述できなくなった。

7.2

定義できない論理体系

相互再帰をサポートし、利用できる体系は大きく広がったが、まだ利用できない体系も多く存在する。例えば、集合を扱う体系は定義するのが難しい。理由としては、集合の中の任意のひとつをとってくるといった操作や、集合の中身の順番が変わっても同じ集合とみなすといった操作をどのように推論規則で表現したら良いか明らかではないためである。

7.3

今後の課題

今後の課題は大きく 2 つ挙げられる。1 つ目は、Mikiβ で多くの論理体系を実装してみることである。定義できる論理体系の例を集め、より多くの研究分野で利用できるようにしていきたい。2
つ目は、入力方法の改善である。本研究においては、フォームを用いて必要な情報を入力しているが、この方法では入力に時間や手間がかかり、まだ初めて見た人には入力が難しいと言える。将来
的にはブロックベースでの入力などを実装し、より直感的に入力できるようにしたい。

16

謝辞
有益なコメントをくださった査読者の皆様に感謝申し上げます。本研究は一部 JSPS 科研費
20K12107 の助成を受けたものです。

参考文献[1] Yves Bertot and Pierre Castéran. Interactive Theorem Proving and Program Development, Coq’Art:
The Calculus of Inductive Constructions. Springer, 2004.
[2] Y. Cong, C. Ishio, K. Honda, and K. Asai. A functional abstraction of typed invocation contexts.
Logical Methods in Computer Science, Vol. 18, 2022.
[3] C. Ishio and K. Asai. Type system for four delimited control operators. Proceedings of the 21st ACM
SIGPLAN International Conference on Generative Programming: Concepts and Experiences (GPCE2022), pp. 45–58, 2022.
[4] Hideyuki Kawabata, Yuta Tanaka, Mai Kimura, and Tetsuo Hironaka. Traf: A graphical proof tree
viewer cooperating with coq through proof general. In Sukyoung Ryu, editor, Programming Languages
and Systems, pp. 157–165, Cham, 2018. Springer International Publishing.
[5] Kazuhisa Miwa, Hitoshi Terai, Nana Kanzaki, and Ryuichi Nakaike. An intelligent tutoring systemwith variable levels of instructional support for instructing natural deduction. Transactions of theJapanese Society for Artiﬁcial Intelligence, Vol. 29, No. 1, pp. 148–156, 2014.
[6] Ulf Norell. Towards a practical programming language based on dependent type theory. PhD thesis,
Chalmers University of Technology, 2007.
[7] Kanako Sakurai and Kenichi Asai. MikiBeta: A general GUI library for visualizing proof trees. 20th
International Symposium on Logic-Based Program Synthesis and Transformation, pp. 1–15, July 2010.
[8] Tim Sheard and Emir Pasalic. Two-level types and parameterized modules. Journal of Functional
Programming, Vol. 14, No. 5, pp. 547–587, 2004.
[9] 戸次大介. 数理論理学. 東京大学出版会, 2016.
[10] 五十嵐淳. プログラミング言語の基礎概念. サイエンス社, 2011.

17