SHARE
TWEET

Untitled

a guest Jun 22nd, 2010 418 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. // compile with
  2. // atscc -o fact fact.dats -lgmp
  3. (* In this file, we are to implement a verified factorial function
  4.  * to serve as an introductory example to programming with theorem
  5.  * proving in ATS.
  6.  *
  7.  * here we define a relation [fact(x,y)] between two natural numbers,
  8.  * with the intended meaning "y = x!". we define [fact] by the use
  9.  * of inductive judgements, and then transliterate them to the syntax of ATS.
  10.  *
  11.  * ----------(fact-bas)
  12.  * fact(0, 1)
  13.  *
  14.  *   fact(x, y)
  15.  * --------------(fact-ind)
  16.  * fact(x+1, y*(x+1))
  17.  *
  18.  * the (fact-bas) rule defines that the factorial of 0 is 1.
  19.  * the (fact-ind) rule states that if [y] is the factorial of [x],
  20.  * then the factorial of [x+1] is [y*x].
  21.  *
  22.  * here is an example derivation of fact(3, 6):
  23.  *
  24.  * ----------(fact-bas)
  25.  * fact(0, 1)
  26.  * ----------(fact-ind)
  27.  * fact(1, 1)
  28.  * ----------(fact-ind)
  29.  * fact(2, 2)
  30.  * ----------(fact-ind)
  31.  * fact(3, 6)
  32.  *
  33.  * due to technical issues it is not possible to express multiplication
  34.  * of integers directly, so we have to use [MUL], which encodes
  35.  * the multiplication relation.
  36.  *)
  37. staload "libats/SATS/intinf.sats"
  38. dynload "libats/DATS/intinf.dats"
  39.  
  40. dataprop FACT (int, int) =
  41.   | FACTbas (0, 1)
  42.   | {a,b,ab:int | a > 0} FACTind (a, ab) of (FACT (a-1, b), MUL (a, b, ab))
  43.  
  44. (* we are now to write the first approximation to the solution.
  45.  * note how we manually associate proofs with programs.
  46.  *)
  47. fun fac0 {a:nat} .<a>. (a: int a): [b:int] (FACT (a, b) | int b) =
  48.   if a > 0 then let
  49.     val (pf_fac | b) = fac0 (a-1)
  50.     val (pf_mul | ab) = a imul2 b
  51.   in (FACTind (pf_fac, pf_mul) | ab) end
  52.   else begin (FACTbas () | 1) end
  53.  
  54. (* this solution is unsatisfactory, because it involves recursion where
  55.  * iteration is more appropriate, so we rewrite it in a tail-recursive
  56.  * fashion.
  57.  *
  58.  * it is also possible to state and prove two lemmas about relation [FACT]:
  59.  * - for any natural number [n], there exists natural number [r] where [FACT (n, r)]
  60.  * - for any natural numbers [n,r0,r1], if [FACT (n, r0)] and [FACT (n, r1)], then [r0 = r1]
  61.  *)
  62.  
  63. prfun fact_istot {a:nat} .<a>. (): [b: int] FACT (a, b) =
  64.   sif a > 0 then let
  65.     prval [b:int] pf_fact = fact_istot {a-1} ()
  66.     prval pf_mul = mul_istot {a, b} ()
  67.   in FACTind (pf_fact, pf_mul) end
  68.   else FACTbas
  69.  
  70. prfun fact_isfun {a,b1,b2:int | a >= 0} .<a>.
  71.   (pf_a: FACT (a, b1), pf_b: FACT (a, b2)): [b1 == b2] void =
  72.   case+ (pf_a, pf_b) of
  73.   | (FACTbas (), FACTbas ()) => ()
  74.   | (FACTind (pf_a, pf_mul_a), FACTind (pf_b, pf_mul_b)) => let
  75.     prval () = fact_isfun (pf_a, pf_b)
  76.     prval () = mul_isfun (pf_mul_a, pf_mul_b)
  77.   in () end
  78.  
  79. (* to rewrite [fac0] in a tail-recursive style, some lemmas on multiplication
  80.  * are stated (one without proof)
  81.  *)
  82. // we need some lemmas on multiplication
  83. // MULlem00 = mul_istot
  84. // 1 * x = x
  85. prfn MULlem10 {x,y:int} (pf: MUL (1, x, y)): [x==y] void =
  86.   case+ pf of MULind (MULbas ()) => ()
  87.  
  88. // x * 1 = x
  89. prfn MULlem11 {x,y:int} (pf: MUL (x, 1, y)): [x==y] void = let
  90.   prval pf' = MULlem10 (mul_commute pf)
  91. in () end
  92.  
  93. // multiplication is associative: (xy)z = x(yz)
  94. extern prval MULlem20 : {x,y,z,xy,yz,xyz:int}
  95.   (MUL (x, y, xy), MUL (y, z, yz), MUL (xy, z, xyz)) -<prf> MUL (x, yz, xyz)
  96.  
  97. // [fac1] implements the factorial function in a tail-recursive style
  98. // the gist of the proof is to show that loop (n,x) = x*n! from which
  99. // loop (n,1) = n! follows
  100. fn fac1 {n:nat} (n: int n): [r0: int] (FACT (n, r0) | int r0) = let
  101.   // [loop] is tail-recursive
  102.   fun loop {n,x:int | n >= 0} .<n>. (n: int n, x: int x)
  103.     : [r,r0:int] (FACT (n, r), MUL (x, r, r0) | int r0) =
  104.     if n > 0 then let
  105.       val (pf_mul_x_n_xn | xn) = x imul2 n
  106.       val (pf_fac_n1_r1, pf_mul_xn_r1_r0 | res) = loop (n-1, xn)
  107.       prval pf_mul_n_r1_nr1 = mul_istot ()
  108.       prval pf_mul_x_nr1_r0 = MULlem20 (pf_mul_x_n_xn, pf_mul_n_r1_nr1, pf_mul_xn_r1_r0)
  109.       prval pf_fac_n_nr1 = FACTind (pf_fac_n1_r1, pf_mul_n_r1_nr1)
  110.     in
  111.       (pf_fac_n_nr1, pf_mul_x_nr1_r0 | res)
  112.     end else let
  113.       prval pf_mul_x_1_y = mul_istot {x,1} ()  // x * 1 = y
  114.       prval () = MULlem11 (pf_mul_x_1_y)       // x = y
  115.     in
  116.       (FACTbas (), pf_mul_x_1_y | x)
  117.     end
  118.   val (pf_fac, pf_mul | res) = loop (n, 1)
  119.   prval () = MULlem10 (pf_mul)
  120. in
  121.   (pf_fac | res)
  122. end
  123.  
  124. // fac2 is another implementation, employing the GMP library for variable-precision arithmetic
  125. // it can cope with very big numbers
  126. fun fac2 {n:nat} .<n>. (n: int n): [r:int] (FACT (n, r) | intinfptr_gc r) =
  127.   if n > 0 then let
  128.     val (pf1 | (pf1_gc, pf1_at | p1)) = fac2 (n-1)
  129.     val (pf_mul | r) = n * !p1
  130.     val () = intinf_free (pf1_gc, pf1_at | p1)
  131.   in
  132.     (FACTind (pf1, pf_mul) | r)
  133.   end else begin
  134.     (FACTbas () | intinf_make 1)
  135.   end // end of [if]
  136.  
  137. fn fac_usage (cmd: string): void =
  138.   prerrf ("Usage: %s [integer]\n", @(cmd))
  139.  
  140. implement main (argc, argv) =
  141.   if argc >= 2 then let
  142.     val n0 = int1_of argv.[1]
  143.     val () = assert_errmsg
  144.       (n0 >= 0, "The integer argument needs to be nonnegative.\n")
  145.     val (pf | res) = fac1 n0
  146.   in
  147.     print "The factorial of "; print n0; print " = "; print res; print_newline ()
  148.   end else begin
  149.     fac_usage (argv.[0]); exit 1
  150.   end
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
 
Top