ATSプログラミング入門:
Prev	Chapter 12. 定理証明によるプログラミング	Next

例: 検証された高速な累乗

整数 x が与えられた時、pow(x, n)、つまり x の n 乗、は次のように帰納的に宣言することができます:

pow (x, 0) = 1
pow (x, n) = x * pow (x, n-1) (for all n > 0)

この定義の直接的な実装は次のようになります:

fun ipow {n:nat} .<n>.
  (x: int, n: int n): int = if n > 0 then x * ipow (x, n-1) else 1
// end of [ipow]

この実装の時間的計算量は (乗法を O(1) と仮定すると) O(n) になります。より効率的な実装は次のようになるでしょう:

fun
ifastpow
{n:nat} .<n>.
(
  x: int, n: int n
) : int =
  if n > 0 then let
    val n2 = half(n)
    val i2 = n-(2*n2)
  in
    if i2 > 0 then ifastpow (x*x, n2) else x * ifastpow (x*x, n2)
  end else 1 // end of [if]
// end of [ifastpow]

ここでは、もし n が偶数であれば pow(x, n) は pow(x*x, n/2) に等しく、もし n が奇数であれば pow(x, n) は x * pow(x*x, n/2) に等しい、という性質を使っています。これは高速な累乗と呼ばれています。 ifastpow の時間的計算量は O(log(n)) であることに注意してください。

明確に、上記は整数の累乗に限定されたものではありません。用いている乗法が結合的である限り、どのような要素の累乗を計算するのにも高速な累乗を使うことができます。特に、正方行列の累乗はこの方法で計算できます。高速な累乗の検証された一般化実装を次に紹介します。

検証された実装の中で一般化されたデータを正確に扱うために、しばしば ATS の型システムにおいて技巧的なテクニックが必要です。はじめに、次のような抽象型コンストラクタ E を導入してみましょう:

sortdef elt = int // [elt] is just an alias for [int]
abst@ype ELT(a:t@ype, x:elt) = a // [x] is an imaginary stamp

これはしばしば スタンプ化 (stamping) と呼ばれます。それぞれの型 T とスタンプ X について、関連するデータ表現に関する限り E(T, x) は単に T です。このスタンプは架空の存在で、仕様の目的にだけ使われます。次に抽象命題型 MUL と関数テンプレート mul_elt_elt を導入します:

//
absprop MUL(elt, elt, elt) // abstract mul relation
//
fun
{a:t@ype}
mul_elt_elt{x,y:elt}
  (x: ELT(a, x), y: ELT(a, y)): [xy:elt] (MUL(x, y, xy) | ELT(a, xy))
// end of [mul_elt_elt]
//

MUL と arith_prf.sats で宣言されている同じ名前の型に混乱しないでください。エンコードされた乗法が結合的であることを示すために、次の証明関数を導入することができます:

praxi
mul_assoc
{x,y,z:elt}{xy,yz:elt}{xy_z,x_yz:elt}
(
  MUL(x, y, xy), MUL(xy, z, xy_z), MUL(y, z, yz), MUL(x, yz, x_yz)
) : [xy_z==x_yz] void // end of [mul_assoc]

キーワード praxi は mul_assoc を実装されることを期待しない公理として扱うことを示します。

抽象的な累乗関数は、抽象命題型 MUL の項ですぐに指定できます:

dataprop
POW (
  elt(*base*), int(*exp*), elt(*res*)
) = // res = base^exp
  | {x:elt}
    POWbas(x, 0, 1(*unit*))
  | {x:elt}{n:nat}{p,p1:elt}
    POWind(x, n+1, p1) of (POW(x, n, p), MUL(x, p, p1))
// end of [POW]

予想される通り、一般化された高速な累乗は次のインターフェイスで与えられます:

fun{a:t@ype}
fastpow_elt_int{x:elt}{n:nat}
  (x: ELT(a, x), n: int n): [p:elt] (POW(x, n, p) | ELT(a, p))
// end of [fastpow_elt_int]

上までで準備が整ったので、fastpow_elt_int の率直な実装は次のようになります:

implement
{a}(*tmp*)
fastpow_elt_int
  (x, n) = let
//
(*
lemma: (x*x)^n = x^(2n)
*)
extern
prfun
lemma
{x:elt}{xx:elt}{n:nat}{y:elt}
  (pfxx: MUL(x, x, xx), pfpow: POW(xx, n, y)): POW(x, 2*n, y)
//
overload * with mul_elt_elt // [*] loaded with mul_elt_elt
//
in
//
if
n = 0
then let
  val res = mulunit<a> () in (POWbas () | res) // res = 1
end // end of [then]
else let
  val n2 = half n
  val (pfxx | xx) = x * x
  val (pfpow2 | res) = fastpow_elt_int<a> (xx, n2) // xx^n2 = res
  prval pfpow = lemma (pfxx, pfpow2) // pfpow: x^(2*n2) = res
in
  if n=2*n2
    then (pfpow | res)
    else let
      val (pfmul | xres) = x * res in (POWind(pfpow, pfmul) | xres)
    end // end of [else]
end // end of [else]
//
end // end of [fastpow_elt_int]

fastpow_elt_int のこの実装は末尾再帰でないことに注意してください。用いる乗法の単位元を作るために呼び出す関数テンプレート mulunit には次のインターフェイスが割り当てられます:

fun{a:t@ype} mulunit (): ELT(a, 1(*stamp*))

証明関数 lemma は、それぞれの自然数 n について pow(x, 2*n)=pow(x*x, n) を立証しています。私が実装した lemma はオンラインから入手できます。けれども興味のある読者には、私の実装を見る前に実装してみることを提案します。 lemma の実装には次の公理が必要になることに注意してください:

//
praxi
mul_istot // MUL is total
  {x,y:elt} ((*void*)): [xy:elt] MUL(x, y, xy)
//
praxi
mul_isfun // MUL is functional
  {x,y:elt}{z1,z2:elt}(MUL(x, y, z1), MUL(x, y, z2)): [z1==z2] void
//

別の興味深い (そしてておそらく少しやりがいのある) 課題は fastpow_elt_int を末尾再帰的に実装することでしょう。

オンラインから入手できる2つのファイル fastexp.sats と fastexp.dats は上記に示したコード全体を含んでいます。

これで fastpow_elt_int を実装するできました。これをどうやって使うのでしょうか？ 2 x 2 行列の高速な累乗を実装した fastpow_elt_int の例がオンラインから入手できます。これでフィボナッチ数を効率的に計算できるようになります。

Prev	Home	Next
例: もう一つの検証された階乗	Up	線形観と線形型を使ったプログラミング