モジュールをサポートする OCaml ステッパの定式化と実装
秋山 雛乃, 浅井 健一
お茶の水女子大学{akiyama.hinano, asai}@is.ocha.ac.jp
概 要
本研究では OCaml プログラムの計算過程を 1 ステップごとに出力するプログラムである OCaml ステッパを拡張して、これまでは不十分であったモジュールをサポートする。先行研究では同ファイル内のモジュール宣言一般を対象とした実装を行なったが、モジュールの上がり下がりに対応していなかった。本研究では、モジュールをサポートするステッパを実装するた
め、まず OCaml ステッパの定式化を行なった。定式化する際、モジュールの上がり下がりに対応するため、レベルを導入した。そして、レベルの変動を表現する drop 関数と lift 関数を導入した。この定式化に基づいて、実際にモジュールをサポートする OCaml ステッパの実装を行な
い、変数や構成子がモジュールを出入りする際、正しくモジュール名が付与されているのを確認
した。

1

はじめに

プログラマにとって、プログラムを確認し、自分の思っている通りの実行がされているか知ることは重要である。しかし、プログラミング初学者にとっては、エラーメッセージや正しくない出力結果から適切なプログラムを導き出す作業は容易ではない。また、デバッガ特有のコマンドなどを覚えデバッグ作業をすることは初学者の負担となってしまう。
そこで本研究室では、初学者のプログラミングを支援するツールとして、OCaml ステッパが開発された。OCaml ステッパとは、入力として型チェックの通ったプログラムを受け取り、プログラムの計算過程
を１ステップごとに出力するプログラムである。使用者はエディタ上のボタンの操作で、プログラムを最初から最後までステップ実行していく流れを確認することができる。広く使われている gdb [1] や OCamlに付属する ocamldebug などでもプログラムのステップ実行を行うことができる。しかし、これらのツールで行われているステップ実行は、プログラム中のどこを実行しているかを示し、その時点での変数の値等を見られるようにしているものである。本研究で示すステッパはそれとは異なり、プログラムが実行されるに従ってプログラム全体がどのように変化していくのかを示すものである。OCaml ステッパはデバッ
ガ特有のコマンドを覚えたり、ブレークポイントを設定したりなどの難しい操作を必要としないため、プ
ログラミングに慣れていない初学者でも使いやすいと考えられている。例えば、OCaml で書かれた

let f x = x + 1 in 8 + (f 3)というプログラムを入力すると以下のように出力される。

(* Step 0 *) let f x = x + 1 in 8 + (f 3)(* Step 1 *) 8 + ((fun x -> x + 1) 3)(* Step 1 *) 8 + ( (fun x -> x + 1) 3 )(* Step 2 *) 8 + ( 3 + 1 )(* Step 2 *) 8 + ( 3 + 1 )(* Step 3 *) 8 + ( 4 )(* Step 3 *) 8 + 4(* Step 4 *) 12
このように１段階ずつ確認することで、具体的にどのような計算がされているのかを観察でき、プログ
ラムの流れを学ぶことができる。また、自分の想定と違うことがどの部分で起きたのか見ることができる

1

ので、バグの原因が分かりやすく、デバッグにおいても有用である。実際にお茶の水女子大学では関数型言語の授業でステッパを使用しており、学習においてある程度役立っている。 [2]
本研究ではモジュール宣言一般を対象としたステップ実行ができる OCaml ステッパを作る。モジュール宣言は実際にお茶の水女子大学の関数型言語の授業で扱われる構文であり、初学者用のステッパとして対応する必要であると考える。また、実装レベルで網羅的にモジュールをサポートすることは難しかった
ため、本研究では OCaml ステッパの定式化に取り組み、その定式化を元に実装を行った。
モジュールをサポートするために問題となった点は、モジュールの内側の値や式をモジュールの外側で使用する際、モジュールの内側で宣言されているものなのか外側で宣言されているものなのか区別できな
かった点である。この問題に対して本研究ではいくつ外側のモジュールで宣言されたかを表すレベルを導入し、そのレベルを変化させることで解決した。また、レベルは多重モジュールに対応するため 0 以上の整数で導入した。
例えば、以下のプログラムを実行するとき、type t = C
module X = struct
let a = Ctype t = C
let b = C
end
let b = X.b
let a = X.a
3 行目の let a = C のコンストラクタ C は、1 行目で宣言されているコンストラクタであるため、一つ外側で宣言されていることを表すレベル 1 が付与される。また、5 行目の let b = C のコンストラクタ C はモジュール X の中で宣言されているため、レベル 0 が付与される。このような情報が付与されることでモジュールの中身が代入される際区別がつくようにした。
そして、5 行目の実行が終わるとモジュール X の中身の実行が終わりとなるため、モジュール X の中身である 3 行目から 5 行目の情報を 7 行目以降のプログラムへ代入しにいく。7 行目の X.b には、モジュー
ル X の中で宣言されたレベル 0 のコンストラクタ C がモジュール X の外側で使用されるため、X. が頭についた X.C が代入される。本研究では、このようにモジュールの中身をモジュールの外側へ代入することを「モジュールが持ち上がる」と定義し、その際、必要に応じてモジュール名をつけることを「レベルを持ち上げる」と定義し、lift 関数として定式化を行った。
次に 8 行目の X.a には、モジュール X の内側にある 3 行目のコンストラクタ C が代入される。この時、レベル 1 のコンストラクタ C はモジュール X の外側で宣言されているため、レベルが持ち上がっても X.
が付与されない。これはレベル 1 からレベルが持ち上げられレベル 0 になり、宣言された場所と同じ階層に持ち上げられたため、X. は付けないという判断をすることで実装する。そのため、1 行目が実行されモジュール X の中へコンストラクタ C の情報を付与する際、一つ上のモジュールで宣言されていることを表すため、レベルを１加算する必要がある。この操作を「レベルを持ち下げる」と本研究では定義し、drop
関数として定式化を行った。また、モジュールの外側で宣言されているプログラムの情報をモジュールの内側へ代入することを「モジュールを持ち下げる」と本研究では定義する。
なお、本論文ではモジュール内の全ての定義がモジュール外から見えることを仮定しており、モジュー
ルインターフェースによる隠蔽は考慮しない。これは隠蔽されているものをどのようにステップ実行すべ
きか明らかではないためである。また、今回はステップ実行を行う部分のみで必要な情報全てを得ることができるようにしたため、型チェックを通った構文木の状態から静的にコンストラクタの名前解決を行う
ための専用の解析器を通ってステップ実行を行う方法は取っていない。
本論文の構成は以下の通りである。まず 2 節でステッパの対象言語について定義をし、3 節で簡約規則、4 節で実行規則、5 節で変数の代入規則、6 節でコンストラクタのレベル設定規則、7 節でモジュールの代
2

パス
値
式

p ::= ϵ | X.p
v ::= c | p.C | p.x | λx. e | let rec f = λx. e in f |p.C[@n] | p.x[@n][@λx. e] | p.f [@n][@let rec f = λx. e in f ]e ::= v | e0 e1 | let x = e in e | let rec f = λx. e in e | try e with p.C → e |raise e | p.x[@n][@c] | p.x[@n′ ][@p.C[@n]] | try e with p.C[@n] → e
F ::= 2 | e F | F v | let x = F in e | raise F
E ::= F | E[try F with p.C[@n] → e]j ::= {let x = v} | {let rec f = λx. e} | {module X = struct r end} |{exception C}
i ::= let x = e | let rec f = λx. e | module X = struct s end | exception C
r ::= [ ] | j :: rs ::= [ ] | i :: s | j :: spure な評価文脈
評価文脈
評価済みストラクチャ
アイテム
ストラクチャアイテム
評価済みストラクチャ
ストラクチャ
ストラクチャのS ::= 2 | j :: S | (module X = struct S end) :: s
評価文脈
図 1. 対象言語の定義

入規則、8 節で実装について説明する。その後、9 節で関連研究について触れ、10 節でまとめる。ステッパの定式化結果は全てを載せることができなかったので付録として掲載する。ただし、重要な規則について
は全て本文で触れ、付録は読まなくても理解できるように説明している。

2

対象言語

パス、値、項、評価文脈、ストラクチャとストラクチャの評価文脈を図 1 に示す。p はモジュールのパスを表す。例えば、X.Y.Z.a の場合は X.Y.Z. の部分を表す。また、モジュール名がつかない a の場合はパ
スは空を表す ϵ となる。
v は値、e は式を表す。c は定数、p.C はコンストラクタを表す。ここで、[@n] とはモジュールの上がり
下がりに対応するために導入したレベル（いくつ外側のモジュールで宣言されたか）を表す。また、[@n]の後についている [@λx. e] や、[@c] は先頭の変数やコンストラクタに代入される値 [@v] を表す。実装した
OCaml ステッパでは、[@n] と [@v] は OCaml の構文木に attribute を付与することで実装している。この時、OCaml ステッパをエディタで使用する際、attribute として付与された [@n] と [@v] は表示されない。そのため、初学者は自分が書いたプログラムがどのように実行されているかのみを確認することができる。また、[@n] と [@v] がついた状態で OCaml プログラムとして実行することは可能である。[@n] と[@v] については 4 節で詳しく説明するが、例えば、以下のプログラムが入力されると、type t = C
let a = C
module X = struct
let b = aend
モジュール X の中の b の値である a にはモジュール X の外側の a の値である C が代入されるため、以下のようにレベルと代入値が付与される。

type t = C
let a = C[@0]module X = struct
let b = a[@1][@C[@1]]3

(λx. e) v
(let rec f = λx. e in f ) v
let x = v in e
let rec f = λx. e1 in e2

→
→
→
→

e[v/x]
e[v/x, let rec f = λx. e in f /f ]e[v/x]
e2 [let rec f = λx. e1 in f /f ]try v with p.C[@n] → etry F [raise p.C[@n]] with p′ .C ′ [@n′ ] → e
try raise p.C[@n] with p.C[@n] → e
try raise p.C[@n] with p′ .C ′ [@n′ ] → e

→
→
→
→

v
try raise p.C[@n] with p′ .C ′ [@n′ ] → eeraise p.C[@n](p.C[@n] ̸= p′ .C ′ [@n′ ])p.x[@n][@c]p.x[@n′ ][@p′ .C[@n]]p.g[@m][@(λx. e)] v′(p .g[@m][@let rec f = λx. e in f ]) v

→
→
→
→

c
p′ .C[@n]e[v/x]
e[v/x, p′ .g[@m][@let rec f = λx. e in f ]/f ](e2 ̸= f )e1 → e2E[e1 ] → E[e2 ]図 2. 簡約規則

end
図 1 の F は try with に囲まれない pure な評価文脈を表し、E は try with も含めた評価文脈を表す。
これを分けることで try with のステップ実行をサポートしているが、この部分については先行研究 [2] にて述べられているため、今回は説明を省略する。
i はストラクチャアイテム、s はストラクチャを表す。OCaml では in のない let 文やモジュール宣言、
例外を含む型宣言などはストラクチャアイテムと呼ばれ、それらが連なったプログラム全体のことをストラクチャと呼ぶ。式 e に対して値 v が存在しているのと同様に、j と r はそれぞれ評価済みのストラクチャ
アイテム、ストラクチャを表す。評価済みのストラクチャアイテムは中括弧で囲って表現する。s は、評
価済みのものとそうでないもののリストとなっているが、実際には評価済みのものがリストの最初に並び、その後に評価済みでないものが並ぶが、構文レベルではそれは表現していない。最後に、S はストラクチャの評価文脈である。

3

簡約規則

簡約規則を図 2 に示す。最初の 4 つは普通の簡約規則、次の 4 つはレベルを無視すれば try with の普通の簡約規則である。（try with については、先行研究 [2] を素直に定式化しただけなので、本論文では説明を省略する。）
その次の 4 つは、変数への代入の様子を示す。let a = 3 in a + 1 のように in のある let 文の場合は、次のステップで a に 3 が代入されて 3 + 1 とする。しかし、in のない let 文の場合、いきなり代入してしまうとわかりにくくなる。例えば、

let a = 3.....（長いプログラム）
let b = a + 1のようになっている場合、let a = 3 を実行した時点で、はるか下にある a + 1 を 3 + 1 にしてしまうと、途中の長いプログラムをステップ実行している際に、a への代入が既に行われていることを忘れがちである。ステップ実行が最後の行にくると、ユーザーは

4

e1 → e2(let x = e1 ) :: s ; (let x = e2 ) :: ss1 ; s2
S[s1 ] ; S[s2 ](let x = c):: s
; {let x = c}:: s[x[@0][@c]/x](let x = λz. e):: s; {let x = λz. e}:: s[x[@0][@λz. e]/x](let x = let rec f = λz. e in f ):: s; {let x = let rec f = λz. e in f }:: s[x[@0][@let rec f = λz. e in f ]/x](let x = p.C[@n]):: s; {let x = p.C[@n]}:: s[x[@0][@p.C[@n]]/x](let x = p.g[@n][@λz. e]):: s; {let x = p.g[@n][@λz. e]}:: s[x[@0][@λz. e]/x]′(let x = p .g[@n][@let rec f = λz. e in f ]) :: s
; {let x = p′ .g[@n][@let rec f = λz. e in f ]} :: s[x[@0][@let rec f = λz. e in f ]/x](let rec f = λx. e):: s; {let rec f = λx. e}:: s[f [@0][@let rec f = λx. e in f ]/f ](module X = struct r end):: s
; {module X = struct r end}:: s[lift(X, r)/X]0(exception C):: s; {exception C}:: s[C[@0]/C]
図 3. 実行規則

let b = 3 + 1という自分で書いた覚えのないプログラムを見ることになるが、ここはユーザーが書いた

let b = a + 1というプログラムを一旦見せてから

let b = 3 + 1を見せた方がわかりやすいと考えられる。このように、既に変数 p.x に値 v が束縛されているが、代入はまだ行われていない式を p.x[@n][@v] と表している。
（このような式は 4 節の実行規則によって作られる。）
このような形の式が現れたときの簡約規則が図 2 の下 4 つの規則である。最初の 2 つは変数が 1 ステッ
プで束縛された値に簡約されることを示す。一方、束縛された値が関数の場合は、変数を展開することはせず、引数が渡された時点で関数の本体に展開する。これは、let f x = x + 1
let _ = f 3のような式をステップ実行する際、f 3 を初心者にはわかりにくいと思われる (fun x -> x + 1) 3 に展開するのではなく、このステップは飛ばしていきなり 3 + 1 に展開するということである。
最後の規則は、これらの簡約規則を任意の評価文脈の元で行って良いことを示す。

4

実行規則

前節では項に対する簡約規則を示した。この節では、ストラクチャがどのように実行されるかを表す実行規則を図 3 に示す。
本論文で扱うストラクチャアイテムは 4 種類ある。このうち、let 文と module 宣言については、まず内部の実行を先に行う。それを示している規則が図 3 の最初の 2 つの推論規則である。前者は let 文で定5

義される式を簡約して値にするもの、後者は、モジュールの中身を実行するものである。これらが済んだ
ら、ストラクチャアイテム自身の実行に入る。その規則を図 3 の後半に示している。
最初は let 文の規則である。let x = v のようなストラクチャアイテムがあった場合、それは {...} で括られて実行済みとなるとともに、以降のストラクチャs に対して「x の値は v である」という情報を代入する。
ただし、3 節で説明したように、いきなり x を v に置き換えてしまうとわかりにくいので、x を x[@0][@v]に置き換える。これは「変数 x だが、その値は v に置き換わる」ということを示す。（[@0] については後述。）のちにステップ実行がこの変数に差し掛かった際、簡約規則に示した通り、1 ステップ使って x が vに置き換わることになる。
他の場合も同様だが、代入される v が p.g[@n][@v] の形の変数の時は注意が必要である。これは以下のような状況を表している。

let f = fun x -> x + 1
let x = f
let f = fun x -> x + 2
let y = x
1 行目の実行で 2 行目の f は f[@0][@λx.x+1] となっている。この状況で 2 行目の実行を行うと、以降のストラクチャアイテムに対して x の値を代入しにいくことになる。しかし、図 3 の実行規則では、
x[@0][@f[@0][@λx.x+1]] ではなく、x[@0][@λx.x+1] が代入されるようになっている。その結果、上の例の 4 行目は
let y = x[@0][@λx.x+1]となることになる。後でステップ実行が 4 行目に差し掛かると、この x は fun x -> x + 1 と解釈される。
このとき、x のもともとの定義を見ると、2 行目では f と書いてあるので、4 行目の実行では 1 ステップで x を fun x -> x + 1 と解釈するのではなく、一度、x を f と解釈してから、2 ステップ目で fun x ->x + 1 と解釈した方がわかりやすいかも知れない。これは実行規則を(let x = p.g[@n][@λz. e]) :: s
; {let x = p.g[@n][@λz. e]} :: s[x[@0][@ p.g[@n][@λz. e] ]/x]とすることに相当する。しかし、このようにすると、上の例で 4 行目の x が f になった時点で、この f は
3 行目の f とみなされ、プログラムとしては正しくなくなってしまう。そのため、定式化では途中で f を表示することなく 1 ステップで値に変換する規則となっている。
一方で、一時的に変数が capture されてしまったとしても、[@v] の部分には正しい式が書かれているので、その後のステップ実行は正しく進む。そのため、実装上は 2 ステップに分かれる形にすることも考えられる。
下から 3 つ目は let rec 文の実行規則を表す。再帰関数 let rec f = λx. e が実行されたときも、let 文と同様にして、以降に現れる f にレベルと値を付与する。この時、付与する形を let rec f = λx. e in f とする。
下から２つ目はモジュール構文の実行規則を表す。ここではモジュールの展開を行っており、詳しくは
7 節で説明する。
最後は、例外を含む型宣言の実行規則を表す。型宣言によりコンストラクタが定義されると、ストラク
チャの中にあるコンストラクタにレベルをつけにいく。実際のレベル設定の規則は 6 節にて説明する。

5

変数の代入規則5.1

変数の代入規則

ストラクチャに対する変数の代入規則を図 4 に示す。まず空のストラクチャは空のストラクチャが返される。次に、代入を行う変数 x と同じ名前の変数の定義が出てきたとき、let 文の場合は後の let 文の中

6

[][v/x]((let x = e) :: s)[v/x]((let y = e) :: s)[v/x]((let rec x = λz. e) :: s)[v/x]((let rec f = λz. e) :: s)[v/x]((module X = struct s′ end) :: s)[v/x]=[]=(let x = e[v/x]) :: s=(let y = e[v/x]) :: s[v/x] (y ̸= x)=(let rec x = λz. e ) :: s=(let rec f = (λz. e)[v/x]) :: s[v/x] (f =
̸ x)′
= (module X = struct s [drop(v)/x] end) :: s[v/x]((exception C) :: s)[v/x] =(exception C) :: s[v/x]図 4. 変数の代入規則（ストラクチャ）

身にのみ代入規則を適用する。そして、let rec 文の場合は、let rec 文の中に出てくる x が let rec で定義された x であるため、let rec 文にも後のストラクチャにも代入規則は適用しない。例えば、以下のようなプログラムがあった時、

let x = 3
let a = x
let x = 5
let b = x
まず最初に let x = 3 が実行され、[3/x] の代入を後のストラクチャに行う。この時、let a = x の x はその上で定義された x を指しているため、3 が代入されるのは正しいが、let b = x には 3 行目の let x= 5 で定義されている 5 が代入されるため、3 が代入されてしまうと 3 行目を実行したときに、4 行目へ代入することができない。そのため、同じ変数名の定義があった場合はそれ以降代入規則を適用しない。
モジュールに対する変数の代入規則は 5.2 節で説明する。最後に例外を含む型宣言の場合は、後のストラクチャに対して代入規則を適用する。
式、値、変数に対する変数の代入規則は付録に示す。ここでは普通の代入を行っている。

5.2

コンストラクタの持ち下げ関数

モジュールに対して変数代入を行う時、レベルを下げることで、モジュールの内側に入ったことを表す
ため、コンストラクタの持ち下げ関数 drop を定義する。定式化は付録に示す。drop 関数はレベルを全て[@n] から [@(n + 1)] にする。例えば、以下のプログラムが入力されるとtype t = C
let x = C
module X = struct
let y = xtype t = C
let z = C
let w = z
end
まずは実行規則より、変数 x の値の C にレベル 0 が付与される。

type t = C
let x = C[@0]module X = struct
let y = xtype t = C
let z = C
let w = z7

[][C[@n]/C]((let x = e) :: s)[C[@n]/C]((let rec f = λx. e) :: s)[C[@n]/C]((module X = struct s′ end) :: s)[C[@n]/C]((exception C) :: s)[C[@n]/C]((exception C ′ ) :: s)[C[@n]/C]

=
=
=
=
=
=

[]
(let x = e[C[@n]/C]) :: s[C[@n]/C](let rec f = λx. e[C[@n]/C]) :: s[C[@n]/C](module X = struct s′ [C[@(n + 1)]/C] end) :: s[C[@n]/C](exception C) :: s(exception C ′ ) :: s[C[@n]/C](C ′ ̸= C)

図 5. コンストラクタのレベル設定規則（ストラクチャ）

end
そして、let x = C[@0] が実行されると実行規則より、後のストラクチャに [x[@0][@C[@0]]/x] の代入を行う。このとき、モジュール X の中に入るときに [drop(x[@0][@C[@0]])/x] となり、モジュール X の中身には [x[@1][@C[@1]]/x] を適用する。そのため、以下のようにモジュール X の中の値 x には [@1][@C[@1]]が付与される。

type t = C
let x = C[@0]module X = struct
let y = x[@1][@C[@1]]type t = C
let z = C
let w = z
end
その後、モジュール X の中が実行され、変数 z の値 C にレベル 0 が付与され、let z = C[@0] が実行されると変数 w の値 z に [@0][@C[@0]] が付与される。

type t = C
let x = C[@0]module X = struct
let y = x[@1][@C[@1]]type t = C
let z = C[@0]let w = z[@0][@C[@0]]end
すると、モジュール X の外側で定義された x やその x に代入される C には [@1] がつき、モジュール X の中で定義された z や w、C、z に代入される C には [@0] がついている。このようにレベルを用いてモジュールの外で定義されたものか、中で定義されたものかを判別している。その後、実行規則より、モジュール
X の中のストラクチャを後のストラクチャに代入しにいくこととなる。モジュールの代入規則については
7 節にて説明する。

6

コンストラクタのレベル設定規則

ストラクチャと値に対するコンストラクタのレベル設定規則を図 5 と図 6 に示す。式に対するコンスト
ラクタのレベル設定規則は付録に示す。まず、この代入が行われるのは 4 節での実行規則より、例外を含
む型宣言が実行されたときである。
図 5 のストラクチャに対するコンストラクタのレベル設定規則では基本的にストラクチャアイテムの中や後のストラクチャにレベル設定規則を適用しているが、モジュールの内側のストラクチャに対してはレ8

c[C[@n]/C] = c(C)[C[@n]/C] = C[@n](p.C ′ )[C[@n]/C](p.C ′ [@m])[C[@n]/C](p.x)[C[@n]/C](λx. e)[C[@n]/C](let rec f = λx. e in f )[C[@n]/C](p.g[@m][@λz. e])[C[@n]/C](p.g[@m][@let rec f = λx. e in f ])[C[@n]/C]

=
=
=
=
=
=
=

p.C ′
(p.C ′ ̸= C)
p.C ′ [@m](p.C ′ ≠ C)p.x
λx. e[C[@n]/C]
let rec f = λx. e[C[@n]/C] in f
p.x[@m][@λz. e]
p.g[@m][@let rec f = λx. e in f ]図 6. コンストラクタのレベル設定規則（値）ベルを持ち下げて設定し、同じ名前のコンストラクタを宣言した場合は、後のプログラムには規則を適用しない。例えば以下のプログラムがあったとき、

type t = C
let a = C
module X = struct
let b = Ctype t = C
let c = C
end
まず、実行規則より、1 行目の型宣言の情報を以降のストラクチャに代入しにいく。コンストラクタのレベ
ル設定規則である [C[@0]/C] を適用し、let a = C の C に [@0] が付与される。その後、モジュール X の中に入ると図 5 より、[C[@1]/C] を適用する。よって、let b = C の C に [@1] が付与される。

type t = C
let a = C[@0]module X = struct
let b = C[@1]type t = C
let c = Cend
ここで、モジュール X の中で同じコンストラクタ名 C の型宣言が行われる。そのため、図 5 より、それ以降のモジュール X 内のストラクチャに [C[@1]/C] は適用しない。そうすることで、let c = C の C には情報が付与されずに、モジュール X 内の型宣言の情報が付与されることで、type t = C
let a = C[@0]module X = struct
let b = C[@1]type t = C
let c = C[@0]endとなり、モジュール X の外で定義されたコンストラクタを使っている C[@1] とモジュール X の中で定義されたコンストラクタを使っている C[@0] とを区別することができる。

9

lift(p, [])lift(p, {let x = e} :: r)lift(p, {let rec x = λz. e} :: r)lift(p, {module Y = struct r′ end} :: r)

=
=
=
=

[]
{let x = lift(p, e)} :: lift(p, r){let rec x = λz. lift(p, e)} :: lift(p, r){module Y = struct lift(p.Y , r ′ ) end} :: lift(p, r)lift(p, {exception C} :: r)= {exception C} :: lift(p, r)

図 7. コンストラクタの持ち上げ関数 lift(p, r)（ストラクチャ）

lift(p, c)lift(p, p′ .C[@n])lift(p, p′ .x)lift(p, λx. e)lift(p, let rec f = λx. e in f )lift(p, p′ .g[@n][@λz. e])lift(p, p′ .g[@n][@let rec f = λx. e in f ])

=
=
=
=
=
=
=

c
lift(p, p′ .C[@n])p′ .x
λx. lift(p, e)
let rec f = λx. lift(p, e) in flift(p, p′ .g[@n])[@λz. lift(p, e)]lift(p, p′ .g[@n])[@let rec f = λx. lift(p, e) in f ]図 8. コンストラクタの持ち上げ関数 lift(p, v)（値）

7

モジュールの代入規則

7.1

コンストラクタの持ち上げ関数

この節では、モジュールの代入規則について説明する。まず、モジュールの代入を表す [r/X]m は 4 節の図 3 の下から 2 つ目の規則で行われる。これは「レベルが m だけ上で定義されたモジュール X の中身である r を代入する」という意味である。そして実行規則では、モジュールの中身をトップレベル（モジュール宣言に囲まれていない部分）で使えるようにするため、コンストラクタの持ち上げ関数 lift が適用されている。ストラクチャ、値、レベル付き変数、コンストラクタそれぞれに対する lift 関数を図 7、図 8、図 9、図 10 に示す。式に対する lift 関数は付録に示す。lift(p, r) は、基本的には r 中のレベルを −1 するが、元々レベルが 0 の場合は頭にモジュール名 p. をつけるという関数である。また、図 8 の 2 行目の右辺と左辺が等しく見えるが、左辺の第二引数である p′ .C[@n] の処理を、図 10 に示したコンストラクタに関する lift 関
数に渡したことを右辺では表している。
例えば以下のプログラムのとき、

type t = C
let a = C
module X = structtype t = C
let b = C
module Z = structtype t = C
let c = C
let x = (a, b, c)
end
end
まず、実行規則とコンスラクタのレベル設定規則、変数の代入規則より、

type t = C
let a = C[@0]module X = struct10

lift(p, p′ .x[@0])= p.p′ .x[@0]lift(ϵ, p′ .x[@n])= p′ .x[@n]lift(p.X, p′ .x[@n]) = lift(p, p′ .x[@(n − 1)])
図 9. コンストラクタの持ち上げ関数 lift(p, x)（レベル付き変数）

lift(p, p′ .C[@0])= p.p′ .C[@0]lift(ϵ, p′ .C[@n])= p′ .C[@n]lift(p.X, p′ .x[@n]) = lift(p, p′ .x[@(n − 1)])
図 10. コンストラクタの持ち上げ関数 lift(p, C)（コンストラクタ）

type t = C
let b = C[@0]module Z = structtype t = C
let c = C[@0]let x = (a[@2][@C[@2]], b[@1][@C[@1]], c[@0][@C[@0]])end
endとなり、次に、モジュール X の情報を付与するため、実行規則より、以降のストラクチャに対して[lift(X, r)/X]m という代入が行われる。（この代入については次の節で説明する。）よって、r はまず、letb = C[@0] が持ち上げられ、type t = C
let b = X.C[@0]module Y = structtype t = C
let c = C[@0]let x = (a[@2][@C[@2]], b[@1][@C[@1]], c[@0][@C[@0]])endとなる。その後モジュール Y の中に入るため、図 7 の 4 行目より、モジュール Y の中身には lift(X.Y , r ′ ) を行う。よって、

type t = C
let b = X.C[@0]module Y = structtype t = C
let c = X.Y.C[@0]let x = (a[@0][@C[@0]], X.b[@0][@X.C[@0]], X.Y.c[@0][@X.Y.C[@0]])end
が後のストラクチャに代入される、[r/X]m の r となる。全体として、全ての変数やコンストラクタが、トッ
プレベルから参照される形になっていることがわかる。

7.2

モジュールの代入規則

次にモジュールの代入規則を説明する。ストラクチャ、変数、コンストラクタに対するモジュールの代
入規則を図 11、図 12、図 13 に示す。式と値に対するモジュールの代入規則は付録に示す。

11

[][r/X]m =((let x = e) :: s)[r/X]m =((let rec f = λx. e) :: s)[r/X]m =[](let x = e[r/X]m ) :: s[r/X]m(let rec f = λx. e[r/X]m ) :: s[r/X]m((module X = struct s′ end) :: s)[r/X]m = (module X = struct s′ [drop(r)/X](m+1) end) :: s((module Y = struct s′ end) :: s)[r/X]m =((exception C) :: s)[r/X]m

(module Y = struct s′ [drop(r)/X](m+1) end) :: s[r/X]m
(Y ̸= X)
(exception C) :: s[r/X]m=

図 11. モジュールの代入規則（ストラクチャ）

x[r/X]m = x
X.X1 . · · · .Xn .x[r/X]m = X.X1 . · · · .Xn .x[@m][@get(r, X1 . · · · .Xn .x)]
Y.X1 . · · · .Xn .x[r/X]m = Y.X1 . · · · .Xn .x(Y ̸= X)図 12. モジュールの代入規則（変数）

まず図 11 のストラクチャに関する代入規則では、基本的に、先頭のストラクチャアイテムの中とその後のストラクチャに代入規則を適用していくが、代入するモジュール名と同じモジュール名のモジュール
宣言が合った場合、その後には代入規則を適用しない。また、代入規則を適用する先がモジュール宣言だった際、その中に代入規則を適用するが、このとき、代入する r のレベルの持ち下げと、添字の m が +1 される。代入する r のレベルの持ち下げを行うのは、7.1 節で説明したように r の中の変数やコンストラクタ
はトップレベルから参照される形になっているためである。モジュール内に入る場合は、ひとつ上のレベ
ルで有効な変数、コンストラクタを参照することになるため、レベルをひとつ上げている。また、添字 m
を +1 しているのは、モジュールの中に入ったため、X が定義されているレベルがひとつ上になったからである。
図 12 の変数に対するモジュール代入規則では、モジュール X の中身 r の中に対応する変数があった場
合、代入される値を求め付与する。このとき、モジュール中の変数を探索する関数 get を用いる。図 14 に
get 関数を示す。get 関数は第一引数の中で、第二引数の x または f に対応する値を探索し、見つからなければ unbound variable となる関数である1 。3 行目の let rec 文の場合は、値を返すため、let f = λx. e in fとなることに注意する。このとき、get 関数は、トップレベルで参照可能な形の値を返す。そのため、図 12の 2 行目では変数に（いくつのモジュール宣言の下に入ったかを示す）レベル m を付与している。
図 13 のコンストラクタに対するモジュールの代入規則では、3 行目で、代入するモジュールのモジュール名が頭についているコンストラクタに添字 m を付与している。また、4 行目は代入するモジュール名が頭についているコンストラクタに既にレベルが付与されているという状況だが、仮に同じ名前のモジュールが定義されており、モジュールの代入が起きたとしても、同じ名前のモジュール宣言があるとそれ以降のストラクチャには代入を行わないため、使用されることはない規則である。
例えば、以下のプログラムについて考える。

module X = structtype t = A
let a = A
end
let g = X.A
let h = X.a
module Y = struct1
OCaml ステッパは、エラーのないプログラム（OCaml インタプリタで型チェックまで通ったプログラム）に対して使われるので、unbound variable がここで起こることは実際にはない。

12

C[r/X]m = C(C[@n])[r/X]m = C[@n](X.X1 . · · · .Xn .C)[r/X]m = X.X1 . · · · .Xn .C[@m](X.X1 . · · · .Xn.C[@n′ ])[r/X]m=

X.X1 . · · · .Xn.C[@n′ ](Y.X1 . · · · .Xn= Y.X1 . · · · .Xn .C′
m(Y.X1 . · · · .Xn .C[@n ])[r/X]= Y.X1 . · · · .Xn .C[@n′ ].C)[r/X]m(conﬁrm X1 . · · · .Xn .C is deﬁned in X)(conﬁrm X1 . · · · .Xn .C is deﬁned in X)(使用されることはない)(Y ̸= X)(Y ̸= X)

図 13. モジュールの代入規則（コンストラクタ）

get({let x = p.y[@n][@v]} :: r, x)get({let x = v} :: r, x)get({let rec f = λx. e} :: r, f )get( :: r, x)get([], x)

=
=
=
=
=

v
v
let rec f = λx. e in fget(r, x)“unbound variable”

get({module X = struct r′ end} :: r, X.p.x) = get(r′ , p.x)get( :: r, X.p.x) = get(r, X.p.x)
get([], X.p.x) = “unbound variable”
図 14. モジュール中の変数を探索する関数 get(r, p.x)

let f = X.A
let i = X.a
end
let g = Y.f
まず、モジュール X の中の型宣言の情報が 3 行目の A に [@0] として付与される。

module X = structtype t = A
let a = A[@0]end
let g = X.A
let h = X.a
module Y = struct
let f = X.A
let i = X.a
end
let g = Y.f
その後モジュール X の情報が以降のストラクチャに代入される。すると、モジュールの代入規則 [r/X]mのrはtype t = A
let a = X.A[@0]であり、m は 0 となる。まず、let g = X.A を見ると、モジュール名 X が頭についたコンストラクタが値となっているため、コンストラクタに対するモジュールの代入規則より、let g = X.A[@0] となる。次に、let h = X.a は変数に対するモジュールの代入規則より、let h = X.a[@0][@get(r, a)] となる。
get(r, a) は get 関数の定義より、X.A[@0] となる。よって、

13

module X = structtype t = A
let a = A[@0]end
let g = X.A[@0]let h = X.a[@0][@X.A[@0]]module Y = struct
let f = X.A
let i = X.a
end
let g = Y.fとなる。X.a の値が正しく X.A となっていることがわかる。次に、モジュール Y の中に入るため、代入規
則 [r/X]m の r はtype t = A
let a = X.A[@1]であり、m は 1 となる。モジュール Y の中を見ていくと、まず、let f = X.A には添字の 1 が付与されるため、let f = X.A[@1] となる。そして、let i = X.a は変数に対するモジュールの代入規則より、leti = X.a[@1][@X.A[@1]] となる。よって、module X = structtype t = A
let a = A[@0]end
let g = X.A[@0]let h = X.a[@0][@X.A[@0]]module Y = struct
let f = X.A[@1]
let i = X.a[@1][@X.A[@1]]end
let g = Y.fとなる。f の値はひとつ上のレベル（[@1]）で定義された X.A で、i はひとつ上のレベルで定義された変数 X.a であり、その値はひとつ上で定義された X.A となっている。いずれも正しくレベルとモジュールパスが付与されていることがわかる。その後モジュール Y の情報を付与するため、モジュール Y の中身が lift
関数にかけられる。すると、モジュール Y の中で定義している f の値が、X.A[@0] となり、それが let g= Y.f に代入され、以下のようになる。

module X = structtype t = A
let a = A[@0]end
let g = X.A[@0]let h = X.a[@0][@X.A[@0]]module Y = struct
let f = X.A[@1]
let i = X.a[@1][@X.A[@1]]end
let g = Y.f[@0][@X.A[@0]]
14

8

実装

7 節までの定式化を元に OCaml ステッパの実装を行った。定式化では最低限の言語構文を扱ったが、実際には if 文や、型定義、match 文、引数付きの例外など初学者が扱いそうな構文についてサポートしている。例えば、ダイクストラ法を使った最短路問題で、内部で木のモジュールを定義して使うようなプログラムに対してもステップ実行ができている。
また、emacs インターフェースがあり、1 節で示したように簡約される場所に色がついた形で使うことができる。他にも、関数呼び出しをスキップする機能や、次のストラクチャアイテムに飛ぶ機能、戻る機能なども実装している。（次期の授業で使用予定。）

9

関連研究

ステッパはもともと Racket に対して作られた。これは Clements ら [3] が設計したもので、スタックに
continuation mark と呼ばれる印をつけることで現在の評価文脈を再構成できるようにしている。しかし、例外処置などの構文には対応していない。
それに対して Cong と Asai [4] は、コンテキストの記録およびそこから再構成したプログラムの出力を限定継続のオペレータ shift/reset を用いて行い、ステッパを実装した。そして、Furukawa ら [2] は shift/reset
を用いて行っていた操作をダイナミックバインディングにて実装した。本研究ではダイナミックバインディ
ングから明示的に引数として渡すように変更した。
Whitington と Ridge [5] は small-step のインタプリタを直接書くことで OCaml に対するステッパを実装した。それに対して本研究のステッパは big-step のインタプリタに手を加える形で作られている。
Schäfer ら [6] は、Jave のネストしたクラス宣言がある状態で、変数名を付け替えるリファクタリング
ツールを提案している。正しく変数名を付け替えるためには、その変数の宣言された場所を特定する必要があり、本論文で行ったような参照関係の解決を行っている。しかし、本論文で必要となったモジュールの上がり下がりのようなことは起きていない。

10

まとめと今後の課題

本研究では OCaml ステッパの定式化を行うことで、処理を明確にしたと同時に先行研究では不十分であったモジュールの上がり下がりに対応するレベルを導入し、実装を行った。今後はモジュール構文を用いた際の表示改善や、さらに複雑なテストケースを用意することでステッパをさらに改良していきたいと考えている。また、大学の授業で学生に OCaml ステッパを使ってもらい、その実行ログやアンケート結果からステッパの教育的効果についても調査していきたい。同時に実行した結果がステッパを通さずに得られた結果と一致することを証明するためにモジュールが入った言語のセマンティクスを定義したいと考
えている。

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

参考文献[1] Richard Stallman, Roland Pesch, Stan Shebs, et al.
51:02110–1301, 2002.

15

Debugging with gdb.

Free Software Foundation,

[2] Tsukino Furukawa, Youyou Cong, and Kenichi Asai. Stepping OCaml. In Proceedings Seventh International
Workshop on Trends in Functional Programming in Education, Chalmers University, Gothenburg, Sweden,
14th June 2018,, Vol. 295 of Electronic Proceedings in Theoretical Computer Science, p. 17–34, 2019.
[3] John Clements, Matthew Flatt, and Matthias Felleisen. Modeling an algebraic stepper. In European symposium
on programming, pp. 320–334, Springer, 2001.
[4] Youyou Cong and Kenichi Asai. Implementing a stepper using delimited continuations. 7th International
Symposium on Symbolic Computation in Software Science, Vol. 39, pp. 42–54, 2016.
[5] John Whitington and Tom Ridge. Direct interpretation of functional programs for debugging. In Sam Lindleyand Gabriel Scherer, editors, Proceedings ML Family / OCaml Users and Developers workshops, Oxford, UK,
Vol. 294 of Electronic Proceedings in Theoretical Computer Science, pp. 41–73, 2019.
[6] Schäfer M, Ekman T, and De Moor O. Sound and extensible renaming for Java. In Proceedings of the 23rd
ACM SIGPLAN conference on Object-oriented programming systems languages and applications, pp. 277–294,
2008.

16

付録 A
定式化結果の中に左辺と右辺が等しく見えるものが存在するが、式に関する規則では左辺の式を値に関する規則に渡したことを右辺は表す。値に関する規則では左辺の値を変数またはコンストラクタに関する規則に渡したことを右辺は表す。
パス値式

p ::= ϵ | X.p
v ::= c | p.C | p.x | λx. e | let rec f = λx. e in f |p.C[@n] | p.x[@n][@λx. e] | p.f [@n][@let rec f = λx. e in f ]e ::= v | e0 e1 | let x = e in e | let rec f = λx. e in e | try e with p.C → e |raise e | p.x[@n][@c] | p.x[@n′ ][@p.C[@n]] | try e with p.C[@n] → e
F ::= 2 | e F | F v | let x = F in e | raise F
E ::= F | E[try F with p.C[@n] → e]j ::= {let x = v} | {let rec f = λx. e} | {module X = struct r end} |{exception C}
i ::= let x = e | let rec f = λx. e | module X = struct s end | exception C
r ::= [ ] | j :: rs ::= [ ] | i :: s | j :: spure な評価文脈
評価文脈
評価済みストラクチャ
アイテム
ストラクチャアイテム
評価済みストラクチャ
ストラクチャ
ストラクチャのS ::= 2 | j :: S | (module X = struct S end) :: s
評価文脈
図 A.1. 対象言語の定義(λx. e) v(let rec f = λx. e in f ) v
let x = v in e
let rec f = λx. e1 in e2

→
→
→
→

e[v/x]
e[v/x, let rec f = λx. e in f /f ]e[v/x]
e2 [let rec f = λx. e1 in f /f ]try v with p.C[@n] → etry F [raise p.C[@n]] with p′ .C ′ [@n′ ] → e
try raise p.C[@n] with p.C[@n] → e
try raise p.C[@n] with p′ .C ′ [@n′ ] → e

→
→
→
→

v
try raise p.C[@n] with p′ .C ′ [@n′ ] → eeraise p.C[@n](p.C[@n] ̸= p′ .C ′ [@n′ ])p.x[@n][@c] →→p.g[@m][@(λx. e)] v →′(p .g[@m][@let rec f = λx. e in f ]) v →cp′ .C[@n]e[v/x]
e[v/x, p′ .g[@m][@let rec f = λx. e in f ]/f ]p.x[@n′ ][@p′ .C[@n]]e1 → e2E[e1 ] → E[e2 ]図 A.2. 簡約規則

17(e2 ̸= f )e1 → e2(let x = e1 ) :: s ; (let x = e2 ) :: ss1 ; s2
S[s1 ] ; S[s2 ](let x = c):: s
; {let x = c}:: s[x[@0][@c]/x](let x = λz. e):: s; {let x = λz. e}:: s[x[@0][@λz. e]/x](let x = let rec f = λz. e in f ):: s; {let x = let rec f = λz. e in f }:: s[x[@0][@let rec f = λz. e in f ]/x](let x = p.C[@n]):: s; {let x = p.C[@n]}:: s[x[@0][@p.C[@n]]/x](let x = p.g[@n][@λz. e]):: s; {let x = p.g[@n][@λz. e]}:: s[x[@0][@λz. e]/x]′(let x = p .g[@n][@let rec f = λz. e in f ]) :: s
; {let x = p′ .g[@n][@let rec f = λz. e in f ]} :: s[x[@0][@let rec f = λz. e in f ]/x](let rec f = λx. e):: s; {let rec f = λx. e}:: s[f [@0][@let rec f = λx. e in f ]/f ](module X = struct r end):: s
; {module X = struct r end}:: s[lift(X, r)/X]0(exception C):: s; {exception C}:: s[C[@0]/C]
図 A.3. 実行規則[][v/x]((let x = e) :: s)[v/x]((let y = e) :: s)[v/x]((let rec x = λz. e) :: s)[v/x]((let rec f = λz. e) :: s)[v/x]((module X = struct s′ end) :: s)[v/x]=[]=(let x = e[v/x]) :: s=(let y = e[v/x]) :: s[v/x] (y ̸= x)=(let rec x = λz. e ) :: s=(let rec f = (λz. e)[v/x]) :: s[v/x] (f =
̸ x)′
= (module X = struct s [drop(v)/x] end) :: s[v/x]((exception C) :: s)[v/x] =(exception C) :: s[v/x]図 A.4. 変数の代入規則（ストラクチャ）

v ′ [v/x](e0 e1 )[v/x](let x = e1 in e2 )[v/x](let y = e1 in e2 )[v/x](let rec x = λz. e1 in e2 )[v/x](let rec f = λz. e1 in e2 )[v/x](try e1 with p.C → e2 )[v/x](raise e)[v/x](p.y[@n][@c])[v/x](p.y[@n][@p′ .C[@m]])[v/x](try e1 with p.C[@m] → e2 )[v/x]

=
=
=
=
=
=
=
=
=
=
=

v ′ [v/x]
e0 [v/x] e1 [v/x]
let x = e1 [v/x] in e2
let y = e1 [v/x] in e2 [v/x](y ̸= x)let rec x = λz. e1 in e2
let rec f = (λz. e1 )[v/x] in e2 [v/x]
(x =
̸ f)
try e1 [v/x] with p.C → e2 [v/x]raise e[v/x]
p.y[@n][@c]p.y[@n][@p′ .C[@m]]try e1 [v/x] with p.C[@m] → e2 [v/x]図 A.5. 変数の代入規則（式）18c[v/x](p.C)[v/x](p.y)[v/x](λx. e)[v/x](λy. e)[v/x](let rec x = λz. e in x)[v/x](let rec f = λz. e in f )[v/x](p.C[@n])[v/x](p.g[@n][@λz. e])[v/x](p.g[@n][@let rec f = λx. e in f ])[v/x]

=
=
=
=
=
=
=
=
=
=

c
p.C
(p.y)[v/x]λx. e
λy. e[v/x](y ̸= x)let rec x = λz. e in x
let rec f = (λz. e)[v/x] in f
(f =
̸ x)
p.C[@n]p.g[@n][@λz. e]
p.g[@n][@let rec f = λx. e in f ]図 A.6. 変数の代入規則（値）x[v/x] = vy[v/x] = y(y ̸= x)X.X1 . · · · .Xn .y[v/x] = X.X1 . · · · .Xn .y
図 A.7. 変数の代入規則（変数）

drop([])drop((let x = e) :: s)drop((let rec x = λz. e) :: s)drop((module X = struct s′ end) :: s)drop((exception C) :: s)

=
=
=
=
=

[]
(let x = drop(e)) :: drop(s)(let rec x = λz. drop(e)) :: drop(s)(module X = struct drop(s′ ) end) :: drop(s)(exception C) :: drop(s)図 A.8. コンストラクタの持ち下げ drop(s)（ストラクチャ）

drop(v)drop(e0 e1 )drop(let x = e1 in e2 )drop(let rec f = λx. e1 in e2 )drop(try e1 with p.C → e2 )

=
=
=
=
=

drop(raise e)drop(p.x[@n][@c])drop(v)drop(e0 ) drop(e1 )let x = drop(e1 ) in drop(e2 )let rec f = λx. drop(e1 ) in drop(e2 )try drop(e1 ) with p.C → drop(e2 )(使用されることはない)= raise (drop(e))= p.x[@(n + 1)] [@c]drop(p.x[@n′ ][@p.C[@n]])=p.x[@(n′ + 1)] [@drop(p.C[@n])]drop(try e1 with p.C[@n] → e2 ) = try drop(e1 ) with p.C[@(n + 1)] → drop(e2 )図 A.9. コンストラクタの持ち下げ drop(e)（式）

19

drop(c)drop(p.C)drop(p.x)drop(λx. e)drop(let rec f = λx. e in f )drop(p.C[@n])

= c
= p.C
(使用されることはない)= p.x= λx. drop(e)= let rec f = λx. drop(e) in f
= p.C[@(n + 1)]

drop(p.x[@n][@λz. e])=drop(p.g[@n][@let rec f = λx. e in f ]) =p.x[@(n + 1)] [@λz. drop(e)]p.g[@(n + 1)] [@let rec f = λx. drop(e) in f ]図 A.10. コンストラクタの持ち下げ drop(v)（値）[][r/X]m =((let x = e) :: s)[r/X]m =((let rec f = λx. e) :: s)[r/X]m =[](let x = e[r/X]m ) :: s[r/X]m(let rec f = λx. e[r/X]m ) :: s[r/X]m((module X = struct s′ end) :: s)[r/X]m = (module X = struct s′ [drop(r)/X](m+1) end) :: s((module Y = struct s′ end) :: s)[r/X]m =((exception C) :: s)[r/X]m

(module Y = struct s′ [drop(r)/X](m+1) end) :: s[r/X]m
(Y ̸= X)
(exception C) :: s[r/X]m=

図 A.11. モジュールの代入規則（ストラクチャ）v[r/X]m(e0 e1 )[r/X]m(let x = e1 in e2 )[r/X]m(let rec f = λx. e1 in e2 )[r/X]m(try e1 with p.C → e2 )[r/X]m(try e1 with p.C[@n] → e2 )[r/X]m(raise e)[r/X]m(p.x[@n][@c])[r/X]m(p.x[@n][@p′ .C[@n′ ]])[r/X]m

=
=
=
=
=
=
=
=
=

v[r/X]me0 [r/X]m e1 [r/X]m
let x = e1 [r/X]m in e2 [r/X]m
let rec f = λx. e1 [r/X]m in e2 [r/X]mtry e1 [r/X]m with (p.C)[r/X]m → e2 [r/X]mtry e1 [r/X]m with (p.C[@n])[r/X]m → e2 [r/X]mraise e[r/X]mp.x[@n][@c]p.x[@n][@p′ .C[@n′ ]]図 A.12. モジュールの代入規則（式）c[r/X]m(p.C)[r/X]m(p.x)[r/X]m(λx. e)[r/X]m(let rec f = λx. e in f )[r/X]m
(p.C[@n])[r/X]m(p.g[@n][@λz. e])[r/X]m(p.g[@n][@let rec f = λx. e in f ])[r/X]m

=
=
=
=
=
=
=
=

c
(p.C)[r/X]m(p.x)[r/X]m
λx. e[r/X]m
let rec f = λx. e[r/X]m in f
(p.C[@n])[r/X]mp.g[@n][@λz. e]
p.g[@n][@let rec f = λx. e in f ]図 A.13. モジュールの代入規則（値）20x[r/X]m = x
X.X1 . · · · .Xn .x[r/X]m = X.X1 . · · · .Xn .x[@m][@get(r, X1 . · · · .Xn .x)]
Y.X1 . · · · .Xn .x[r/X]m = Y.X1 . · · · .Xn .x(Y ̸= X)

図 A.14. モジュールの代入規則（変数）C[r/X]m = C(C[@n])[r/X]m = C[@n](X.X1 . · · · .Xn .C)[r/X]m = X.X1 . · · · .Xn .C[@m](X.X1 . · · · .Xn.C[@n′ ])[r/X]m

(Y.X1 . · · · .Xn(Y.X1 . · · · .Xn .C[@n′ ])[r/X]m.C)[r/X]m=

X.X1 . · · · .Xn.C[@n′ ](conﬁrm X1 . · · · .Xn .C is deﬁned in X)(conﬁrm X1 . · · · .Xn .C is deﬁned in X)(使用されることはない)= Y.X1 . · · · .Xn .C(Y ̸= X)′
= Y.X1 . · · · .Xn .C[@n ]
(Y =
̸ X)

図 A.15. モジュールの代入規則（コンストラクタ）

get({let x = p.y[@n][@v]} :: r, x)get({let x = v} :: r, x)get({let rec f = λx. e} :: r, f )get( :: r, x)get([], x)

=
=
=
=
=

v
v
let rec f = λx. e in fget(r, x)“unbound variable”

get({module X = struct r′ end} :: r, X.p.x) = get(r′ , p.x)get( :: r, X.p.x) = get(r, X.p.x)
get([], X.p.x) = “unbound variable”
図 A.16. モジュール中の変数の探索 get(r, p.x)

lift(p, [])lift(p, {let x = e} :: r)lift(p, {let rec x = λz. e} :: r)lift(p, {module Y = struct r′ end} :: r)

=
=
=
=

[]
{let x = lift(p, e)} :: lift(p, r){let rec x = λz. lift(p, e)} :: lift(p, r){module Y = struct lift(p.Y , r ′ ) end} :: lift(p, r)lift(p, {exception C} :: r)= {exception C} :: lift(p, r)

図 A.17. コンストラクタの持ち上げ lift(p, r) （ストラクチャ）

lift(p, v)
lift(p, (e0 e1 ))lift(p, (let x = e1 in e2 ))lift(p, (let rec f = λx. e1 in e2 ))lift(p, (try e1 with p′ .C → e2 ))

=
=
=
=
=

lift(p, v)
lift(p, e0 ) lift(p, e1 )let x = lift(p, e1 ) in lift(p, e2 )let rec f = λx. lift(p, e1 ) in lift(p, e2 )try (lift(p, e1 )) with p′ .C → lift(p, e2 )(使用されることはない)
lift(p, (raise e))= raise (lift(p, e))′lift(p, p .x[@n][@v])= lift(p, p′ .x[@n])[@lift(p, v)]
lift(p, (try e1 with p′ .C[@n] → e2 )) = try lift(p, e1 ) with lift(p, p′ .C[@n]) → lift(p, e2 )図 A.18. コンストラクタの持ち上げ lift(p, e)（式）

21

lift(p, p′ .x[@0])= p.p′ .x[@0]lift(ϵ, p′ .x[@n])= p′ .x[@n]lift(p.X, p′ .x[@n]) = lift(p, p′ .x[@(n − 1)])
図 A.19. コンストラクタの持ち上げ lift(p, x)（レベル付き変数用）

lift(p, p′ .C[@0])= p.p′ .C[@0]lift(ϵ, p′ .C[@n])= p′ .C[@n]lift(p.X, p′ .x[@n]) = lift(p, p′ .x[@(n − 1)])
図 A.20. コンストラクタの持ち上げ lift(p, C)（コンストラクタ用）

lift(p, c)lift(p, p′ .C[@n])lift(p, p′ .x)lift(p, λx. e)lift(p, let rec f = λx. e in f )lift(p, p′ .g[@n][@λz. e])lift(p, p′ .g[@n][@let rec f = λx. e in f ])

=
=
=
=
=
=
=

c
lift(p, p′ .C[@n])p′ .x
λx. lift(p, e)
let rec f = λx. lift(p, e) in flift(p, p′ .g[@n])[@λz. lift(p, e)]lift(p, p′ .g[@n])[@let rec f = λx. lift(p, e) in f ]図 A.21. コンストラクタの持ち上げ lift(p, v)（値）[][C[@n]/C]((let x = e) :: s)[C[@n]/C]((let rec f = λx. e) :: s)[C[@n]/C]((module X = struct s′ end) :: s)[C[@n]/C]((exception C) :: s)[C[@n]/C]((exception C ′ ) :: s)[C[@n]/C]

=
=
=
=
=
=

[]
(let x = e[C[@n]/C]) :: s[C[@n]/C](let rec f = λx. e[C[@n]/C]) :: s[C[@n]/C](module X = struct s′ [C[@(n + 1)]/C] end) :: s[C[@n]/C](exception C) :: s(exception C ′ ) :: s[C[@n]/C](C ′ ̸= C)

図 A.22. コンストラクタのレベル設定規則（ストラクチャ）v[C[@n]/C](e0 e1 )[C[@n]/C](let x = e1 in e2 )[C[@n]/C](let rec f = λx. e1 in e2 )[C[@n]/C](try e1 with p.C → e2 )[C[@n]/C](try e1 with p.C[@m] → e2 )[C[@n]/C](raise e)[C[@n]/C](p.x[@m][@c])[C[@n]/C](p.x[@m′ ][@p′ .C ′ [@m]])[C[@n]/C]

=
=
=
=
=
=
=
=
=

v[C[@n]/C]
e0 [C[@n]/C] e1 [C[@n]/C]
let x = e1 [C[@n]/C] in e2 [C[@n]/C]
let rec f = λx. e1 [C[@n]/C] in e2 [C[@n]/C]
try e1 [C[@n]/C] with p.C[C[@n]/C] → e2 [C[@n]/C]
try e1 [C[@n]/C] with (p.C[@m])[C[@n]/C] → e2 [C[@n]/C]
raise e[C[@n]/C]
p.x[@m][@c]p.x[@m′ ][@p′ .C ′ [@m]]図 A.23. コンストラクタのレベル設定規則（式）22c[C[@n]/C] = c(C)[C[@n]/C] = C[@n](p.C ′ )[C[@n]/C] ==(p.x)[C[@n]/C] =(λx. e)[C[@n]/C] =(let rec f = λx. e in f )[C[@n]/C] =(p.g[@m][@λz. e])[C[@n]/C] =(p.g[@m][@let rec f = λx. e in f ])[C[@n]/C] =(p.C ′ [@m])[C[@n]/C]

p.C ′(p.C ′ ̸= C)′
p.C [@m](p.C ′ ≠ C)p.x
λx. e[C[@n]/C]
let rec f = λx. e[C[@n]/C] in f
p.x[@m][@λz. e]
p.g[@m][@let rec f = λx. e in f ]図 A.24. コンストラクタのレベル設定規則（値）23