Размер пропозиционально-логической формулы в стандарте ML

Question

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

datatype fmla =
     F_Var of string
   | F_Not of fmla
   | F_And of fmla * fmla
   | F_Or of fmla * fmla 

Я пытаюсь написать функцию, которая возвращает размер формулы логики высказываний. Пропозициональная переменная имеет размер 1; логическое отрицание имеет размер 1 плюс размер его подформулы; логическое соединение и дизъюнкция имеют размер 1 плюс размеры их подформул.

Как бы я попытался решить эту проблему?

Answer 1

В общем, когда у вас есть такой тип суммы, лучше начать с определения функции, которое просто перечисляет каждый случай, но не учитывает реализацию:

fun size (F_Var v) =
  | size (F_Not f) =        
  | size (F_And (f1, f2)) =
  | size (F_Or (f1, f2)) =

и затем вы заполняете определения дел по одному, как только вы их выясняете.

Поскольку у вас уже есть список того, что размер в каждом конкретном случае;

• Пропозициональная переменная имеет размер 1.
• Отрицание имеет размер 1 плюс размер его подформулы.
• Соединение имеет размер 1 плюс сумму размеров его подформул.
• У дизъюнкции размер 1 плюс сумма размеров его подформул.

Вы можете в значительной степени перевести его непосредственно в ML:

fun size (F_Var _) = 1
  | size (F_Not f) = 1 + size f
  | size (F_And (f1, f2)) = ...
  | size (F_Or (f1, f2)) = ...

где я оставил два дела для вас, чтобы заполнить.
Обратите внимание, что существует очень близкое соответствие между определением на английском языке и определением на ML в каждом случае.