ATSプログラミング入門:
PrevNext

Chapter 12. 定理証明によるプログラミング

Table of Contents
非線形の制約を回避する
例: 安全な行列の添字演算
強化された正確性を使って明記する
例: もう一つの検証された階乗
例: 検証された高速な累乗

定理証明によるプログラミング - Programming with Theorem-Proving (PwTP) は豊かで広いプログラミングパラダイムで、プログラムと証明が構文的に絡み合って密着させることができます。 PwTP をサポートすることは ATS の主要な機能で、ATS の新規性は主にここにあります。 カリー＝ハワード同型対応に馴染んだ人々にとって、少しでも証明とプログラムの間でこの同型を本質的に使ったことがあれば、ATS でサポートされている PwTP は簡単であることを強調したいです: 書かれた ATS プログラムの動的な部分はもちろん純粋ではありませんし、 ATS/LF にエンコードされた証明は積極的に必要なわけでもありません。 けれども、ATS での関数型プログラミングのスタイルで記述できる証明の構築は ATS のデザインの観点で根本的に重要です。 プログラムを証明と結合することが必要なのです。

この章では、単純だけれど説得力のある例を使って ATS でサポートされる PwTP のパワーと柔軟性を説明します。 けれでも、PwTP を使った実用例は ATS の線形型を導入した後まで紹介できません。 線形型の証明はプログラムと結合して、メモリやオブジェクト (例: ファイルハンドル) のようなリソースを追跡したり安全に操作したりすることができます。 特に、PwTP は ATS における命令型プログラミングをサポートする土台となります。

この章で解説するコードと追加のテストコードは オンライン から入手できます。

非線形の制約を回避する

ATS の制約ソルバはやや非力な力しか持っていません。 特に、非線形の整数項を含む制約 (例: 値の乗法の使用を意味するような制約) はただちに破棄されます。 この非力さは当然対策されるべきです。さもなくば ATS の型システムの実用性における深刻な制限になってしまいます。 ここでは単純な例を使って、非線形の制約を直接扱う必要性を回避して定理証明を使うことができるのか説明します。

関数テンプレート list_concat は次のような実装です: 

//
// [list_concat] does typecheck in ATS2
// [list_concat] does not typecheck in ATS1
//
fun{
a:t@ype
} list_concat{m,n:nat}
(
  xss: list (list (a, n), m)
) : list (a, m * n) =
  case+ xss of
  | list_nil () => list_nil ()
  | list_cons (xs, xss) => list_append<a> (xs, list_concat xss)
// end of [list_concat]

list_append のインターフェイスは次のようになります: 

fun{
a:t@ype
} list_append {n1,n2:nat}
  (xs: list (a, n1), ys: list (a, n2)): list (a, n1+n2)

長さ m のリスト xss が与えられ、その要素がある型 T について型 list(T,n) である時、list_concat<T>(xss) は型 list(T,m*n) のリストをコンストラクトします。 list_concat のコードの最初のマッチ節が型検査されると、本質的に次のような制約が発生します: 

全ての自然数 m, m1, n について、m = m1 + 1 は n + (m1 * n) = m * n を意味している。

この制約は単純に見えますが、非線形な整数の項 (例: m1*n や m*n) を含んでいるので ATS の制約ソルバは破棄してしまいます。 この制限を克服 (もしくは回避) すれば、定理証明を使えるようになるはずです。 list_concat の別の実装は次のようになります: 

fun{
a:t@ype
} list_concat{m,n:nat}
(
  xss: list(list(a, n), m)
) : [p:nat] (MUL(m, n, p) | list(a, p)) =
(
//
case+ xss of
| list_nil () =>
    (MULbas() | list_nil())
| list_cons (xs, xss) => let
    val (pf | res) = list_concat (xss)
  in
    (MULind pf | list_append<a> (xs, res))
  end // end of [list_cons]
//
) (* end of [list_concat] *)

型 list(list(T,n),m) のリスト xss が与えられた時、 list_concat(xss) はペア (pf | res) を返します。 このペアの中で、自然数 p があるとき pf は命題型 MUL(m,n,p) の証明で、 res は型 list(T,p) のリストです。 この記号バー (|) は証明と値を分離するために使われます。 別の言い方をすると、pf は等式 p=m*n の証拠となります。 証明が削除されると、list_concat のこの実装は本質に (関係する動的な意味論に関する限りは) 以前のバージョンに変換されます。 特に実行時には証明の構成は不要になります。

PrevHomeNext
プログラマ中心の定理証明Up例: 安全な行列の添字演算