日本ソフトウェア科学会第 31 回大会 (2014 年度) 講演論文集

コード生成のための自然演繹
須藤 悠斗

オレッグ・キセリョーヴ

亀山 幸義

表現力の高いコード生成は，入出力や例外，オープンコードを格納できる参照セルなどのエフェクトを必要とする．しかし，これらのエフェクトを用いたコード生成は，束縛されない変数や意図せず束縛された変数を生じる恐れがある．
本研究の目的は，コード生成を行う前に，生成されたコードやコード片が，スコープ安全であることを静的に保証する事である．理論的には，我々は，生成されるコードの変数スコープを，コード生成器の型でどのように表すかに興味がある．このためには，コードが含む自由変数を意識した型システムにする必要があるが，型が直接自由変数の集合を含むとα変換で閉じていない，環境多相へ対応できない等の問題が生じる．本研究では，自由変数を完全に抽象化して表現する方法を提案し，自然演繹における固有変数条件に相当する条件を用いて型システムを構築することにより，この問題を解決した．

Side-effects such as IO, exceptions, or mutable cells storing open code are necessary for expressive code generation. Sideeffects also have the danger of producing code with unbound or unexpectedly bound variables. We aim to statically ensure
the well-scopedness of the generated code, even for code fragments, before actually generating the code. Theoretically, we
are interested in how to refrect the variable scope in the type of the generated code. Naively including free variable names
in code types, however, leads to problems with alpha-conversion, environment polymorphism, etc. To solve these problems
we propose a fully abstract representation of the variable environment, and design the type system based on Prawitz’ natural
deduction and its eigen-variable condition.

ング言語 (多段階計算言語，MSP 言語) の研究が行わ

1 はじめにれており，MetaML [1], MetaOCaml [2] [3], MetaHaskell

プログラムによるプログラムの生成 (プログラム生[4], Template Haskell [5], Scala LMS [6] などの言語が提成，コード生成) は，特定のパラメータ・ハードウェ案されている．多くの MSP 言語はコード生成器を簡ア・問題毎の性質に特化したプログラムを生成した

潔に書くための機構を備えており，安全性を静的に保後に，そのプログラムを実行するという手法であり，証することを目標としている．ここで安全性は，生成プログラムの保守性・再利用性の向上と，実行性能されたコードが，プログラムが構文的に正しい，型にの高さを両立させることができるという特徴を持っ関する矛盾がない，意図した変数束縛を行なう，といている．本稿では，このようにして生成されるプロう３つの性質を意味する．

グラムを，生成するプログラム (コード生成器，code

本研究は，計算エフェクトを持つ MSP 言語に対しgenerator) と区別してコード (code) と呼ぶことにする．て安全性を静的に保証する計算体系の構築に関する質の高いコード生成器を書くことを支援するためのものである．計算エフェクトは副作用ともよばれ，変プログラム言語，すなわちマルチステージプログラミ数への破壊的代入，制御，入出力などの効果を総称する．従来の MSP 言語に対する基礎理論は，計算エNatural Deduction for Code Generation
Yuto Sudo, Oleg Kiselyov, Yukiyoshi Kameyama, 筑波大学
コンピュータサイエンス専攻, Department of ComputerScience, University of Tsukuba.

フェクトを持たない部分体系に対する安全性のみを保証していたが，実行性能の高いコードを生成するためには，様々な計算エフェクトを用いる必要があるた

め，不十分であった．効率的なコード生成を行なうた

れる固有変数条件に着目し，この条件に似た形の規則めのテクニックとして，メモ化や let 挿入，ループのを導入することで，コードにおける変数のスコープを順番の交換，不変式のループ外への括り出しなどがよ限定し，これにより変数スコープを侵害する束縛が発く知られているが，これらは変数束縛のスコープを越生しないことを保証する．

えたコード移動を伴うため，計算エフェクトの利用が本論文の範囲では，計算エフェクトは局所的な破必須であり，従来研究ではその安全性が保証されていない．たとえば，旧版の MetaOCaml†1 では，以下の壊的代入 (OCaml の ref を局所的に使ったもの) に限

コード生成器:行を含めて 2 段階) に限定した範囲とする．この範囲

let r = ref .<0>. inの言語に対する型システムと操作的意味論を定義し，定し，また，コード生成のレベルも 1 段階 (コード実.<fun y -> .~(r := .<y>.; .<10>.)>.;型システムの健全性を証明することにより，上記の安! r全性が得られることを示す．

は型が整合するためコンパイルして実行できるが，これを実行すると.<y>. という，自由変数を持つコード2 対象とする体系が得られてしまうため，安全性を満たさない．ここで本節では，MSP 言語をモデル化した小さな計算体

は，ref キーワードで作成されたセルに対する破壊的系を導入する．この体系は，ラムダ計算に，コード生代入という計算エフェクトを MSP 言語で用いたため，成機構と ref による破壊的代入を加えたものであり，このような安全性が破られる例となっている．一部の安全性を議論するためには十分な構文を持つ．

先行研究では，計算エフェクトを用いた場合のこのよ

本体系は，コードの表現方法として，Scheme やうな問題について検討し，ある程度の解を得ている．

MetaML/MetaOCaml における Quasi quotation による

しかし，それらは，計算エフェクトがコードにおける方法ではなく，Code Combinator による方法を採用変数スコープを越えてはいけない，という厳しい制限

した [9]．これを Scheme の構文で説明すると，Quasiがある [7] か，あるいは，非常に複雑な型システムをquotation 方式では，必要とするもの [8] であり，種々の効率的コードを生成するためには，改善が必要である．
本論文では，この問題をなるべく一般的な形で，かつ，簡潔に解決することで，安全性を保ったまま効率的なプログラム生成を実現することを目的とする．

(let ((x ’(* 3 5)))‘(+ ,x 10))==> (+ (* 3 5) 10)となるが，Code combinator 方式では，(define (mk-+ a b)

ここで特に大事な点は，型システムの簡潔さであり，(list ’+ a b))

これは OCaml など非常に大きな仕様を持つ言語全体(let ((x ’(* 3 5)))に安全性を広げることを目標としているからである．

(mk-+ x ’10))安全性を保証する鍵となる静的型システムは，特に==> (+ (* 3 5) 10)

コードにおける変数のスコープを簡潔に表現する必となる．前者の方が，全体としてのプログラム量は要がある．このため，我々は，論理における自然演繹少ないが，後者は，+などの構成子だけを mk-+のよう体系における存在除去規則や任意導入規則で用いらな code combinator に変更すれば，そのままコード生成器になるという利点がある．Code Combinator 方式†1 最新の MetaOCaml である BER MetaOCaml は，コード生成器のチェックを厳しく行なうため，ここで掲げた例は型エラーとなり，実行できない．しかし BER
MetaOCaml においても，コード生成器がコンパイルに成功するのに，生成されたコードがコンパイルできない例を作ることができ，安全性の問題は完全には解消できていない．

では，quasi quotation や comma に相当するものはな
く，+ や関数適用，関数抽象などの項の構成子に対して，すべて， 「通常レベル」のものと「コードレベル」のものとの 2 つを用意する必要がある†2 ．
図 1 が今回用いる構文の定義である．

た，コード <e> も値である．
今回の体系では，計算エフェクト (副作用) として局所的な破壊的代入のみを導入している．let ref r = e1 in e2(var)

x

∈ Var

は，書き換え可能変数 r を e2 内で用いるための式で(cvar)γ∈ CVarある．e1 := e2 , ! e はそれぞれ対応する OCaml のもの(rvar)r∈ RVarと同じ意味を持つ．

(type)

t::= Int | Bool | t → t | <t>γ | t ref

図 2 は、構文の定義における定数 c を、その型と(rtype)

tr::= Int|Bool|<t>γともに具体的に列挙したものである。ここで，n は整(term)

e::= x | c | λ x. e | λ x. e | λ x. e | e1 e2 |数定数、b はブール型定数を表し、項の定義と同様、<e> | let ref r = e1 in e2 | r := e |コードレベルの定数は、通常レベルの定数の名前に下! r | if e1 then e2 else e3

線を引いたものとしている。たとえば、+ は、コード(value)v::= x | c | λ x. e | <e>レベルでの加算を表す。%は整数を整数のコードに変える単項演算子であり、cbool はブール値に対する同図1

構文の定義

変数は 3 種類あり、x は通常の変数、γ は型付け文様の演算子である。

c ::=n: Int

脈を表す変数 (後述)、r は局所的な参照を表す変数を|

b: Bool表す。

|(+): Int → (Int → Int)|(+)

: <Int → (Int → Int)>γ|(∗): Int → (Int → Int)|(∗)

: <Int → (Int → Int)>γ|fix: ((t1 → t2 ) → (t1 → t2 ))型 Int は整数型，t → t は関数型，t ref は参照型であり，これらは OCaml におけるそれぞれの型に対応する．<t>γ は，t 型のコードを表す型である．

tr は let ref r = x in e に関する型付けに用いる型であり，後に詳述する．
項 <e> は完成したコードを表す．Code Combinator→ (t1 → t2 )|fix方式であるので，quasi quotation や comma はないが，完成したコードを表現する記法が必要であるため，

MetaOCaml における <e> という表現を流用している．
MetaOCaml との違いは，<e> の中に Escape (Schemeの comma に相当) がないので，<e> はそのままで値に: <((t1 → t2 ) → (t1 → t2 ))→ (t1 → t2 )>γ|

makeapp: <t1 → t2 >γ → (<t1 >γ → <t2 >γ )|%: Int → <Int>γ|cbool: Bool → <Bool>γ

なる点である．たとえば，<1 + 2> はコードである．

図2定数項の構成子のうち，下線がついているものは，コードレベルの演算子である．たとえば，λ x. e は，e の計

次に、この計算体系に対する操作的意味論を定義

算結果がコード <e0 > であるとき，<λ x.e0 > というコーする。ここでは評価文脈に基づく定義を与える。図 3

ドを返す．λ x. e は λ x. e の，e の計算を行なっているは評価文脈の定義である。ここで [ ] は穴を表す。他

状態を表現する便宜上の記法である．の規則は値呼び計算体系における通常の評価文脈と

値 v は計算結果を表す．ここでは値呼びの評価順序同様であるが、λ x. E において、ラムダ抽象の内部にを想定しているため，変数 x も値にふくめている．ま評価文脈がはいりこんでいることに注意されたい。これは、λ x. e の形の項の計算では、e を評価することを†2 Scala LMS では，コードレベルの演算子を言語処理系が自動で用意してくれる．

意味している。
評価文脈 Er は、E 0 [let ref r = v in E 00 ] の形にならな図 5 は、この体系のプログラム例をその型ととも

E ::=[ ] | Ee | vE | let ref r = E in e | let ref r = v in E |r := E | if E then e1 else e2 | λ x. Eに示す．
ここで，+ は makeapp (makeapp (+) e1 ) e2 の糖衣構文であり，整数のコードを加算したコードを生成

図3する．

評価文脈

図 5 の 1 行目の例の 3+2 は通常の計算である。3い評価文脈、すなわち、参照変数 r に対する束縛で、行目の <%3+%2> は、3 と 2 が，それぞれ、% により穴をスコープに持つものがないような評価文脈をあ整数のコード <3>, <2> に簡約され，+ により、それららわす。の加算を表す <3+2> というコードが値として返る．そ次に、図 4 において操作的意味論を与える。の型は、整数のコードの型を表す <Int>γ である。

λ x. e はコードレベルのラムダ抽象である．通常のe → e0

ラムダ抽象では、引数に適用されるまで本体の評価はE[e] → E[e0 ]行なわれないが，λ x. e の本体 e は、(引数に適用され(λ x. e)v → e[v/x]if δ (c, v) is defined
c v → δ (c, v)る前に) 評価される。最後の例では、本体 %3+x は、その評価をはじめる前に、その中の変数 x がフレッ
シュな変数 y のコード <y> にリネームされて %3+<y>

if True then e1 else e2 → e1となり、評価される。その評価結果は、<3+y> であり、

if False then e1 else e2 → e2

λ x. e → λ y. e[<y>/x] (ただし y はフレッシュな変数)

その後ラムダ抽象が追加され，<λ y. 3+y> が計算結果となる。

λ x. <e> → <λ x. e>
let ref r = v in Er [!r] → let ref r = v in Er [v]let ref r = v1 in Er [r := v2 ] → let ref r = v2 in Er [v2 ]3 Scope Extrusion
ここでは、副作用を用いてコード生成を行なったと

let ref r = v1 in v2 → v2

きに起こる Scope Extrusion という問題について述べ
図4

る．Scope Extrusion とは，変数が意図した束縛から操作的意味論飛び出してしまうことである．本研究の目的である副
図 4 において δ は、定数がプリミティブ関数のと作用とコード生成機能のある体系での安全性を保証すきのふるまいを決める関数であり、δ (c, v) は c に引数るためには，この問題に的確に対処する必要がある．

v を与えたときの計算結果を表す。c が引数 v に対し下の項は、コードレベルのラムダ抽象 λ x. e と破壊て定義されていないときは、δ (c, v) は未定義である。

的変数を組み合わせることで Scope Extrusion が発生してしまう例である．

3+2,→ 5: Int(λ x. 3+x)2,→ 5: Int%3+%2,→ <3+2>: <Int>γ(λ x. %3),→ <λ x. 3>: <Int → Int>γ(λ x. %3+x),→ <λ x. 3+x>

: <Int → Int>γ(1)

ここで，let x = e1 in e2 は λ x. e2 e1 の糖衣構文である(本論文では、let 多相については考えない)。(1) の例
では，まず let 式によって r に書き換え可能な値 <0>をもつ参照が束縛される．次に，コードレベルのラム(let z = %3 in

λ x. z+x)

let r = ref %0 in let = λ x. r := x in ! r,→ <λ y. 3+y>: <Int → Int>γ

ダ抽象 λ x. e の本体 r := x が (x を束縛することなく)コードとなるまで簡約される．ここで書き換え可能

図5

プログラム例な変数 r に x が新たに割り当てられた後，コード x が返るため，λ x. r := x は <λ x. x> に簡約される．その後

! r により r を参照した値が返ることになる．問題は示する。

r に割り当てられた変数 x が未束縛だということであ(CAbs) 規則がこの型システムで最も重要なものでる．これにより r は未束縛の x という変数を参照し，ある。これを説明する前に、まず、型付けの文脈をあ結果として実行時エラーとなってしまう．これは，関らわす変数 γ について説明する。これは、通常の型数適用後にしか本体の簡約がなされない，通常のラムシステムにおける判断を Γ ` e : t と書くとすると、 Γ

ダ抽象では起こらなかった問題である．の部分を抽象的に表現した変数である。この論文の体系では、γ 等は常に変数であり、文脈をあらわす定4 自然演繹に基づく解数や構成子はない。Γ が x : t の形の変数宣言を含むよ

本研究では，自然演繹における固有変数条件を用うに、文脈変数 γ は、e : <t>γ の形で出現し、e が、γ

いて，前章で述べた Scope Extrusion の問題を解決すという型付けのもとで t 型のコード (を値として持つる．固有変数条件とは，述語論理の量化子に関する導式) を表していることを意味する。いいかえれば、e入と除去の規則に現れる変数が，満たさなければならの中で使ってよい、コードレベルの自由変数 (とその型) の集合を γ は表している。γ の上には半順序†3 がない条件のことである．
次のものは、自然演繹体系における存在の除去規則である．

[A[a/x]]
..
..
∃x.AB
B

定義されており、γ1 ≤ γ は γ1 が γ より「長い」文脈であること、つまり、γ で使える変数はすべて γ1 でも使えることを意味する。
これらの知識を前提にして、(CAbs) 規則を説明する。λ x. e の自由変数 x は，本体 e 中でコードとしてここで，a はこの規則の固有変数であり，「右側の B を扱われるため，自由変数はコード型を持つと仮定され導く証明における A[a/x] 以外の (まだ除去されていなている．それに加え，型付け文脈に関する包含関係がい) すべての仮定と B に自由に現れてはいけない」と仮定されている．これはどの文脈で新しい γ が導入いう固有変数条件を満たさなければならない．これにされたのかを表している．例えば，γ1 ≥ γ0 は γ0 中でより a が証明中の他のいかなる場所 (上記の B より下γ1 が導入されたことを表している．この包含関係はの部分も含む) にも出現しないことが保証される．

(Subsumption) 規則で用いられる．(CAbs) 規則の形式

副作用とコード生成を組み合わせた場合に発生す自体はきわめて自然なものであるが、その最も重要なる Scope Extrusion は，未束縛の変数が，あるべき範点は、γ1 がこの規則に対する固有変数となっているこ囲の外側に染み出してしまうという問題だった．そことである。すなわち、この規則の上にある x : <t1 >γ1 とで，コードレベルのラムダ抽象 λ x. e の x の型が，固γ1 ≤ γ という 2 つの仮定以外のすべての (まだ除去さ有変数条件を満たさなければならないという制約をれていない) 仮定に、γ1 は現れてはならない。また、加え，この問題を解決することとした．

この規則より下のあらゆる場所に γ1 は現れてはなら

図 6 がこの制約を考慮して設計した型システムでない。これは、自然演繹における「任意」の導入規則ある．(CAbs) 規則を見ると，固有変数 γ1 を導入して，と類似した制限であり、これにより Scope Extrusion

x 型に添えている．これにより λ x. e の変数スコープが起きないことを保証する (実例は後述)。の外に x の型が飛び出すことを排除した．
図 6 の型付け規則では通常の型システムで現れる型環境の代わりに仮定を置く．

(Abs) 規則は，自由変数の型判定を仮定としておい(Subsumption) 規則が表しているのは，文脈 γ 中でγ1 が導入されており，かつ e が文脈 γ で型付けできれば，γ1 でも型付けができるということである．これは γ1 より持っている情報が少ない γ で型が付くのでた上で，ラムダ抽象の本体の型 t2 を導く．また，仮定はラムダ抽象の型が導かれる際に除去される．除去された仮定は、自然演繹の記法に従い [ ] で囲って表†3 正確には反対称律は成立するとは限らないので、擬順序である。

あれば γ1 でも当然型付けができることを示している．

また，λ x. e の固有変数条件より，r に関する仮定(RLet) 規則では，r, e1 , e2 の型を tr と限定していr : <Int>γ ref の γ は γ1 以外である．よって γ (6= γ1 ) かる．これは r, e1 , e2 が任意の型を持つとすると，以下ら下の導出を行なう必要がある．のような変数スコープを飛び出すプログラムを許し(let ref r = v1 in λ x. ! r) ()[r : <Int>γ ref] [γ1 ≤ γ ]..
..
r : <Int>γ1 ref

上の項は，λ x. ! r が値であるため，直ちに (λ x. ! r) ()しかし，これを導出できる規則は図 6 にはないため，に簡約される．そして関数適用後，! r を得るが，r は型付けできない．てしまうためである．

ローカルな書き換え可能変数であったため，これは未束縛の変数を参照している．

一方，図 8 は型付けできる例である．これは (1) のr へ代入する値を未束縛の変数 x から整数のコード

let ref r = v1 in λ x. r := λ y. let z = x in <e>%10 へ変えたもので，型が付くべき項である．こちまた，上の項は，r := λ y. let z = x in <e> により r に値

らは図 7 とは違い，r の型に γ1 が出現していない．

λ y. let z = x in <e> が代入され，これは，図 6 の (Subsumption) ルールを用いることでlet ref r = (λ y. let z = x in <e>) in <λ x. e> となる．このr := %10 の型付けから γ1 を排除しているためである．

時 r に代入されたラムダ抽象に含まれる変数 x は変数スコープを飛び出してしまっている．

また，オープンコードと破壊的代入を正しく扱った場合の項(Code) はコードに関する規則である．コード型に

λ x. let ref r = %0 in let = λ y. r := x in ! rは，型付け文脈を表す変数が必要となるため，他の型に対する型付けを図 9 に示す．(2) では，自由変数 x付けとは無関係な，フレッシュな γ を導入している．

を持つコードレベルのラムダ抽象 λ x. e の本体 e 中で，(Const) は定数に関する規則である．ここでの定数書き換え可能変数 r が定義されているため，e 中で xは Int, Bool 型を持つ整数やブール値に加えて，例えを参照することは正しい操作である．図 9 では，仮定ば ((t1 → t2 ) → (t1 → t2 )) → (t1 → t2 ) という型を持つに出現する r の持つコード型の型付け文脈を x の型fix(不動点コンビネータ) 等の単項演算子を含む．

がもつ型付け文脈変数としている．これは，λ x. e の(2)(LetRef) 規則を除く，破壊的代入に関する規則は型の導出を終える前に，r に関する仮定が除去される(Assgn),(Dref) である．これらは単純型付きラムダ計ため固有変数条件に反していない．また，図 10 は r算に，純粋に破壊的代入を加えた場合の規則と同じもに代入される変数を x から y に変更した場合の型付ので，簡易に表されている．

けである．この時，r に代入した未束縛の変数 y が変

この型システムを用いて，次章では型付けを行う．

数スコープを越えて参照されているため，型付けを行うことはできないことが望まれる．変数 y を持つコー

5 型付け例

ドレベルのラムダ抽象は，r が定義されたあとで出現

ここでは，上述の型システムで副作用とコード生するため，この場合は仮定 r : <Int>γ1 ref に出現する r成の組み合わせで Scope Extrusion が起きる例が型の型の型付け文脈を y の型がもつ型付け文脈変数にエラー (型が付かない) となるかを確認する．Scopeすることはできない．なぜならば，y の型付け文脈変Extrusion が起きる例は (1) を用いる．図 7 が例題の数は今ある仮定 (r に関する仮定を含む) とは無関係で型付けである．一見正しく型付けが行なわれているよなければならないからである．よって図 7 のように下うに見えるが，(Assgn) 規則により下のように r の型の導出が必要となるが，(Subsumption) 規則は，コーと x の型は同じになる必要がある．

ド型以外には適用できないため，型付けできないこと

r : <Int>γ1 ref [x : <Int>γ1 ]r := x : <Int>γ1が分かる．

[r : <Int>γ1 ref] [γ 2 ≤ γ 1]..
..
r : <Int>γ2 ref

6 関連研究MetaOCaml として実際に実装されている型システ
ムのベースとして λ i [10] がある．λ i ではコード生成ができる体系で型安全性を保証してる．しかし λ i では副作用を導入した場合については対象外である．
また，亀山らの研究 [9] ではモナドと型クラスを用いて Haskell 上で安全なコード生成を実装した．しかし，モナド，型クラスを用いたことで体系が複雑になっており，論理的な安全性の証明を与えることが難しくなっている．本研究では体系を簡素化することで，将来的には論理的に証明を与えることも１つの目標としている．

7 まとめと今後の予定
副作用を用いたコード生成を安全に行なうために，自然演繹における固有変数条件をもとにして型システムを設計した．副作用として書き換え可能変数を加え，複数の例についてきちんと型付けができていることを確認した．今後の課題としては，まず論理的に正しいことを保証するために今までの範囲について証明を与えることが挙げられる．次に，let 挿入やループの交換に必要となる，限定継続を新たに導入した型システムについて考察する．また，論理 (Kripke 意味論) との関連について考察する．

参考文献[ 1 ] Walid Taha and Tim Sheard. Multi-stage programmingwith explicit annotations. In Proceedings of the 1997 ACM
SIGPLAN Symposium on Partial Evaluation and Semanticsbased Program Manipulation, PEPM ’97, pp. 203–217,
New York, NY, USA, 1997. ACM.
[ 2 ] Walid Taha. A gentle introduction to multi-stage programming. In Domain-Specific Program Generation, pp.
30–50, 2003.
[ 3 ] Walid Taha and Michael Florentin Nielsen. Environment
classifiers. In Proceedings of the 30th ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, POPL ’03, pp. 26–37, New York, NY, USA, 2003.
ACM.
[ 4 ] Geoffrey Mainland. Explicitly heterogeneous metaprogramming with MetaHaskell. In Proceedings of the 17th
ACM SIGPLAN International Conference on Functional
Programming, ICFP ’12, pp. 311–322, New York, NY,USA, 2012. ACM.
[ 5 ] Tim Sheard and Simon Peyton Jones. Template metaprogramming for Haskell. In Proceedings of the 2002 ACM
SIGPLAN Workshop on Haskell, Haskell ’02, pp. 1–16,
New York, NY, USA, 2002. ACM.
[ 6 ] Tiark Rompf and Martin Odersky. Lightweight modular
staging: A pragmatic approach to runtime code generationand compiled dsls. In Proceedings of the Ninth International Conference on Generative Programming and Component Engineering, GPCE ’10, pp. 127–136, New York,NY, USA, 2010. ACM.
[ 7 ] Yukiyoshi Kameyama, Oleg Kiselyov, and Chung-chieh
Shan. Shifting the stage: Staging with delimited control. In
Proceedings of the 2009 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM ’09, pp.
111–120, New York, NY, USA, 2009. ACM.
[ 8 ] Edwin M. Westbrook, Mathias Ricken, Jun Inoue, Yilong Yao, Tamer Abdelatif, and Walid Taha. Mint: Java
multi-stage programming using weak separability. In Benjamin G. Zorn and Alexander Aiken, editors, PLDI, pp.
400–411. ACM, 2010.
[ 9 ] Yukiyoshi Kameyama, Oleg Kiselyov, and Chung-chieh
Shan. Combinators for impure yet hygienic code generation. In Proceedings of the ACM SIGPLAN 2014 Workshop
on Partial Evaluation and Program Manipulation, PEPM
’14, pp. 3–14, New York, NY, USA, 2014. ACM.
[10] Cristiano Calcagno, Eugenio Moggi, and Walid Taha.
Ml-like inference for classifiers. In David Schmidt, editor,
Programming Languages and Systems, Vol. 2986 of Lecture Notes in Computer Science, pp. 79–93. Springer Berlin
Heidelberg, 2004.

[x : t1 ]..
..
e : t2(Abs)λ x. e : t1 → t2

[x : <t1 >γ1 ] [γ1 ≤ γ ]..
..
e : <t2 >γ1(CAbs, γ1 is eigen)
λ x. e : <t1 → t2 >γ[r : tr1 ref]..
..
e1 : tr1
e2 : tr2(LetRef)
let ref r = e1 in e2 : tr2

x:t(Var)e:t(Code, γ is eigen)<e> : <t>γγ ≤γ(Ref-Relation)c : tc[x : <t1 >γ1 ] [γ1 ≤ γ ]..
..
e : <t2 >γ1(IAbs, γ1 is eigen)
λ x. e : <t1 → t2 >γ(Const)

e1 : t ref e2 : t(Assgn)
e1 := e2 : tγ1 ≤ γ2 γ2 ≤ γ3(Trans-Relation)
γ1 ≤ γ3
図6e1 : t1 → t2 e2 : t1(App)e1 e2 : t2
e : t ref(Dref)!e:te : <t>γ γ1 ≤ γ(Subsumption)e : <t>γ1

型付け規則[r : <Int>γ ref] [γ1 ≤ γ ]..
..
r : <Int>γ1 ref[x : <Int>γ1 ][r : <Int>γ ref]r := x : <Int>γ1(γ1 is eigen)γ
λ x. r := x : <Int → Int>! r : <Int>γ
0 : Int%0 : <Int>γlet = (λ x. r := x) in ! r : <Int>γlet ref r = %0 in let = (λ x. r := x) in ! r : <Int>γ

図7

型付けできない例

10 : Int[r : <Int>γ ref] %10 : <Int>γr := %10 : <Int>γ[γ1 ≤ γ ][r : <Int>γ ref]r := %10 : <Int>γ1(γ1 is eigen)γ
λ x. r := %10 : <Int → Int>! r : <Int>γ0 : Int
γ
γ%0 : <Int>
let = (λ x. r := %10) in ! r : <Int>
let ref r = %0 in let = (λ x. r := %10) in ! r : <Int>γ

図8

型付けできる例

[r : <Int>γ1 ref] [x : <Int>γ1 ]r := x : <Int>γ1[γ2 ≤ γ1 ]γ2[r : <Int>γ1 ref]r := x : <Int>(γ2 is eigen)γ1λ y. r := x : <t → Int>! r : <Int>γ10 : Int
γ
γ%0 : <Int> 1let = λ y. r := x in ! r : <Int> 1let ref r = %0 in let = λ y. r := x in ! r : <Int>γ1(γ1 is eigen)
λ x. let ref r = %0 in let = λ y. r := x in ! r : <Int → Int>γ

図9型付けできる例 2[r : <Int>γ1 ref]..
..
r : <Int>γ2 ref [y : <Int>γ2 ][r : <Int>γ1 ref]r := y : <Int>γ2(γ2 is eigen)γ1λ y. r := y : <t → Int>! r : <Int>γ10 : Int
γ
γ%0 : <Int> 1let = λ y. r := y in ! r : <Int> 1let ref r = %0 in let = λ y. r := y in ! r : <Int>γ1(γ1 is eigen)
λ x. let ref r = %0 in let = λ y. r := y in ! r : <Int → Int>γ

図 10

型付けできない例 2