⚡

操作语义定义器Skill operational-semantics-definer

操作语义定义器是一种用于定义编程语言的操作语义的技能，包括小步和大步语义。它支持语言设计、语义形式化、证明程序属性以及从规范生成可执行解释器。关键词：操作语义，编程语言，语义定义，证明，解释器，语言设计，形式化方法，计算机科学理论。

其他 0 次安装 0 次浏览 更新于 3/13/2026

名称: 操作语义定义器 描述: ‘定义编程语言的操作语义。使用场景：(1) 设计新语言，(2) 证明语言语义属性，(3) 实现解释器。’ 版本: 1.0.0 标签:

  • 语义
  • 操作语义
  • 编程语言基础
  • 语言设计 难度: 中级 语言:
  • OCaml
  • Coq
  • Python 依赖: []

操作语义定义器

定义编程语言的小步和大步操作语义。

使用时机

  • 设计新的编程语言
  • 形式化语言语义
  • 证明程序属性
  • 从规范实现解释器

技能功能

  1. 定义语法 - 为术语和值定义BNF/EBNF
  2. 指定语义 - 结构化操作语义（SOS）
  3. 证明属性 - 进展和保持性质
  4. 生成解释器 - 可执行语义

实现

大步解释器

@dataclass
class Store:
    """内存存储：变量 -> 值"""
    data: dict
    
    def __getitem__(self, x):
        return self.data[x]
    
    def __setitem__(self, x, v):
        return Store({**self.data, x: v})

def eval_expr(e: Expr, s: Store) -> Value:
    match e:
        case Const(n): return n
        case True_(): return True
        case False_(): return False
        case Add(e1, e2):
            v1 = eval_expr(e1, s)
            v2 = eval_expr(e2, s)
            return v1 + v2
        case Eq(e1, e2):
            v1 = eval_expr(e1, s)
            v2 = eval_expr(e2, s)
            return v1 == v2
        case Not(e):
            return not eval_expr(e, s)

def eval_cmd(c: Command, s: Store) -> Store:
    match c:
        case Skip():
            return s
        case Assign(x, e):
            v = eval_expr(e, s)
            return Store({**s.data, x: v})
        case Seq(c1, c2):
            s1 = eval_cmd(c1, s)
            return eval_cmd(c2, s1)
        case If(e, c1, c2):
            if eval_expr(e, s):
                return eval_cmd(c1, s)
            else:
                return eval_cmd(c2, s)
        case While(e, c):
            if eval_expr(e, s):
                s1 = eval_cmd(c, s)
                return eval_cmd(While(e, c), s1)  # 递归
            else:
                return s

小步规约器

from typing import Callable

# 配置: (命令, 存储)
Config = tuple[Command, Store]

def reduce_step(c: Command, s: Store) -> Optional[Config]:
    """执行一步规约，或返回None如果卡住"""
    
    match c:
        # E-上下文
        case Seq(Skip(), c2):
            return (c2, s)
        
        case Seq(c1, c2):
            if can_step(c1):
                c1', s1 = step(c1)
                return (Seq(c1', c2), s1)
        
        # E-赋值
        case Assign(x, e) if is_value(e):
            return (Skip(), Store({**s.data, x: eval_expr(e, s)}))
        
        # E-赋值上下文
        case Assign(x, e) if not is_value(e):
            e' = step_expr(e)
            return (Assign(x, e'), s)
        
        # E-如果真/假
        case If(e, c1, c2) if is_value(e):
            if eval_expr(e, s):
                return (c1, s)
            else:
                return (c2, s)
        
        # E-循环
        case While(e, c):
            return (If(e, Seq(c, While(e, c)), Skip()), s)
    
    return None  # 卡住（无规则适用）

def run_small_step(c0: Command, s0: Store, max_steps=1000):
    """运行程序至完成"""
    c, s = c0, s0
    for _ in range(max_steps):
        if is_value(c) and isinstance(c, Skip):
            return s  # 完成
        result = reduce_step(c, s)
        if result is None:
            raise RuntimeError(f"卡住在: {c}")
        c, s = result
    raise RuntimeError("步骤过多")

核心概念

大步（自然）语义

  • 判断: ⟨e, s⟩ ⇓ v （表达式e在存储s中求值为值v）
  • 优点: 易于阅读，直接连接解释器
  • 缺点: 无法很好表达非终止

小步（结构）语义

  • 判断: ⟨e, s⟩ → ⟨e’, s’⟩ （一步求值）
  • 优点: 处理非终止、并行性、中间状态
  • 缺点: 更多规则，可能复杂

上下文规则

使用求值上下文减少语法冗余：

求值上下文:
  E = [] | E + e | v + E | not E | if E then c1 else c2
  
  ⟨E[e], s⟩ → ⟨E[e'], s'⟩  如果  ⟨e, s⟩ → ⟨e', s'⟩

技巧

  • 首先定义值（什么不能进一步规约）
  • 使用命名约定：(⇒) 用于大步，(→) 用于小步
  • 证明进展 + 保持性质以确保健全性
  • 使用上下文简化小步规则
  • 考虑弱与强双模拟

需要证明的属性

进展

如果 ⊢ e : τ 且 e 不是值，则存在 e’ 使得 e → e’

保持性质

如果 ⊢ e : τ 且 e → e’，则 ⊢ e’ : τ

相关技能

  • denotational-semantics-builder - 指称语义模型
  • hoare-logic-verifier - 公理语义
  • lambda-calculus-interpreter - 兰姆达演算语义

经典参考文献

参考文献 重要性
戈登，《编程语言的指称描述》（1979） 指称语义入门
雷诺兹，《编程语言理论》（1998） 综合语义教材
温斯克，《编程语言的形式语义》（1993） 标准教科书
普洛特金，《结构化操作语义的结构方法》（1981） 原始结构化操作语义
皮尔斯，《类型与编程语言》，第3章（2002） 第3章涵盖操作语义

权衡与限制

语义方法权衡

方法 优点 缺点
大步（自然） 直观，类似解释器 无非终止，无中间状态
小步（SOS） 处理非终止、并行性 规则更多，可能爆炸
指称语义 组合性，代数推理 更难证明属性

何时不使用操作语义

  • 用于验证: 使用公理（霍尔）或指称语义
  • 用于无限状态: 考虑下推自动机或抽象机
  • 用于实时/连续: 使用定时自动机或混合系统

限制

  • 非终止: 大步无法表达发散计算；使用小步
  • 状态爆炸: 小步可能有许多中间配置
  • 并行性: 难以表达并发语义（使用进程演算）
  • 上下文规则: 对于可处理的小步语义必需

研究工具与成果

形式语义在证明助手中：

形式化 证明助手 形式化内容
POPLMark Coq 核心兰姆达演算，属性
机械语义库 Coq 多种语言
SEtP Coq 基于栈的语言
Ott Coq/Isabelle/Agda 语言定义
Lem Coq/Isabelle 生成定义

交互式工具

  • PLT Redex （Racket） - 语义定义，可视化
  • K-框架 - 语言定义，验证
  • Maude - 重写逻辑语义

研究前沿

1. 参数性

  • 目标: 仅从类型证明属性
  • 技术: 关系参数性（雷诺兹）
  • 论文: 《类型、抽象与参数多态》（雷诺兹，1983），《自由定理！》（瓦德勒，1989）
  • 应用: 自由定理

2. 上下文等价

  • 目标: 形式化程序何时行为相同
  • 技术: 应用双相似，环境双相似
  • 论文: 《环境双相似》（桑乔吉等）

3. 关系推理

  • 目标: 证明程序间关系
  • 技术: 逻辑关系，步索引方法
  • 论文: 《单子状态的逻辑关系》（比克达尔等）

4. 指称语义集成

  • 目标: 连接操作和指称语义
  • 技术: 完全抽象证明
  • 论文: 《PCF的完全抽象》（阿布拉姆斯基、贾加迪桑、马拉卡里亚；海兰、翁 - 独立，1990年代）

实现陷阱

陷阱 实际例子 解决方案
卡住状态 语义无效最终状态 首先定义值
非终止 大步错过非终止 使用小步或共归纳
非汇合 不同规约顺序给出不同结果 证明丘-罗瑟
缺失上下文 规则未覆盖所有情况 使用完整性检查
存储传递 可变状态需要谨慎 明确定义存储

“存储”问题

添加可变状态时，必须明确定义存储：

# 配置包括存储
Configuration = (Command, Store)  # 不仅仅是命令

# 存储的求值上下文
def eval_cmd(c, s):
    match c:
        case Assign(x, e):
            v = eval_expr(e, s)
            return (Skip(), s[x := v])  # 返回新存储！

“大步非终止”差距

大步语义无法表达发散：

# 这个循环在大步中永远不会产生结果：
# while true: skip
# 无规则产生值！

# 在小步中，可以建模：
# (while true: skip) → (while true: skip)  -- 无限路径

这就是为什么我们需要小步来处理非终止程序！