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

検証済みのコードによる Coq から Scala へのコード
抽出
逸見 港

田辺 良則

今井 宜洋

萩谷 昌己

定理証明支援系 Coq では，記述したアルゴリズムとその正当性証明から OCaml や Haskell などの関数型言語のコードを抽出することができる．本研究では Scala コードの抽出を目標とする．従来の抽出手順は，Coq の項を MiniMLと呼ばれる中間言語の構文木に変換したあと抽出先言語のコードとして書き出すというものである．MiniML は本
質的には型なしλ計算であるため，型を明示する必要がある Scala コードの書き出しはできない．そこで私たちは，アルゴリズム M をベースにして MiniML の項に型の情報を付加する方式を取ることにし，この方式で抽出された
コードは型検査を通ることを証明した．この方式自体を Coq 上で記述・証明して OCaml へ抽出することにより，Scala コード抽出プログラムを得た．

れる．Letouzey [3] はこれらの性質を満たす OCaml

1 はじめにへのコード抽出アルゴリズムを考案した．

プログラムの検証手法の一つに，満たすべき性質

上記の言語以外にも，Scala [7] にコード抽出できを定理として記述してその証明をする定理証明があれば Coq の利用機会が広がる．Scala は Java 仮想マ

る．Coq [6] は定理証明を支援するシステムの一つでシン上で動作するため，これによって広く使われてあり，関数，型，命題を関数型言語のスタイルで記述いる言語である Java のプログラムから検証済みのする．命題には対話的に証明を付けることができる．

関数を呼び出すことができる．しかし従来の方法でCoq には，記述した関数と正当性証明を他の関数

は，型を明示する必要がある Scala へコード抽出す

型言語にコード抽出する機能がある．抽出先の言語ることはできない．なぜならその方法では，Coq かとしては OCaml、Haskell、Scheme が公式にサポーら MiniML と呼ぶ中間言語へ変換したあと抽出先言トされている．この機能を利用すると，他言語でプロ語のコードとして書き出すという手順を踏んでおり，グラムを書いているとき，検証したい一部分の関数

MiniML に変換する過程で型の情報が捨てられてしを Coq 上で実装し，正当性を証明したのちにコードまうからである．

抽出することで元の言語から呼び出すということができる．

Scala コードの書き出しは，MiniML に型の情報が加わった言語 MiniML′ の項からであれば可能であ

コード抽出自体の正当性としては抽出したコードがる．MiniML′ の項を作るために考えられる方針の一

型検査を通ること (型の妥当性) と，抽出の前後で計算つとして，既存のコード抽出の実装に手を加えるこ

が等しいこと (計算の妥当性) の二つの性質が考えらとで，Coq から MiniML への変換と同様に Coq から

MiniML′ に変換するというものが考えられる．しかVerified Code Extraction from Coq to Scala
Ko Hemmi，Masami Hagiya, 東京大学, The Universityof Tokyo.
Yoshinori Tanabe, 国立情報学研究所, National Institute of Informatics.
Yoshihiro Imai, 有限会社 IT プランニング, IT Planning,
Inc..

しこの方針では，既存の実装に変更があるたびに対応しなければならないという短所がある．
私たちはこれとは別の方針によって MiniML′ の項を作り，Scala へのコード抽出を可能にした．この抽出方式では，Coq から MiniML への変換，MiniML

から MiniML′ への変換という二段階の変換を行う．

例 2.1

一段階目は既存の実装をそのまま利用できるので，こInductive nat : Set :=の部分の実装に変更があっても対応する必要がない．

| O : nat

本研究では二段階目の変換を実現する型推論アルゴ| S : nat -> nat.

′′

リズム M を定義したあと，この新しい抽出方式は型の妥当性を満たすことを証明した．
アルゴリズム M′′ の実装と証明は Coq 上で行った．
それによって証明に誤りがないことを確認するとともに，M′′ 自体をコード抽出することで検証済みの M′′のコードを利用した Coq から Scala へのコード抽出を OCaml で実装できた．このプログラムによって抽出される Scala コードが型検査を通ることは保証されている．
本論文の構成は以下のとおりである．第 2 節で従来のコード抽出について述べる．第 3 節では新しい

Scala へのコード抽出方式の概略と，その核となるア
ルゴリズム M′′ について説明する．第 4 節ではコー

これは自然数の要素が以下の 2 つのコンストラクタで構成されることを表す．

1) O は自然数である．
2) n が自然数ならば，S n は自然数である．
この定義に則ると 0 は O，1 は (S O)，2 は (S (S O))
で表現される．
次の nat or bool という集合は真偽値から型への関数であり，引数の b が真ならば nat，偽ならば bool
を返す．
例 2.2

Definition nat_or_bool : bool -> Set :=fun b : bool =>ド抽出の正当性とその証明について述べる．第 5 節

if b then nat else bool.

では最終的に書き出される Scala コードについて述べる．第 6 節では Coq で行った実装について述べる．
最後の節でまとめと今後の課題について述べる．

zero or false は引数の b が真ならば自然数 0，偽ならば偽を返す．この返り値は nat or bool b という型が付くので定義可能である．

2 従来のコード抽出
2. 1 Coq における定義
通常の言語では，型と項を明確に区別する．型とは
集合 (たとえば整数) に対応し，その型を持つ項はその集合に属する要素 (たとえば 1) に対応する．

例 2.3

Definition zero_or_false :
forall b : bool, nat_or_bool b :=fun b : bool =>match b with

それに対して Coq の型には集合と命題の二種類が| true => O

ある．集合に要素が属するように，命題にはその命題| false => falseの証明が属している．また Coq においては型自身もend.

項である．つまり，Coq の項には集合・要素・命題・証明が含まれる．この他に集合と命題両方を含むような型も存在するが，話を簡単にするため本論文では触
れない．

例 2.4

Definition zero_or_false_true : nat :=zero_or_false true.

以下に Coq の項の定義例として，Inductive コマ
ンドによる集合の帰納的定義と Definition コマン

次の subtract は自然数の差を計算する関数である．

ドによる集合の定義，Definition コマンドによる要

2 つの自然数 m と n に加えて m < n であるという素の定義を載せる．

命題の証明を受け取り，n = m + d であるような自自然数 (nat) という集合は Coq では以下のように帰納的に定義される．

然数 d を返す．

MiniML と呼ぶ中間言語に変換する．MiniML は通常の関数型言語のサブセットとなっているので，Min-

例 2.5

Definition subtract :forall m n : nat, m<n ->{d : nat | n = m+d}.
induction m.
intros.
exists n; auto.
destruct n.
intros.
contradict H; apply lt_n_0.
intros.
apply lt_S_n，(IHm n) in H.
destruct H as [d Hd].

iML の項や型は自然に OCaml や Haskell のコードとして書き出すことができる．

CIC の項からコード抽出する具体的な手順は以下のようになる [3]．Ê は CIC の集合を MiniML の型に変換する関数，E は CIC の要素を MiniML の項に変換する関数である．抽出例として第 2. 1 節の Coq
上の定義を OCaml へ抽出したコードを載せる．

• 命題・証拠の抽出
抽出しない．

• 帰納的な集合の抽出
各コンストラクタの型 Ti に Ê を適用して Min-iML の型を得る．コンストラクタがその型を持つものとして書き出す．

exists d; rewrite Hd; auto.
Defined.
このように定義すると，subtract は次のように

n − m の計算をする．

例 2.6

type nat = O | S of nat• 帰納的でない集合の抽出 Ê を適用して MiniML(1) m が 0 である場合 n を返す．

の型を得る．それを抽出先言語の型として書き(2) m が 1 以上の場合

出す．

(2-1) n が 0 の場合，m < n に反するのでありえない．

(2-2) n が 1 以上の場合，帰納的に (n−1)−(m−1)
を計算して返す．

m < n であるという命題の証明は自然数 n − m が存在することを言うために使われており，計算結果には直接影響していない．

例 2.7

type nat_or_bool = Obj.t
引数の真偽値に依存するような型は通常の言語では表せないため，どんな値でも持つことができる型に変換される．OCaml の場合は Obj.t である．

• 要素の抽出2. 2 コード抽出の手順
Coq で記述されたプログラムは内部では Calculusof Inductive Construction (CIC) と呼ばれる言語で表現される．上の例で見たように，CIC では命題・証
明・型を要素と同等に扱うことで複雑な項を表現できる．しかし subtract においてそうだったように，命
題・証明・型の部分は計算結果に影響しない．コード
抽出とは CIC からそのような部分を消去し，計算に要素 t とその型 T からは次の手順で抽出する．

1. MiniML の型 TMiniML =Ê(T ) を得る．
2. MiniML の項 tMiniML =E(t) を得る．
3. tMiniML が TMiniML を型として持つかどうか検査する．持たなければ，tMiniML の必要なところに型キャストを挿入する．

4. 型キャスト挿入後の MiniML の項を抽出先
言語のコードとして書き出す．

関係のある部分のみを取り出して別の言語のコードとして書き出すことである．
従来のコード抽出の手順では，CIC の項を一度

例 2.8

let zero_or_false = function

| true -> Obj.magic O

O.asInstanceOf[Nat_or_bool]| false -> Obj.magic false

case False =>let zero_or_false_true =Obj.magic (zero_or_false true)
zero or false の 型 は bool → nat or bool に ，zero or false true の型は nat に変換され，項がこれらの型を持つように型キャストが挿入される．単に

let zero_or_false = function| true -> O
| false -> falseとすると OCaml では型が付かないので，型キャ
スト Obj.magic は必要である．

False.asInstanceOf[Nat_or_bool]}def zero_or_false_true : Nat =(zero_or_false True).asInstanceOf[Nat](1) 変数 b が束縛される型 Bool，(2) O と False の型
キャスト先の型 Nat or bool，(3) (zero or false True)の型キャスト先の型 Nat という 3 つの型を明示している．この例では (1) は Scala の文法上省略可能であり，(2) は (アップキャストであるので) 同様である．
しかし (3) は (ダウンキャストであるので) 省略する
ことはできない．一般には型を明示する必要がある．

2. 3 Scala へのコード抽出

例 2.9

let rec subtract m n =match n with
| O -> m| S n0 ->(match m with
| O -> assert false| S m0 -> subtract m0 n0)
subtract の型からは m < n であるという命題がScala コードの書き出しは，MiniML に型の情報が加わった中間言語の項からであれば可能である．CICの要素からこのような中間言語 MiniML′ の項に変換する方針は 2 通り考えられる．

1. CIC の要素に含まれる型の情報を捨てないようにしながら MiniML′ の項に変換する．

2. CIC の要素から MiniML の項に変換した後に，型の情報を付加することで MiniML′ の項に変換
する．

消え，nat → nat → nat に変換される．m < n

一つ目の方針は Coq から MiniML′ に直接変換しなに反する項の部分は，実行されない部分であるのければならないため，実装の手間が掛かるのが短所でで例外を発生させるコードに変換される．

ある．既存の Coq から MiniML への変換の実装を一しかしこの手順では，要素を Scala へコード抽出す部変更して利用することもできるが，その場合は既存ることはできない．これは CIC の要素に含まれていの実装に変更があるたびに対応しなければならない．

た型の情報が E によって MiniML の項に変換される

これに比較すると，二つ目の方針は実装の手間は軽間に捨てられてしまい，様々な場所で型を明示する必い．なぜなら，Coq から MiniML の変換は既存の実要がある Scala コードとして書き出すことはできない

装をそのまま利用できるため，必要なのは MiniMLからである．

から MiniML′ の変換の実装のみだからである．しか

例えば nat or bool と zero or false，zero or false

し，二つ目の方針は一度捨てた型の情報を再度付け加に対応する Scala コードは次のようになるはずである．

えるという非効率なことをしている点が短所である．

type nat_or_bool = Any
def zero_or_false : Bool -> Nat_or_bool =Coq8.3 において，著者の一人である今井は従来のコード抽出の実装に手を加えることで，一つ目の方針(b : Bool) =>による Scala へのコード抽出を可能にした [2]．しかb match {し Coq のバージョンが 8.4 になると抽出過程の実装

case True =>に変更があり，上でこの方針の短所として述べたよう

に再び手を加えなければならなくなった．

型キャストを表す．

本研究では二つ目の方針による Scala へのコード

ml ast e ≡
|x

変数参照

という点を挙げたが，MiniML から MiniML への変

|ee

関数適用

換の実行時間は短いため，実際には問題にならない．

| fun x → e

先の Coq8.3 における実装と異なり，従来のコード抽|c

出の実装に手を加える必要がなく Coq のバージョン| let x = e in e

変更による影響は少ない．

| match e with

抽出を考える．この方針の短所として非効率である′関数
グローバル参照

let 式

c⃗
x → e | · · · | c⃗x → e

3 提案する Scala へのコード抽出方式
私たちが取った方式は，従来の抽出で得た MiniML′′の項に型推論アルゴリズム M によって型の情報を′

match 式| fix x = e with · · · with
再帰関数

x = e for x| magic e

magic 式′′

復活させ，中間言語 MiniML の項を作るというもの

MiniML の項 ml ast は下の構文で表される．変である．この節では M′′ を詳細に定義したあと，M′′

数参照とグローバル参照には型引数が，関数と let 式を用いた抽出の手順全体について説明する．

と再帰関数には変数の型が，magic 式にはキャスト先

以後 ⃗a は {a1 , . . . , an } を表す．∀⃗
α は ∀α1 . . . ∀αnの型が付け加えられている．

ml ast′ e′ ≡| x[T⃗ ]

を表す．

変数参照

| e′ e′3. 1 MiniML，MiniML′ の表現
型 ml type と型スキーム ml type scheme は下のように表される．ここで定義する型・型スキームは′MiniML のものであり同時に MiniML のものでも関数適用| fun x : T → e| c[T⃗ ]′′| let x : τ = e in e関数
グローバル参照
′

let 式

′

| match e withある．

c⃗x → e′ | · · · | c⃗x → e′

ml type T ≡
|α

(型変数)

| C[T⃗ ]

(定数型)

|T →T

(関数型)

match 式′| fix x : T = e with . . . withx : T = e′ for x′| magic (e , T )再帰関数

magic 式

ml type scheme τ ≡| ∀α.τ

3. 2 その他の定義|T

型環境は変数から型スキームへの部分関数である．

MiniML の項 ml ast は下の構文で表される．特徴

型環境全体を env で表す．型環境 Γ と変数 x，型ス的なのは magic を含む項である．これは安全でない

キーム τ に対して，型環境の拡張 Γ + {x : τ } は{x 7→ τ } ∪ {y 7→ τ ′ | y ̸= x, y 7→ τ ′ ∈ Γ} を表す．グ
ローバルな型環境 E は定数から型スキームへの部分関数である．
型 T に対して，tv(T ) は T に現れる型変数の集合を表す．型スキーム τ = ∀⃗α.T に対して，ftv(τ ) は

τ に現れる自由変数の集合，つまり tv(T )\⃗α を表す．
∪型環境 Γ に対して，ftv(Γ) は x∈dom(Γ) ftv(Γ(x)) を

表す．

1. t と T から既存の方法によって MiniML の項

代入は型変数の列を α⃗ ，型の列を T⃗ として {⃗α 7→ T⃗ }tMiniML ，MiniML の型 TMiniML を得る．

で表す．代入全体を subst で表す．型スキーム τ に対

2. M′′ (∅, tMiniML , TMiniML ) を実行して MiniML′する代入 {⃗
α 7→ ⃗τ } の適用 {⃗α 7→ ⃗τ }τ は，τ に出現すの項 tMiniML’ を得る．この実行の際，TMiniML にる自由変数 αi を τi で置き換える．型環境 Γ に対する

含まれる型変数は代入してはいけない型変数で代入 σ の適用 σΓ は {x 7→ στ | x 7→ τ ∈ Γ} を表す．

あるので，定数として扱う．

型スキーム τ に対して，型の一般化 GenΓ (τ ) は∀⃗
α.τ (ただし α⃗ = ftv(τ )\ftv(Γ)) を表す．型スキーム τ = ∀⃗
α.T0 に対して，型の具体化 Inst(T⃗ , τ ) は

3. tMiniML’ : TMiniML を Scala コードとして書き出す．

4 抽出の正当性{⃗
α 7→ T⃗ }T0 を表す．

コード抽出が正当であるために満たすべき性質と

3. 3 アルゴリズム M′′

して，以下の 2 つがある．

アルゴリズム M は O．Lee ら [5] による型推論ア
ルゴリズムである．項をトップダウンに検査しながら分からない型を一時的にフレッシュな型変数で置き，型の妥当性 抽出したコードは型検査を通る．
計算の妥当性 抽出したコードの実行と，抽出前のコードの実行が等しい．

型に関する制約を集め，集めた型制約を解くことに従来のコード抽出がこれらの性質を満たすことは，よって型が何であったかを推論する．Letouzy [3] はLetouzey [3] が証明した．抽出の過程で MiniML の

CIC から MiniML への変換において，MiniML の項

項が型が付くように型キャストが挿入されるので，型に適切に型キャストを挿入するために M を改変したの妥当性を満たす．

′

アルゴリズム M を用いた．M は代入のみを返すのに対し，M′ は代入に加えて型キャストを挿入した項を返す．

定理 1 任意の CIC の要素から変換された MiniMLの項 tMiniML と型 TMiniML は，∅ ⊢ tMiniML : TMiniMLM : env × ml ast × ml type

→ substを満たす．

M ′ : env × ml ast × ml type

→ subst × ml ast

また CIC の項 t とその抽出後の MiniML の項 tMiniML

アルゴリズム M はアルゴリズム M をベースにしがあるとき，t を評価した結果と tMiniML を評価した

た型推論アルゴリズムである．MiniML の項 e とそ

結果が抽出前後の関係にあることを証明することで，の型を受け取り，推論した型の情報を e に付け加えた計算の妥当性を示した．

′′′

MiniML の項を返す．
M ′′ : env × ml ast × ml type → subst × ml ast′

この節では，提案する Scala へのコード抽出方式が型の妥当性を満たすことを示す．

詳細な動作は図 1 のようになる．

4. 1 型付け規則

ここで呼び出している unify 関数は型制約を解く関

まず，ある型環境のもとで MiniML の項，MiniML′数である．型の組 (T, T ′ ) を受け取り，σT = σT ′ での項が型付けされるとはどういうことか定義する．正あるような最小の代入 σ を返す．そのような代入がしく型付けされた MiniML の項は OCaml や Haskell

存在しないとき失敗し，呼び出している M′′ も失敗に書き出したときに型検査を通り，また正しく型付けする．

された MiniML′ の項は Scala に書き出したときに型検査を通るはずである．
′′

3. 4 M による Scala への抽出
CIC の要素 t とその型 T からこの方式によってScala コードを抽出する手順は次のようになる．

型環境 Γ，MiniML の項 e，型 T に対して Γ ⊢ e : Tを判定する型付け規則は図 2 のようになる．
型環境 Γ，MiniML′ の項 e′ ，型 T に対して Γ ⊢図1

アルゴリズム M′′

e′ : T を判定する型付け規則は図 3 のようになる．

することである．
補題 1 任意の型環境 Γ，MiniML の項 e，型 τ ，代

4. 2 提案方式の型の妥当性
提案方式が型の妥当性は，定理 1 と下の定理から

入 σ について，σΓ ⊢ e : στ ならば M ′′ (Γ, e, τ ) は失
敗せずに値を返す．

示される．

その組を (σ ′ , e′ ) = M ′′ (Γ, e, τ ) とおくと σ ⊑Γ σ ′ か定理 2 MiniML の 項 tMiniML と 型 TMiniML に
ついて ∅

⊢

tMiniML:

TMiniML な ら ば ，′′M (∅, tMiniML , TMiniML ) は失敗せずに MiniML’ の項 tMiniML’ を返して ∅ ⊢ tMiniML’ : TMiniML が成立する．

つ σ ′ Γ ⊢ e′ : σ ′ τ が成立する．
補題 1 の証明は ml ast の構成に関する帰納法による．証明は多くの場合はアルゴリズム M と同じである [5] ので省略し，M にはない magic 項に関する場
合を載せる．

定理 2 が成立することは，次の補題 1 が成立する(証明）e = magic a の場合仮定から σΓ ⊢ magic a : στ が成立する．これと型ことから分かる．=Γ ，⊑Γ は次の関係である．

付け規則 (MAGIC) から，ある τa が存在して
定義 1 代入 σ ，σ ′ ，型環境 Γ について，σ =Γ σ ′ であ′るとは任意の型変数 X ∈ ftv(Γ) について σX = σ Xが成立することである．
定義 2 代入 σ ，σ ′ ，型環境 Γ について σ ⊑Γ σ ′ であるとは，ある代入 γ が存在して σ =Γ γ ◦ σ ′ が成立σΓ ⊢ a : τa(1)が成立する．フレッシュな型変数 α を用意して

σ ′ = σ ◦ {α → τa }(2)とおけば，(1) からσ′ Γ ⊢ a : σ′ α

(3)

図2

MiniML の型付け規則

図3

MiniML′ の型付け規則が成立する．(3) を帰納法の仮定に用いると，あるが成立する．したがって M ′′ (Γ, magic a, τ ) は失敗

ϕa ，γ ，a′ が存在してせずに (ϕa , magic (a′ , τ )) を返す．α は ftv(Γ) に含

σ ′ =Γ γ ◦ ϕ a′′′(ϕa , a ) = M (Γ, a, α)′

ϕa Γ ⊢ a : ϕa α

(4)
(5)
(6)

まれないから，(2) より

σ =Γ σ ′(7)def x[⃗α] : T = e 1

である．Γ は推移律を満たすので，(7) と (4) から

ϕa ⊑Γ σe2(8)が成立する．また (5) と型付け規則 (MAGIC′ ) から}

ϕa Γ ⊢ magic’(a′ , τ ) : τmatch 式(9)が成立する．(8) と (9) から，返す値は条件を満たす．

(MiniML’)
match e0 with

5 Scala コードの書き出し| c1 ⃗x1 ⇒ e1

5. 1 MiniML′ の書き出し| ...

MiniML の型，すなわち MiniML’ の型は Scala の| cn ⃗xn ⇒ en

型として自然に書き出せる．型スキーム ∀⃗α.T は型 T
として書き出す．型スキームが現れる場所では必ず変(Scala)e0 match {数がその型スキームに束縛されており，α⃗ がその変数case c1 (⃗x1 ) => e1の型パラメータであることを書く．

...

MiniML′ の項 e′ は Scala コード e′ として以下のように書き出す．
変数参照(MiniML’)x[T⃗ ](Scala)x[T⃗ ]
関数適用

case cn (⃗xn ) => en}
再帰関数(MiniML’)fix x1 :T1 =e1
with . . .
with xn :Tn =en
for xk [T⃗ ](MiniML’)(Scala)e1 e2{
def x1 : T1 = e1

(Scala)...

e1 (e2 )関数

def xn : Tn = enxk

(MiniML’)fun x:T → e(Scala)(x : T ) => e
グローバル参照(MiniML’)c[T⃗ ](Scala)c[T⃗ ]
let 式(MiniML’)let x:∀⃗
α.T =e1 in e2(Scala){}magic 式(MiniML’)magic (e, T )(Scala)e．asInstanceOf[T ]5. 2 Coq 上の定義と Scala コードの対応
Coq 上で定義した集合や要素が最終的にどのような Scala コードとして書き出されるのか説明する．例
として第 2. 1 節に載せた定義を抽出する．E は第 2. 2
節と同じく CIC の項を MiniML′ の型に変換する関数である．

集合の帰納的な定義 集 合 は abstract class とDefinition f : T := e.

して，コンストラクタはそれを継承した caseが あ る と き ，e:T を 本 論 文 で 述 べ た 手 順 でclass として書き出される．

MiniML′ の項 tMiniML’ と MiniML′ の型 TMiniML(Coq)に変換し，次のように書き出す．ただし α⃗ はInductive I (α1 :T1 ). . . (αm :Tm )tv (TMiniML ) である．
(Scala): Set :=
| C : U1 -> . . . -> Un -> I α1 . . . αm

def f[α1 , . . . ,αn ] : TMiniML = {tMiniML’(Scala)abstract sealed class′
I[α′1 , . . . ,αm′]}case class′C[α1′ . . . αm′ ](x1 :E(U1 ), . . . ,xn :E(Un ))′extends I[α1′ , . . . ,αm′]

例 5.3 subtract を抽出する．

def subtract : Nat => Nat => Nat = {′ここで α1′ . . . αm
′ は α1 . . . αm のうち集合を表す(m : Nat) => (n : Nat) =>変数のみを抜き出したもの，つまり {αi | Ti =m match {Set} である．

case O() => ncase S(m0) => {例 5.1 nat を抽出する．コンストラクタの O はn match {引数を取らず，S は nat 型の引数を一つ取るのcase O() =>で，次のようなコードになる．

throw
new Exception("absurd case")

abstract sealed class Nat

case S(n0) =>case class O extends Nat

subtract m0 n0case class S(x1:Nat) extends Nat}

帰納的でない型の定義 Scala では type キーワー}

ドによる型の別名定義として書き出される．

(Coq)

}
}

Definition t (α1 . . . αm : Set) : Set :=T.
(Scala)type t[α1′ , . . . ,α′m′ ] = E(T )6 実装
アルゴリズム M′′ の実装は Coq 上で行い，上記の′先の例と同様に，α1′ . . . αm
′ は {αi | Ti = Set}

定理を確かに満たす実装を得た．この M′′ をコードである．

抽出することで Coq から Scala へのコード抽出プロ
グラムを作成した．言語は OCaml を使用した．

例 5.2 nat or bool を抽出する．すべての項が全体の構成は以下の三つから成る．

持てるような型を OCaml では Obj.t で表した

1. CIC を MiniML に変換するコード．Coq の実

ように，Scala では Any クラスで表す．

type Nat_or_bool = Any
要素の定義 要素は def キーワードによる関数定義として書き出される．

(Coq)

装の一部を用いた．

2. MiniML を MiniML′ に変換するコード．M′′ を
OCaml へコード抽出して用いた．
3. MiniML′ を Scala コードとして書き出すコード．第 5 節を直接 OCaml で実装したものを用

いた．

の変換の正当性に依存している．実際の Coq から

Coq8．4pl2 に対応するプログラムを [1] にて公開

MiniML への変換の実装では複雑な最適化が行われてしている．このプログラムを含めて Coq をビルドしおり，正当性を満たすことは示されていない．Scala

たあと Coq 上で以下のように入力することで，Scalaへの抽出方式の正当性を確実に保証するには，この変へコード抽出することができる (定義済みの f を抽出

換の正当性を示す必要がある．

したい場合)．

本研究により，抽出先の言語が型推論を備えている

Extraction Language Scala.

必要はなくなった．Scala 以外の Java8 [4] のようなRecursive Extraction f.

型推論のない言語へのコード抽出にも取り組んで行

7 まとめと今後の課題

く予定である．

従来の方法では Coq から型推論の弱い Scala へのコード抽出はできなかった．そこで本論文では，謝辞 本研究の一部は科研費 (課題番号 25330096)の助成を受けて行われた．

MiniML 上で型推論を行うことによって Coq 上のプ
ログラムを Scala コードへ抽出する方式を考えた．そ参 考 文 献の核となるアルゴリズム M′′ を Coq 上で実装し，こ[1] Hemmi, K.: Coq2Scala for Coq8.4. https://github.com/hemmi/coq2scala.
[2] Imai, Y.: Coq2Scala for Coq8.3.
http://
proofcafe.org/wiki/Coq2Scala.
[3] Letouzey, P.: Certified functional programming Program extraction within Coq proof assistant, PhD
Thesis, University Paris-sud, 2004.
[4] Oracle: Oracle Technology Network for Java Developers. http://www.oracle.com.
[5] Oukseh Lee, K. Y.: Proofs about a folklore letpolymorphic type inference algorithm, ACM Transactions on Programming Languages and Systems,
Vol. 20, No. 4(1998), pp. 707–723.
[6] The Coq Development Team: The Coq Proof Assistant. http://coq.inria.fr.
[7] The Scala Development Team: The Scala Programming Language. http://scala-lang.org.

の方式は型の妥当性を満たすことを証明した．
しかし計算の妥当性に関する証明はまだできていな
い．MiniML 上の計算と MiniML′ 上の計算は基本的には等しいが，一点のみ異なる．MiniML 上の型キャ
ストはどんな場合でも必ず実行するが，MiniML′ 上では不適切な型キャストは許されないという点である．したがって，M′′ が返す MiniML′ の項に含まれる型キャストが必ず適切であることを証明する必要がある．
この抽出方式の正当性は，Coq から MiniML へ