• API
• FAQ
• Tools
• Archive
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.  *)
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.
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.); 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.

Top