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

無限の入出力を行う関数型プログラムの K 正規化の形式的検証
水野 雅之

住井 英二郎コンパイラの形式的検証は盛んに研究されているが，入出力等の副作用がある高階関数型プログラミング言語のコンパイラの検証はあまり行われていない．これは無限に入出力を行うプログラムの意味論の形式化が自明でないためである．我々は，入出力等の副作用を持つ外部関数の呼び出しや再帰関数，高階関数，組を持つ値呼びの関数型プログ
ラミング言語に対する K 正規化を定理証明支援系 Coq を用いて形式的に検証した．K 正規化とは let 式を用いて全ての中間式に対し陽に名前を与えるプログラム変換であり，束縛の操作を伴う点で形式化が自明でない．本研究では，余帰納的大ステップ操作的意味論によりプログラムの意味を外部関数呼び出しの無限列として与えた．また，束縛の表現としては，他の手法と比較検討した上で de Bruijn インデックスを採用した．

Although formal verification of compilers is extensively studied, compilers for higher-order functional programming languages with side eﬀects such as input and output are rarely verified. This is due to the diﬃcultyof formalizing the semantics of programs performing infinite input and output. We have mechanically verified the K-normalization of call-by-value higher-order functional programs with recursive functions, pairs,and external function calls that can possibly cause side eﬀects, by the Coq proof assistant. K-normalization
is a program transformation that gives explicit names to all subexpressions via let-expressions. Its formalization is non-trivial because of the manipulation of bindings. We defined the meanings of programs
as infinite sequences of external function calls, using coinductive big-step operational semantics. We also
adopted de Bruijn indices by comparison with other techniques to represent bindings.

いといった問題のためである．

1 序論

例えば，コンパイラの形式的検証の中でもよく知1. 1 背景られた研究として，CompCert [2] が挙げられる．こコンパイラの誤りは生成されるコードに影響を及れは C 言語のほとんどの機能をサポートするコンパ

ぼすため，信頼性の高いソフトウェアを開発するためイラを Coq によって検証する試みである．C 言語にには信頼性の高いコンパイラが必要である．そのたは入出力の機能が含まれているため，CompCert でめ，定理証明支援系によるコンパイラの形式的検証も入出力の機能はサポートされている．その一方，Cが盛んに試みられてきた．しかしながら，入出力等の言語では自由変数を持つ関数が許されていない上，副作用がある高階関数型プログラミング言語のコン

CompCert では関数定義の先頭でしか変数を宣言でパイラに対する形式的検証はあまり行われていない．

きないため，束縛の操作は限定的となっている．

これは，(自由変数を持つ) 関数を第一級の値として本研究と類似した，純粋でない関数型プログラミ

扱える言語は複雑な束縛の操作を伴うほか，無限に入ング言語を対象とするコンパイラの検証としては出力を行うプログラムの意味論の形式化が自明でな

Lambda Tamer [5] が挙げられる．その対象言語は高Formal Verification of Functional Programs Performing Infinite Input/Output
Masayuki Mizuno, Eijiro Sumii, 東北大学大学院情報科学研究科, Graduate School of Information Sciences,Tohoku University.

階関数，参照，例外，二つ組といった機能を有している一方，入出力はサポートされていない．

1. 2 本研究の貢献

Bruijn インデックスを採用した理由を述べる．5 節

本研究では，無限に入出力を行うことができる高階

では de Bruijn インデックスを採用した K 正規化の関数型プログラミング言語のコンパイラの一フェーズ実装について述べる．6 節では余帰納的大ステップ意である K 正規化の形式的検証を行う．K 正規化とは，味論に基づく，対象言語の意味論について説明する．

let 式を用いて全ての中間式に対し陽に名前を与える

7 節では K 正規化の正当性の証明について説明し，8プログラム変換である．

節では結論を述べる．

関数型プログラミング言語の形式化では，束縛の表現が重要な問題の一つになる．本研究では取り扱

2 対象言語いの容易さから de Bruijn インデックスを採用した

本研究における対象言語の構文は図 1 の通りであ(4 節)．

る．プリミティブとして定数（整数や真偽値），算術

対象言語の意味論は余帰納的大ステップ意味論によ演算，if や let，再帰関数や二つ組を持つ．本研究のり定義した (6 節)．これは，通常の帰納的大ステップ手法は論理関係と異なり，再帰関数の扱いが容易であ意味論では無限に入出力を行うプログラムの意味をることを示すため，再帰関数はプリミティブとしてい定義できず (行き詰まり状態すなわちエラーとなり評る．fix f x. e の e において f が現れない場合は関数価できないプログラムと区別がつかない)，また，小抽象 λx. e に等しい．let x = e1 in e2 は (λx. e2 ) e1

ステップ操作的意味論では評価文脈や内部遷移の扱いで表せるが，K 正規形を表すためにプリミティブとしが煩雑になるためである．ている．算術演算としては加算，減算，乗算と比較演

無限の入出力を含む関数型プログラミング言語

算が実装されている (除算などを扱うためには対象言の処理系の検証としては，本研究と独立に行われた語を例外処理で拡張する必要があると思われる)．本

CakeML [10] と Pilsner [7] も挙げられる．CakeML

研究の対象言語では関数の引数の数や，同時に定義さはソース言語では名前によって束縛を表現している一れる再帰関数の数，及び組の要素の数を一つか二つに方，中間言語では de Bruijn インデックスを用いてい固定している．これは構文木の帰納的定義において，る．また，ソース言語ではクロックとタイムアウトに任意長の再帰的出現の扱いが Coq では困難だったた

よって拡張された大ステップ操作的意味論を用いていめである．

る一方，中間言語では小ステップ操作的意味論を用い入出力専用の構文は存在しないが，自由変数にている．正当性の証明は本研究と同じように，評価結対する関数呼び出しは外部関数の呼び出しとみな果同士の対応関係を定義することで命題を一般化しし，外部関数が副作用を持つことを許す．例えば，式ている．一方，Pilsner は束縛を名前によって表現しprint int 42 を評価すると，自由変数である外部関ているほか，対象言語の意味を定めるために小ステッ

数 print int が引数 42 に適用され，値を返す．ただプ操作的意味論を用いており，また，正当性の証明にし，簡単化のために外部関数は整数を受け取って整数は論理関係 (logical relation) を用いている．これらを返すものに限定する．以上のような意味論は 6 節の手法は後に述べる理由により，本研究の手法より証で定義する．

明が煩雑になると思われる．
本研究の Coq のソースコードは https://github.

com/fetburner/sotsuron/blob/master/kNormal.vで公開している．

3 K 正規化本研究ではコンパイラが行う処理のうち，束縛の付け替えを伴う非自明なプログラム変換である K 正規化に注目する．K 正規化とは，与えられたプログラム

1. 3 本論文の構成を中間表現の一つである K 正規形 [1] に変換する操作

2 節では本研究の対象言語を，3 節では K 正規化をである．K 正規形とは直観的には全ての部分式を変数説明する．4 節では束縛を表現する手法を概説し，deに束縛して名前を付けた形式である．式 e の K 正規形

ev

式る．本節ではこれらの手法を比較検討し，本研究でc定数de Bruijn インデックスを採用する理由を述べる．

|

e1 ⊙ e2

算術演算|

if e1 then e2 else e3

条件分岐

4. 1 de Bruijn インデックス|

let x = e1 in e2

変数定義

De Bruijn インデックスは，内側から数えて何番目|x

変数の束縛に対応するかにより変数の出現を表現する手|

fix f x. e

再帰関数法である．例えば，名前によって束縛を表現した式

|

e1 e2

関数呼び出しλx. x(λy. x y) を de Bruijn インデックスで表現する|(e1 , e2 )二つ組の作成と λ. 0 (λ. 1 0) となる．De Bruijn インデックスで|πi e

射影 (i ∈ {0, 1})

は代入の際にシフトと呼ばれる操作が必要になる．例

値えば，λz. (λx.λy. x) z を λz.λy. z に簡約する場合，c

定数de Bruijn インデックスでは前者は λ. (λ.λ. 1) 0，後|x外部関数

者は λ.λ. 1 となり，変数 z の出現のインデックスが|fix f x. e

再帰関数

0 から 1 に増えている．このようにインデックスを増|(v1 , v2 )二つ組

やす操作をシフトと呼び，一般に式 e に現れる全ての::=::=

図1

対象言語の抽象構文

自由変数のインデックスを d ずつ増やした式を ↑d eと表す．

k::=

本研究では de Bruijn インデックスを採用しつつ，自由変数は名前で表現している．例えば式cx1 ⊙ x2
if x then k1 else k2
let x = k1 in k2(fix f x. print int x) 42
は Coq 上ではApp (Fix (App (ExtVar v) (Var 1))) (Int 42)x(ただし v は print int を表す自然数) と表される．

fix f x. k

De Bruijn インデックスのシフト操作に伴う算術演算

xyや，それに関する証明は必要となるが，Presburger(x, y)算術などによりほぼ自動化できる．

πi x
図2K 正規形の抽象構文

4. 2 局所名前無し表現
局所名前無し表現 [3] は名前による束縛の表現とを K(e) と書くことにすると，例えば e1 + e2 の K 正

de Bruijn インデックスの折衷案であり，自由変数は規形は let x1 = K(e1 ) in let x2 = K(e2 ) in x1 + x2

名前によって表現し，束縛変数は de Bruijn インデッと表される．図 2 に K 正規形の抽象構文を示す．

クスによって表現する．ただし上述の我々の手法とは異なり，例えば先の λz. (λx.λy. x) z を λz.λy. z に4 束縛の表現簡約する場合，まず前者の λz に対し open と呼ばれ紙の上で定式化を行う場合によく用いられる名前にる操作を行い，本体を fresh な z に対し (λ.λ. 1) z とよる表現は，α 等価性の取り扱いや変数の捕獲 (cap-表してから λ. z に簡約した後，close と呼ばれる操作ture) の回避が面倒であるという欠点が存在する．そを行い λ.λ 1 を得る．このように局所名前無し表現でれらの欠点を回避した束縛の表現として，de Bruijn

はシフト操作が不要になる一方，(λ.λ. 1) z のようにインデックス [8]，局所名前無し表現 [3] やパラメト

open された本体が元の式の部分式にならないため，

リック高階抽象構文 (PHOAS) [4] といった手法があK 正規化のような帰納的定義の停止性や，K 正規化

の結果に対して locally closed という性質を証明する

われたかで表され，引数 n により外部関数 x を呼び必要があり煩雑である．また，open や close につい出して戻り値 m が得られたことを x(n) = m と書くての補題も必要となる．

ことにする．対象言語の評価規則の一部を図 4 に示
す．代入の代わりに環境を用いて対象言語の意味を定

4. 3 パラメトリック高階抽象構文義することもできるが．環境を用いた場合は形式的検

高階抽象構文 (HOAS) とは，対象言語の束縛をホス証の際にクロージャ同士の等価性の議論が煩雑になるト言語の束縛で表す手法である．例えば，λx. x を表ため，本研究では代入を用いた意味論を採用した．

す抽象構文木は Abs (fun x ⇒ x) となる．PHOAS [4]は HOAS の改良であり，式の負の位置の再帰的出現

6. 2 余帰納的大ステップ操作的意味論

を型パラメターで置き換えることにより，Coq のよ大ステップ操作的意味論において停止しない評価

うな定理証明支援系において帰納的定義を可能としと行き詰まり状態を区別するため，余帰納的大ステッている．PHOAS は名前の付け替えや代入をメタ言語

プ操作的意味論が提案されている [6]．これは，評価に任せることができる一方，束縛に関する証明においが停止しないことを表す述語を余帰納的に定義するてメタ言語の性質に関する証明が必要となり，しばしことで，通常の帰納的な評価規則を補うものである．

ば本質的な困難がある．

余帰納的大ステップ操作的意味論を用いた，本研究の対象言語の評価規則の一部を図 5 に示す (二重線は余5 K 正規化の実装

帰納的規則を表す．Coq では単に CoInductive を用

本節では de Bruijn インデックスで束縛を表現したいている)．

場合，どのように K 正規化が実装されるかを述べる．

本研究では入出力を扱うため，評価関係を式 e

例えば if true then e1 else e2 の K 正規化を考えと，評価の際に行われた入出力の列 t (無限列でもる．名前による表現では，新しい変数名 a を選べばよい) との二項関係 e ⇑ / t としている．これによっ

let a = true in if a then K(e1 ) else K(e2 ) のよて評価が停止しないプログラム同士も入出力の内容

うに単純に let を挿入するだけで K 正規形が得られで区別できる．例えば (fix. 0 1) (print int 42) とる．一方，de Bruijn インデックスによる表現では let(fix. 0 (print int 42)) 0 は共に停止しないプログが挿入されると束縛の対応関係がずれてしまうため，ラムであるが，前者は一回のみ print int の呼び出

let true in if 0 then ↑ K(e1 ) else ↑ K(e2 )しが行われるのに対し，後者は無限回の呼び出しがのようにシフト操作が必要となる．本研究における行われる点で異なる．本研究の評価規則では前者はK 正規化の実装の一部を図 3 に示す．

(fix. 0 1) (print int 42) ⇑ / print int(42) = 0

1

1が 成 り 立 ち ，後 者 は (fix. 0 (print int 42)) 0 ⇑6 意味論/ print int(42) = 0, print int(42) = 0, · · · が成り

6. 1 大ステップ操作的意味論

立つ．行われる入出力の列が異なることから，両者を本研究では対象言語の意味論として大ステップ操区別できる．

作的意味論を採用する．大ステップ操作的意味論の評

本研究では余帰納的大ステップ操作的意味論を選択

価規則は構文とほぼ一対一に対応しており，プログラしたが，入出力を含む言語の意味を定義する手法としム変換の検証には小ステップ操作的意味論より適してラベル付きの小ステップ操作的意味論も知られていている．本研究では入出力を扱うために，一般的な大る．双模倣を用いれば余帰納的大ステップ操作的意味

ステップ操作的意味論を入出力の列によって拡張し，論と同様に無限に入出力を行うプログラム同士の等評価関係を式 e，評価結果 v ，評価の際に行われる入価性を議論できる利点はあるが，入出力を含む簡約と出力の (有限) 列 t との三項関係 e ⇓ v / t とする．こ

入出力を含まない簡約 (内部遷移) を区別して扱わな

こでの入出力は，どのような外部関数呼び出しが行くてはならず，弱双模倣性の定義や up-to reduction

K(c)

≡c

K(if e1 then e2 else e3 )≡let K(e1 ) in if 0 then ↑1 K(e2 ) else ↑1 K(e3 )K(let e1 in e2 )≡let K(e1 ) in K(e2 )

K(x)

≡x

K(fix. e)≡fix. K(e)K(e1 e2 )≡let K(e1 ) in let ↑1 K(e2 ) in 1 0

図3

K 正規化の実装の一部

fix. e ⇓ fix. e /e1 ⇓ fix. e / t1

E-Fix

e2 ⇓ v2 / t2

[0 7→ fix. e, 1 7→ v2 ]e ⇓ v / t3
E-AppFixe1 e2 ⇓ v / t1 t2 t3

▷cx

▷

x

∀i ∈ {2, · · · , n + 1}. vi ▷ vi′
fix. [2 7→ v2 , · · · , n + 1 7→ vn+1 ]ee1 ⇓ x / t1
e 2 ⇓ n / t2
E-AppExtVar
e1 e2 ⇓ m / t1 t2 , x(n) = m
図4c′▷ fix. [2 7→ v2′ , · · · , n + 1 7→ vn+1]K(e)v1 ▷ v1′v2 ▷ v2′(v1 , v2 ) ▷ (v1′ , v2′ )本研究における対象言語の評価規則の一部

図6e1 ⇑ / t1

値同士の対応関係

D-AppLe1 e2 ⇑ / t 1なる

e1 ⇓ fix. e / t1e2 ⇑ / t 2

e1 e2 ⇑ / t1 t2
e1 ⇓ fix. e / t1

定理 2. e ⇑ / T が成り立つならば K(e) ⇑ / t が成D-AppRり立つ
しかし，定理 1 を帰納法によって証明しようとす

e2 ⇓ v2 / t2

[0 7→ fix e, 1 7→ v2 ]e ⇑ / t3
e1 e2 ⇑ / t1 t2 t3
図5ると帰納法の仮定が弱すぎるため，一般化が必要とD-Appなる．その際一見誤った命題 1 が成り立つように思

余帰納的大ステップ意味論を用いた評価規則の一部

える．
誤った命題 1. e ⇓ v / t が成り立つならば K(e) ⇓などの手法が必要になる．

K(v) / t が成り立つ
実際，二つ組のように複合的な値が存在しなけれ

7 Coq による形式的検証

ばこの性質は成り立つが，本研究の対象言語は二つ

K 正規化に期待される性質について考える．K 正組を含むため，反例が存在する．例えば v = (v1 , v2 )規形はソース言語のサブセットになっているが，値呼の場合，K(v) = let v1 in let ↑1 v2 in (1, 0) となびの評価戦略では関数抽象の中は簡約されないため，り，K(v) が値にならず，K(e) ⇓ K(v) / t は成り立K 正規後のプログラムは K 正規化前のプログラムとたない．

値呼びの簡約では等価ではない．従って，プログラムそこで，対象言語の式を評価した結果として得らの振る舞いに注目した等価性を考える．プログラム

れる値と，K 正規形を評価した結果として得られ全体の実行結果は整数または真偽値になるとすると，る値との間に成り立つことが期待される図 6 の関以下の二つの定理が期待される．

係 v ▷ v ′ を定義する．これを用いた以下の補題は′定理 1. e ⇓ v / t が成り立つならば K(e) ⇓ v / t′が成り立ち．v が整数または真偽値ならば v = v と[0 7→ e0 , · · · , n − 1 7→ en−1 ]e の導出についての帰納法で証明できる．

補題 1.

した結果，比較的簡潔な証明が可能となった．

[0 7→ v0 , · · · , n − 1 7→ vn−1 ]e ⇓ v / t

謝辞

かつ∀i ∈ {0, · · · , n − 1}. vi ▷ vi′が成り立つならば，

い た 松 田 一 孝 先 生 に 感 謝 し ま す．本 研 究 は JSPS′]K(e) ⇓ v ′ / t[0 7→ v0′ , · · · , n − 1 7→ vn−1′

本 稿 を 執 筆 す る に あ た り 様々な コ メ ン ト を 頂′及び v ▷ v が成り立つような v が存在する

科 研 費 JP22300005，JP25540001，JP15H02681，

JP16K12409 の助成を受けた．

ここで ∀i ∈ {0, · · · , n − 1}. vi ▷ vi′ となるような値 vi および vi′ を代入してから評価しているのは，関参 考 文 献

数適用や let のように評価の際に代入が伴う場合でも[ 1 ] Birkedal, L., Tofte, M., and Vejlstrup, M.: FromRegion Inference to Von Neumann Machines via Region Representation Inference, POPL ’96.
[ 2 ] Blazy, S., Dargaye, Z., and Leroy, X.: Formal
Verification of a C Compiler Front-End, FM ’06:
Int. Symp. on Formal Methods.
[ 3 ] Charguéraud, A.: The Locally Nameless Representation, Journal of Automated Reasoning, (2011),
pp. 1–46. 10.1007/s10817-011-9225-2.
[ 4 ] Chlipala, A.: Parametric Higher-order Abstract
Syntax for Mechanized Semantics, ICFP ’08, ACM.
[ 5 ] Chlipala, A.: A Verified Compiler for an Impure
Functional Language, POPL ’10.
[ 6 ] Leroy, X. and Grall, H.: Coinductive bigstep operational semantics, Inf. Comput., Vol. 207,No. 2(2009), pp. 284–304.
[ 7 ] Neis, G., Hur, C., Kaiser, J., McLaughlin, C.,
Dreyer, D., and Vafeiadis, V.: Pilsner: a compositionally verified compiler for a higher-order imperative language, ICFP ’15.
[ 8 ] Pierce, B. C.: Types and Programming Languages, MIT Press, 2002.
[ 9 ] Pierce, B. C.: Advanced Topics in Types andProgramming Languages, The MIT Press, 2004.
[10] Tan, Y. K., Myreen, M. O., Kumar, R., Fox, A.,
Owens, S., and Norrish, M.: A New Verified Compiler Backend for CakeML, ICFP ’16.

帰納法の仮定を用いるためである．図 6 の定義でも代入を導入している理由は，式 e が関数抽象 fix. e′の場合に本体 e′ に値 vi が代入されても関係 v ▷ v ′ が成り立つようにするためである．
なお，プログラムの等価性を証明するためによく用いられる手法の一つに論理関係 [9] があるが，再帰関数を含む言語や型無しの言語 (ないし再帰型を含む言語) では定義が煩雑になるため，本研究では用いなかった．

8 結論
入出力等の副作用を持つ外部関数の呼び出しや再帰関数，高階関数，組を持つ値呼びの関数型プログ
ラミング言語に対する K 正規化を，定理証明支援系

Coq を用いて形式的に検証できた．無限の入出力も考慮しつつ様々な手法を比較検討して，余帰納的大ス
テップ操作的意味論と de Bruijn インデックスを採用