メタラムダ計算の定式化
理学専攻

情報科学コース

岩井亜里紗(指導教員：浅井健一)

はじめに

1f v(ζX. M )f v(M N )メタラムダ計算 (Meta Lambda Calculus, MLC)[1]とは、通常のラムダ式に加えて、メタレベルのラムダ式を扱うことができる計算体系である。これはプログラミング言語の視点から捉えると、2 レベルの式を扱うことのできるステージ言語の一つと考えられる。先行研究として、[2] においてメタラムダ計算の圏論的意味付けが与えられている。この中で、紙上による健全性の証明は行われているが、本研究では定理証明系である Isabelle/HOL における証明を行うことにより、より確かな定式化を得たいと考えている。

メタラムダ計算2

以下で、本研究で扱う MLC の型、構文、自由変数、変数の代入、型規則について述べる。

2.1

型

MLC の型は以下のように与えられる。
type
meta typeατ::=::=

Int | α → α(Γ ` α) | τ ⇒ τ

MLC では、ベースレベルの項とメタレベルの項を扱うため、型も 2 レベルの形で与えられている。→ と⇒ は、それぞれベースレベルとメタレベルの関数型を表わす。Γ は、ベースレベルのコンテキスト（ベースレベルの変数と型のペアの集合）であり、項 M が型(Γ ` α) を持つというのは、コンテキスト Γ のもとで、M が α 型を持つという意味である。
2.2構文

X
Λ

::=::=

X | X[Λ/x]c | x | λx. Λ | Λ Λ | X | ζX. Λ | Λ Λ

単純型付きラムダ計算 (Simply Typed Lambda Calculus, STLC) の構文に加え、メタレベルの構文が定義されている。メタレベルの項については、変数、関数抽象、関数適用を表わす構文を導入した。また、メタ変数に関しては、メタ変数に対する変数の代入も X[Λ/x]のように構文に導入されている。これは、X が具体的な項に置き換わった時点で、実際に変数の代入を行うためである。

2.3

自由変数

MLC の自由変数は、以下のように与えられる。
f v(x)f v(c)=={x}{}f v(λx. M )f v(M N )==f v(M ) − {x}f v(M ) ∪ f v(N )f v(X)f v(X[L/x])

=
=

G(X)
(f v(X) − {x}) ∪ f v(L)f v(M )f v(M )

mf v(x)mf v(c)mf v(λx. M )

=
=
={}
{}
mf v(M )mf v(M N )mf v(X)==mf v(M ) ∪ mf v(N ){X}

mf v(X[L/x])
mf v(ζX. M )mf v(M N )===mf v(X) ∪ mf v(L)mf v(M ) − {X}
mf v(M ) ∪ mf v(N )関数 G は、各メタ変数に自由変数の集合を割り当てる関数である。MLC では、この関数が与えられているものと考える。また、MLC の構文が相互再帰的に定義されていることから、ベースレベル、メタレベルともに自由変数の定義についても実際は相互再帰的に定義している。
これに付随して、各項に対してある変数 x が項の自由変数の集合に現れないことを示す、fresh の定義も行った。
Deﬁnition 1 (fresh variables)f resh x M = x ∈/ f v(M )Deﬁnition 2 (fresh meta-variables)
meta f resh X M = X ∈/ mf v(M )2.4

MLC の構文は、以下のように与えられる。

==変数の代入

MLC におけるベースレベルの変数の代入は、以下のように与えられる。ただし、x 6= y とする。
c[L/x] ≡ cx[L/x] ≡ Ly[L/x] ≡ y(λx. M )[L/x] ≡ λx. M(λy. M )[L/x] ≡ λy. (M [L/x])∗ただし、f resh y L(M N )[L/x] ≡ (M [L/x]) (N [L/x])
X[L/x] ≡ X[L/x](X[M/y])[L/x] ≡ X[M/y][L/x](ζX. M )[L/x] ≡ ζX. (M [L/x])∗ただし、meta f resh X L(M N )[L/x] ≡ (M [L/x]) N
2.5

型規則

MLC の judgment は以下のような形で表わされる。
∆°M :τ

ここで、∆ は、メタレベルのコンテキスト（メタレベルの変数と型のペアの集合）、M は項、τ は、メタレベルの型を表わす。
実際に使用される型の推論規則は以下の通りである。

∆ ° c : (Γ ` Int)

(CON )∆ ° x : (x : α, Γ ` α)

(V AR)∆ ° M : (x : α1 , Γ ` α2 )(LAM )∆ ° λx. M : (Γ ` α1 → α2 )∆ ° M : (Γ ` α1 → α2 ) ∆ ° N : (Γ ` α1 )(AP P )
∆ ° M N : (Γ ` α2 )X : τ, ∆ ° X : τ∆ ° X : τ14

初めに、ベースレベルの α、β 、η 変換の健全性を示すために必要な代入補題の証明を行った。
Lemma1 (Base-level Substitution Lemma)

Γ ° M : τ1(M V AR1)x ∈/ f v(X) weaken x τ1 τ2(M V AR2)
∆ ° X : τ2Isabelle による定式化

Γ ° N : τ2 sub rel x τ1 τ2 τ3
Γ ° M [N/x] : τ3

P roof. 項 M に関する帰納法より。

X : τ1 , ∆ ° M : τ2(M LAM )∆ ° ζX. M : τ1 ⇒ τ2

また、代入補題の証明に必要な、メタレベルのコンテキストにおける weakening の証明も行った。
Lemma2 (Meta-level Weakening)∆ ° M : τ1 ⇒ τ2 ∆ ° N : τ1(M AP P )∆ ° M N : τ2

Γ ° M : τ1 meta f resh X MX : τ2 , Γ ° M : τ1

∆ ° X : τ1

∆ ° M : τ2 sub rel x τ1 τ2 τ3(SU B)∆ ° X[M/x] : τ3(SUB) の型推論に含まれる sub rel x τ1 τ2 τ3 は、メタレベルの型が二通りあるために導入したものである。
具体的には、以下のように定義している。
sub rel x (x : α1 , Γ ` α2 ) (Γ ` α1 ) (Γ ` α2 )sub rel x τ1 τ2 τ3
sub rel x (τ ⇒ τ1 ) τ2 (τ ⇒ τ3 )また、weaken x τ τ 0 とあるのは、型 τ をベースレベルの変数 x で weakening した結果が τ 0 になるという意味である。

3

このように、項 (ζX. (λx. X) c) x は定数 c へと変換されるが、メタレベルの関数適用の引数 x は、関数部分に含まれる λx に束縛されている。つまりこの場合、xはこの式の自由変数に含まれず、Nominal Isabelle を使用すると問題が生じてしまう。以上のような理由により、Nominal の機能を含まない Isabelle による証明へと変更した。

Isabelle/HOL

Isabelle/HOL は、高階論理に基づく定理証明系である。Isabelle で使用される記述言語を Isar と言い、人が書く証明に近いスタイルの証明を記述することができる。また Nominal Isabelle という、Isabelle/HOL の拡張で、Nominal Logic に基づく定理証明系も存在する。これは、α 変換などの問題を上手く解決できるもので、STLC などはこの Nominal Isabelle を用いると比較的楽に証明することができる。本研究でも当初、こちらの Nominal Isabelle による証明を行っていたが、メタラムダ計算では通常のラムダ計算と自由変数の定義が異なるため、使用できないことがわかった。具体的な例として、MLC の式とその変換を提示する。
(ζX. (λx. X) c) x=M β((λx. X) c)[x/X]==β=(λx. x) cx[c/x]c

P roof. 項 M に関する帰納法と、型の推論木に関する帰納法より。
ただし、MLC の構文がメタ変数とその他の項とで相互再帰的に定義されているため、提示したいずれの補題も相互再帰の形をとっている。

5

まとめと今後の課題

本研究では、ステージ言語の一つであるメタラムダ計算の定式化に向けて、構文などの各種定義とベースレベ
ルの代入補題の証明、そしてメタレベルの weakeningの証明を、Isabelle を用いて行った。残りのベースレ
ベルの weakening、α、β 、η 変換の証明、そしてメタレベルについても同様に証明を行い、定式化を完成させることが今後の課題である。また、[2] における証明と今回 Isabelle 上にて行った証明との違いについても考察したい。

参考文献[1] Bekki, D. ”Monads and meta-lambda calculus”,
In Hattori, H., editor, New Frontiers in ArtiﬁcialIntelligence (JSAI 2008 Conference and Workshops, Asahikawa, Japan, June 2008, Revised Selected Papers), volume LNAI 5447, pp.193-208,
Springer, 2009.
[2] 増子萌. 戸次大介. ”メタラムダ計算の圏論的意味論”, 第 13 回プログラミングおよびプログラミング
言語ワークショップ (PPL2011), pp.60-74, 2011.