void main() { int n500 = 0, n250 = 0, n100 = 0, n25 = 0, n10 = 0, n5 = 0, a = 500, m = 0; while (a >= 0) { while (a >= 0) { while (a >= 0) { while (a >= 0) { while (a >= 0) { m++; n10++; a -= 10; } a += 10 * n10; n10 = 0; n25++; a -= 25; } a += 25 * n25; n25 = 0; n100++; a -= 100; } a += 100 * n100; n100 = 0; n250++; a -= 250; } a += 250 * n250; n250 = 0; n500++; a -= 500; } printf("Number of combinations is %d\n", m); }
void main() { int m[100][5]; int i,j; int v[] = { 2, 5, 20, 50, 100 }; for (i = 0; i < 100; i++) for (j = 0; j < 5; j++) m[i][j] = 0; for(i = 0; i <=500; i++) for (j = 0; j < 5; j++) m[i%100][j] = (j == 0 ? 1 : m[i%100][j-1]) + m[(i + 100 - v[j])%100][j]; printf("Number of combinations is %d\n", m[500%100][4]); }The answer is that these programs both print the value of
c(500, {5, 10, 25, 100, 250, 500})
,
where the function c
is defined (using some common math
notations) as follows:
c(a : nat, V : P nat) = count({ { (v_1, c_1), .. , (v_n, c_n) } : P (nat, nat) | v_1 * c_1 + .. + v_n * c_n = a and {v_1, .. , v_n} = V} and |V| = n)Or to say it in words: In how many ways can I pay 500 if I do have sufficient amouth of coins with the values 5, 10, 25, 100, 250, and 500.
This shows that two vastly different programs calculate exactly the same thing. The question, which of the two is the best, is not easy to answer. If you only need to calculate this question once, it does not matter which one you use. But what if there are restrictions to the number of coins you have, or if you have to do it for other amounth as well. Or what if you have a different set of coins.
While implementing a specification, one makes the following kind of choices related to:
An implementating languages, is a language which expresses how a certain specification is implemented. Such a language would describe how a given specification is transformed into a program. An implementation language operates on expression representing data and algorithms. Because the transformations performed on the specification can be rather complex, such a language should have very powerful features to describe these transformations.
c(a : nat, V : L nat) = count({ S : L nat | count(S) = count(V) and (sum v * s for (v,s) in V.S) = a }A problem with this specification is that the expression V.S, where `.' stands for the structural inproduct operation, is ill-defined if V and S are of different lenght. Lets replace the list with arrays:
c(a : nat, V : array[n] nat) = count({ S : array[n] nat | (sum V[i] * S[i] for i in { 1 .. n }) = a }
all_sol(a : nat, V : array[n] nat, S : array[m] nat) : P array[l] nat = if n = 0 then if a = 0 then { S } else {} endif else unnest(collect all_sol(a - V[1] * s, V[2..n], S:(s)) for s in { 0 .. a mod V[1] }) endifIt is far from trivial to prove that all_sol(a, V, ()) is indeed equal to:
{ S : array[n] nat | (sum V[i] * S[i] for i in { 1 .. n }) = a }
c(a : nat, V : array[n] nat, S : array[m] nat) : nat = if n = 0 then if a = 0 then count({ S }) else count({}) endif else count(unnest(collect all_sol(a - V[1] * s, V[2..n], S:(s)) for s in { 0 .. a mod V[1] }) endifThe count(unnest(collect .. )) construct can be simplified under the condition that all the sets produced by the calls of all_sol are disjunct. It can be shown that this is indeed true. With some more simplifications, this leads to:
c(a : nat, V : array[n] nat, S : array[m] nat) : nat = if n = 0 then if a = 0 then 1 else 0 endif else sum c(a - V[1] * s, V[2..n], S:(s)) for s in { 0 .. a mod V[1] } endifNow we observe that the parameter S has become obsolete. Removing it leads to:
c(a : nat, V : array[n] nat) : nat = if n = 0 then if a = 0 then 1 else 0 endif else sum c(a - V[1] * s, V[2..n]) for s in { 0 .. a mod V[1] } endif
c1(a : nat) : nat = if 6 = 0 then if a = 0 then 1 else 0 endif else sum c(a - 500 * s, (250, 100, 25, 10, 5)) for s in { 0 .. a mod 500 } endifWe notice that the above can be simplified, and that we can apply another specialisation of the function c. If we apply this several times, we get:
c1(a : nat) : nat = sum c2(a - 500 * s) for s in { 0 .. a mod 500 } c2(a : nat) : nat = sum c3(a - 250 * s) for s in { 0 .. a mod 250 } c3(a : nat) : nat = sum c4(a - 100 * s) for s in { 0 .. a mod 100 } c4(a : nat) : nat = sum c5(a - 25 * s) for s in { 0 .. a mod 25 } c5(a : nat) : nat = sum c5(a - 10 * s) for s in { 0 .. a mod 10 } c6(a : nat) : nat = sum c5(a - 5 * s) for s in { 0 .. a mod 5 } c7(a : nat) : nat = if a = 0 then 1 else 0 endif
c6(a : nat) : nat = sum let a1 = (a - 5 * s) in if a1 = 0 then 1 else 0 endif for s in { 0 .. a mod 5 }Applying some simplifications, this results in:
c6(a : nat) : nat = sum if (a - 5 * s) = 0 then 1 else 0 endif for s in { 0 .. a mod 5 }Some reasoning about this expression, leads us to the conclusion that (a - 5 * s) = 0 cannot be true for s < a mod 5. This leads to the simplification:
c6(a : nat) : nat = if (a - 5 * s) = 0 then 1 else 0 endif where ( s = a mod 5)Another substitution leads to:
c6(a : nat) : nat = if (a - 5 * (a mod 5)) = 0 then 1 else 0 endifWhich can be simplified into:
c6(a : nat) : nat = if (a mod 5) = 0 then 1 else 0 endif
c(a : nat) : nat = sum let a1 = a - n500 * 500 in (sum let a2 = a1 - n250 * 250 in (sum let a3 = a2 - n100 * 100 in (sum let a4 = a3 - n25 * 25 in (sum let a5 = a4 - n10 * 10 in (if (a5 mod 5) = 0 then 1 else 0 endif) for n10 in { 0 .. a4 mod 10 }) for n25 in { 0 .. a3 mod 25 }) for n100 in { 0 .. a2 mod 100 }) for n250 in { 0 .. a1 mod 250 }) for n500 in { 0 .. a mod 500 }