Как преобразовать пропозициональную формулу в ДНФ в Coq

Я определил свои пропозициональные формулы следующим образом:

Inductive propForm : Set :=
| top : propForm
| bot : propForm
| var : propVar -> propForm
| orp : propForm -> propForm -> propForm
| andp : propForm -> propForm -> propForm.

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

Fixpoint distribute (f:propForm) : propForm -> propForm :=
fix distribute1 (g:propForm) : propForm :=
match f with
| f1 \/p f2 => match g with
            | g1 \/p g2 => distribute1 g1 \/p distribute1 g2
            | _ => distribute f1 g \/p distribute f2 g
            end
| _ => match g with
       | g1 \/p g2 => distribute1 g1 \/p distribute1 g2
       | _ => f /\p g
       end
end.

Эта функция работает нормально. Однако мне все еще нужно определить функцию, которая преобразует пропозициональную формулу в ДНФ. Следующая функция будет делать то, что я хочу, однако Coq не принимает ее, потому что функция не убывает структурно по f' для последнего случая. Любые подсказки и советы будут оценены.

Fixpoint toDNF (f':propForm):propForm :=
match f' with
| top => f'
| bot => f'
| var _ => f'
| f1 \/p f2 => toDNF f1 \/p toDNF f2
| f1 /\p f2 => toDNF (distribute f1 f2)
end.

normalization coq
person Myrthe van Delft    schedule 19.02.2016    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Ваша функция — это частный случай нормализации выражения из полукольца. Я написал сообщение, объясняющее, как это сделать в случай арифметических выражений с использованием библиотек Ssreflect и MathComp, но я включу здесь более прямой ответ.

Одна из идей состоит в том, чтобы использовать списки списков для представления формул в ДНФ: в конце концов, они являются просто конъюнкцией списка дизъюнкций, которые являются просто списками литералов. Затем вы можете повторно использовать библиотеку списка для написания своей функции:

Module Sol1.

Require Import Coq.Lists.List.
Import ListNotations.

Notation propVar := nat.

Inductive propAtom :=
| top | bot | var :> propVar -> propAtom.

Inductive propForm : Set :=
| atom :> propAtom -> propForm
| orp : propForm -> propForm -> propForm
| andp : propForm -> propForm -> propForm.

Definition dnfForm := list (list propAtom).

Fixpoint andd (f1 f2 : dnfForm) : dnfForm :=
  match f1 with
  | [] =>
    (* false && f2 = false *)
    []
  | cf :: f1 =>
    (* (cf || f1) && f2 = cf && f2 || f1 && f2 *)
    map (app cf) f2 ++ andd f1 f2
  end.

Fixpoint toDNF (f : propForm) : dnfForm :=
  match f with
  | atom a => [[a]]
  | orp f1 f2 => toDNF f1 ++ toDNF f2
  | andp f1 f2 => andd (toDNF f1) (toDNF f2)
  end.

Compute (toDNF (andp (orp 3 4) (orp 1 2))).

End Sol1.

Здесь следует отметить две вещи. Во-первых, я факторизовал переменные и константы как отдельный тип propAtom и назвал distribute andd, потому что вы можете думать об этом как о вычислении И двух выражений в ДНФ.

Вот еще одно решение, основанное на вашем исходном коде. Кажется, что ваша функция distribute сохраняет инвариант нахождения в DNF; то есть, если f1 и f2 находятся в ДНФ, то и distribute f1 f2 тоже. Таким образом, вы можете просто поменять порядок вызовов:

Module Sol2.

Notation propVar := nat.

Inductive propForm : Set :=
| top : propForm
| bot : propForm
| var :> propVar -> propForm
| orp : propForm -> propForm -> propForm
| andp : propForm -> propForm -> propForm.

Fixpoint distribute (f:propForm) : propForm -> propForm :=
fix distribute1 (g:propForm) : propForm :=
match f with
| orp f1 f2 => match g with
            | orp g1 g2 => orp (distribute1 g1) (distribute1 g2)
            | _ => orp (distribute f1 g) (distribute f2 g)
            end
| _ => match g with
       | orp g1 g2 => orp (distribute1 g1) (distribute1 g2)
       | _ => andp f g
       end
end.

Fixpoint toDNF (f':propForm):propForm :=
match f' with
| top => f'
| bot => f'
| var _ => f'
| orp f1 f2 => orp (toDNF f1) (toDNF f2)
| andp f1 f2 => distribute (toDNF f1) (toDNF f2)
end.

Compute (toDNF (andp (orp 3 4) (orp 1 2))).

End Sol2.
person Arthur Azevedo De Amorim    schedule 19.02.2016
comment
Спасибо, я уже фактически всем доказал, что мой дистрибутив действительно сохраняет инвариант нахождения в DNF. Однако я не осознавал последствия того, что я мог изменить порядок вызовов. Поскольку мне нужна эквивалентность между пропозициональными формулами, определение отдельного типа потребовало бы много работы, поскольку мне также потребовались бы полные и надежные преобразования. - person Myrthe van Delft; 19.02.2016
comment
Я понимаю вашу точку зрения, но на самом деле это не так уж плохо, поскольку вы всегда можете написать функцию для преобразования формулы DNF (как списка списков) обратно в общую. Если у вас есть хорошая инфраструктура для рассуждений о списках и алгебраических структурах (как предоставляет Ssreflect), то объем кода, который вы сэкономите, определенно оправдывает использование этого подхода. - person Arthur Azevedo De Amorim; 19.02.2016