5
$\begingroup$

I have been reading a couple of texts on operational semantics.

In [1], the evaluation of expressions is done as in this rule:

$\frac{<e_1,s>\;\Rightarrow \;n_1\;\;\;<e_2,s>\;\Rightarrow \;n_2} {<e_1+e_2,s> \;\Rightarrow \; n_3}$,

where $n_3 = n_1+n_2$.

That is, the state $s$ is represented in a tuple with the expression to be evaluated.

But in [2] a rule for evaluation of a function as this:

$\frac{\rho\; \vdash\; e \;\Rightarrow\; v, \;\;\;\;\rho[v'/x]\;\vdash\;e \;\Rightarrow\; v} {\rho\; \vdash \;F(e) \Rightarrow v}$

I am confused: why in the first case, the state $s$ was passed along with the expression as a pair, and in the second case, the environment $\rho$ was not (it was to the left of $\vdash$). Does $\vdash$ here have the same meaning as in formal logic? Are the two notations that I have shown (using a pair/tuple and using $\vdash$) interchangeable in operational semantics?

In this text ([2]), the author writes, before the first time he uses $\vdash$,

In a given environment an expression will evaluate to a numeral. We will write this as $\rho \; \vdash\; e \;\Rightarrow \;v$

But he doesn't explain why, and in another text ([1]) the same author uses the pair notation for the same purpose.

$\endgroup$

1 Answer 1

15
$\begingroup$

This is something that I think is not explicitly pointed out or not pointed out with enough emphasis in many, even introductory, CS/type theory/logic texts.

$\vdash$ doesn't mean anything.

Instead, in this example, the three place relation $- \vdash - \Rightarrow -$ is what has meaning.

Except that was a lie. It doesn't a priori have meaning either. That relation is what is being defined. $- \vdash - \Rightarrow -$ is just a (mixfix) name. It does, of course, have some informal meaning we are hoping to capture with this definition, and after it is defined it does have meaning.

In most cases, such relationships are being inductively defined which makes them identical to inductive families in a dependently typed language. For example, here are the rules for the arithmetic language fragment from figure 3.2 in section 3.1: $$ \frac{}{\langle n,s \rangle \Downarrow n} \qquad \frac{\langle e_1, s\rangle \Downarrow n_1 \qquad \langle e_2, s\rangle \Downarrow n_2}{\langle e_1 + e_2, s \rangle \Downarrow n_1+n_2} \qquad \frac{}{\langle \mathtt{L}, s \rangle \Downarrow s(\mathtt{L})} $$

and here's Agda code for this fragment:

data Expr : Set where 
    Num : Nat -> Expr
    Add : Expr -> Expr -> Expr
    Lookup : Label -> Expr

data Eval : (e : Expr) (s : Label -> Nat) (n : Nat) -> Set where
    EvalNat : {n : Nat}{s : Label -> Nat}
        -> Eval (Num n) s n
    EvalAdd : {e1 e2 : Expr}{n1 n2 : Nat}{s : Label -> Nat}
        -> Eval e1 s n1 
        -> Eval e2 s n2 
        -> Eval (Add e1 e2) s (n1+n2)
    EvalLookup : {l : Label}{s : Label -> Nat} 
        -> Eval (Lookup l) s (s l)

A proof of a statement like $\langle 3+4,s \rangle \Downarrow 7$ looks like:

threePlusFourIsSeven : {s : Label -> Nat} -> Eval (Add (Num 3) (Num 4)) s 7
threePlusFourIsSeven = EvalAdd EvalNum EvalNum

Rule induction, which is the topic of section 2.3, is induction over data types like this.

I hope at this point that you can see that the answer to:

Are the two notations that I have shown (using a pair/tuple and using ⊢) interchangeable in operational semantics?

is "yes, but only because whenever you see such notation it is being or has been defined, and we can use whatever notation we want to mean whatever we want if we define it." In other words, nothing is stopping us from having used the syntax $s \vdash e \Rightarrow n$ instead of $\langle e, s\rangle \Rightarrow n$. We'd just be defining a relation named $- \vdash - \Rightarrow -$ instead of being named $\langle -,- \rangle \Rightarrow -$.

That said, there are (unwritten) conventionsnaming conventions no less – that are commonly abided by. So $\vdash$ is normally used to separate some "context" or "environment" from "terms". The tuple notation is often used for state components because we (denotationally) model state as a function from the old state to the output plus the new state. If we also have input, this results in a function (Input, State) -> (Output, State). This intuition gets reflected in the naming of the operational semantics, as in, for example, figure 3.6 which includes rules like $\langle \mathtt{skip};C_2, s\rangle \rightarrow \langle C_2, s\rangle$. Nothing stops us from writing that $s \vdash \mathtt{skip};C_2 \rightarrow s \vdash C_2$, but I think you can agree that that is harder to read.

I got around to posting a blog article that goes into this notation in more detail.

$\endgroup$
1
  • $\begingroup$ I agree. But I should point out that, for example, Dave Schmidt does exactly the opposite in this pdf file: on page 11, he writes e,s |- C1 => s... :-) $\endgroup$
    – Jay
    Mar 16, 2016 at 1:37

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.