sml - 标准 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

一般来说，当你有这样的 sum 类型时，最好从一个只列出每个案例但忽略实现的函数定义开始：

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)) = ...

这里我留了两个case给你填写。
注意每个case的英文定义和ML的定义都有非常密切的对应关系。