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 :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.nat, V :P nat) =count({ { (v_1, c_1), .. , (v_n, c_n) } :P(nat,nat) | v_1 * c_1 + .. + v_n * c_n = aand{v_1, .. , v_n} = V}and|V| = n)

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:

- Generic versus specific solutions.
- Order of calculation.
- Algorithms to be used.
- Which intermediate results to store.
- Representation of the data.

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 :A problem with this specification is that the expressionnat, V :L nat) =count({ S :L nat|count(S) =count(V)and(sumv * sfor(v,s)inV.S) = a }

c(a :nat, V :array[n]nat) =count({ S :array[n]nat| (sumV[i] * S[i]foriin{ 1 .. n }) = a }

all_sol(a :It is far from trivial to prove thatnat, V :array[n]nat, S :array[m]nat) :P array[l]nat=ifn = 0thenifa = 0then{ S }else{}endifelseunnest(collectall_sol(a - V[1] * s, V[2..n], S:(s))forsin{ 0 .. amodV[1] })endif

{ S :array[n]nat| (sumV[i] * S[i]foriin{ 1 .. n }) = a }

c(a :Thenat, V :array[n]nat, S :array[m]nat) : nat =ifn = 0thenifa = 0thencount({ S })elsecount({})endifelsecount(unnest(collectall_sol(a - V[1] * s, V[2..n], S:(s))forsin{ 0 .. amodV[1] })endif

c(a :Now we observe that the parameternat, V :array[n]nat, S :array[m]nat) : nat =ifn = 0thenifa = 0then1else0endifelsesumc(a - V[1] * s, V[2..n], S:(s))forsin{ 0 .. amodV[1] }endif

c(a :nat, V :array[n]nat) : nat =ifn = 0thenifa = 0then1else0endifelsesumc(a - V[1] * s, V[2..n])forsin{ 0 .. amodV[1] }endif

c1(a :We notice that the above can be simplified, and that we can apply another specialisation of the functionnat) : nat =if6 = 0thenifa = 0then1else0endifelsesumc(a - 500 * s, (250, 100, 25, 10, 5))forsin{ 0 .. amod500 }endif

c1(a :nat) : nat =sumc2(a - 500 * s)forsin{ 0 .. amod500 } c2(a :nat) : nat =sumc3(a - 250 * s)forsin{ 0 .. amod250 } c3(a :nat) : nat =sumc4(a - 100 * s)forsin{ 0 .. amod100 } c4(a :nat) : nat =sumc5(a - 25 * s)forsin{ 0 .. amod25 } c5(a :nat) : nat =sumc5(a - 10 * s)forsin{ 0 .. amod10 } c6(a :nat) : nat =sumc5(a - 5 * s)forsin{ 0 .. amod5 } c7(a :nat) : nat =ifa = 0then1else0endif

c6(a :Applying some simplifications, this results in:nat) : nat =sumleta1 = (a - 5 * s)inifa1 = 0then1else0endifforsin{ 0 .. amod5 }

c6(a :Some reasoning about this expression, leads us to the conclusion thatnat) : nat =sumif(a - 5 * s) = 0then1else0endifforsin{ 0 .. amod5 }

c6(a :Another substitution leads to:nat) : nat =if(a - 5 * s) = 0then1else0endifwhere( s = amod5)

c6(a :Which can be simplified into:nat) : nat =if(a - 5 * (amod5)) = 0then1else0endif

c6(a :nat) : nat =if(amod5) = 0then1else0endif

c(a :nat) :nat=sumleta1 = a - n500 * 500in(sumleta2 = a1 - n250 * 250in(sumleta3 = a2 - n100 * 100in(sumleta4 = a3 - n25 * 25in(sumleta5 = a4 - n10 * 10in(if(a5mod5) = 0then1else0endif)forn10in{ 0 .. a4mod10 })forn25in{ 0 .. a3mod25 })forn100in{ 0 .. a2mod100 })forn250in{ 0 .. a1mod250 })forn500in{ 0 .. amod500 }

home page