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

多段階計算 λ▷ のための越段階埋込花田 裕一朗五十嵐 淳

多段階プログラミングとは，実行時のプログラムコードの生成や実行により，プログラムの再利用性を高めたり，最適化を容易にするためのプログラミング技法である．疑似引用， eval などの多段階プログラミングのための特殊な機構を持つ言語のモデルとなる型付計算体系が盛んに研究されており，その中の一つに，Tsukada と Igarashi (2009)
によって提案された λ▷ がある．λ▷ は，型安全性や強正規化性を持ち，カリー・ハワード同型対応を通じて様相論理に対応する計算体系であるが，ある実行段階において計算された値をプログラムコード中に埋め込む操作である越段
階埋込 (cross-stage persistence) を持たない．そこで本稿では， λ▷ を越段階埋込によって拡張した体系 λ▷% を定義し，操作的意味論と型システムを与える．そして，型付け可能な項はその項を実行した結果生成されるプログラムコードも含めて安全なものであるという意味での型安全性を持つことを示す．さらに， λ▷ に対応する論理体系をどのように拡張すれば，越段階埋込に論理的な意味付けができるかについても考察する．

んでいる操作で， bracket の中でその bracket を脱出

1 はじめにして計算をし，その結果得られる値を bracket の中へ

多段階プログラミングとは，実行時にプログラム

埋め込む操作である．escape との違いは escape が計

コードを生成、組み合わせ、実行することによって，算の結果得られたコードを埋め込むのに対し， 越段

プログラムの再利用性を高めたり，最適化を容易にす

階埋込は計算の結果の値を埋め込むことにある．

るためのプログラミング技法である．

このような機構を備えた言語においては，入れ子

多段階プログラミングのための特殊な機構を持つになった bracket によってプログラムコードを生成す

言語のモデルとなる型付計算体系 (多段階計算と呼るプログラムコードの値など，多重にコード化さればれる) が盛んに研究されている．多段階プログラミ

た値が登場する．あるプログラムを取り囲んでいるングを実現する方法はいくつか考えられるが，本稿bracket の数がそのプログラムが何段階後の実行時にではプログラム中でプログラムコードを値として扱おいて実行されるかを表わすのである．この何段階後

う操作 bracket， escape， run，cross-stage persistenceの実行時に実行されるかという概念は計算のステーといった機構 [7] を持つ型付計算体系に注目する．

ジと呼ばれている．

bracket はプログラムから値としてのコードを作り出

bracket， escape， run， cross-stage persistence を備す操作であり， escape は bracket の中でその bracket

えるプログラミング言語のモデルとなる計算体系のを脱出して計算をしその結果として得られるコード

1 つとして Taha と Nielsen (2003) によって λα [6] がを bracket の中に埋め込む操作である．この 2 つの操提案されている．λα では bracket と escape が環境分

作は，Lisp における疑似引用と unquote に似た操作で類子と呼ばれる変数によってラベル付けされている．

ある．run はコード片を実際に計算し値を得る操作でこの環境分類子は各コード片に含まれる自由変数のあり， cross-stage persistence は本稿で越段階埋込と呼情報を型レベルへと反映する役割を果たしている．

Yuichiro Hanada, Atsushi Igarashi, 京都大学大学院情報学研
究科, Graduate School of Informatics, Kyoto University.

を束縛し，他の環境分類子によって具体化する機能

bracket や escape といった操作に加えて，環境分類子

を持つことによって，項に含まれる自由な変数が存

1. 1 本論文の構成

在しないという普通の意味での closedness よりも弱次節では，越段階埋込が多段階計算においてどのよい，ある環境分類子 α によってラベル付けされていうな役割をはたす操作であるか，また既存の研究にるコードの中には自由な変数が存在しないという意

おいて越段階埋込がどのように扱われているかにつ

味の α-closedness を考えることができるようになる．

いて詳しく見る．3 節では， 計算体系 λ▷% を定義し，λα では，この α-closedness によってあるコード片が小ステップ (small-step) 形式による意味論と型システ

安全に実行できるかを検査することができる．また，ムを与える．4 節では λ▷% の持ついくつかの性質を示

λα では bracket に環境分類子が紐付いていることかす．5 節では越段階埋込の論理的な意味について考察

ら，計算のステージを環境分類子の列として表現する

する．

ことが可能である．

Tsukada と Igarashi (2009) によって提案された λ▷[8] も bracket， escape を備えた多段階型付計算体系で▷2 越段階埋込 (cross-stage persistence)
多段階計算における越段階埋込 (cross-stage persis-

ある．λ においては， bracket や escape は遷移変数

tence) とは，現在のステージでの値を後のステージにとよばれる変数によってラベル付けされており，さらおいても自由に使うことを可能にする機能である．

αに遷移変数を束縛し，代入を行うことができる．λライブラリとして提供される関数や言語に組みこも，同様に環境分類子を束縛し，代入することができ

みの関数のように，様々な場所で使われることを想定▷

るが，λ では束縛された遷移変数を遷移変数の列にしている関数は，任意の計算のステージで使うことがよって具体化できるという違いがある．この違いにできるべきである．しかし，越段階埋込を持たない言

よって， λ▷ は run の操作を言語に組み込みの機能と語の場合，ある計算のステージで定義された関数や定して備える必要がなく，コード片の実行が束縛された数をその後のステージで使うことはできない．

遷移変数への空列の代入によって表現できる．コード

他にも，その計算した値を後のステージで自由に参中の全ての遷移変数が束縛されている時，その遷移変照できるという性質を利用して，計算結果のメモ化に数を適当な遷移変数の列で具体化することで任意の利用することができる．計算に時間のかかる値をはじステージの値として埋め込むことができる．しかし，めに計算しておき，生成されるコードの中でその値を関数などのコード片ではない値や束縛されていない

使う場合に，その計算を行うコードを生成するのでは遷移変数を含むようなコード片に対する越段階埋込

なく直接，計算結果を埋め込むことでプログラムの計▷が可能ではない．多少の違いはあるが，λ における
α

算時間を短縮することができる．

遷移変数は λ における環境分類子と似通った役割を

例えば， λ▷ では閉じたコード (そのコードにおい

果たしており， λ▷ においても計算のステージが遷移て登場する全ての遷移変数が束縛されているような変数の列によって表現できる．

コード) についてのみ後のステージに自由に埋め込む▷

本論文では，λ を越段階埋込によって拡張した体系λ▷%を定義し，full reduction，評価文脈を使った値▷%

呼び意味論，型システムを定義する．さらに， λが強正規化性や合流性，型安全性を持つことを示す．ま▷ことを許している．したがって，コードの中で使用する関数は全てそのコードと同じステージで定義されている必要がある．
越段階埋込を表現するために 2 種類の手法が考えた，越段階埋込の論理的な意味が λ に対応する論理

られる．1 つは λα が用いているもので越段階埋込に体系をどのように拡張すれば与えられるかについて

よって段階を越える値に明示的にどの bracket を飛び考察する．

越えるかを書くものである．もう 1 つは，暗黙の内に越段階埋込を行うもので，ある段階で計算された値を自由に後のステージで使うことができ，いくつのbracket を飛び越える値であるかは暗黙のうちに決められるというものである．

える．

α

λ の bracket や escape をもとにして OCaml を拡張(Λα.(▶α (λx : τ.x))) (βγ)

した言語 MetaOCaml [5] を例として，いくつかのプ

このプログラムは，α でラベル付けされたコード

ログラムを考える．MetaOCaml では，bracket を .<λx : τ.x の α を βγ という遷移に置きかえるというプと >. で囲むことで表現し， escape は .˜ を run は !. を

ログラムになっている．したがって，このプログラム

使って表現する．MetaOCaml は変数に対してのみ暗を実行した結果は，▶β ▶γ (λx : τ.x)

黙的な越段階埋込が可能である．
まず，越段階埋込が登場しない例であるが，となる．さらに，

let a = .< 1 + 2 >. in .< .˜a + .˜a >.
というプログラムは，変数 a を 1+ 2 というプログラム(λx : ▷α τ. ▶α ◀α x) ▶α yというプログラムは，まず適用によってコードに束縛し，それを組み合わせて (1 + 2) + (1 + 2)というプログラムコードを生成するプログラムになっ▶α ◀α ▶α yとなり， ◀α が ▶α と打ち消しあうことによって

▶α y

ている．
越段階埋込を用いた MetaOCaml のプログラム例ととなる．

λ▷% は，λ▷ に加えて越段階埋込を表現する構成子

して，.< · · · (map f l) · · · >.

%α を持つ．%α の働きは，%α に与えられた部分項ののようなプログラムが考えられる．map 関数は MetaO-

計算を % の外側よりも前のステージにすることであCaml がもともと持っているライブラリ関数であるが，る．つまり，計算のステージが Aα であるような部分

ライブラリ関数は一番外側のステージにおいて定義さに %α M という項があった場合， M の計算のステーれている関数なので，そのままでは bracket の中で使ジは A となる．例として次のプログラムを考える．

うことはできない．しかし， MetaOCaml は暗黙的なλx : τ. ▶α ((λy : τ.y) (%α x))

越段階埋込を持っているので，ひとつ bracket の中に

このプログラムは，τ 型の変数を受け取りその変数を入ったステージでも map を使用できる．よって，このλy : τ.y という関数へ適用するコードを生成する関数

ようなプログラムを書くことが可能になるのである．

である．%α x の計算のステージは α であるので，そのままではステージ ε に属する変数 x を使うことは3 λ▷%できない．そこで越段階埋込を使って，▶α の外側の▷

この節では， λ を越段階埋込によって拡張した体▷%系λの定義を与える．

ステージの値である x を ▶α の中へと持ちこんでいるのである．

まず， λ▷ において多段階計算がどのように形式化されているかを見る．λ▷ はコードを操作するための3. 1 文法

構成子 ▶α , ◀α を持つ．▶α はコードを生成するための

Var を変数の可算無限集合， TV を遷移変数の可算構成子で， bracket に対応する．◀α は escape に対応

無限集合とする．λ▷% において，コードは遷移変数にする構成子である．この 2 つの構成子は遷移変数と呼よってラベル付けされている．λ▷% の項，型，値の定ばれる変数でラベル付けされている．▶α , ◀α の α が義を図 1 に示す．

▷

遷移変数である．さらに， λ ではこの遷移変数に関

主要な部分は λ▷ の定義と変わっていない．越段階

する抽象と，遷移変数の列による具体化を行うことが埋込を表現するための構成子である %α が新たに加できる. 遷移変数を束縛するための構成子が Λα. であわっている．越段階埋込にラベル付けされている遷移

り，束縛された遷移変数には遷移変数の列，遷移を代

変数は，越段階埋込によって飛び越える引用にラベル入することができる．例として次のプログラムを考付けされている遷移変数である．
項 M にたいして， M に現われる自由な変数と遷

x, y ∈ Var

変数
遷移変数

α, β, γ ∈ TV

遷移

A, B, C ∈ TV∗(λx : τ.M)[y := N] = λx : τ.M[y := N] (x , y, y < FV(N))(▶α M)[x := N] = ▶α (M[x := N])型

τ, σ ::= b | τ → τ | ▷α τ | ∀α.τ項

M, N ::= x | λx : τ.M | M M | ▶α M
| ◀α M | Λα.M | M A | %α Mvε ∈ V ε ::= λx : τ.M | ▶α vα | Λα.vε

値(%α M)[x := N] = %α M[x := N](Λα.M)[x := N] = Λα.M[x := N](α < FTV(N))(M A)[x := N] = (M[x := N]) A
図3

変数への代入vA ∈ V A ::= x | λx : τ.vA | vA vA | ▶α vAα| Λα.vA | vA B′

| ◀α vA (A′ α = A, A′ , ε)′

| %α vA (A′ α = A)Rε ::= (λx : τ.M) N | (Λα.M) A

簡約基

Rα ::= ◀α ▶α M
図1

λ▷% の文法

移変数の集合をそれぞれ FV(M), FTV(M) と書き， MAα[α := B] = (A[α := B])BAα[β := B] = (A[β := B])α (α , β)(τ → σ)[α := A] = τ[α := A] → σ[α := A](▷α τ)[α := A] = ▷A (τ[α := A])(▷β τ)[α := A] = ▷β (τ[α := A])(α , β)(∀α.τ)[β := A] = ∀α.(τ[β := A]) (α , β)の構造について帰納的に定義される．それぞれの定義を一部抜粋したものが図 2 である．λx : τ.M におけるx， Λα.M における α が束縛変数である．

(λx : τ.M)[α := A] = λx : τ[α := A].(M[α := A])(▶α M)[α := A] = ▶A (M[α := A])(▶α M)[β := A] = ▶α (M[β := A]) (α , β)FV(x) = {x}FV(λx : τ.M) = FV(M) \ {x}FV(M N) = FV(M) ∪ FV(M)FV(▶α M) = FV(M)FV(Λα.M) = FV(M)FTV(x) = ∅FTV(λx : τ.M) = FTV(M)FTV(▶α M) = FTV(M) ∪ {α}FTV(Λα.M) = FTV(M) \ {α}
図2

自由な変数の集合と自由な遷移変数の集合(%α M)[α := A] = %A (M[α := A])(%α M)[β := A] = %α (M[β := A])(α , β)(Λα.M)[β := A] = Λα.(M[β := A])(α , β)(M A)[α := B] = (M[α := B]) (A[α := B])
図4

遷移変数への代入

ただし，A = α1 α2 · · · αn であるとき，▷A τ = ▷α1 ▷α2 · · · ▷αn τ▶A M = ▶α1 ▶α2 · · · ▶αn M◀A M = ◀αn · · · ◀α2 ◀α1 M%A M = %αn · · · %α2 %α1 Mであるとする．また特に，A = ε であるとき，▶ε M = ◀ε M = %ε M = M
3. 2 意味論

であると定義する．

操作的意味論を与えるために変数と遷移変数の両▶ と ◀ ， % において，遷移変数の展開の順序が逆方について代入操作を定義する．全ての場合をつくし転しているのは， ▶ が計算のステージをひとつ引きた完全な定義ではなく，主要な場合についてのみ抜粋

上げる操作であるのに対し，◀ と % が計算のステーしたものが図 3 ，図 4 である．

ジをひとつ引き下げる操作であるからである．

λ▷% の小ステップ形式による操作的意味論を 2 つの方法で与える．ひとつ目は λ▷ の小ステップ形式による操作的意味論と同様の形式による full reduction で例えば評価文脈は，

Eεε = □ (λx : τ.x)

ある．もう一つは，評価文脈を利用し，評価の順序をEαε = (λx : τ.x) (▶α □)明らかにした意味論である．

εEβγ= ▶β ◀α ▶α ▶γ □3. 2. 1 full reduction
簡約 −→ f はといったものになる．

(λx : τ.M) N −→ M[x := N]
f

(βv )

((Λα.M) A) −→ M[α := A]f◀α ▶α M −→ f M(βα )EεA [(λx : τ.M) vε ] −→e EεA [M[x := vε ]](◀ ▶)という 3 つの規則と，任意の部分項の簡約を許す規則(βv )EεA [(Λα.M) B] −→e EεA [M[α := B]](βα )EαA [◀α ▶α M] −→e EαA [M](◀ ▶)によって作られる最小の関係である．単純型付きラム

図6

ダ計算 [4] の簡約規則に新しく 2 つの規則が加わって簡約規則

いる．1 つは， ◀ と ▶ が打ち消しあうという規則であり，もう 1 つは， 束縛された遷移変数への遷移の

図 6 が λ▷% の簡約規則の定義である．(βv ) は通常代入を行う規則である．ここには越段階埋込に関するの (値呼び) β 簡約である．(βα ) は遷移変数への遷移の簡約規則が含まれていないが，全ての越段階埋込には代入操作を表現した規則である．(◀ ▶) は ◀ が ▶ と対応する引用が存在し，その引用が消えてしまう時，打ち消しあうことを表現している．

すなわち引用と越段階埋込に付随する遷移変数に空列 ε が代入された時にはその引用と同時に越段階埋込も消失してしまうので，明示的に越段階埋込に関す

簡約 −→ f と同様に， −→e の反射的かつ推移的な閉包を −→e∗ と書く．
例えば計算のステージが ε であるような，▶α (λx : τ. ◀α ▶α x)

る簡約規則は必要ない．
また，簡約 −→ の反射的かつ推移的閉包を −→ff∗というプログラムは，評価文脈として Eαε = ▶α (λx :τ.□) をとることで簡約規則 (◀ ▶) を適用することがと書く．

3. 2. 2 評価文脈を使った値呼び意味論

でき，▶α (λx : τ. ◀α ▶α x) −→e ▶α (λx : τ.x)

評価文脈の定義は図 5 である．ただし，図 5 において A , ε かつ B , ε であるとする．

となる．別の例として，同じく計算のステージが ε であるような

Eεε ::= □ | vε Eεε | Eεε M | ▶α Eεα | Λα.Eεε | Eεε A
E Aε ::= vε E Aε | E Aε M | ▶α E Aα | Λα.E Aε | E Aε B
E BA ::= □ (A = B) | vA E BA | E BA M | ▶α E BAαというプログラムは，まず評価文脈を □ とすること
で簡約規則 (βα ) が適用でき，次に評価文脈を □ とすることで簡約規則 (βv ) をつかって簡約することがで′| ◀α E BA (A′ α = A)′

| %α E BA (A′ α = A) | Λα.E BA | E BA C
図5

(Λα.(λx : τ → τ. ▶α %α x) (λy : τ.y)) ε

評価文脈

評価文脈は 2 つの遷移によってパラメタライズさきる．

(Λα.(λx : τ → τ. ▶α %α x) (λy : τ.y)) ε−→e (λx : τ → τ.x) (λy : τ.y)(βα )−→ (λy : τ.y)

(βv )

e

れている．右上の添字は，評価文脈全体がどの計算のステージに属しているかを表わしており，右下の添字
は，評価文脈にただ 1 つ含まれている □ がどの計算

3. 3 型システムのステージに属しているかを表わしている．

この節では λ▷% の型システムを定義する．

定義 1 (型環境). λ▷% における型環境 Γ はして扱う操作であることを，あるステージでの型を変Γ = • | Γ, x : τ@A

えずに，その次のステージの型とすることで表現してと帰納的に定義される，変数と型と遷移の 3 つ組の有限列である．x : τ@A という 3 つ組は変数 x がステー
ジ A において型 τ を持つことを表わす．
また，型環境 Γ に含まれる変数の集合を dom(Γ) といる．

4 λ▷% の性質
この節では，前節で定義した体系 λ▷% についてい
くつかの性質を示す．

書き，まず，簡約 −→ f についてdom(•) = ∅• 強正規化性

dom(Γ, x : τ@A) = {x} ∪ dom(Γ)• 合流性のように帰納的に定義する．

• Subject Reduction

さらに型環境に対する遷移変数への代入をを示し，次に簡約 −→e について•[α := A] = •(Γ, x : τ@A)[α := B] = Γ[α := B], x : τ[α := B]@(A[α := B]) • 評価文脈による分解の一意性と定義する．

• 簡約 (−→e ) が簡約 (−→ f ) に含まれること

定義 2 (型判断). ステージ A，型環境 Γ のもとで，項• Progress

M に型 τ がつくことをの 3 つを示す．

Γ⊢ e:τ
A

4. 1 簡約 −→ f の性質と書く．

λ▷% の型付け規則を図 7 のように定義する．

定 理 1 (強 正 規 化 性). 項 M が 型 付 け 可 能 な ら ば ，

M −→ f M1 −→ f M2 · · · となるような無限列は存在し
Γ, x : τ@A ⊢A x : τ(Var)Γ, x : τ@A ⊢A M : σΓ ⊢A λx : τ.M : τ → σΓ ⊢A M : τ → σΓ ⊢A N : τΓ ⊢A M N : σ
Γ⊢

Aα

M:τ

Γ ⊢A ▶α M : ▷α τΓ, α ⊢A M : τ(◀)Γ ⊢A M : ▷α τ
Γ ⊢Aα ◀α M : τΓ ⊢A Λα.M : ∀α.τΓ ⊢A M B : τ[α := B]
図7

(Ins)

定理 1 を証明するために， λ▷% の項を 単純型付きラムダ計算 [4] の項へと変換する操作 ♮ を以下のよう(App)

α < dom(Γ) ∪ FTV(A)Γ ⊢A M : ∀α.τ

ない．

(Abs)

に定義する．

♮(x) = x(▶)♮(λx : τ.M) = λx : τ.♮(M)♮(M N) = ♮(M) ♮(N)♮(▶α M) = ♮(M)(Gen)Γ ⊢A M : τΓ ⊢Aα %α M : τ♮(◀α M) = ♮(M)♮(%α M) = ♮(M)(%)♮(Λα.M) = ♮(M)

型付け規則♮(M A) = ♮(M)
操作 ♮ について，次の性質が成り立つ．

(Var), (Abs), (App) の規則は，型判断が遷移によっ

補題 2. ある A, τ について ⊢A M : τ であるならば，てパラメタライズされていることをのぞいて，単純♮(M) も単純型付きラムダ計算において型付け可能で型付きラムダ計算における型付け規則と変わらない．

ある．

残りの 5 つの規則のうち， (▶)， (◀)，(Gen)，(Ins) は証明. ⊢A M : τ に関する帰納法による．

λ▷ の型付け規則と同じである．(%) が新たに追加さ□れた越段階埋込のための型付け規則である．越段階埋補題 3. 項 M, N について， M −→ f N であるとき，使込が前のステージにおける値を次のステージの値と用した簡約規則が (βv ) であるならば， ♮(M) −→ f ♮(N)

補題 5. (−→ f ) ⊆ (=⇒) ⊆ (−→ f ∗ ) である．

であり，それ以外ならば， ♮(M) = ♮(N) である．
証明. 項 M の構造に関する帰納法による．

□以上の 2 つの補題を用いて定理 1 を証明する．
証明. 型付け可能な項 M について簡約の無限列が存在したと仮定する．このとき，簡約規則 (βα ) と ◀ ▶
は項の大きさを小さくすることから，この無限列には(βv ) による簡約が無限に存在する．補題 2 より ♮(M)
は単純型付きラムダ計算において型付け可能であり，補題 3 より，♮(M) からはじまる簡約の無限列が存在証明. (−→ f ) ⊆ (=⇒) であることは， M −→ f N の
導 出 に 関 す る 帰 納 法 に よって 証 明 で き る ．ま た ，(=⇒) ⊆ (−→ f ∗ ) であることは， M =⇒ N の導出に関する帰納法によって証明できる．
補題 6.

□

1. M1 =⇒ N1 か つ M2 =⇒ N2 な ら ば

M1 [x := M2 ] =⇒ N1 [x := N2 ] である．
2. M =⇒ N ならば M[α := A] =⇒ N[α := A] である．

するといえる．しかし，これは単純型付きラムダ計算

証明. 1 は M1 =⇒ N1 の導出に関する帰納法によってが強正規化性を持つことに反する．したがって，この証明できる．2 は M =⇒ N の導出に関する帰納法にような M についての簡約の無限列は存在しない． □よって証明できる．

定理 4 (合流性). 項 M について， M −→ f ∗ M1 かつ M −→

M1 −→

f∗

f∗

M2 な ら ば ，あ る 項 M3 が 存 在 し て ，M3 かつ M2 −→f∗

M3 である．

□

次に項 M の complete development M ∗ を図 9 のよ
うに帰納的に定義する．ただし，適用できる規則が複数あるときはより上に書かれている規則を優先する．

▷[8] における λ の合流性の証明とほぼ同様に並行

簡約と complete development を用いて証明できる．
並行簡約 (=⇒) を図 8 のように定義する．

M1 =⇒ N1

(λx : τ.M)∗ = λx : τ.M ∗((λx : τ.M) N) = M ∗ [x := N ∗ ]M =⇒ Nx =⇒ xx∗ = x(M N)∗ = M ∗ N ∗λx : τ.M =⇒ λx : τ.N
M2 =⇒ N2

M1 M2 =⇒ N1 N2
M1 =⇒ N1

M =⇒ N(◀A ▶A M)∗ = M ∗(◀α M)∗ = ◀α M ∗Λα.M =⇒ Λα.NM2 =⇒ N2

(λx : τ.M1 ) M2 =⇒ N1 [x := N2 ](Λα.M)∗ = Λα.M ∗M =⇒ N((Λα.M) A)∗ = M ∗ [α := A]

M A =⇒ N A(M A)∗ = M ∗ A

M =⇒ NM =⇒ N▶α M =⇒ ▶α N

◀α M =⇒ ◀α N

M =⇒ NM =⇒ N◀A ▶A M =⇒ N

(Λα.M) A =⇒ N[α := A]
M =⇒ N%α M =⇒ %α N
図8(▶α M)∗ = ▶α M ∗並行簡約

この並行簡約について以下の 2 つの補題が成立する．

(%α M)∗ = %α M ∗図9complete development

項の complete development について以下の 2 つの性質が成り立つ．
補題 7. M =⇒ N ならば N =⇒ M ∗ である．
補題 8. M =⇒ N1 かつ M =⇒ N2 ならばある項 N が存在して N1 =⇒ N かつ N2 =⇒ N である．
証明. N = M ∗ とすれば補題 7 より N1 =⇒ M ∗ かつ

N2 =⇒ M ∗ である．

□

ので，Γ ⊢Aα (%α M0 )[x := N] : τ である．

(2) の証明

以上の補題を用いて，定理 4 が証明できる．

• M = ▶β M0 の場合

証明. 補題 5 より並行簡約が合流性を持てば，簡約f仮定 Γ ⊢A ▶β M0 : τ と型付け規則から，Γ ⊢Aβ(−→ ) もまた合流性を持つ．また，補題 8 より並行簡

M0 : τ0 かつ τ = ▷β τ0 である．帰納法の仮定

約はダイアモンド性を持つから明らかに合流性を持から Γ[α := B] ⊢Aβ[α:=B] M0 [α := B] : τ[α := B] が□成り立つ．β[α := B] の長さが n であるとする

次に， Subject Reduction を証明する．そのために，と，型付け規則 (▶α ) を n 回適用することによっ

まず変数，遷移変数への代入によって型が変化しないて Γ ⊢ A[α := B] ▶β[α:=B] M0 : ▷β[α:=B] τ0 をえる．

という補題を証明する．

遷移変数の代入の定義から， ▶β M0 [α := B] =補題 9 (Substitution Lemma). 2 つの代入について以下▶β[α:=B] M0 [α := B] であるので，これで示された．

fつ．したがって，簡約 (−→ ) は合流性を持つ．

• M = %β M0 の場合

2 つの性質が成り立つ．
M : τ が導Γ ⊢A %β M0 : τ を仮定すると，型付け規則から，出可能であり Γ ⊢B N : σ も導出可能ならば，

A = A′ β となるような A′ が存在し， Γ ⊢A M0 : τΓ ⊢A M[x := N] : τ が導出可能である．

で あ る ．帰 納 法 の 仮 定 よ り Γ[α := B] ⊢A [α:=B]

1. 項 M に つ い て ， Γ, x : σ@B ⊢

A

′

′

2. 項 M について， Γ ⊢A M : τ であるとき，任M[α := B] : τ[α := B] である．ここで，β = α

意の α, B について Γ[α := B] ⊢A[α:=B] M[α := B] :である場合とそうでない場合で場合分けを行う．

τ[α := B] である．
証明. (1)， (2) どちらについても型の導出に関する帰納法によって証明する．

(1) の証明• M = ▶α M0 の場合
仮定より， Γ, x : σ@B ⊢A ▶α M0 : τ かつ Γ ⊢B

N : σ である．型付け規則から， Γ, x : σ@B ⊢Aα
M0 : τ0 かつ τ = ▷α τ0 であるような τ0 が存在す
る．帰納法の仮定から， Γ ⊢Aα M0 [x := N] : τ0
が 成 り 立 つ ．こ れ に 規 則 ▶α を 適 用 す れ ば ，Γ ⊢A ▶α (M0 [x := N]) : ▷α τ0 が得られる．代入の定義より ▶α (M0 [x := N]) = (▶α M0 )[x := N] なので， Γ ⊢A (▶α M0 )[x := N] : ▷α τ0 である．

• M = %α M0 の場合

1. β = α の場合
規 則 %α を B の 長 さ の 回 数 だ け 繰 り 返′

し 適 用 す る こ と に よって ，Γ[β := B] ⊢A B

%B (M0 [β := B]) : τ がえられる．代入の定義より，(%β M0 )[β := B] = %β[β:=B] M0 [β := B] であるので，Γ[β := B] ⊢A[β:=B] (%β M0 )[β := B] :

τ[β := B] である ．
2. β , α の場合(A′ β)[α := B] = (A[α := B])β なので，一度規′則 %α を適用することで Γ[α := B] ⊢(A β)[α:=B]%β (M0 [α := B]):τ[α := B] が え ら れる ．よって ，遷 移 変 数 の 代 入 の 定 義 か′ら ， Γ[α := B] ⊢(A β)[α:=B] (%β M0 )[α := B] :

τ[α := B] である．
□

Γ, x : σ@B ⊢Aα %α M0 : τ，Γ ⊢B N : σ と
仮 定 す る と ，型 付 け 規 則 か ら Γ, x : σ@B ⊢A

定理 10 (Subject Reduction). Γ ⊢A M : τ かつ M −→ f

M0 : τ が成り立つ．帰納法の仮定から， Γ ⊢A

M ′ ならば，Γ ⊢A M ′ : τ である．

M0 [x := N] : τ を得る．これに規則 % を使えば，証明. M −→ f M ′ についての帰納法によって示す．補Γ ⊢Aα %α (M0 [x := N]) : τ が得られる．代入の定

題 9 を用いれば， λ▷ における同定理の証明と同様に

義より %α (M0 [x := N]) = (%α M0 )[x := N] である

証明できる．

□

4. 2 簡約 −→e の性質

このとき，帰納法の仮定から M2 = E BA [R] −→e定理 11 (評価文脈による分解の一意性). 項 M につい

E BA [N] = M1′ と な る E BA , R, N, M2′ が 存 在 すて， ⊢A M : τ が導出可能ならば， M ∈ V A であるかる ．し た がって ， M = (M1 E BA [R])または， M = E BA [RB ] を満たす E, R が唯一存在する．

(M1 E BA [N]) = M ′ となる M ′ が存在する．

証明. ⊢A M : τ の導出に関する帰納法による．

□−→e

2. Case (▶)
M = ▶α M ′ となる M ′ が存在する． M ′ ∈ V Aα な

定理 12. (−→ ) ⊆ (−→ )らば M ∈ V A である． M ′ < V Aα ならば，帰納法

証明. 簡約 (−→e ) の規 則 につい ての場合分けに よの仮定より M ′ −→e M ′′ となる M ′′ が存在する．

e

f

□

る．

定理 12 より簡約 −→e は強正規化性と Subject

Reduction を満たすと言える．

よって， M = ▶α M ′ −→e ▶α M ′′ である．

3. Case (Ins)
このとき， M = M ′ B となる M ′ , B が存在する．

M ′ ∈ V A であるかどうかと M の計算のステージ

次に Progress を示す．
定理 13 (Progress). 任意の項 M について， Γ がステー
ジ ε に属する宣言を 1 つも含まずかつ Γ ⊢A M : τ であるならば， M ∈ V A であるかもしくは M −→e M ′となる M ′ が存在する．

が ε であるかどうかで場合分けを行う．

(a) M ′ ∈ V ε かつ計算のステージが ε
こ の と き ， Γ ⊢ε M ′ B : τ の 導 出 か ら ，

M ′ = Λα.M ′′ と な る M ′′ , α が 存 在 す る ．
し た がって ，簡 約 規 則 (βα ) が 適 用 で き ，証明. ⊢A M : τ についての帰納法によって示す．

M ′ B = Λα.M ′′ B −→e M ′′ [α := B] である．
(b) M ′ ∈ V A かつ計算のステージが A , ε

1. Case (App)
このとき M = M1 M2 となる M1 , M2 が存在し，ある型 σ について Γ ⊢A M1 : σ → τ， ⊢A M2 : σ

このとき， M ′ B ∈ V A である．

(c) M ′ < V A

が導出できる． M1 , M2 ∈ V A であるかどうかで場帰納法の仮定から， M ′ −→e M ′′ となる M ′′合分けをする．

が存在する．よって， M = M ′ B −→e M ′′ B(a) M1 ∈ V かつ M2 ∈ V
A

A

である．

このとき， A , ε ならば M ∈ V である．
Aε4. Case (λ)

A = ε ならば， Γ ⊢ M1 M2 : τ の導出から，

このとき， M = λx : σ.N となる x, σ, N が存在す

M1 = λx : σ.N となる N が存在する．よって，る．N ∈ V A であるかどうかと M の計算のステー

Eεε = □ とすれば， Eεε [(λx : τ.N)M2 ] = M でジが ε であるかどうかで場合分けを行う．

あり，簡約規則 (βv ) が適用可能である．した(a) 計算のステージが εがって，M = Eεε [(λx : σ.N)M2 ] −→ Eεε [N[x :=このとき， λx : σ.N ∈ V ε である．

M2 ]] = M ′ となるような M ′ が存在している．

(b) 計算のステージが A かつ N ∈ V A(b) M1 < V A

このとき， λx : σ.N ∈ V A である．

このとき，帰納法の仮定から M1 = E BA [R] −→e(c) 計算のステージが A かつ N < V A

E BA [N] = M1′ と な る E BA , R, N, M1′ が 存 在 す

このとき， Γ ⊢A λx : σ.N : τ が導出可能

る ．し た がって ， E ′ ABとすればであることから， Γ, x : σ@A ⊢A N : τ′ がE ′ AB [N] = M ′ を満たす M ′導出できる．よって，帰納法の仮定より，

M = E ′ AB [R]−→eが存在する．

(c) M1 ∈ V A かつ M1 < V A=

E BA M2

N −→e N ′ となる N ′ が存在する．したがって， M = λx : σ.N −→e λx : σ.N ′ である．

□

5 カリー・ハワード同型対応

Γ ⊢A τ

Tsukada と Igarashi の λ▷ も含め，多段階計算のいΓ ⊢Aα τくつか [8] [9] [3] [2] [6] はカリー・ハワード同型対応に

図 10

越段階埋込に対応する推論規則

よって，(直観主義) 様相論理の証明体系と対応することが知られている．この節では，λ▷% がどのように論

味論との整合性がとれない．

理として捉えることができるかについて考察を行う．

Tsukada と Igarashi による論理との対応の枠組みを

まず，λ▷ に対応する論理がどのようなものであっ保ったまま，越段階埋込を解釈する方法のひとつは，たかを見る．この論理は，ラベル付状態遷移系 (より状態遷移系をラベルの集合 L が空集合であるような正確には，各状態に対してラベル a で遷移できる状態

遷移系に制限することである．ラベルの集合が空集が一意に定まる，すなわち各ラベルについて遷移関係

合であれば，必然的に遷移 (列) の集合は空列のみかが関数になっているようなラベル付状態遷移系) につらなる一元集合 {ε} であり，命題 ▷α τ は α が ∀ で束いての様相論理として考えることができる．計算体系

縛されている時のみ意味を持つ．ただし，そのようなの型は論理での命題に対応するが，▷α τ は「(現在着命題 ∀α. ▷α τ も，結局 α の動く範囲が ε だけなので，目している状態から) ラベル列 α で遷移する先の状態

実質的に τ[α := ε] と同じ意味の命題となる．越段階で τ である」という意味で ∀α.τ は「任意の (ラベル埋込に対応する推論規則については，Aα も A も結局

列 A で表現される) 遷移について τ」という意味となのところ意味的には ε につぶれてしまうので論理的る．実際，Tsukada と Igarashi [8] においては，ラベルな妥当性に問題はない．

付状態遷移系をもとに Kripke 意味論が与えられ，型

このような解釈においては，状態間の遷移がない

付け規則から項と型環境中の変数を無視することに(状態数が実質ひとつである) ような系を考えることに

よって得られる自然演繹体系 (に二重否定除去規則をなってしまうので，もはやこの論理は様相論理と呼べ追加したもの) が，意味論に対して健全かつ完全であるものではないかもしれない．しかし，越段階埋込のることが示されている．

計算としての意味や，MetaOCaml のような越段階埋

この対応で重要なのは，状態の違いがステージの違込みを備えた言語のプログラム実行モデルを考える

いに対応していることである．このことより，部分計と，この制限はそれなりに妥当なのではないかと考え算における部分計算時の計算と残余プログラムの実ている．

行の区別が，状態の違いに対応していると理解でき，部分計算のように，ステージ毎のプログラムの実行∀α. ▷α τ 型のプログラムが (現在の状態を含めて) 到

環境が同一でない可能性がある状況と違い，MetaO-

達可能な任意の状態のコードとして使えること，a をCaml プログラムで扱われるデータとしてのコードは空列で具体化することで，run，すなわちコード辺を結局はそのプログラムの実行中に run するために構築

現在の状態で実行すること，として考えられるのでされるものである．すなわち，MetaOCaml プログラある．

ムにおけるステージの違いは見かけ上のもので，結局▷さて， [8] において与えられている λ に対応するは同じステージ・実行環境で実行されるものであり，論理体系を λ▷% の越段階埋込に関する規則 (から得ら実行環境の違いを表現していると考えられる状態をれる推論規則) で拡張することを考える． この体系に複数考える必要はない．また，3 節の冒頭で述べたよ

おいて，ステージは状態と対応するのであったから，うに，越段階埋込はいかなる簡約規則にも陽には現

この規則の意味するところは ”ある状態において成りれない，評価の順序を制御するための印にすぎず，越立っている命題はそこから到達できるいかなる状態に

段階埋込によって埋め込まれた値が使用されるのはおいても成り立つ” ということを意味する．しかし，それを取り囲むコード片が run によって実行される時

このような解釈では [8] で与えられていた Kripke 意(すなわち型付け規則に現れる α が ε で具体化される時) であるということから，型付け規則の妥当性を理応する論理体系をどのように拡張することによってえ解することができる．

られるかについて考察した．
今後の課題として，多相的な型システムの定義や

6 関連研究限定継続や参照などといった機構によってさらに λ▷%Tsukada と Igarashi [8] によって，λ▷ といくつかのαを拡張することがあげられる．

多段階計算との比較がなされている．特に，λ とそ

また， [8] において定義されていた λ▷ から遷移変れを制限した MetaOCaml の基礎となる計算体系であ数を取りのぞいた erasure semantics を同様に λ▷% へる λi [1] との比較が行われており， λi から越段階埋と拡張することも課題の 1 つである．

▷

込に関する部分を取り除いた体系が λ へと埋め込めることが示されている．
越段階埋込の意味については λ▷% と λα の間に，runの意味の違いに由来する差異がある．例えば，λ▷% において，(Λα.(▶α λx.%α (λz. ▶α x))) εというプログラムを評価すると，2 つの ▶α の両方が消え，λx.(λz.x) になる．それに対して， λα におけるこのプログラムと同等なプログラムは，run ((α) < λx.%(λz. < x >α >α ))となる． (λα では，< と > が bracket を表現し，(α) が

α を束縛していることを表わす) λα において，run は一番外側の bracket を外すことしかしない．単に一番
外側の bracket を外してしまうと，

λx.λz. < x >αのようになってしまう．このままでは， x のステージが合わないので，λα では，run が実行された時に、demo-

tion と呼ばれる操作を行い、越段階埋込の数を調節している．この場合，このプログラムは λx.λz. < %x >α
へと評価される．

7 おわりに
本稿では多段階計算の体系 λ▷ を越段階埋込によって拡張した言語 λ▷% を定義し， 2 つの操作的意味論と 1 つの型システムを与えた．また，それぞれの操作的意味論について合流性や型安全性を持つことを示した．さらに， λ▷% に対応する論理体系が λ▷ に対

参考文献[1] Calcagno, C., Moggi, E., and Taha, W.: ML-Like Inference for Classifiers, Proceedings of the European Symposium on Programming (ESOP’04), Schmidt, D.(ed.), Lecture Notes in Computer Science, Vol. 2986, SpringerVerlag, 2004, pp. 79–93.
[2] Davies, R.: A temporal-logic approach to binding-time
analysis, Proceedings of the Eleventh Annual IEEE Symposium on Logic in Computer Science (LICS 1996), IEEE
Computer Society Press, July 1996, pp. 184–195.
[3] Davies, R. and Pfenning, F.: A modal analysis of staged
computation, J. ACM, Vol. 48, No. 3(2001), pp. 555–604.
[4] Hindley, J. R. and Seldin, J. P.: Lambda-Calculus andCombinators an introduction, Cambridge University Press,
August 2008.
[5] Taha, W.: A Gentle Introduction to Multi-stage Programming, Domain-Specific Program Generation, Lengauer, C.,
Batory, D., Consel, C., and Odersky, M.(eds.), Lecture
Notes in Computer Science, Vol. 3016, 2004, pp. 30–50.
[6] Taha, W. and Nielsen, M. F.: Environment Classifiers,
Proceedings of the ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages (POPL’03), 2003,
pp. 26–37.
[7] Taha, W. and Sheard, T.: MetaML and multi-stage programming with explicit annotations, Theoretical Computer
Science, Vol. 248(2000), pp. 211–242.
[8] Tsukada, T. and Igarashi, A.: A Logical Foundation forEnvironment Classifiers, Logical Methods in Computer Science, Vol. 6, No. 4:8(2010), pp. 1–43.
[9] Yuse, Y. and Igarashi, A.: A Modal Type System for Multi-level Generating Extensions with PersistentCode, Proceedings of the 8th ACM SIGPLAN Symposiumon Principles and Practice of Declarative Programming(PPDP’06), Venice, Italy, 2006, pp. 201–212.