I. Introduction to Operational Semantics A. definition ------------------------------------------ OPERATIONAL SEMANTICS def: an operational semantics of a language L is: ------------------------------------------ Have we made any progress in defining L? what's an example? B. problems 1. well-definedness 2. using the semantics to reason about a program in the original language C. advantages 1. applications to compilation 2. easiest kind of semantics to write down 3. best for semantics of concurrency (it seems) D. remarks E. Things to think about specifying II. Structural operational semantics A. two styles ------------------------------------------ STYLES OF STRUCTURAL OPERATIONAL SEMANTICS names better for big step, reasoning about program evaluation, natural little step compilers, concurrency computation TTS ------------------------------------------ B. evaluation, big step, or natural semantics 1. idea ------------------------------------------ EVALUATION (BIG STEP) SEMANTICS evaluation relation: evalsto is a idea: ------------------------------------------ 2. example ------------------------------------------ EXAMPLE: ARITHMETIC EXPRESSIONS Concrete Syntax: ::= | ::= + | - ::= | * Abstract Syntax: ------------------------------------------ How could we code the abstract syntax for this in \Prolog? --------------------------------------------------------- BIG STEP SEMANTICS FOR ARITHMETIC (num N) ==> N E1 ==> V1, E2 ==> V2, (ap Oper V1 V2) ==> Ans _______________________ (op Oper E1 E2) ==> Ans (ap add N1 N2) ==> Ans, where Ans = N1 + N2 (ap sub N1 N2) ==> Ans, where Ans = N1 - N2 (ap mult N1 N2) ==> Ans, where Ans = N1 * N2 --------------------------------------------------------- can you show the proof for: (op mult (num 10) (op sub (num 5) (num 3)))? 3. in lambda Prolog ------------------------------------------ % abstract syntax for arithmetic % concrete syntax: % ::= % | % ::= + | - % ::= | * sig arith_abstract_syntax. kind expression type. kind operator type. % abstract syntax type add operator. type sub operator. type mult operator. type divide operator. type num int -> expression. type op operator -> expression -> expression -> expression. module arith_abstract_syntax. % see the signature file. ------------------------------------------ ------------------------------------------ sig arith. accum_sig arith_abstract_syntax. type evalsto expression -> int -> o. end % Evaluation semantics for arithmetic % expressions, adapted from M. Hennessy: % The Semantics of Programming Languages % (Wiley, 1990). module arith. accumulate arith_abstract_syntax. % auxilliary semantic relations local ap operator -> int -> int -> int -> o. % the evalsto relation (evalsto (num N) N). ((evalsto E1 V1), (evalsto E2 V2), (ap Oper V1 V2 Ans)) => % ---------------------------------- (evalsto (op Oper E1 E2) Ans). (ap add N1 N2 Ans) :- Ans is N1 + N2. (ap sub N1 N2 Ans) :- Ans is N1 - N2. (ap mult N1 N2 Ans) :- Ans is N1 * N2. ------------------------------------------ a. side conditions and other variations What is the best way to show use of side-conditions in proofs? b. dealing with errors Can you add division to this? What about division by zero? C. terminal transition system, little step, computation semantics 1. idea ------------------------------------------ COMPUTATION (LITTLE STEP) SEMANTICS Meaning Programs <-------> Answers | ^ input | | output | | v reducesto* | Gamma <-----------> T def: a in Meaning[[P]] iff ------------------------------------------ 2. terminal transition systems ------------------------------------------ TERMINAL TRANSITION SYSTEM (TTS) (Gamma, reducesto, T) Gamma: reducesto: T: reducesto* reflexive, transitive closure ------------------------------------------ 3. example: arithmethic expressions ------------------------------------------ COMPUTATIONAL SEMANTICS OF ARITHMETIC EXPRESSIONS Programs = Gamma = T = Answers = int input[[P]] = output[[(num N)]] = ------------------------------------------ ------------------------------------------ sig comput_arith. accum_sig arith_abstract_syntax, rtc. type reducesto exp -> exp -> o. type output_fun exp -> int -> o. end % Computation semantics for the language % of arithmetic expressions. Adapted % from M. Hennessy: The Semantics of % Programming Languages (Wiley, 1990). module comput_arith. accumulate arith_abstract_syntax, rtc. % the reducesto relation (ap Oper V1 V2 N) => % ------------------------------------ (reducesto (op Oper (num V1) (num V2)) (num N)). (reducesto E1 E1') => % ---------------------------- (reducesto (op Oper E1 E2) (op Oper E1' E2)). (reducesto E2 E2') => % -------------------------- (reducesto (op Oper (num V1) E2) (op Oper (num V1) E2')). % the output relation (output_fun (num N) N). % auxilliary semantic relations local ap operator -> int -> int -> int -> o. (ap add N1 N2 Ans) :- Ans is N1 + N2. (ap sub N1 N2 Ans) :- Ans is N1 - N2. (ap mult N1 N2 Ans) :- Ans is N1 * N2. ------------------------------------------ how would you describe the order of evaluation? what has to be done? 4. Example: the lambda calculus (just mention if already did this) ------------------------------------------ SYNTAX OF THE UNTYPED LAMBDA CALCULUS M ::= term I identifier | (\I . M) abstraction | (M1 M2) application ------------------------------------------ Is this an abstract or concrete syntax? ------------------------------------------ COMPUTATIONAL SEMANTICS OF LAMBDA CALCULUS TERMS Programs = LambdaTerm Gamma = T = Answers = input[[M]] = output[[M]] = ------------------------------------------ a. axioms for transitions and inference rules ------------------------------------------ TRANSITION AXIOMS AND RULES [beta] ((\I.M) N) --> [eta] (\I.(M I)) --> [reduce-body] ------------------ (\I.M) --> (\I.M') [app-operator] ---------------- (M N) --> (M' N) [app-operand] ---------------- (M N) --> (M N') ------------------------------------------ Is this little step or big step? Can you trace the execution of (((\x.(\y. (y x))) i) z)? What is the meaning of ((\x. (x x)) (\x.x))? What is the meaning of ((\x.(x f)) (\x.(z x))? What is the meaning of ((\x.(x x)) (\x.(x x)))? b. remarks c. variations D. Nondeterminism how would you specify angelic, demonic nondeterminism? E. process calculi III. operational semantics of recursion A. adding recursion to the lambda calculus ------------------------------------------ RECURSION IN OPERATIONAL SEMANTICS OF THE \-CALCULUS Extended abstract syntax: M, N \in LambdaTerm I \in Identifier M ::= I | (\ I . M) | (M N) | (rec I = M) Additional Transition Axioms: [unroll] (rec I = M) --> Example: (rec fact = (\n . (((IF (eq n 0)) 1) ((mult n) (fact ((sub n) 1)))))) --> (\n . (((IF (eq n 0)) 1) ((mult n) ((rec fact = (\n . (((IF (eq n 0)) 1) ((mult n) (fact ((sub n) 1)))))) ((sub n) 1))))) ------------------------------------------ can you "simplify" ((rec ohno = (\n. (ohno n))) 3) for a few transitions? B. while loops in an imperative language ------------------------------------------ WHILE LOOPS IN AN IMPERATIVE LANGUAGE Abstract Syntax: L \in Location B, E \in Expression C \in Command C ::= E | skip | L := E | C1 ; C2 | if E then C1 else C2 | while B do C Computation Semantics: Programs = Command Gamma = T = Answers = input[[C]] = output(g) = ------------------------------------------ ------------------------------------------ STORES Domains: V \in Value Storable = Value Sigma \in Store = Location -> Storable Auxiliary functions: empty_store: Store empty_store = \L.unbound update: Store -> Location -> Storable -> Store update Sigma L V = \L'. if L = L' then V else Sigma(L') access: Store -> Location -> Storable access Sigma L = Sigma(L) ------------------------------------------ ------------------------------------------ TRANSITION AXIOMS AND RULES Auxiliary semantic relation: ==>e : Expression * Store -> Value * Store -> o ------------------------------------------ Can you define a suitable grammar for E and a big step semantics for ==>e (this should allow side effects in expressions)? ------------------------------------------ IMPERATIVE COMMANDS PART 1 --> : Command * Store -> Command * Store -> o E, Sigma ==>e V, Sigma' [exp-cmd] ------------------------- E, Sigma --> skip, Sigma' [assign] ------------------------------- L := E, Sigma --> skip, Sigma'' ------------------------------------------ What rule(s) would you have for C1 ; C2 ? What is the semantics of L1 := 1; L2 := 2 ? Can you give a 2 rules for if-commands? ------------------------------------------ IMPERATIVE COMMANDS PART 2 B, Sigma ==>e false, Sigma' [whileF] ------------------------------ while B do C, Sigma --> skip, Sigma' B, Sigma ==>e true, Sigma' [whileT] ------------------------------ while B do C, Sigma --> C;while B do C, Sigma' ------------------------------------------ What is the meaning of the program L1 := 1; while L1 < 3 do L1 := L1 + 1 ? Can you give a big step semantics for commands? Can you give a little step semantics for expressions and modify the above rules to use that? C. summary IV. Structural operational semantics of BeCecil A. overview 1. what has to be done ------------------------------------------ WHAT HAS TO BE DONE TO WRITE A SEMANTICS FOR BECECIL? Tasks: (informal understanding) concrete syntax (examples, informal explanations) abstract syntax big step or little step? data structures (domains) rules for each piece of syntax ------------------------------------------ 2. abstract syntax Do we want recursive declaration sequences as a type? What about class names? 3. semantic domains a. objects ------------------------------------------ OBJECTS module object. import inherits set. % kind objectId = int. kind object type. ------------------------------------------ How do we make objects? How to program oid? b. inheritance relationships Why are inheritance relationships represented as things in BeCecil? ------------------------------------------ INHERITANCE RELATIONSHIPS module inherits. import finite_rel. type leq_inh finite_rel int int -> int -> int -> o. leq_inh I ID1 ID2 :- related I ID1 ID2. leq_inh I ID ID. ((leq_inh I ID1 ID2), (leq_inh I ID2 ID3)) => %------------------------------------- (leq_inh I ID1 ID3). ------------------------------------------ Will this cause computational problems for us? Can you write a \Prolog rule for ancestors membership (figure A-4)? c. generic functions d. contexts, environments, elaborateds e. stores 4. rules How would you write a little step semantics for BeCecil? V. Operational semantics summary A. good points of operational semantics what are some of the good points of operational semantics? B. problems with operational semantics what are some of the bad points of operational semantics?