形式语义学 • 操作语义

是什么

一种着重于描述语言的执行过程的，对程序语言语义的形式化描述方法。

An operational semantics for a programming language is a mathematical definition of its computation relation, $e ⇒ v$ ¹, where e is a program in the language.

为什么

the goal is to give a precise mathematical model of computations/programs —— Lecture notes of DAT350, Chalmers/GU

操作语义 vs 指称语义 vs 公理语义

指称语义更重视“找到代表程序所做所为的数学对象”，比如把无类型 lambda 演算映射到 Martin Lof type theory，从而证明这个语言是 soundness 的。

公理语义的想法是“给出一些公理，以此定义程序的含义”，最常见的例子就是 Hoare logic，可以理解为是关注程序在一些（作为 pre/postcondition 的 ）prediction 上的作用效果。

操作语义则关注“程序的执行过程”，它的目标是给出一个形式化的执行模型。

怎么做

比如说我们要给只有整数的数学表达式定义操作语义。

这个语言的语法是：

data Nat : Set where
    zero : Nat
    suc  : Nat -> Nat

data exp : Set where
    Const : Nat -> exp
    Add : exp -> exp -> exp

我们可以定义一些语义规则：

add : Nat -> Nat -> Nat
add n zero    = n
add n (suc m) = suc (add n m)

data _=>_ : exp -> exp -> Set where
    =>A : {n0 n1 : Nat} -> Add (Const n0) (Const n1) =>  Const (add n0 n1)

    =>L : {e e' e1 : exp} ->
    e => e'
    ->  Add e e1 => Add e' e1

    =>R : {n : Nat} -> {e e' : exp} ->
    e => e'
    ->  Add (Const n) e => Add (Const n) e'

这里的 => 指是“左边的表达式可以（一步）转化为右边的表达式”。

这些规则就构成了一个可以用数理逻辑证明程序的各种性质的证明系统。

比如我们可以证明一个符合这个语法的数学表达式一定是 "progress"² 的：

makes-progress-add : {e0 e1 : exp} -> makes-progress e0 -> makes-progress e1 ->
                                   makes-progress (Add e0 e1)
makes-progress-add isValue isValue = hasReduction =>A
makes-progress-add isValue (hasReduction x) = hasReduction (=>R x)
makes-progress-add (hasReduction x) progress1 = hasReduction (=>L x)

exp-makes-progress : (e : exp) -> makes-progress e
exp-makes-progress (Const x) = isValue
exp-makes-progress (Add e1 e2) = makes-progress-add (exp-makes-progress e1) (exp-makes-progress e2) 

如果我们无法根据这些语义规则进一步 reduce 某个表达式，这个表达式就称之为“范式”（normal form）。

data ⊥ : Set where

elim-⊥ : {A : Set} -> ⊥ -> A
elim-⊥ {A} ()

¬ : Set -> Set
¬ A = A -> ⊥

cannot-reduce-further : exp -> Set
cannot-reduce-further e = {e' : exp} -> ¬ (e => e')

我们可以证明，在这个系统中范式一定是一个值：

data is-value : exp -> Set where
 ConstIsVal : {n : Nat} -> is-value (Const n)

norm-form-is-value : {e : exp} -> cannot-reduce-further e -> is-value e
norm-form-is-value {e} = lemma (exp-makes-progress e)
    where lemma : {e : exp} -> makes-progress e -> cannot-reduce-further e -> is-value e
        lemma isValue cannotReduceEFurther = ConstIsVal
        lemma (hasReduction eToe') cannotReduceEFurther = elim-⊥ (cannotReduceEFurther eToe') -- absurd

小步语义和大步语义

上面的例子是小步语义，它是一步一步地描述程序的执行过程。

而大步语义定义如何从一个表达式或者语句直接得到它的结果。

例如上面的小步语义对应的大步语义可以是：

data _⇓_ : exp -> exp -> Set where
    ⇓suc : {e v : exp} -> e ⇓ v ->
        suc e  ⇓ suc v 

    ⇓prd0 : {e : exp} -> e ⇓ zero ->
        prd e ⇓ zero

    ⇓prdS : {e v : exp} -> e ⇓ suc v ->
        prd (suc e) ⇓ v

    v0 : zero ⇓ zero

小步语义相当于为程序实现了一种迭代式的解释器，而大步语义则相当于为程序实现了一种递归式的解释器。