% Operational semantics for L1 % Sam Staton. March 2011. % Tested with SWI Prolog. % Examples % To load this file, type [l1]. % Slide 14 in the notes: % [while (deref l >= 1) do ((k := ((deref k) + (deref l))) seq (l := (deref l + -1))),[l := 3, k := 0]] ===> X. % [while (deref l >= 1) do ((k := ((deref k) + (deref l))) seq (l := (deref l + -1))),[l := 3, k := 0]] ---> X. % In swipl, you can step through a run like this. % \$X ---> X. :-op(700, xfx, --->). :-op(700, xfx, --->*). :-op(700, xfx, ===>). :-op(250, xfx, >=). :-op(300, xfx, :=). :-op(200, fx, deref). :-op(650, xfx, seq ). :-op(650, xfx, do ). :-op(660, xfx, then ). :-op(665, xfx, else ). :-op(670, fx, if ). :-op(670, fx, while ). value(N) :- integer(N). value(true). value(false). value(skip). % 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 % NB because of prolog syntax we have to use "deref" instead of ! [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 % NB because of prolog syntax we have to use "seq" instead of semicolon [skip seq E2,S] ---> [E2,S]. % Rule SEQ2 [E1 seq E2,S] ---> [E1a seq E2,Sa] :- [E1,S] ---> [E1a,Sa]. % RULE IF1 [if true then E2 else _,S] ---> [E2,S]. % RULE IF2 [if false then _ else E3,S] ---> [E3,S]. % RULE IF3 [if E1 then E2 else E3,S] ---> [if E1a then E2 else E3,Sa] :- [E1,S] ---> [E1a,Sa]. % RULE WHILE [while E1 do E2,S] ---> [if E1 then (E2 seq (while E1 do E2)) else skip,S]. % 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).