(訳注: この日本語マニュアルは Verified programming in F* の翻訳です。 翻訳に参加するには 翻訳リポジトリ を参照してください。)

1. イントロダクション

F* は検証指向のプログラミング言語で、Microsoft Research, MSR-Inria, Inria によって開発されています。 それは、型付で正格な関数型プログラミング言語である ML 族の言語の伝統を受け継いでいます。 けれども、その型システムは ML のそれよりも著しく豊かで、表明されて半自動的に検査される関数的な正確さの仕様を許します。 このチュートリアルは F* における検証されたプログラミングの最初の体験を提供します。 論文とテクニカルレポートを含む F* に関するより多くの情報が F* ウェブサイト で見つかります。

もし ML 族の関数型プログラミング言語 (例: OCaml, F#, Standard ML) や Haskell に馴染みがあれば、それは役立つでしょう—もし馴染みがなくても、この文書で基本的な概念を簡単に説明します。より多くのバックグラウンドを知りたい場合には、Web 上に無料の有用な文書が多数あります。例えば、TryF#, F# for fun and profit, Introduction to Caml, Real World OCaml などです。

F* を試したりこのチュートリアルの検証の練習問題を解く最も簡単な方法は オンライン F* エディタ を使ってウェブブラウザ上で直接動かすことです。 それぞの練習問題の本体中にある “エディタに読み込む” リンクをクリックすることで、それぞれの練習問題に必要なボイラープレートコードをオンラインエディタに読み込むことができます。 それぞれの練習問題でのあなた進捗はウェブブラウザのローカルストレージに保存されるので、(例えばウェブブラウザがクラッシュなどしても) 後であなたのコードを復帰できます。 (訳注: この文書では上記の オンライン F* エディタ との連携は使えません。“エディタに読み込む” リンクをクリックすると、相当するソースコードをダウンロードできます。)

また F* をローカルのマシンにインストールしてこの練習問題を解くこともできます。 F* はオープンソースでクロスプラットフォームです。 Windows, Linux, MacOS X 向けの バイナリパッケージ をダウンロードでき、またこれらの 手順 を用いて github 上のソースコード から F* をコンパイルできます。

お好きなテキストエディタを使って F* コードを編集できます。 そして Emacs, Atom, Vim には F* を特別にサポートする拡張があり、シンタックスハイライトやインタラクティブな開発ができます。 エディタのサポート の詳細は F* wiki を参照してください。

デフォルトでは F* は入力されたコードを検証するだけで、それを実行しません。 F* コードを実行するためには、OCaml や F# にエクストラクトし、OCaml や F# コンパイラを使ってコンパイルする必要があります。 F* コード実行 の詳細は F* wiki を参照してください。

1.1. はじめての F* プログラム: アクセスコントロールの単純なモデル

ファイルに対するアクセスコントロールの単純なモデルからはじめましょう。 この中で、一般的な関数型プログラミング由来のいくつかの基本的なコンセプトと、いくつかの F* 固有の機能を見ることになるでしょう。

ファイルの単純なアクセスコントロールをモデル化したいとしましょう—あるファイルは読み書き可能で、一方で他のファイルはアクセスできません。 それぞれのファイルに対する権限を表わすポリシーを作り、このポリシーに照らしてプログラムのファイルアクセスのパターンをチェックし、アクセスできないファイルが決っして間違ってアクセスされてないことを静的に保証したいのです。

このシナリオでのモデル (これは後の章でより現実的にします) は3つの簡単なステップで進展します。

1. 単純な純粋関数を使ってポリシーを定義します。

2. プログラムにおけるセキュリティセンシティブなプリミティブを特定し、それらをポリシーを使って保護します。

3. プログラムの残りを書きます。ポリシーで保護されたプリミティブは決っして不適切にアクセスされないことを F* の型検査器は静的に検証することを保証されます。

1.1.1. ポリシーを定義する

F* の構文は OCaml 構文と F# の non-light 構文に基づいています。 F* プログラムは数個のモジュールで構成されます。 それぞれのモジュールはそのモジュールの名前を定義する module 宣言ではじまります。 その本体は多数の定義と任意に ‘main’ 式を含みます。

ここでは2つのモジュールがあります: 1つは FileName と呼ばれ、もう1つは (Access-Control Lists を表わす) ACLs と呼ばれます:

module FileName
  type filename = string

module ACLs
  open FileName

  (* canWrite is a function specifying whether or not a file f can be written *)
  let canWrite (f:filename) = 
    match f with 
      | "demo/tempfile" -> true
      | _ -> false

  (* canRead is also a function ... *)
  let canRead (f:filename) = 
    canWrite f               (* writeable files are also readable *)
    || f="demo/README"       (* and so is this file *)

FileName モジュールは型シノニムを定義します: filename をモデル化するのに string を使えます。 ACLs モジュールははじめに FileName モジュールを open するので、その型シノニムは直接使えるようになります。(そうしない場合、長いフル修飾された名前: FileName.filename で呼び出す必要があります。)

その後 ACLs は2つのブール関数としてセキュリティポリシーを定義します: canWrite と canRead です: canWrite 関数はその引数 f を パターンマッチ式 を使って検査します: f="demo/tempfile" であったらブール true を返し、そうでなければ false を返します。 関数 canRead も同様です—ファイルが書き込み可能もしくは "demo/README" ファイルであったなら、そのファイルは読み出し可能です。

1.1.2. ポリシーをファイルアクセスプリミティブと結びつける

ポリシーを強制するためには、ファイルを読み書きを実際に実装するプログラムのプリミティブにポリシーを接続する必要があります。

F* は別に実装された外部のモジュールへのインターフェイスを指定する機能を提供しています。 例えば、ファイルの入出力操作は OS によって実装されていますが、例えば .NET や OCaml のような下層のフレームワークを通じて F* プログラム中で有効にできます。 次のように、そのフレームワークによって提供された単純なインターフェイスを表現できます:

module FileIO
  open ACLs
  open FileName
  assume val read  : f:filename{canRead f}  -> string
  assume val write : f:filename{canWrite f} -> string -> unit

ここでは、ACLs モジュールを使う FileIO と呼ばれる インターフェイス を定義しました。 より重要なことは、FileIO は2つの関数 read と write を提供し、それらはおそらく相当するファイル操作を実装しています。

assume val 表記を使って、FileIO が read と write 操作 (それらは 値 です) を提供すると 宣言 しましたが、ここではそれらの値を 定義していません —それらは外部のモジュールで提供されます。 assume val の使用はC言語や他のプログラミング言語の extern キーワードと良く似ています。

extern を使って値を宣言するとき、その型シグニチャも提供します。

• read の型は、それが引数 f に canRead f が true に評価されるような filename を取り、string 型の結果を返す関数であると主張しています。 したがって型検査器は、引数に対して述語 canRead が静的に証明されないようなどのような read 呼び出しも防止します。

• write の型は、それが次のような2引数の関数です: 1つ目は canWrite f が true に評価されるような filename f です; 2つ目は string で、そのデータはファイル f に書き込まれます。 write 関数は unit を返し、それはおおざっぱにC言語の void 型に似ています。 型 unit は唯一の値を持ち、() と書きます。

もちろん、これらの宣言の重要な点は型シグニチャにおける canRead と canWrite の使用です。 それらによってセキュリティセンシティブな関数の型をポリシーに接続できます。

1.1.3. プログラムを書き、そのセキュリティを検証する

コード片がアクセスコントロールポリシーに従っていることをチェックするのは退屈でエラーしやすいでしょう。 たとえそれぞれのアクセスがセキュリティチェックで保護されていたとしても、どうすればそれぞれのチェックが適切であることを確認できるでしょうか？ F* を使うことで、この種のコードレビューを自動化できます。

ここではいくらか単純な信頼できないクライアントコードを示します。 このコードは共通のファイル名を定義する FileIO を使い、それから複数のファイルを読み書きする staticChecking と呼ばれる関数を使います。

module UntrustedClientCode
  open FileIO
  open FileName
  let passwd  = "demo/password"
  let readme  = "demo/README"
  let tmp     = "demo/tempfile"

  let staticChecking () =
    let v1 = read tmp in
    let v2 = read readme in
    (* let v3 = read passwd in -- invalid read, fails type-checking *)
    write tmp "hello!"
    (* ; write passwd "junk" -- invalid write , fails type-checking *)

型検査器は、この信頼できないコードがセキュリティポリシーと共にコンパイルされるされることを静的に保証します。 tmp と readme の読み出しと tmp への書き込みはポリシーで許されているので、このプログラムの型検査は成功します。 一方、password ファイルを読んだり "junk" を書き込む行のコメントを外すと、F* 型検査器は passwd ファイルがそれぞれ型 f:filename{canRead f} や f:filename{canWrite f} を持たないことを訴えます。 例えば、この write のコメントを外すと、次のようなエラーメッセージが得られます:

Error ex1a-safe-read-write.fst(38,2-47,5): The following problems were found:
    Subtyping check failed; expected type f:filename{(canWrite f)};
    got type string (ex1a-safe-read-write.fst(43,17-43,23))

このチュートリアルを読み進めることで、このメッセージの意味がより理解できるようになるでしょう。 ここでは、F* が canWrite passwd が true に評価されると期待しているのに、この場合成立しないことを意味しています。

上記の staticChecking 関数は、セキュリティポリシーを指定し、ポリシーの完全で正確な調停を型検査を通じて静的に強制するのにどのように F* を使うことができるかを説明しています。 ここで、ポリシーのチェックは全て静的に行なわれる必要はなく、プログラマが追加した動的なチェックが型システムによって検討されることを説明します。 具体的には、ポリシーを調べてポリシーが許可するときだけ read を行ない、そうでなければ例外を発生させる checkedRead 関数を実装してみましょう。

  exception InvalidRead
  val checkedRead : filename -> string
  let checkedRead f =
    if ACLs.canRead f then FileIO.read f else raise InvalidRead

checkRead 型は入力ファイル f の条件を強制していないことに注意してください。 ACLs.canRead f チェックが成功したなら、型検査器は FileIO.read f 安全であることがわかります。

  assume val checkedWrite : filename -> string -> unit

  exception InvalidWrite
  let checkedWrite f s =
    if ACLs.canWrite f then FileIO.write f s else raise InvalidWrite

これで、staticChecking の read と write を checkedRead と checkedWrite で置き換えることで、passwd へのアクセスが型付けできます。

  let dynamicChecking () =
    let v1 = checkedRead tmp in
    let v2 = checkedRead readme in
    let v3 = checkedRead passwd in (* this raises exception *)
    checkedWrite tmp "hello!";
    checkedWrite passwd "junk" (* this raises exception *)

checkedRead と checkedWrite は F* によってコンパイル時にあらかじめ行なわれたのと同じチェックを実行時に延期させ、それらのチェックが成功した場合のみその入出力アクションを行なうため、これは安全です。

2. 基本: 型と作用

全てを知らされていませんでしたが、F* 独特の機能のいくつかを最初の例で既に見てきました。 より詳細に見てみましょう。

2.1. リファインメント型

F* の1つの特徴的な機能はリファインメント型の使用です。 この機能を既に2度使いました。 例えば、型 f:filename{canRead f} は型 filename の リファインメント です。 filename 値のサブセットのみがこの型、すなわち述語 canRead を満たす型を持つので、それはリファインメントなのです。 FileIO.write の型のリファインメントも同様です。 伝統的な ML 族の言語では、このような型は表現できません。

一般に、F* におけるリファインメント型は x:t{phi(x)} の形を取ります。 このときそれは型 t のリファインメントで、その要素 x は式 phi(x) を満たします。 今のところ、phi(x) は式を評価すると得られる純粋なブールであると考えることができます。 詳細には 3.5 で、より一般化します。

2.2. 推論された型と計算のための作用

canRead や canWrite のような関数の型を書きませんでしたが、(ML 族の他の言語と同様に) F* は (その型が正しいなら) プログラムの型を推論します。 けれども、F* によって推論される型は ML で表現される型よりもより詳細です。 例えば、型推論に加えて、F* は式の 副作用 (例: 例外、状態など) も推論します。

例えば、ML では (canRead "foo.txt") は型 bool を持つと推論されます。 けれども、F* では (canRead "foo.txt" : Tot bool) と推論します。 これは canRead "foo.txt" 純粋で全域な式で、常にブールに評価されることを示しています。 ついでに言うと、型と作用 Tot t を持つと推論された式は、(コンピュータが十分なリソースを持っていれば) t で型付けされた結果に評価されることが保証されます。 そしてこの式は無限ループに入らず、プログラムの状態を読み書きせず、例外を発生せず、入出力を行なわず、その他の作用を引き起こしません。

一方、(FileIO.read "foo.txt") のような式は型と作用 ML string を持つと推論されます。 これはこの項が任意の作用 (ループ、入出力、例外発生、ヒープの変更など) を持つ可能性があり、けれどももしそれがリターンしたなら、常に文字列を返すことを意味しています。 作用の生 ML はデフォルト、つまり全ての ML プログラムの暗黙の作用を表わしています。

Tot と ML は取りうる作用の全てではありません。 それ以外に次のような作用があります:

• Dv、分岐を共なう計算の作用
• ST、分岐やヒープ中の参照の読み書きや確保を共なう計算の作用
• Exn、分岐や例外を共なう計算の作用

作用 {Tot, Dv, ST, Exn, ML} は束として配置されます。 Tot は (その他全ての作用より下位である) 下限に、ML は (その他全ての作用より上位である) 上限に配置され、ST と Exn は関係がありません。 これは特定の作用を共なう計算が、作用の順序においてその作用より大きいその他の作用を持つと扱えることを意味しています—私達はこの機能を サブ作用 と呼んでいます。

実際、F* では、独自の作用と作用の順序を構成でき、F* にそれらの作用を推論させることができます—しかしそれはより高度な機能で、このチュートリアルの範囲外です。

今後は (例えば Tot が作用で int が結果の型である Tot int のような) 型と作用のペアを、単に型と呼ぶことにします。.

2.3. 関数型

F* は関数型言語で、関数は関数型が割り当てられた第一級の値です。 例えば ML では、ある整数が正であるか判別する関数には型 int -> bool が与えられます。 すなわち、この関数は整数を引数に取り、ブールを結果として生成します。 同様に、整数の最大値を計算する関数 max には型 int -> int -> int が与えられます。 すなわち、この関数は2つの整数を取り、1つの整数を生成します。 F* における関数型はより詳細で、引数と返り値の型だけでなく、関数本体の作用も捕捉します。 このように、全ての関数値は t1 -> ... -> tn -> E t のような型を持ちます。 このとき t1 .. tn は引数それぞれの型で; E は関数本体の作用; そして t はその結果の型です。 (*上級者への注意: これは作用でインデックスされた依存した関数に一般化されます。) F* では、上記の純粋関数には作用 Tot を使った型が与えられます:

val is_positive : int -> Tot bool
let is_positive i = i > 0

val max : int -> int -> Tot int
let max i1 i2 = if i1 > i2 then i1 else i2

ファイルの内容を読むような、純粋でない関数には同様に作用が与えられます:

val read : filename -> ML string

(OCaml や F# と同様に、Haskell や Coq と異なり) F* は 値渡し の関数型言語で、関数の引数はその関数に渡される前に、完全に評価されて値になります。 値は (直接の) 作用を持たないので、関数の引数の型は作用の注釈を持ちません。 一方で、関数の本体は非自明な計算を行なうかもしれません。 そのため上記で説明したように、その結果は常に型と作用の両方で与えられます。

module FileName
  type filename = string

module ACLs
  open FileName

  val canWrite : unit (* write a correct and precise type here *)
  let canWrite (f:filename) =
    match f with 
      | "demo/tempfile" -> true
      | _ -> false

  val canRead : unit (* write correct and precise type here *)
  let canRead (f:filename) =
    canWrite f               (* writeable files are also readable *)
    || f="demo/README"       (* and so is this file *)

val canRead: filename -> Tot bool
val canWrite: filename -> Tot bool

2.3.1. デフォルトの作用は ML

注釈がない場合、F* は、入出力を行なうかもしれないか、停止しないかもしれない関数を、作用 ML を持つと (ときに保守的に) 推論します。 そのため、下記どちらの関数も型 (int -> ML int) を持つと推論されます。 (注意: 再帰関数は ML 族の言語では let rec で定義されます。)

let hello_incr i = IO.print_string "hello"; i + 1
let rec loop i = i + loop (i - 1)

もし明示的な注釈を与えると、これらの関数により正確な型を割り当てることができます:

val hello_incr i : int -> IO int
let hello_incr i = IO.print_string "hello"; i + 1

val loop : int -> Dv int
let rec loop i = i + loop (i - 1)

プログラムを ML から F* に移植するために、私達はデフォルトの作用を ML に選び、通常はそれを書かずに済むようにしました。 そのため hello_incr と loop を表わす通常の ML シグニチャを以下の示すように書くことができます。 これはより明示的な (int -> ML int) と単に同義です。

val hello_incr: int -> int
val loop: int -> int

2.3.2. 計算する関数

もし関数型プログラミングの初学者なら、はじめて読む際にこの章を飛ばしてください。

ときに、なんらかの計算を行なった後に関数を返すことが有用です。 例えば、次の関数は新しいカウンタを作り、それを init で初期化します。

let new_counter init =
  let c = ST.alloc init in
  fun () -> c := !c + 1; !c

F* は new_counter が型 int -> ST (unit -> ST int) を持つと推論します。 型によるとこの関数は、整数が与えられ、参照を読み書きもしくは確保するかもしれず、それから unit -> ST unit 型の関数を返します。 この型を書いて、F* にチェックさせることができます; もしくはサブ作用を使って、下記のように型を書いて new_counter が上手く型付けできることを F* にチェックさせることもできます。

val new_counter: int -> ML (unit -> int)

上記の型、int -> ML (unit -> ML int) の短縮形は、int -> unit -> int と同じでは ありません 。 注意してください。 後者は int -> Tot (unit -> ML int) の短縮形です。

3. 整数を扱う関数の最初の証明

アクセスコントロールリストの最初の例では、どのように F* の型システムがセキュリティ属性の自動的な検査に使うことができるか示しました。 けれども、より興味深いセキュリティに関連したプログラミングと検証を行なう前に、F* の基礎についてより理解を深める必要があります。 ここで戻って、整数を扱う単純な関数のプログラミングと性質の証明を見てみましょう。

3.1. 静的に検査される表明

F* のコードにおける性質を証明する1つの方法は表明を書くことです。

let a = assert (max 0 1 = 1)

最初の表明は max に関する明らかな性質です。 別の言語で assert と呼ばれる構成物を見たことがあるかもしれません—一般に、そのような assert はコードの性質を 実行時に 検査するために使われ、その表明条件が true でない場合には表明に失敗した例外が発生します。

F* では、表明は実行時の意味を持ちません。 その代わりに、F* はその表明条件が真であることを静的に証明しようとします。 そのため実行時に検査されたとしても決っして失敗しません。

この場合、max 0 1 = 1 の証明は簡単です。 裏で F* は max の定義と表明された性質を Z3 と呼ばれる定理証明器に渡して、その性質を自動的に証明します。

max のより一般的な性質を表明して、自動的に検査することができます。例えば次のようになります:

let a = assert (forall x y. max x y >= x
                 && max x y >= y
                 && (max x y = x || max x y = y))

3.2. 階乗とフィボナッチ関数

階乗関数を見てみましょう:

let rec factorial n = if n = 0 then 1 else n * factorial (n - 1)

以前解説した通り、注釈がない場合、F* はこの関数の型を int -> int であると推論します。これは int -> ML int の短縮形です—これは F* がこの factorial が (もしくはどのような再帰関数が) 純粋で全域関数であることを自動的に証明しようとしないことを意味しています。 実際、階乗は任意の整数に対して全域関数ではないのです! factorial (-1) を考えてみましょう。

けれども、factorial 関数は非負の整数については全域関数です。 これを実際に書いた場合、検査を F* に支持できます:

val factorial: x:int{x>=0} -> Tot int

上記の行にはいくつかの主張があります:

• factorial は値です (‘val factorial’ 部分で主張しています)

• それは 関数 です (矢印型 ‘->’ で主張しています)

• それは 0 以上の整数 x に対してのみ適用できます (リファインメント型 ‘x:int{x>=0}’ で主張しています)

• x に適用されると、それは常に停止し、作用を持たず (‘Tot’ 部分で主張しています)、そして整数を返します (返り値の型 ‘int’ で主張しています)

このように書くと、F* は factorial がこれら全ての性質を満たすことを自動的に証明します。 もちろん、証明における主な興味は x が非負の場合に factorial x が実際に停止するかどうかです。 これがどのように行なわれるかその詳細は章 5 で議論しますが、この場合 F* が非負な数値に対する全ての再帰的な呼び出しは以前の呼び出しでの引数より厳密に小さくなることを証明できると理解すれば十分です。 これは無限に続くかない (最終的に基底ケース 0 に収束する) ので、F* は factorial の型に関する主張に同意します。

非負な整数 (もしくは自然数) の型はありふれたもので、それは省略して定義できます。 (実際、F* では標準の prelude 中でこれは既に定義済みです。)

type nat = x:int{x>=0}

val factorial: x:int{x>=0} -> Tot int
let rec factorial n = if n = 0 then 1 else n * factorial (n - 1)

val factorial: int -> int                     (* inferred by default *)
val factorial: int -> ML int                  (* same as above *)
val factorial: nat -> Tot int                 (* total function on nat inputs *)
val factorial: nat -> Tot nat                 (* stronger result type *)
val factorial: nat -> Tot (y:int{y>=1})       (* even stronger result type *)

let rec fibonacci n =
  if n <= 1 then 1 else fibonacci (n - 1) + fibonacci (n - 2)

module Fibonacci

(* val fibonacci : nat -> Tot nat *)
(* val fibonacci : int -> int *)
(* val fibonacci : int -> ML int (same as above) *)
val fibonacci : int -> Tot (x:nat{x>0})
let rec fibonacci n =
  if n <= 1 then 1 else fibonacci (n - 1) + fibonacci (n - 2)

3.3. 補題

factorial 関数を書いて、型 (nat -> Tot nat) を与えたとしましょう。 すると例えば x > 2 ならば factorial x > x といったような、他の性質が気になるでしょう。 1つの方法は factorial の型を修正して、その型を F* に再度証明させることです。 しかしこれは常に柔軟なわけではありません。 x > 3 ならば factorial x > 2 * x も証明したいとしたらどうなるでしょうか: factorial の型に対するこれらの性質による汚染は、明確に実用的ではありません。

けれども、factorial に関するさらなる性質を証明するために、factorial を定義して nat -> Tot nat のような一般的な型を与えた後に、F* では (補題と呼ばれる) 他の関数を書くことができます。

補題は、常に単純な unit の値 () を返す ゴースト 全域関数です。 計算上、補題それ自体は役立ちません—それらは作用を持たず、常に同じ値を返します。それならばポイントはなんでしょうか？ そのポイントは、補題によって返される値の型がプログラムに関する有用な性質を有していることにあります。

factorial に関する最初の補題として、それが正の数を常に返すことを証明してみましょう。

val factorial_is_positive: x:nat -> GTot (u:unit{factorial x > 0})
let rec factorial_is_positive x =
  match x with
  | 0 -> ()
  | _ -> factorial_is_positive (x - 1)

この補題のステートメントは factorial_is_positive に与えられた型です。 それは x:nat に対するゴースト全域関数で、リファインメント factorial x > 0 と共にユニットを返します。 次の3行で factorial_is_positive を定義しており、x に対する帰納による証明を使ってこの補題を証明しています。 ここでの基本的なコンセプトは、全域関数を使ったプログラミングによって他の純粋な式に関する証明を書けることです。 この章の残りでこのような証明について詳細に議論します。

3.3.1. 依存関数型

この補題のステートメントをもう少しよく見てみましょう。

val factorial_is_positive: x:nat -> GTot (u:unit{factorial x > 0})

これは F* における 依存関数型 です。 なぜ 依存 するのでしょうか？ その結果の型はパラメータ x:nat の 値 に依存しているのです。 例えば、factorial_is_positive 0 は型 Tot (u:unit{factorial 0 > 0)) を持ちます。 これは factorial_is_positive 1 の型と異なります。

依存関数を紹介したので、関数型の一般的な形を少し詳しく見てみましょう:

関数の正規のパラメータそれぞれは xi と名付けられていて、それらの名前のスコープはそれに続く最初の矢印の右側です。 表記 t[x1 ... xm] は t 中に変数 x1 ... xm が自由出現することを示しています。

3.3.2. リファインメント型と補題に対するシンタックスシュガー

引数が2より大きいとき、factorial がその引数より厳密に大きいことをどうやって明記すべきでしょうか？ 次は最初の試みです:

val factorial_is_greater_than_arg1: x:(y:nat{y > 2}) -> GTot (u:unit{factorial x > x})

これは上手く行きますが、2つの名前が必要になるため、関数の引数の型は少し不恰好です: y はそのドメインを 2 より大きい自然数に制限するためで、x は返り値の型で引数に言及するためです。 このパターンはありふれていて、F* はそのためのシンタックスシュガーを提供しています—factorial に与えた最初の型で既に見てきました。 それを使うことで、上記の型と等価で、より簡潔な次のような型を書くことができます。

val factorial_is_greater_than_arg2: x:nat{x > 2} -> GTot (u:unit{factorial x > x})

もう1つの疑いようのない不恰好な点は補題の返り値の型で、それは unit 型のリファインメントを含んでいます。 これを簡潔にするために、F* は Lemma キーワードを提供していて、作用 GTot の代わりに使うことができます。

例えば、factorial_is_greater_than_arg2 の型は (下記の) factorial_is_greater_than_arg3 の型と等価で、それは少し読み書きしやすいでしょう。

val factorial_is_greater_than_arg3: x:nat{x > 2} -> Lemma (factorial x > x)

また都合が良ければ、次のように書くこともできます:

val factorial_is_greater_than_arg4: x:nat -> Lemma (requires (x > 2))
                                              (ensures (factorial x > x))

requires の後の式は関数/補題の 事前条件 で、ensures の後の式はその 事後条件 です。

3.3.3. 帰納によって証明された単純な補題について詳細に

ここで factorial_is_greater_than_arg の証明を詳細に見てみましょう。 それは次のようになります:

let rec factorial_is_greater_than_arg x =
  match x with
  | 3 -> ()
  | _ -> factorial_is_greater_than_arg (x - 1)

この証明は (let rec で示された) 再帰関数です; この関数は x に対する場合分けで定義されています。

最初のケースは、引数が 3 で; そのため factorial 3 > 3 を証明する必要があります。 F* はこの性質に相当する証明を生成し、前に提供された factorial の定義が与えられたとき、それを証明できるかどうかを確かめるよう Z3 に要求します—Z3 は factorial 3 = 6 であり、もちろん 6 > 3 で、このケースの証明は完了します。 これはこの帰納の基底ケースです。

ケースは順番に解釈されるため、2番目のケースに辿り着いた場合、最初のケースに当てはまらないことを知っています。 すなわち、2番目のケースでは factorial_is_greater_than_arg の型から x:nat{x > 2} を、前のケースに当てはまらなかったので x <> 3 であることを知っています。 別の言い方をすると、2つ目のケースは帰納ステップで、x > 3 のときの証明を扱います。

くだけた表現をすると、このケースの証明は、次で与えられる帰納法の仮定を使って行なわれます:

forall n, 2 < n < x ==> factorial n > n

そしてゴールは factorial x > x を証明することです。 もしくは等価に、factorial (x - 1) > x - 1 が既知であるときに x * factorial (x - 1) > x を証明することでう; さらにもしくは x*x - x > x を証明することになり—これは x > 3 のとき真です。 どのように F* でこれが形式的に行なわれるか見てみましょう。

全域再帰関数を定義するとき、定義されるその関数 (この場合 factorial_is_greater_than_arg) はその定義の本体で使うことができます。 しかしそれは再帰呼び出しが停止することを確認できる型である場合のみです。 このケースでは、定義本体中の factorial_is_greater_than_arg の型は:

n:nat{2 < n && n < x} -> Lemma (factorial n > n)

これはもちろん正確に帰納法の仮定です。 2番目のケースで factorial_is_greater_than_arg (x - 1) を呼び出すことで、実質的に帰納法の仮定を使用して factorial (x - 1) > x - 1 を証明し、2 < x - 1 && x - 1 < x を証明できます—これを Z3 に証明させると、このケースでは x > 3 であることを知っているのでそれは成功します。 最後に、x > 3 と 帰納法の仮定を使って得られた性質からゴールである factorial x > x を証明しなければなりません: Z3 は再びこれをたやすく証明してくれます。

val fibonacci : nat -> Tot nat
let rec fibonacci n =
  if n <= 1 then 1 else fibonacci (n - 1) + fibonacci (n - 2)

val fibonacci_greater_than_arg : n:nat{n >= 2} -> Lemma (fibonacci n >= n)

let rec fibonacci_greater_than_arg n =
  match n with
  | 2 -> ()
  | _ -> fibonacci_greater_than_arg (n-1)

3.4. Admit

証明を構築する際、証明の部品を仮定して別の部品に集中することはしばしば有用です。 例えば、ケース分析を行なっている際、ケースは自明で F* が自動的に解決できるのか、ケースが手動での証明を必要としているのかしばしば知りたくなります。 1つのケースの全てを承認 (admit) することでこれを実現できます。 F* が補題を自動的に証明できるなら、そのケースは自明です。 このような目的のために、F* は admit 関数を提供していて、それは次のように使います:

    let rec factorial_is_greater_than_arg x =
      match x with
      | 3 -> ()
      | _ -> admit()

この型検査には成功するので、帰納の基底ケースは自明に証明され、帰納ケースにフォーカスすべきであることがわかります。

3.5. bool と Type の詳細

もしこのタイトルが不可解に思えたなら、はじめて読む際にこの章をスキップすることができます。 けれどもリファインメント型で量化された式を使いはじめるなら、この章を理解しているか確かめるべきです。

以前、リファイメント型は x:t{phi(x)} の形を取ると言及しました。 その初期の形では、phi は実際には型で、値 x:t 上の述語です。 型の代わりにブール関数を使うことができ、次のような変換を加えることで、型にブールを暗黙に反感します:

b2t (b:bool) : Type = (b == true)

型 ‘==’ は等式の述語を表わす型コンストラクタです; それは ‘=’ とは異なり、値のペアを比較するブール関数です。 加えて ‘==’ はヘテロジニアスです: その型にかかわらず、どのような値のペアに関して等式を主張することができます。 対照的に ‘=’ はホモジニアスです。

命題の結合 /\, \/, ~ はそれぞれ論理積, 論理和, 否定を表わし、それらは型コンストラクタです。 また単方向と双方向の論理包含を表わす ==> と <==> もあります。 対照的に &&, ||, not はブール関数です。

bool から Type への暗黙の変換のために、これら2つの間の差異をほとんど気にせずに済みます。 けれども、量化を共なうリファインメント式を書きはじめるなら、両者の差異は明白になります。

全称量化 forall と存在量化 exists は Type でのみ有効です。 ブール関数と量化を含むリファインメントを混ぜる場合、命題の結合を使う必要があります。 例えば、次の式は正しい形です:

canRead e /\ forall x. canWrite x ==> canRead x

これは次のようなより複雑な形の短縮形です:

b2t(canRead e) /\ forall x. b2t(canWrite x) ==> b2t(canRead x)

一方、次の式は正しくありません; F* はこれを拒否します:

canRead e && forall x. canWrite x ==> canRead x

その理由はこの量化は型で、その一方 && はブールを期待しているためです。 ブールは型に変換できますが、別の方向の変換はありません。

4. 単純な帰納型

次は F* での (イミュータブルな) リストの標準的な定義です。

type list 'a =
  | Nil  : list 'a
  | Cons : hd:'a -> tl:list 'a -> list 'a

F* でのデータ型のコンストラクタにはいくつかの重要な慣習があります。

• コンストラクタ名は大文字ではじまらなければなりません。

• コンストラクタ型に作用を書かなかった場合、その結果のデフォルトの作用 (関数型とは対照的に) は Tot です。 そのため Cons: 'a -> list 'a -> list 'a と書いたなら、F* はそれを Cons: 'a -> Tot (list 'a -> Tot (list 'a)) と解釈します。

• コンストラクタはカリー化できます。 そのため通常上記のような帰納型を定義して、(アンカリー化された) Cons(hd,tl) ではなく (カリー化された) Cons hd tl と書くことができます。

• コンストラクタは部分適用できます。 そのため Cons hd は正しく、hd:'a のときその型は list 'a -> Tot (list 'a) になります。

list 型は F* の標準の prelude で定義されていて、全ての F* プログラム中で暗黙的に有効です。 リストコンストラクタに対して特別な (しかし標準的な) 構文が提供されています:

• [] は Nil です。
• [v1;...;vn] は Cons v1 ... (Cons vn Nil) です。
• hd::tl は Cons hd tl です。

(例えば Cons を部分適用するといった) 有用な場面では、Nil と Cons のようなコンストラクタを明示的に書くことができます。

4.1. リストに対する基本的な関数の証明

リストに対する通常の関数は、他の ML 方言と同様に F* でも書くことができます。 次は length 関数です:

val length: list 'a -> Tot nat
let rec length l = match l with
  | [] -> 0
  | _ :: tl -> 1 + length tl

length の型は、この関数が 'a 型の値のリストに対する全域関数で、非負の整数を返すことを証明しています。

let rec append l1 l2 = match l1 with
  | [] -> l2
  | hd :: tl -> hd :: append tl l2

    l1:list 'a -> l2:list 'a -> Tot (l:list 'a{length l = length l1 + length l2})

val append:list 'a -> list 'a -> Tot (list 'a)

val append_len: l1:list 'a -> l2:list 'a
             -> Lemma (requires True)
                      (ensures (length (append l1 l2) = length l1 + length l2)))
let rec append_len l1 l2 = match l1 with
    | [] -> ()
    | hd::tl -> append_len tl l2

val append_mem:  l1:list 'a -> l2:list 'a -> a:'a
        -> Lemma (ensures (mem a (append l1 l2)  <==>  mem a l1 || mem a l2))

val mem: 'a -> list 'a -> Tot bool
let rec mem a l = match l with
  | [] -> false
  | hd::tl -> hd=a || mem a tl

val append_mem:  l1:list 'a -> l2:list 'a -> a:'a
    -> Lemma (ensures (mem a (append l1 l2)  <==>  mem a l1 || mem a l2))
let rec append_mem l1 l2 a = match l1 with
  | [] -> ()
  | hd::tl -> append_mem tl l2 a

4.2. 本質的に型となるのか、もしくは補題を証明するか？

前章の練習問題のように、関数の型を強化したり、その関数に関する分離した補題を書くことで性質を証明できます—私達はそれらをそれぞれ ‘intrinsic’ スタイルと ‘extrinsic’ スタイルと呼んでいます。 どちらのスタイルが向いているかは好みと利便性の問題です: (例えば length が nat を返すといったような) 一般に有用な性質は intrinsic な仕様が相応しいでしょう; より具体的な性質は補題で表明して証明した方が良いでしょう。 けれども次の例のようにいくつかの場合では、型で直接関数の性質を証明するのは不可能なときがあります—補題に頼らねばなりません。

val reverse: list 'a -> Tot (list 'a)
let rec reverse = function
  | [] -> []
  | hd::tl -> append (reverse tl) [hd]

リストを二度逆順する関数が恒等関数であることを証明してみましょう。 リファインメント型を使って reverse の型にこの性質を 明記 することができます。

val reverse: f:(list 'a -> Tot (list 'a)){forall l. l = f (f l)}

けれども、F* はこれを reverse の有効な型として許容しません: この性質を証明するには2つの分離された帰納が必要で、そのどちらも F* は自動的に行ないません。

その代わりに、2つの補題を使ってこの性質を証明できます。 それらの補題は次のようになります:

let snoc l h = append l [h]

val snoc_cons: l:list 'a -> h:'a -> Lemma (reverse (snoc l h) = h::reverse l)
let rec snoc_cons l h = match l with
  | [] -> ()
  | hd::tl -> snoc_cons tl h

val rev_involutive: l:list 'a -> Lemma (reverse (reverse l) = l)
let rec rev_involutive l = match l with
  | [] -> ()
  | hd::tl -> rev_involutive tl; snoc_cons (reverse tl) hd

rev_involutive の Cons ケースでは、帰納法の仮定だけでなく上記せ証明済みの補題 snoc_cons も明示的に適用しています。

val rev_injective: l1:list 'a -> l2:list 'a
                -> Lemma (requires (reverse l1 = reverse l2))
                         (ensures  (l1 = l2))

val snoc_injective: l1:list 'a -> h1:'a -> l2:list 'a -> h2:'a 
                 -> Lemma (requires (snoc l1 h1 = snoc l2 h2))
                          (ensures (l1 = l2 && h1 = h2))
let rec snoc_injective l1 h1 l2 h2 = match l1, l2 with
  | _::tl1, _::tl2 -> snoc_injective tl1 h1 tl2 h2
  | _ -> ()

val rev_injective1: l1:list 'a -> l2:list 'a 
                -> Lemma (requires (reverse l1 = reverse l2))
                         (ensures  (l1 = l2)) (decreases l1)
let rec rev_injective1 l1 l2 =
  match l1,l2 with
  | h1::t1, h2::t2 ->
      // assert(reverse (h1::t1) = reverse (h2::t2));
      // assert(snoc (reverse t1) h1  = snoc (reverse t2) h2);
      snoc_injective (reverse t1) h1 (reverse t2) h2;
      // assert(reverse t1 = reverse t2 /\ h1 = h2);
      rev_injective1 t1 t2
      // assert(t1 = t2 /\ h1::t1 = h2::t2)
  | _, _ -> ()

val rev_injective2: l1:list 'a -> l2:list 'a 
                -> Lemma (requires (reverse l1 = reverse l2))
                         (ensures  (l1 = l2))
let rev_injective2 l1 l2 = rev_involutive l1; rev_involutive l2

4.3. リストに対する高階関数

4.3.1. マップ

リストに対する高階関数、すなわち引数として別の関数を取る関数を書くことができます。 次はおなじみの map です:

  let rec map f l = match l with
    | [] -> []
    | hd::tl -> f hd :: map f tl

これは関数 f とリスト l を取り、l のそれぞれの要素に f を適用して新しいリストを生成します。 より正確には map f [a1; ...; an] はリスト [f a1; ...; f an] を生成します。 例えば:

map (fun x -> x + 1) [0;1;2] = [1;2;3]

通常、仕様がない場合、F* は map の型を ('a -> 'b) -> list 'a -> list 'b と推論します。 明確に書くと、map の型は ('a -> ML 'b) -> Tot (list 'a -> ML (list 'b)) です。 f の型もデフォルトでは作用 ML を持つ関数となることに注意してください。

型注釈を追加することで、map に 異なる 型を与えることができます:

val map: ('a -> Tot 'b) -> list 'a -> Tot (list 'b)

この型は F* が推論した型のサブタイプでもスーパータイプでもありません。

作用に対するパラメトリック多相はありません: map にもっと汎用的な型を与えたいと思うかもしれません。 あらゆる作用 E を共ない、同じ作用を持つ関数を返す関数を許容したいと思うでしょう。 これは作用に対して多相の一種を要求することになりますが、F* はそのような多相をサポートしていません。 このためいくらかードの重複を誘発します。 私達はこれを解決するために、アドホックなオーバライド機構を用いて、値に対して1つ以上の型を書けるようになるよう計画しています。

4.3.2. 検索

    type option 'a =
       | None : option 'a
       | Some : 'a -> option 'a

    let rec find f l = match l with
      | [] -> None
      | hd::tl -> if f hd then Some hd else find f tl

module Find

type option 'a =  
   | None : option 'a
   | Some : 'a -> option 'a

(* The intrinsic style is more convenient in this case *)
val find : f:('a -> Tot bool) -> list 'a -> Tot (option (x:'a{f x}))
let rec find f l = match l with
  | [] -> None
  | hd::tl -> if f hd then Some hd else find f tl

(* Extrinsically things are more verbose, since we are basically duplicating
   the structure of find in find_some. It's still not too bad. *)

val find' : f:('a -> Tot bool) -> list 'a -> Tot (option 'a)
let rec find' f l = match l with
  | [] -> None
  | hd::tl -> if f hd then Some hd else find' f tl

val find_some : f:('a -> Tot bool) -> l:list 'a -> x:'a -> Lemma
                  (requires (find' f l = Some x))
                  (ensures (f x = true))
let rec find_some f l x =
  match l with
  | [] -> ()
  | hd::tl -> if f hd then () else find_some f tl x

fold_left f [b1; ...; bn] a = f (bn, ... (f b2 (f b1 a)))

val fold_left_cons_is_reverse: l:list 'a -> l':list 'a ->
      Lemma (fold_left Cons l l' = append (reverse l) l')

val fold_left: f:('b -> 'a -> Tot 'a) -> l:list 'b -> 'a -> Tot 'a
let rec fold_left f l a = match l with
  | Nil -> a
  | Cons hd tl -> fold_left f tl (f hd a)

val append_cons: l:list 'a -> hd:'a -> tl:list 'a ->
                 Lemma (append l (Cons hd tl) = append (append l (Cons hd Nil)) (tl))
let rec append_cons l hd tl = match l with
  | Nil -> ()
  | Cons hd' tl' ->
    append_cons tl' hd tl

val snoc_append: l:list 'a -> h:'a -> Lemma (snoc l h = append l (Cons h Nil))
let rec snoc_append l h = match l with
  | Nil -> ()
  | Cons hd tl ->
    snoc_append tl h

val reverse_append: tl:list 'a -> hd:'a ->
                  Lemma (reverse (Cons hd tl) = append (reverse tl) (Cons hd Nil))
let reverse_append tl hd = snoc_append (reverse tl) hd

val fold_left_cons_is_reverse: l:list 'a -> l':list 'a ->
                             Lemma (fold_left Cons l l' = append (reverse l) l')
let rec fold_left_cons_is_reverse l l' = match l with
  | Nil -> ()
  | Cons hd tl ->
    fold_left_cons_is_reverse tl (Cons hd l');
    append_cons (reverse tl) hd l';
    reverse_append tl hd

4.4. 帰納型に対して暗黙に定義された関数

帰納型のそれぞれの定義対して、F* は多くの有用な関数を自動的に導入します: それぞれのコンストラクタには、discriminator が手に入り; それぞれのコンストラクタのそれぞれの引数には、projector が手に入ります。 実行例として (以下に繰り返し示す) リスト型を使ってこれらを次に説明します。

type list 'a =
  | Nil  : list 'a
  | Cons : hd:'a -> tl:list 'a -> list 'a

4.4.1. Discriminator

discriminator はブール値の全域関数で、項が個別のコンストラクタの適用であるかどうか調べます。 list 型に対して、2つの discriminator が手に入ります:

val is_Nil: list 'a -> Tot bool
let is_Nil xs = match xs with [] -> true | _ -> false

val is_Cons: list 'a -> Tot bool
let is_Cons xs = match xs with _::_-> true | _ -> false

4.4.2. Projector

Cons コンストラクタの型から、F* は次のシグニチャを生成します:

val Cons.hd : l:list 'a{is_Cons l} -> Tot 'a
val Cons.tl : l:list 'a{is_Cons l} -> Tot (list 'a)

(ここでは Cons.hd は限定された名前です)

これは、Cons の型での名前 hd と tl が意味がある理由を示しています: それらは自動生成された projector の名前に相当します。 もしデータコンストラクタの引数に名前をつけなかったら、F* は名前を自動生成します。 (とはいえ、これらの名前は引数の位置から導出され、その形は仕様化されていません; そのため、自分自身で引数に名前をつけるのは良い習慣です。)

module HdTl

val hd : l:list 'a{is_Cons l} -> Tot 'a
val tl : l:list 'a{is_Cons l} -> Tot (list 'a)

val hd : l:list 'a{is_Cons l} -> Tot 'a
let hd l =
  match l with
  | h :: t -> h

val tl : l:list 'a{is_Cons l} -> Tot (list 'a)
let tl l =
  match l with
  | h :: t -> t

(* ここにコードを書いてください *)

val nth : l:list 'a -> n:nat{n < length l} -> 'a
let rec nth l n =
  match l with
  | h :: t -> if n = 0 then h else nth t (n-1)

4.5. タプルとレコード

F* はタプルに対するシンタックスシュガーを提供しています。 タプルは単なる帰納型です: 2–8 サイズのタプルは標準 prelude で定義されています。 (もし必要なら追加できます。) 次は prelude におけるペアの定義です:

type tuple2 'a 'b =
  | MkTuple2: _1:'a -> _2:'b -> tuple2 'a 'b

MkTuple2 5 7 の代わりに (5, 7) と書くことができ、ペアには tuple2 int int を短縮した型 (int * int) を与えることができます。

この表記は、prelude で定義された関連した tupleN データ型と同じサイズのタプルを生成します。

また F* はレコードに対する構文も提供します。 けれどもレコードは (タプルと同じように) 単一コンストラクタのデータ型に内部で要約されます。 次はこの例です:

type triple 'a 'b 'c = {fst:'a; snd:'b; third:'c}
let f x = x.fst + x.snd + x.third

F* はこのプログラムを受け付け、f に型 (triple int int int -> Tot int) を与えます。

これは次のようなより冗長なソースコードを等価です:

type triple 'a 'b 'c =
  | MkTriple: fst:'a -> snd:'b -> third:'c -> triple 'a 'b 'c

let f x = MkTriple.fst x + MkTriple.snd x + MkTriple.third x

5. 停止性の証明

F* は全ての純粋な関数は停止することが証明されています。 F* で使われている停止性の検査は syntactic condition ではなく semantic criterion に基づいています。 F* の停止性検査の基本の概略を説明します—より興味深いプログラムを書くためには停止性について理解が必要になります。

5.1. 値に対する整礎半順序

F* で関数の停止を証明するために、ある尺度を提供します: それはその関数の引数に依存した純粋な式です。 F* はそれぞれの再帰呼び出しでこの尺度が厳密に減少することを検査します。 呼び出しにおける引数に対するこの尺度は、F* の値に対する整礎半順序に従って、前回の呼び出しでの尺度と比較されます。 この順序で v1 が v2 より 小さい とき、v1 << v2 と書きます。

もし R が S に対する半順序で、R に関する S 中の無限降鎖がなければ、集合 S に対する関係 R は整礎半順序です。 例えば、自然数の集合 nat である S を取るとき、整数の順序 < は整礎半順序です (実際にはこれは全順序です)。

この尺度はそれぞれの再帰呼び出しで厳密に減少し、かつ無限降鎖がないので、これは再帰呼び出しで関数が最終的に停止することを保証します。

5.1.1. 減少関係

1. 整数に対する順序: i, j : nat が与えられたとき、i << j <==> i < j が得られます。

   注意: 単なる 半 順序なので、負の整数は << 関係ではありません。

2. 帰納型に対するサブ項順序: (D が v1 から vn の引数に適用されたコンストラクタであるような) 帰納型のどのような値 D v1 ... vn に対しても、全ての i において v_i << v が得られます。 すなわち、正しく型付けされた項のサブ項はその項より小さくなります。 (この規則の例外は次の lex_t です。)

3. lex_t に対する辞書式順序: 以下で説明します。

5.1.2. 辞書式順序のペア

昔ながらの関数 ackermann を見てみましょう:

val ackermann: m:nat -> n:nat -> Tot nat
let rec ackermann m n =
  if m=0 then n + 1
  else if n = 0 then ackermann (m - 1) 1
  else ackermann (m - 1) (ackermann m (n - 1))

なぜこれは停止するのでしょうか？ それぞれの再帰呼び出しにおいて、全ての引数が前回の呼び出しでの引数より厳密に小さく ならない ケースがあります。 例えば2番目の分岐において n は 0 から 1 に増加します。 けれどもこの関数は実際に停止し、F* はそれを証明します。

その理由は、全ての再帰呼び出しにおいてそれぞれの引数は減少していませんが、それらを一緒に取るとき、引数 (m,n) の順序ペアはペアの 辞書式順序 に従って減少しているからです。

標準 prelude では、F* は次の帰納型を定義しています:

type lex_t =
  | LexTop  : lex_t
  | LexCons : #a:Type -> a -> lex_t -> lex_t

(# 記号は1番目の引数が暗黙的であるとマークしています。8.3.1 を見てください。)

lex_t の辞書式順序 は次のようになります:

• もし v1 << v1' もしくは、v1=v1' かつ v2 << v2' ならば、LexCons v1 v2 << LexCons v1' v2' です。

• もし v:lex_t かつ v <> LexTop ならば v << LexTop です。

次のシンタックスシュガーを使えます:

%[v1;...;vn] は (LexCons v1 ... (LexCons vn LexTop)) の短縮形です

5.2. 停止性証明の詳細

次の形を使って再帰による関数を定義しているとしましょう:

val f: y1:t1 -> .. -> yn:tn -> Tot t
let rec f x1 .. xn = e

通常 ML では e を型検査するとき、再帰的に束縛された関数 f に、型 y1:t1 -> .. -> yn:tn -> Tot t で e を用いることができます。 この型はプログラマによって正確に書き下されます。 けれどもこの型は、f の呼び出しが無限の再帰呼び出しを誘発してしまわないことを保証するのに十分ではありません。

停止性を証明するために (すなわちを無限の深い再帰呼び出しを除外するために)、F* は再帰関数の型検査に異なる規則を用います。 次に示すより制限された型においてのみ、再帰的に束縛された名前 f は e で用いることができます:

   y1:t1
-> ...
-> yn:tn{%[y1;...;yn] << %[x1;...;xn]}
-> Tot t

すなわち、デフォルトでは F* は関数のパラメータが (全ての関数型のパラメータを除いてパラメータが出現する順序で) そのパラメータの辞書式順序に従って減少することを要求します。 (このデフォルトを上書きする方法があります—章 5.2.2 を見てください。)

いくつかの例でこれがどのように働くのか見てみましょう。

5.2.1. アッカーマン

F* は ackermann 関数

1.  let rec ackermann m n =
2.    if m=0 then n + 1
3.    else if n = 0 then ackermann (m - 1) 1
4.    else ackermann (m - 1)
5.                   (ackermann m (n - 1))

が停止することを自動的に示すことができます。このときその型は次のようになります:

ackermann : nat -> nat -> Tot nat

F* はこの関数にデフォルトの停止性メトリクスを与えます。 そのためこの関数は次のように展開されます:

ackermann : m:nat -> n:nat -> Tot nat (decreases %[m;n])

decreases 節は次の章で議論します。 この例では、この節は ackermann の本体中の再帰呼び出しを表わす次のようなより制限された型を F* 型検査器に使わせます:

ackermann: m':nat
        -> n':nat{%[m';n'] << %[m;n]}
        -> Tot nat

ackermann への3つの再帰呼び出しそれぞれにおいて、その引数が非負であるだけでなく、それらが上記のリファインメント式に従って前回の引数より小さくなることも証明する必要があります。

• 行3の呼び出しに対して、%[(m - 1);1] << %[m;n] を示す必要があります。 整数の順序に従って m - 1 << m であるので、これは解決します。 そしてこの項の残りは無視できます。

• 行4の呼び出しは同じ理由で検査できます—1番目の引数が減少しています。

• 行5の呼び出しに対して、%[m; (n-1)] << %[m; n] を示す必要があります。 ここではそれぞれのペアの1番目の要素は等しいため、2番目の要素を見ます。 そしてそれは n - 1 << n であるので、証明は完了します。

5.2.2. decreases 節

もちろん、ときどき再帰関数のデフォルト尺度を上書きする必要があります。 もし単純に ackermann 関数の引数を入れ換えたら、デフォルト尺度はもはや働きません。 そして、最初に m を比較してから n を比較するような辞書式順序を選択する decreases 節を明示的に追加する必要があります:

val ackermann_swap: n:nat -> m:nat -> Tot nat (decreases %[m;n])
let rec ackermann_swap n m =
   if m=0 then n + 1
   else if n = 0 then ackermann_swap 1 (m - 1)
   else ackermann_swap (ackermann_swap (n - 1) m)
                       (m - 1)

この任意の decreases 節は作用 Tot の2番目の引数です。 一般にこれはその関数の引数の全域の式です。

val rev : l1:list 'a -> l2:list 'a -> Tot (list 'a) (decreases l2)
let rec rev l1 l2 =
  match l2 with
  | []     -> l1
  | hd::tl -> rev (hd::l1) tl

val rev_is_ok : l:list 'a -> Lemma (rev [] l = reverse l)

val append_assoc : xs:list 'a -> ys:list 'a -> zs:list 'a -> Lemma
      (ensures (append (append xs ys) zs = append xs (append ys zs)))
let rec append_assoc xs ys zs =
  match xs with
  | [] -> ()
  | x::xs' -> append_assoc xs' ys zs

val rev_is_ok_aux : l1:list 'a -> l2:list 'a -> Lemma
      (ensures (rev l1 l2 = append (reverse l2) l1)) (decreases l2)
let rec rev_is_ok_aux l1 l2 =
  match l2 with
  | [] -> ()
  | hd::tl  -> rev_is_ok_aux (hd::l1) tl; append_assoc (reverse tl) [hd] l1

val append_nil : xs:list 'a -> Lemma
      (ensures (append xs [] = xs))
let rec append_nil xs =
  match xs with
  | [] -> ()
  | _::tl  -> append_nil tl

val rev_is_ok : l:list 'a -> Lemma (rev [] l = reverse l)
let rev_is_ok l = rev_is_ok_aux [] l; append_nil (reverse l)

val fib : nat -> nat -> n:nat -> Tot nat (decreases n)
let rec fib a b n =
  match n with
  | 0 -> a
  | _ -> fib b (a+b) (n-1)

val fib_is_ok : n:nat -> Lemma (fib 1 1 n = fibonacci n)

val fib_is_ok_aux : i:nat -> n:nat{i<=n} ->
      Tot (u:unit{fib (fibonacci i) (fibonacci (i+1)) (n-i) = fibonacci n})
      (decreases (n-i))
let rec fib_is_ok_aux i n =
  if i=n then ()
  else fib_is_ok_aux (i+1) n

val fib_is_ok : n:nat -> Lemma (fib 1 1 n = fibonacci n)
let fib_is_ok n = fib_is_ok_aux 0 n

5.3. 相互再帰関数

相互再帰関数に対しても、停止性の証明に対する同じ戦略が使えます。 相互再帰関数の場合、 F* の停止性検査器は、全ての直接もしくは相互再帰呼び出しが呼び出された関数の停止性メトリクスを減少させることを要求します。 これは非常に強い要求です。 次の例を考えてみましょう:

val foo : l:list int -> Tot int
val bar : l:list int -> Tot int
let rec foo l = match l with
    | [] -> 0
    | x::xs -> bar xs
and bar l = foo l

(bar を通して) foo は常にサブリストに対して呼び出されるので、この関数は停止します。 けれども bar からの foo 呼び出しはより小さなリストに対してではありません。 デフォルトのメトリクスを用いるとこの例は検査できません。

2つの関数が停止することを F* に納得させるために、カスタムのメトリクスを使うことができます:

val foo : l:list int -> Tot int (decreases %[l;0])
val bar : l:list int -> Tot int (decreases %[l;1])

foo と bar のメトリクスは両方とも、1つ目は引数 l で2つ目は 0 もしくは 1 であるような辞書式のタプルです。 foo からの bar 呼び出しは l を減少させ、bar からの foo 呼び出しは l を同じ値で保ちますが2番目の要素を 1 から 0 に減少させます。

6. これまでの要素をまとめる

ここで、これまで学んできた様々な機能を練習する2つの完全なプログラムを見てみましょう。 そのぞれの練習では、それらのプログラムを修正したり一般化したりするための練習問題があります。

6.1. リストのクイックソート

プログラムの検証に対する標準的な例は、様々なソートアルゴリズムが正しいことを証明することです。

整数のリストからはじめて、いくつかの性質を表現しましょう。 整数のリストを昇順にソートする関数 sorted からはじめて、ソートアルゴリズムが真であることを言いたいのです。

  val sorted: list int -> Tot bool
  let rec sorted l = match l with
      | [] -> true
      | [x] -> true
      | x::y::xs -> x <= y && sorted (y::xs)

ソートアルゴリズム sort が与えられたとき、次の性質を証明したいとします。 このとき mem は、先のリストの練習問題でのリストのメンバーシップ関数です (章 4.1 を見てください)。

sorted (sort l) /\ ( forall i. mem i l <==> mem i (sort l) )

この仕様が改良できることを以降で見てみましょう。

6.1.1. クイックソートを実装する

次はクイックソートアルゴリズムの単純な実装です。 この実装は常にリストの1つ目の要素をピボットとして取り出し; リストの残りをピボット以上の要素を含む区画とそれ以外を含む区画に分け; それらの区画を再帰的にソートし; そして返る前に中央にピボッドを挿入します。

let rec sort l = match l with
  | [] -> []
  | pivot::tl ->
    let hi, lo  = partition (fun x -> pivot <= x) tl in
    append (sort lo) (pivot::sort hi)

val partition: ('a -> Tot bool) -> list 'a -> Tot (list 'a * list 'a)

val partition: ('a -> Tot bool) -> list 'a -> Tot (list 'a * list 'a)
let rec partition f = function
  | [] -> [], []
  | hd::tl ->
     let l1, l2 = partition f tl in
     if f hd
     then hd::l1, l2
     else l1, hd::l2

6.1.2. sort を明記する

本質的に sort を検証します。 けれどもいくつか追加の補題を使う必要があります。 次は仕様の最初の試みです。 F* にこれを証明させてみてください。

val sort0: l:list int -> Tot (m:list int{sorted m /\ (forall i. mem i l <==> mem i m) })

当然これはいくつかの点で失敗します:

1. この関数が全域であることの証明に失敗します。 どうすればそれぞれの sort 呼び出しが小さくなる引数を取ることを主張できるでしょうか？ 直感的にそれぞれの再帰呼び出しにおいて、引数として渡されるリストの長さは、tl の区画なので、厳密に小さくなります。 これを表わすために、decreases 節を追加する必要があります。

2. ソートの性質とメンバーシップの性質の両方の証明に失敗します—partition と sorted 関数に関する補題が必要です。

再び挑戦してみましょう:

val sort: l:list int -> Tot (m:list int{sorted m
                                     /\ forall i. mem i l <==> mem i m})
                            (decreases (length l))

そして次は partition と sorted に関する2つの補題です:

 val partition_lemma: f:('a -> Tot bool)
    -> l:list 'a
    -> Lemma (requires True)
             (ensures ((length (fst (partition f l))
                      + length (snd (partition f l)) = length l
                  /\ (forall x. mem x (fst (partition f l)) ==> f x)
                  /\ (forall x. mem x (snd (partition f l)) ==> not (f x))
                  /\ (forall x. mem x l = (mem x (fst (partition f l))
                                        || mem x (snd (partition f l)))))))
 let rec partition_lemma f l = match l with
   | [] -> ()
   | hd::tl -> partition_lemma f tl

 val sorted_concat_lemma: l1:list int{sorted l1}
                       -> l2:list int{sorted l2}
                       -> pivot:int
                       -> Lemma (requires ((forall y. mem y l1 ==> not (pivot <= y))
                                        /\ (forall y. mem y l2 ==> pivot <= y)))
                                (ensures (sorted (append l1 (pivot::l2))))
 let rec sorted_concat_lemma l1 l2 pivot = match l1 with
  | [] -> ()
  | hd::tl -> sorted_concat_lemma tl l2 pivot

最後に、以前の練習問題で示した補題の全称量化された変種 append_mem も必要になります:

 val append_mem:  l1:list 'a
               -> l2:list 'a
               -> Lemma (requires True)
                        (ensures (forall a. mem a (append l1 l2) = (mem a l1 || mem a l2)))
 let rec append_mem l1 l2 = match l1 with
   | [] -> ()
   | hd::tl -> append_mem tl l2

これらの補題とともに、クイックソートの実装に戻りましょう。 不幸にも、これらの補題を使っても、クイックソートの元の実装が正しいことをまだ証明できません。 (章 4.1 の) rev_injective の証明で見たように、それらの性質を使うために明示的に補題を呼び出す必要があります。 すぐに上手く行きますが、証明を通すために補題を呼び出して sort をどうやって修正するのか見てみましょう。

let cmp i j = i <= j
val sort_tweaked: l:list int -> Tot (m:list int{sorted m /\ (forall i. mem i l = mem i m)})
                                    (decreases (length l))
let rec sort_tweaked l = match l with
  | [] -> []
  | pivot::tl ->
    let hi', lo' = partition (cmp pivot) tl in
    partition_lemma (cmp pivot) tl;
    let hi = sort_tweaked hi' in
    let lo = sort_tweaked lo' in
    append_mem lo (pivot::hi);
    sorted_concat_lemma lo hi pivot;
    append lo (pivot::hi)

これは上手く行きますが、少し不恰好です。 補題を呼び出して実装を汚す必要があっただけでなく、それらの呼び出しのために、それらの補題への引数のために名前を束縛できるようにコードを書き換えなければなりませんでした。 これは改善することができます。

6.1.3. SMT 補題: intrinsic と extrinsic な証明のギャップを埋める

もし partition と sorted に補題を使って早明した性質を捕捉するより豊かな intrinsic な型を与えたいだけなら、クイックソートの実装を汚したくありませんでした。 これは intrinsic な証明スタイルを使う重要な利点です—partition (fun x -> pivot <= x) tl のような関数の全ての呼び出しは、その関数に関して本質的に証明された全ての性質を直接持っています。

けれども、アプリケーション特有の型を持つ一般目的の関数の型に対する汚染もまたひどいものでしょう。 sorted の型を sorted_concat_lemma によって証明された性質で改良することを考えてみましょう。 sorted は一般的な仕様で挿入ソートやマージソートでも働くのに対して、この補題はクイックソートに高度に特化されています。 その型を汚すことは役立たずです。 そのため困難に陥いっているようです。

もし補題によって関数 f について証明された性質を、遡って直接 f と結びつける方法があったら良いと思いませんか？ 全ての適用 f x が直接その補題の性質を持てるようにするのです。 F* は、このような intrinsic と extrinsic な証明のギャップを埋める方法を提供します。

仮に次のような partition_lemma の型を書いたとします—唯一の違いは最後の行で、[SMTPat (partition f l)] を追加しています。 この行は、項 partition f l の全ての出現とその補題によって証明された性質を関連付けるよう、F* と SMT ソルバに支持します。

val partition_lemma: f:('a -> Tot bool)
  -> l:list 'a
  -> Lemma (requires True)
           (ensures ((length (fst (partition f l))
                    + length (snd (partition f l)) = length l
                /\ (forall x. mem x (fst (partition f l)) ==> f x)
                /\ (forall x. mem x (snd (partition f l)) ==> not (f x))
                /\ (forall x. mem x l = (mem x (fst (partition f l))
                                      || mem x (snd (partition f l)))))))
                     [SMTPat (partition f l)]

同様に、次は sorted_concat_lemma の改良された型です。 このとき、補題の性質を特化した項にのみ関連付けるよう、F* と SMT ソルバに支持します: その項は次のような形です。

sorted (append 11 (pivot::l2))

受け入れ可能な検証時間にするために、より特化したパターンを与えることで、SMT ソルバが補題をより区別して適用するようになります。

val sorted_concat_lemma: l1:list int{sorted l1}
                      -> l2:list int{sorted l2}
                      -> pivot:int
                      -> Lemma (requires ((forall y. mem y l1 ==> not (pivot <= y))
                                       /\ (forall y. mem y l2 ==> pivot <= y)))
                               (ensures (sorted (append l1 (pivot::l2))))
                         [SMTPat (sorted (append l1 (pivot::l2)))]

最後に、同じ方法で append_mem の型も改良します:

val append_mem:  l1:list 'a
              -> l2:list 'a
              -> Lemma (requires True)
                       (ensures (forall a. mem a (append l1 l2) = (mem a l1 || mem a l2)))
                       [SMTPat (append l1 l2)]
let rec append_mem l1 l2 = match l1 with
  | [] -> ()
  | hd::tl -> append_mem tl l2

これらの改良されたシグニチャを使って、元に行なっていたのと同じ sort を書き、その関数に望んだ型を与えることができます。 SMT ソルバは与えた補題から必要な性質を暗黙的に導出します。

let cmp i j = i <= j
val sort: l:list int -> Tot (m:list int{sorted m /\ (forall i. mem i l = mem i m)})
                            (decreases (length l))
let rec sort l = match l with
  | [] -> []
  | pivot::tl ->
    let hi, lo = partition (cmp pivot) tl in
    append (sort lo) (pivot::sort hi)

6.1.4. 練習問題

(* "エディタに読み込む" リンクのコードからはじめてください *)

module QuickSortPoly


val mem: 'a -> list 'a -> Tot bool
let rec mem a l = match l with
  | [] -> false
  | hd::tl -> hd=a || mem a tl


val append : list 'a -> list 'a -> Tot (list 'a)
let rec append l1 l2 = match l1 with
  | [] -> l2
  | hd :: tl -> hd :: append tl l2


val append_mem:  l1:list 'a
              -> l2:list 'a
              -> Lemma (requires True)
                       (ensures (forall a. mem a (append l1 l2) = (mem a l1 || mem a l2)))
                       [SMTPat (append l1 l2)]
let rec append_mem l1 l2 = match l1 with
  | [] -> ()
  | hd::tl -> append_mem tl l2


val length: list 'a -> Tot nat
let rec length l = match l with
  | [] -> 0
  | _ :: tl -> 1 + length tl


(* Specification of sortedness according to some comparison function f *)
val sorted: ('a -> 'a -> Tot bool) -> list 'a -> Tot bool
let rec sorted f l = match l with
    | [] -> true
    | [x] -> true
    | x::y::xs -> f x y && sorted f (y::xs)


val partition: ('a -> Tot bool) -> list 'a -> Tot (list 'a * list 'a)
let rec partition f = function
  | [] -> [], []
  | hd::tl ->
     let l1, l2 = partition f tl in
     if f hd
     then hd::l1, l2
     else l1, hd::l2


val partition_lemma: f:('a -> Tot bool)
   -> l:list 'a
   -> Lemma (requires True)
            (ensures ((length (fst (partition f l))
                     + length (snd (partition f l)) = length l
                  /\ (forall x. mem x (fst (partition f l)) ==> f x)
                  /\ (forall x. mem x (snd (partition f l)) ==> not (f x))
                  /\ (forall x. mem x l = (mem x (fst (partition f l))
                                        || mem x (snd (partition f l)))))))
            [SMTPat (partition f l)]
let rec partition_lemma f l = match l with
    | [] -> ()
    | hd::tl -> partition_lemma f tl


(* Defining a new predicate symbol *)
opaque type total_order (a:Type) (f: (a -> a -> Tot bool)) =
    (forall a. f a a)                                           (* reflexivity   *)
    /\ (forall a1 a2. (f a1 a2 /\ a1<>a2)  <==> not (f a2 a1))  (* anti-symmetry *)
    /\ (forall a1 a2 a3. f a1 a2 /\ f a2 a3 ==> f a1 a3)        (* transitivity  *)

val sorted_concat_lemma: f:('a -> 'a -> Tot bool)
                      -> l1:list 'a{sorted f l1}
                      -> l2:list 'a{sorted f l2}
                      -> pivot:'a
                      -> Lemma (requires (total_order 'a f
                                       /\ (forall y. mem y l1 ==> not (f pivot y))
                                       /\ (forall y. mem y l2 ==> f pivot y)))
                               (ensures (sorted f (append l1 (pivot::l2))))
                               [SMTPat (sorted f (append l1 (pivot::l2)))]
let rec sorted_concat_lemma f l1 l2 pivot = match l1 with
    | [] -> ()
    | hd::tl -> sorted_concat_lemma f tl l2 pivot


val sort: f:('a -> 'a -> Tot bool){total_order 'a f}
       -> l:list 'a
       -> Tot (m:list 'a{sorted f m /\ (forall i. mem i l = mem i m)})
              (decreases (length l))
let rec sort f l = match l with
  | [] -> []
  | pivot::tl ->
    let hi, lo = partition (f pivot) tl in
    append (sort f lo) (pivot::sort f hi)

(* "エディタに読み込む" リンクのコードからはじめてください *)

module QuickSortPoly


val mem: 'a -> list 'a -> Tot bool
let rec mem a l = match l with
  | [] -> false
  | hd::tl -> hd=a || mem a tl


(* append now duplicates the elements of the first list *)
val append : list 'a -> list 'a -> Tot (list 'a)
let rec append l1 l2 = match l1 with
  | [] -> l2
  | hd :: tl -> hd :: hd :: append tl l2


val append_mem:  l1:list 'a
              -> l2:list 'a
              -> Lemma (requires True)
                       (ensures (forall a. mem a (append l1 l2) = (mem a l1 || mem a l2)))
                       [SMTPat (append l1 l2)]
let rec append_mem l1 l2 = match l1 with
  | [] -> ()
  | hd::tl -> append_mem tl l2


val length: list 'a -> Tot nat
let rec length l = match l with
  | [] -> 0
  | _ :: tl -> 1 + length tl


val sorted: list int -> Tot bool
let rec sorted l = match l with
    | [] -> true
    | [x] -> true
    | x::y::xs -> x <= y && sorted (y::xs)


val partition: ('a -> Tot bool) -> list 'a -> Tot (list 'a * list 'a)
let rec partition f = function
  | [] -> [], []
  | hd::tl ->
     let l1, l2 = partition f tl in
     if f hd
     then hd::l1, l2
     else l1, hd::l2


val partition_lemma: f:('a -> Tot bool)
                   -> l:list 'a
                   -> Lemma (requires True)
                            (ensures ((length (fst (partition f l)) + length (snd (partition f l)) = length l
                                  /\ (forall x. mem x (fst (partition f l)) ==> f x)
                                  /\ (forall x. mem x (snd (partition f l)) ==> not (f x))
                                  /\ (forall x. mem x l = (mem x (fst (partition f l)) || mem x (snd (partition f l)))))))
                            [SMTPat (partition f l)]
let rec partition_lemma f l = match l with
    | [] -> ()
    | hd::tl -> partition_lemma f tl


val sorted_concat_lemma: l1:list int{sorted l1}
                      -> l2:list int{sorted l2}
                      -> pivot:int
                      -> Lemma (requires ((forall y. mem y l1 ==> not (pivot <= y))
                                       /\ (forall y. mem y l2 ==> pivot <= y)))
                               (ensures (sorted (append l1 (pivot::l2))))
                               [SMTPat (sorted (append l1 (pivot::l2)))]
let rec sorted_concat_lemma l1 l2 pivot = match l1 with
    | [] -> ()
    | hd::tl -> sorted_concat_lemma tl l2 pivot


opaque type match_head (l1:list int) (l2:list int) =
  (l1 = [] /\ l2 = []) \/
  (exists h t1 t2. l1 = h::t1 /\ l2 = h::t2)

val dedup: l:list int{sorted l} -> Tot (l2:list int{sorted l2 /\ (forall i. mem i l = mem i l2) /\ match_head l l2})
  let rec dedup l =
    match l with
    | [] -> []
    | [x] -> [x]
    | h::h2::t ->
      if h = h2 then dedup (h2::t)
      else  h::dedup (h2::t)


let cmp i j = i <= j
val sort: l:list int -> Tot (m:list int{sorted m /\ (forall i. mem i l = mem i m)})
                            (decreases (length l))
let rec sort l = match l with
  | [] -> []
  | pivot::tl ->
    let hi, lo = partition (cmp pivot) tl in
    let l' = append (sort lo) (pivot::sort hi) in
    dedup l'