Доказательство множества достижимых состояний функции семантики конечно в Изабель - PullRequest
Новая
       9

Доказательство множества достижимых состояний функции семантики конечно в Изабель

0 голосов
/ 11 января 2019

Рассмотрим следующее свойство: 

lemma "finite {t. (c,s) ⇒ t}"

Что относится к следующей семантике большого шага: 

inductive gbig_step :: "com × state ⇒ state ⇒ bool" (infix "⇒" 55) 
where
  Skip: "(SKIP, s) ⇒ s"
| Assign: "(x ::= a, s) ⇒ s(x := aval a s)"
| Seq: "⟦(c1, s1) ⇒ s2;  (c2, s2) ⇒ s3⟧ ⟹ (c1;;c2, s1) ⇒ s3" 
| IfBlock: "⟦(b,c) ∈ set gcs; bval b s; (c,s) ⇒ s'⟧ ⟹ (IF gcs FI, s) ⇒ s'"
| DoTrue: "⟦(b,c) ∈ set gcs; bval b s1; (c,s1) ⇒ s2;(DO gcs OD,s2) ⇒ s3⟧ 
            ⟹ (DO gcs OD, s1) ⇒ s3"
| DoFalse: "⟦(∀ (b,c) ∈ set gcs. ¬ bval b s)⟧ ⟹ (DO gcs OD, s) ⇒ s"

Для меня очевидно, что свойство имеет место по индукции по отношению большого шага. Тем не менее, я не могу получить его из набора, поэтому я не могу эффективно индуцировать его.

Как я мог это сделать?

1 Ответ

0 голосов
/ 11 января 2019

Конечность - это ничто, что вы могли бы доказать непосредственно с помощью правила индукции индуктивного предиката. Проблема состоит в том, что рассмотрение отдельного прогона (как и правило индукции) ничего не говорит о поведении ветвления, которое также должно быть конечным для выполнения оператора.

Я вижу два подхода к доказательству конечности:

  1. Моделируйте деривационное дерево явно как тип данных в Изабель / HOL и докажите, что оно адекватно представляет деривационные деревья за индуктивным. Затем докажите, что у дерева конечное число листьев (индукцией по дереву). Если вы проектируете тип данных таким образом, чтобы состояния в листьях были параметром типа, то соответствующая функция множества, сгенерированная пакетом типа данных, - это то, что вы хотите доказать как конечное. (Обратите внимание, что вы не можете доказать конечность по правилу индукции функции set, потому что это снова будет просто один прогон.)

  2. Посмотрите на внутреннюю конструкцию индуктивного определения. Он определяется как наименьшая точка фиксации функционала. Вы можете получить доступ к этим внутренним элементам, поместив индуктивное определение в контекст, в котором объявлено [[inductive_internals]]. Затем вы можете доказать, что функционал сохраняет конечность за один шаг, а затем поднять ее через индукцию.

Аргумент доказательства в обоих подходах одинаков. Явный тип данных в # 1 просто использует аргумент с фиксированной точкой # 2. Таким образом, вы можете думать о # 1 как о глубоком встраивании # 2. Конечно, вы также можете заново вывести внутреннюю конструкцию (в более подходящем формате) только из теорем о введении и индукции, а затем следовать подходу № 2.

Я бы попробовал сделать именно это, так как ваша семантика мала. Для большой семантики реального мира, возможно, имеет смысл потратить усилия на автоматизацию шага № 2 в ML.

...