Programming Language Qualifier Fall, 2000

Question 1:

Choose x 1,2,3

From choose keyword, we know it is “tree structure”.

Semantic Algebra

C: Command x Store à Store * _^

Valuation Function:

P : Program à Store *

P[C] = C[C](empty store)

C[ I:= E ] = ls. (cons(update[I]E[E]s s ) [ ])

C[ if B then C1 else C2 ] = ls. (B[B]sà C[C1]s | C[C2] )

C[C1;C2] = ls. let l = C[C1]s in apply( l,C2 ), where

apply = ll. lc. (emptylist(l)à[] | (append C[C](head l), apply (tail l, C) )

C[ choose I L ] = ls. let l = L[L] in multiple ( l, I, s), where

multiply = ll. li. ls. (emptylist(l)à[] |

(cons(update I (head l) s multiply (tail(l), I, s)

C[fail] = ls ([ ])

Question 2:

Key point: Backtracking. Undo, throw away the intermediate steps.

Choose x 45, 39, 27

y = x + 2;

z = y + x;

if ! (y+z == 121) then fail;

Each time, we put an element of x to the choice stack, and y and z

To the Trail. After testing the if condition, if succeed, then done, else

Pop the stack value, and push in the next x value, and so on, until

All the x values have been tested