时间戳

首页 > 解决方案 > 如何在 Coq 中为 Big Step 和 Small Step 语义定义一个单一的配置？

coq - 如何在 Coq 中为 Big Step 和 Small Step 语义定义一个单一的配置？

问题描述

我试图定义有助于语句/代码/程序/算术/布尔表达式的配置，但我发现自己必须为似乎不必要的每种类型定义一个。是否可以在 Coq 中以某种方式合并所有不同的情况？

Inductive BigConfig : Type :=
  | B_AExpConf : AExp -> State -> BigConfig
  | B_BExpConf : BExp -> State -> BigConfig
  | B_StmtConf : Statement -> State -> BigConfig
  | B_BlkConf : Block -> State -> BigConfig
  | B_StateConf : State -> BigConfig
  | B_PgmConf : Program -> BigConfig.

然后我注意到我也有大步和小步的单独配置。是否可以将它们合并为 1 个单一配置？

Inductive SmallConfig : Type :=
  | S_AExpConf : AExp -> State -> SmallConfig
  | S_BExpConf : BExp -> State -> SmallConfig
  | S_StmtConf : Statement -> State -> SmallConfig
  | S_BlkConf : Block -> State -> SmallConfig
  | S_PgmConf : Program -> SmallConfig.

标签： coq

解决方案

正如我在评论中所说， aBigConfig是SmallConfig + State，意思是，如果你SmallConfig像你一样定义：

Inductive SmallConfig : Type :=
  | S_AExpConf : AExp -> State -> SmallConfig
  | S_BExpConf : BExp -> State -> SmallConfig
  | S_StmtConf : Statement -> State -> SmallConfig
  | S_BlkConf : Block -> State -> SmallConfig
  | S_PgmConf : Program -> SmallConfig.

那么定义的一种方法BigConfig是：

Definition BigConfig : Type := sum SmallConfig State.

然后，您必须对( / ) 和案例中的构造函数进行模式匹配，而不是对BigConfig构造函数（不再存在）进行模式匹配。suminlinrSmallConfiginl

match bconf with
| inl (S_AExpConf a s) => ...
| inl (S_BExpConf b s) => ...
...
| inr s (* this represents B_StateConf *) => ...
end

推荐阅读