情報証明論 第8章 プログラムの関数化

第1節 配列と関数の値

目次


第1節 配列と関数の値

第2節 関数が関数を呼ぶ

第3節 引数への結果代入


テスト

Logをみる

Back
 

第8章 プログラムの関数化 第1節 配列と関数の値

 配列はAFINSQ_1で導入されているXFinSequence という概念を使うといいでしょう。これは0から添え字が始まる有限数列です。添え字が1から始まるときはFINSEQ_1で導入されているFinSequenceがいいでしょう。

 配列を使い、かつ関数の形をしたプログラムの論理モデルはMizarの関数になります。次の例を見ましょう。

例1

 整数配列aの1からnまでの要素を加えて和を出力する、次のようなプログラムの関数がある。

int sumarray_prg(int a[MAX_N],int n)
{
 int s[MAX_N],i;
 if (!(0< n && n< MAX_N))return -1;
 s[0]=0;
 for (i=0;i< n;i++)
  { s[i+1]= s [i] + a[i+1];
  } 
 return s[n];
}

これがn< MAX_N のときに正しく和が計算されることを証明せよ。ここでMAX_Nはコンパイル時に指定される十分大きな整数とする。なお 0< n && n< MAX_N という条件で使われるのを前提としている。

解)このプログラムの関数の論理モデルは次のようなMizarの定義になる。

definition let a be XFinSequence of INT,n be Integer;
 assume A1: 0<  n & n< len a;
  func sumarray_prg(a,n) -> Integer means
 :SS00: ex s being XFinSequence of INT st s.0=0 &
 (for i being Nat st i< n holds s.(i+1)=s.i +a.(i+1))
      & it=s.n;
 existence;
 uniqueness;
end;

この定義でexistenceが証明されれば関数の値がいつも与えられることを示す。

 またuniquenessが証明されれば結果は一意であることを示す。

 定義ができただけでは論理モデルの正しさがいえたことにはならない。それに引き続く一つあるいは複数の定理によって正しさが保証される。ここでは一つだけ定理を(証明無しで)挙げる。

 またredefine(再定義)という定義を前もって与えたのは、b.n というXFinSequenceの要素が整数型をもつようにするためである(通常はset型)。整数型にしないと計算式が書けないためである。

 以下に証明(長いが)を掲げる。新しいVOCファイルはSUMN_2.VOCで内容は

Osumarray_prg

である。

environ
 vocabulary FUNCT_1,BOOLE,ORDINAL1,FINSEQ_1,FINSET_1,RELAT_1,ORDINAL2,CARD_1,
      ALGSEQ_1,ARYTM_1,AFINSQ_1,ARYTM,INT_1,RLVECT_1,SUMN_2;
 notation TARSKI,XBOOLE_0,ZFMISC_1,SUBSET_1,NUMBERS,XCMPLX_0,XREAL_0,RELAT_1,
      FUNCT_1,ORDINAL1,ORDINAL2,REAL_1,NAT_1,FINSET_1,CARD_1,FINSEQ_1,
      INT_1,RVSUM_1,BINARITH,FUNCOP_1,RLVECT_1,AFINSQ_1;
 constructors XCMPLX_0,REAL_1,NAT_1,XREAL_0,MEMBERED,AFINSQ_1,FINSEQ_1,
      FUNCT_1,INT_1,RVSUM_1,BINARITH,NUMBERS;
 clusters FUNCT_1,RELAT_1,RELSET_1,SUBSET_1,ORDINAL1,ARYTM_3,NAT_1,XREAL_0,
      MEMBERED,ORDINAL2,FINSEQ_1,AFINSQ_1,INT_1,FUNCOP_1;
 requirements REAL,NUMERALS,SUBSET,BOOLE,ARITHM;
 definitions TARSKI,FUNCT_1,WELLORD2,ORDINAL2,XBOOLE_0;
 theorems TARSKI,AXIOMS,FUNCT_1,REAL_1,NAT_1,ZFMISC_1,RELAT_1,ORDINAL1,CARD_1,
      ORDINAL2,CARD_2,ORDINAL3,AFINSQ_1,SQUARE_1,BINARITH,NUMBERS,XBOOLE_0,
      INT_1;
 schemes NAT_1;

begin
 reserve k,m,n,i for Nat,
         D,x,y,z,y1,y2 for set;

AA130: for x,y,n,m st x=n & y=m holds
  x in y iff n < m
proof let x,y,n,m;assume A1: x=n & y=m;
  A12: Card n <` Card m iff n < m by CARD_1:73;
  Card n=n by CARD_1:66;
 hence x in y iff n < m by A1,A12,CARD_1:66;
end;

definition let b be XFinSequence of INT,n be Nat;
 redefine func b.n -> Integer;
coherence
proof
 now per cases;
 case n in dom b;then
  B1: b.n in rng b by FUNCT_1:def 5;
  rng b c= INT by ORDINAL1:def 8;
 hence b.n is Integer by B1,INT_1:12;
 end;
 case not n in dom b;then
  b.n = 0 by FUNCT_1:def 4;
 hence b.n is Integer;
 end;
 end;
 hence b.n is Integer;
end;                             
end;

:: Non-overwriting program calculating sum of elements of vectors
definition let a be XFinSequence of INT,n be Integer;
 assume A1: 0< n & n< len a;
  func sumarray_prg(a,n) -> Integer means
 :SS00: ex s being XFinSequence of INT st s.0=0 &
 (for i being Nat st i as XFinSequence of INT;
  dom q0=1 & q0.0=0 by AFINSQ_1:def 5;then
  A71: len q0=1 & q0.0=0 by AFINSQ_1:def 1;
  for k st k< 0 & k< nn2 holds q0.(k+1)=q0.k+(a.(k+1))
                          by NAT_1:18;then
  A50: P[0] by A71;
  A51: for k be natural number st P[k] holds P[k + 1]
  proof let k be natural number;
   assume P[k];then
    consider q2 being XFinSequence of INT such that
     B2: (len q2= k+1 &
     q2.0=0 & (for k2 being Nat st k2< k & k2< nn2 holds q2.(k2+1)
     =q2.k2+(a.(k2+1))));
     reconsider k0=k as Nat by ORDINAL2:def 21;
     q2.k0+(a.(k0+1)) is Element of INT by INT_1:12;then
     reconsider kk= q2.k0+(a.(k0+1)) as Element of INT;
     reconsider q3=q2^<% kk %>
                  as XFinSequence of INT;
     B10: len q3=len q2+len (<% q2.k0+(a.(k0+1)) %>)
                            by AFINSQ_1:20
          .=k+1+1 by B2,AFINSQ_1:37;
     0 < k+1 by NAT_1:19;then
     0 in len q2 by B2,AA130;then
     0 in dom q2 by AFINSQ_1:def 1;then
     B11: q3.0=q2.0 by AFINSQ_1:def 4 .=0 by B2;
     for k2 being Nat st k2).0
               = q2.k0+(a.(k0+1)) by AFINSQ_1:38;
           k2< k2+1 by NAT_1:38;then
           k2 in len q2 by AA130,D0,B2;then
           k2 in dom q2 by AFINSQ_1:def 1;then
           D4: q3.(k2)=q2.(k2) by AFINSQ_1:def 4;
           0 in 1 by AA130;then
           0 in dom (<% q2.k0+(a.(k0+1)) %>)
                                   by AFINSQ_1:def 5;then
           q3.(k2+1+0) =q2.(k0)+(a.(k0+1))
                           by D3,B2,D0,AFINSQ_1:def 4;
          hence q3.(k2+1) =q3.k2+(a.(k2+1)) by D0,D4;
        end;
        end;
       hence q3.(k2+1) =q3.k2+(a.(k2+1));
      end;
   hence P[k + 1] by B10,B11;
  end;
 for k being natural number holds P[k] from NAT_1:sch 2(A50,A51);then
 consider q being XFinSequence of INT such that
 B12: (len q=n2-'1+1 &
  q.0=0 & (for k3 being Nat st k3=0+1 by A89,NAT_1:38;then
 n2-1>=0 by SQUARE_1:12;then
 B71: n2-'1=n2-1 by BINARITH:def 3;then
 A60: len q=len a & q.0=0 by B12;
  for i being Nat st i< nn
  holds q.(i+1)=q.i + (a.(i+1))
   proof let i be Nat;
    assume E0: i< nn;then E1: i< nn2;
     nn+1<=n2 by A1,NAT_1:38;then
     nn+1-1<=n2-1 by REAL_1:49;then
     i< n2-'1 by B71,E0,AXIOMS:22;
    hence q.(i+1)=q.i + (a.(i+1)) by B12,E1;
 end;then
  A2: len q=len a
& q.0=0
& (
 for i being Nat st i< nn 
 holds q.(i+1)=q.i + (a.(i+1))
 )
& q.nn=q.nn by A60;
 reconsider ss2=q.nn2 as Integer;
 ex s being XFinSequence of INT st
 len s=len a & s.0=0 &
 (for i being Nat st i< n holds s.(i+1)=s.i +a.(i+1))
      & ss2=s.n by A2;
 hence thesis;
end;
uniqueness
 proof
  thus for w1,w2 being Integer st
 (ex s being XFinSequence of INT st
 s.0=0
& (
 for i being Nat st i< n
 holds s.(i+1)=s.i + (a.(i+1))
 )
& w1=s.n)
&
( ex s being XFinSequence of INT st
  s.0=0
& (
 for i being Nat st i< n
 holds s.(i+1)=s.i + (a.(i+1))
 )
& w2=s.n) holds w1=w2
  proof let w1,w2 be Integer;
   assume B1: (ex s being XFinSequence of INT st
     s.0=0 
    & (
    for i being Nat st i< n
    holds s.(i+1)=s.i + (a.(i+1))
    )
   & w1=s.n)
   &
   ( ex s being XFinSequence of INT st
    s.0=0 
   & (
    for i being Nat st i< n
    holds s.(i+1)=s.i + (a.(i+1))
    )
   & w2=s.n);then
   consider s1 being XFinSequence of INT such that
   B2: s1.0=0 
    & (
    for i being Nat st i< n
    holds s1.(i+1)=s1.i + (a.(i+1))
    )
   & w1=s1.n;
   consider s2 being XFinSequence of INT such that
   B3: s2.0=0
    & (
    for i being Nat st i< n
    holds s2.(i+1)=s2.i + (a.(i+1))
    )
   & w2=s2.n by B1;
   reconsider n as Nat by A1,INT_1:16;
   defpred P2[Nat] means
    $1<=n implies  s1.$1=s2.$1;
    B5: P2[0] by B2,B3;
    B6: for k being Nat st P2[k] holds P2[k+1]
    proof let k be Nat;assume
      P2[k];then
      C7: k<=n implies  s1.(k)=s2.(k);
      now assume C1: k+1<=n;
        C2: k< n by C1,NAT_1:38;
        s1.(k+1)=s1.k + (a.(k+1)) by B2,C2;
       hence s1.(k+1)=s2.(k+1) by C7,C2,B3;
      end;
     hence P2[k+1];
    end;
    D4: for k being Nat holds P2[k] from NAT_1:sch 1(B5,B6);
    reconsider n11=n as Nat;
    s1.n11=s2.n11 by D4.=s2.n;
   hence w1=w2 by B2,B3;
  end;
end;
end;

theorem  for a being XFinSequence of INT,b being FinSequence of REAL,
 n being Integer
 st len b=n &
 (for i being Nat st i<=n holds b.i=a.i)
 & 0< n & n< len a
 holds  Sum b =sumarray_prg(a,n);
::>                            *4
::>
::> 4: This inference is not accepted