Locally Nameless 手法を使った型システムの健全性の証明
廣田知子

1(指導教官: 浅井健一)

はじめに

5

評価規則

型システムの重要な性質として健全性（つまり、型式の評価規則は e ; e0 で表現する。これは「e は e0チェックを通ったら、実行時には型エラーが決して起らへと評価できる」という意味である。以下に本研究にない）を挙げることができる。本研究では、定理証明系おける型システムの評価規則を示す。

システム Coq を用いて行われた Locally Nameless 手

e1 e2v e2法を用いた単純λ計算の型システムの健全性の既存の証明 [2] を拡張し、元のシステムに shift/reset を付加(λ.e) v
let e1 e2

した多相の型システム [1] における健全性を検証する。

2

Locally Nameless 手法

if e1 ; e01
if e2 ; e02; ev; let e01 e2

if e1 ; e01let v e ; ev(S.e1 ) e2 ; S.let λ.h1 (0 e2 )i e1v (S.e1 ) ; S.let λ.h1 (v 0)i e1

Locally Nameless 手法は、α-equality の問題を解消するための変数の名前付けの手法であり、自由変数にhei ; he0 i
hS.ei ; hlet λ.0 ei
hvi ; v

は x, y, ... 等の名前を付けるが、局所変数（束縛変数）には名前を付けず、de Bruijn index を採用する。局
所変数名を 0 以上の整数で表し、その式における一番内側の binder の変数名を 0 と考え、外にいくに従っ

if e ; e0

ここで ev は e の中に含まれる局所変数 0 に v を代入て 0, 1, 2,... と大きくしていく。例えば、λ 計算式のしたものを表す。

λx.λy.λz.y x z は λ.λ.λ.1 2 0 となる。

3; e01 e2; v e02

6

継続と shift / reset

型規則
式の型規則は以下の様に表記する。

shift/reset は継続を扱うための命令であり、これら
Γ; α ` e : T ; βを使ってプログラムの例外処理等を実現することが出来る。継続はいわば現在の計算が終了した後にする仕これは「型環境 Γ において、式 e は T 型を持ち、その事であり、shift は現在の継続を取得し、reset は取得実行によって継続の返す型が α から β に変化する」こする継続の範囲を限定する命令である。

4とを表す。又、どんな型 α においても Γ; α ` e : T ; α

型付き言語の構文が得られる時は以下の様に書く。

本研究で使用する型付き関数型言語の構文は以下のΓ `p e : T通り。

v

式:e := v| e1 e2|||

単相型 :
多相型 :

7:= n | x | λ.e

値:S.eheilet e1 e2(値)(関数適用)

型の推論規則上の表記法を使い、式を型付けするために必要な型の推論規則を以下に示す。

(shif t 式)
(reset 式)(let 式)ok Γ (x : M ) ∈ ΓΓ `p x : M Xs(var)∀x ∈/ L. (Γ, x : σ; α ` ex : T ; β)(f un)Γ `p λ.e : (σ/α → T /β)α, β, γ, δ := tb | tf | (α/γ → β/δ)A := α | ∀.AΓ; γ ` e1 : (σ/α → T /β); δ Γ; β ` e2 : σ; γ(app)Γ; α ` e1 e2 : T ; δn は局所変数、x は自由変数、tb は (n と同じく deBruijn index で表された) 局所型変数、tf は自由型変∀Xs ∈/ L. (Γ `p e1 : M Xs Γ, x : M ; α ` ex2 : T ; β)(let)Γ; α ` let e1 e2 : T ; β数を表す。(α/γ → β/δ) は α → β 型の関数で、実行
すると現在の継続の返す型が γ から δ に変化するよう∀x ∈/ L. (Γ, x : ∀.(T /0 → α/0); σ ` ex : σ; β)(shif t)Γ; α ` S.e : T ; βな式の型である。shift や reset が出てこなければ、γと δ は常に等しくなる。∀.A は多相の型を表す。∀ でΓ; σ ` e : σ; T(reset)Γ `p hei : T

束縛される型変数や shif t 式 S.e は λ 式と同じく deBruijn index で表される。
13Γ `p e : T(exp)Γ; α ` e : T ; α∀x ∈/ L2 . (Γ, x : ∀.(σ1 /0 → σ1 /0); σ ` ex : σ; T )(shif t)Γ; σ1 ` S.e : σ1 ; T(reset)Γ `p hS.ei : Tok (Γ, y : σ1 ) (y : σ1 ) ∈ (Γ, y : σ1 )(var)∀y ∈/ L3 . (Γ, y : σ1 `p y : σ1 )(exp)∀y ∈/ L3 . (Γ, y : σ1 ; α ` 0y : σ1 ; α)(f un)∀Xs ∈/ L1 . (Γ `p λ.0 : M Xs )∀x ∈/ L2 . (Γ, x : M ; σ ` ex : σ; T )(let)Γ; σ ` let λ.0 e : σ; T(reset)Γ `p hlet λ.0 ei : T
M = ∀.(σ1 /0 → σ1 /0),

Xs = α :: nil,M Xs = (σ1 /α → σ1 /α)

図 1: 型の推論規則の適用例（証明木）A
この規則の読み方は、B においては「B が成り立つ

評価前の式に推論規則を適用して証明木を作り、それためには A が成り立つ必要がある」である。例えばを用いて評価後の式の証明木が作れることを示してい定理 1 の証明は評価規則について場合分けを行い、(var) の規則は「Γ `p x : M Xs が成り立つためには型く。その例が図 1 である。図 1 では評価規則 hS.ei ;環境 Γ が ok であり、かつ x が M 型を持つという情報が Γ に含まれていなくてはならない」と読める。Γ

hlet λ.0 ei に関して hS.ei と hlet λ.0 ei のそれぞれに対して証明木を作成し、両式が同じ型を持つことを示が ok であるとは、Γ 中に現れる変数名が全て異なるした。評価前の式の証明木に現れる x は Γ; σ1 ` S.e :ことを意味している。又、M Xs は M 中に現れる局所

σ1 ; T に現れない（つまり Γ に現れない）変数なので、その条件を満たすように L2 を定めることが出来、評変数を全て自由変数のリスト Xs 中の要素で置き換えたものを表す。(f un) や (shif t) に現れる ∀x ∈/ L. はL に含まれない x(自由変数) を、(let) での ∀Xs ∈/ L.
は自由変数のリスト Xs のどの要素も L に含まれてい価後の式における証明木の (let) に現れる x も又 Γ に含まれない変数であるから、前者で定義した L2 を持ってくることが出来る。ここで例えば x を他のどこにもないことを表している。L には何も制限を付けていな現れない変数と規定すると、左式で現れる変数（Xs 中いので、後述の健全性の証明に際して自分で自由に Lの要素や y ）とも異なる必要があるので、(let) の時点を定めることが出来る。ex は上述の評価規則の場合とで値を定めることが出来ず、証明が複雑になる。これ同じである。

8が推論規則で x ∈/ L と定義した利点である。又、定理

Coq による定式化

2 の証明については型の推論規則で場合分けを行い、それぞれについて定理が成立することを示していく。

型システムとして、前述した言語の構文、式の評価

10

規則、型規則と型の推論規則を定式化するが、その前まとめと今後の課題にこれら諸規則の定式化に必要な、局所 (型) 変数を自本研究では単純λ計算に shift/reset を付加した多相由 (型) 変数に置き換える関数を導入する。その後さらの型システムにおける健全性を Locally Nameless 手に健全性の証明に必要となる諸々の補題を導入する。

法を用いて Coq 上で証明した。今後はこの型システム

なお、型規則が二種類存在するため、Coq においてはにさらに部分評価器を導入したシステムに関する健全型の推論規則を相互再帰的に宣言する。

性を Coq を用いて検証する予定である。

9型システムの健全性

参考文献

型システムの健全性 (Type Soundness) を証明する[1] Asai, K., and Y. Kameyama “Polymorphicには、以下の二つの定理が成立することを示せばよい。

Delimited Continuations,” APLAS’07, LNCS
4807, pp. 239–254 (November 2007).

定理 1 (type preservation)∧Γ; α ` e : T ; βe ; e0 ⇒ Γ; α ` e0 : T ; β∧Γ `p e : Te ; e0 ⇒ Γ `p e0 : T[2] Aydemir. B., A. Charguéraud, B. C. Pierce,
R. Pollack, and S. Weirich “Engineering For-定理 2 (type progress)∨ 0`p hei : T ⇒ e ∈ v∃e , hei ; e0mal Metatheory,” POPL’08, pp. 3–15 (January2008).
14