% Operational semantics for L1 Plus the Par operation from Lecture 12. % Sam Staton. November 2010. % Tested with GNU Prolog. % Examples % To load this file, type [l1]. % Slide 14 in the notes: % [while(deref l >= 1,(k := (deref k + deref l)) seq (l := (deref l + -1))),[l := 3, k := 0]] ===> X. % Page 98 in the notes: % [l := (1 + deref l) par l := (7 + deref l),[l := 0]] ===> X. :-op(700, xfx, --->). :-op(700, xfx, --->*). :-op(700, xfx, ===>). :-op(250, xfx, add). :-op(250, xfx, >=). :-op(300, xfx, :=). :-op(650, xfx, par). :-op(200, fx, deref). :-op(650, xfx, seq ). value(N) :- integer(N). value(true). value(false). value(skip). value(V1 par V2) :- value(V1), value(V2). % Rule OP + [N1 + N2,S] ---> [M,S] :- integer(N1) , integer(N2) , M is (N1+N2) . % Rule OP >= [N1 >= N2,S] ---> [true,S] :- integer(N1) , integer(N2) , N1 >= N2 . [N1 >= N2,S] ---> [false,S] :- integer(N1) , integer(N2) , N1 < N2 . % Rule OP1 [E1 + E2,S] ---> [E1a + E2,Sa] :- [E1,S] ---> [E1a,Sa]. [E1 >= E2,S] ---> [E1a >= E2,Sa] :- [E1,S] ---> [E1a,Sa]. % Rule OP2 [N1 + E2,S] ---> [N1 + E2a,Sa] :- [E2,S] ---> [E2a,Sa], value(N1). [N1 >= E2,S] ---> [N1 >= E2a,Sa] :- [E2,S] ---> [E2a,Sa], value(N1). % Rule DEREF [deref L,S] ---> [N1,S] :- member((L := N1),S). % Rule ASSIGN1 [L := N1,S] ---> [skip,[(L := N1)|Saa]] :- value(N1), member((L := N2), S), delete(S,(L := N2),Saa). % Rule ASSIGN2 [L := E1,S] ---> [L := E1a,Sa] :- [E1,S] ---> [E1a,Sa]. % Rule SEQ1 [skip seq E2,S] ---> [E2,S]. % Rule SEQ2 [E1 seq E2,S] ---> [E1a seq E2,Sa] :- [E1,S] ---> [E1a,Sa]. % (NB I am not using infix notation for if and while.) % RULE IF1 [ifthenelse(true,E2,_),S] ---> [E2,S]. % RULE IF2 [ifthenelse(false,_,E3),S] ---> [E3,S]. % RULE IF3 [ifthenelse(E1,E2,E3),S] ---> [ifthenelse(E1a,E2,E3),Sa] :- [E1,S] ---> [E1a,Sa]. % RULE WHILE [while(E1,E2),S] ---> [ifthenelse(E1,(E2 seq while(E1,E2)),skip),S]. % RULE PARALLEL1 [E1 par E2,S] ---> [E1a par E2,Sa] :- [E1,S] ---> [E1a,Sa]. % RULE PARALLEL2 [E1 par E2,S] ---> [E1 par E2a,Sa] :- [E2,S] ---> [E2a,Sa]. % Multi-steps [E,S] --->* [E,S]. [E,S] --->* [Ea,Sa] :- [E,S] ---> [Eaa,Saa], [Eaa,Saa] --->* [Ea,Sa]. % Evaluation % (reduce until you get a value) [E,S] ===> [Va,Sa] :- [E,S] --->* [Va,Sa], value(Va).