ATSプログラミング入門:
PrevChapter 11. ATS/LF を使った定理証明Next

例: 乗法の分配法則

加法に対する乗法の分配法則は次の等式を意味しています: 

m * (n1 + n2) = m * n1 + m * n2

m, n1, n2 は整数の範囲を持ちます。 この等式を直接エンコードすると次のような (証明の) 関数インターフェイスが得られます: 

//
prfun
mul_distribute
  {m,n1,n2:int}{p1,p2:int}
  (MUL(m, n1, p1), MUL(m, n2, p2)): MUL(m, n1+n2, p1+p2)
//

端的に言うと、このエンコードは m と n1 の積が p1 でありかつ m と n2 の積が p2 であったなら m と (n1+n2) の積は p1+p2 になる、と言っています。 mul_distribute の実装は次のようになります: 

primplement
mul_distribute
{m,n1,n2}{p1,p2}
  (pf1, pf2) = let
//
prfun
auxnat
{m:nat}{p1,p2:int} .<m>.
(
  pf1: MUL(m, n1, p1), pf2: MUL(m, n2, p2)
) : MUL(m, n1+n2, p1+p2) =
(
  case+ (pf1, pf2) of
  | (MULbas(), MULbas()) => MULbas()
  | (MULind pf1, MULind pf2) => MULind(auxnat (pf1, pf2))
) (* end of [auxnat] *)
//
in
//
sif
m >= 0
then (
  auxnat (pf1, pf2)
) // end of [then]
else let
  prval MULneg(pf1) = pf1
  prval MULneg(pf2) = pf2
in
  MULneg(auxnat (pf1, pf2))
end // end of [else]
//
end // end of [mul_distribute]

本質的に、 内部の関数 auxnat は次の等式を満たす数学的帰納法の証明を素直にエンコードしています: 

m * (n1 + n2) = m * n1 + m * n2

m は自然数の範囲を取り、n1 と n2 は整数の範囲を取ります。 関数 mul_distribute は auxnat を使ってすぐに実装できます。

PrevHomeNext
全域関数を使って証明を組み立てるUp例: 乗法の交換法則