Как определить одну единственную конфигурацию для семантики Big Step и Small Step в Coq? - PullRequest
Новая
       7

Как определить одну единственную конфигурацию для семантики Big Step и Small Step в Coq?

0 голосов
/ 22 декабря 2018

Я пытался определить конфигурацию, которая поможет выражению оператор / код / ​​программа / арифметика / bool, но я обнаружил, что должен определить один для каждого типа, который кажется ненужным.Можно ли как-то объединить все разные случаи в 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.

, тогда я заметил, что у меня также есть отдельные конфигурации для больших и маленьких шагов.Возможно ли объединить их в одну конфигурацию? 

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.

1 Ответ

0 голосов
/ 26 декабря 2018

Как я уже сказал в комментариях, BigConfig - это 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 (которых больше не существует) необходимо сопоставить с рисунком на sum (inl / inr) и *Конструкторы 1015 * в корпусе inl. 

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