logic - 评估 OCaml 中所有可能的解释

Question

我需要评估两个公式是否等价。在这里，我使用了一个简单的公式定义，即前缀公式。

例如，And(Atom("b"), True)表示b and true，而And(Atom("b"), Or (Atom("c"), Not(Atom("c")))) 表示 (b and (c or not c))

我的想法很简单，获取所有原子，应用每个组合(对于我的案例，我将有 4 种组合，即真-真、真-假、假-真和假-假)。问题是，我不知道如何创建这些组合。

目前，我已经知道如何获得所有涉及的原子，所以如果有 5 个原子，我应该创建 32 种组合。在 OCaml 中如何实现？

Answer 1

好的，所以您需要的是一个函数combinations n，它将生成所有长度为n 的 bool 组合；让我们将它们表示为 bool 值列表的列表(即，单个变量赋值将是 bool 值列表)。然后这个函数就可以完成这项工作:

let rec combinations = function
  | 0 -> [[]]
  | n ->
    let rest = combinations (n - 1) in
    let comb_f = List.map (fun l -> false::l) rest in
    let comb_t = List.map (fun l -> true::l) rest in
    comb_t @ comb_f

只有一个长度为 0 的空组合，对于 n > 0，我们生成 n-1 的组合，并在它们前面加上 false 和 true 生成所有可能的长度组合 n。

你可以写一个函数来打印这样的组合，比方说:

let rec combinations_to_string = function
  | [] -> ""
  | x::xs ->
      let rec bools_to_str = function
        | [] -> ""
        | b::bs -> Printf.sprintf "%s%s" (if b then "T" else "F") (bools_to_str bs)
      in
      Printf.sprintf "[%s]%s" (bools_to_str x) (combinations_to_string xs)

然后用以下方法测试:

let _ =
  let n = int_of_string Sys.argv.(1) in
  let combs = combinations n in
  Printf.eprintf "combinations(%d) = %s\n" n (combinations_to_string combs)

得到:

> ./combinations 3
combinations(3) = [TTT][TTF][TFT][TFF][FTT][FTF][FFT][FFF]