时间戳

首页 > 解决方案 > Prolog: show truth table for arbitrary expression using is/2 for some subexpressions

prolog - Prolog: show truth table for arbitrary expression using is/2 for some subexpressions

问题描述

Suppose I have some expressions that look like a /\ b \/ c. I would like to generate the truth table for this, something like:

 a |  b |  c | a /\ b \/ c
---+----+----+-------------+-
 F |  F |  F | F
 F |  F |  T | T
 F |  T |  F | F
 F |  T |  T | T
 T |  F |  F | F
 T |  F |  T | T
 T |  T |  F | T
 T |  T |  T | T

A key idea here is to handle operators that are not already handled by is/2, such as logical implication ->. By the way, this question is derived from a post by reddit user u/emergenthoughts.

The code I have for this is as follows:

bool(0).
bool(1).

negate(1, 0).
negate(0, 1).

eval(Assignments, A, V) :- atom(A), memberchk(A=V, Assignments).
eval(Assignments, \+ E, V) :- eval(Assignments, E, NotV), negate(NotV, V).
eval(Assignments, E1 /\ E2, V) :-
    eval(Assignments, E1, V1),
    eval(Assignments, E2, V2),
    V is V1 /\ V2.
eval(Assignments, E1 \/ E2, V) :-
    eval(Assignments, E1, V1),
    eval(Assignments, E2, V2),
    V is V1 \/ V2.
eval(Assignments, E1 -> E2, V) :-
    eval(Assignments, E1, V1),
    V1 = 1 -> eval(Assignments, E2, V) ; V = 1.

generate_assignment(Variable, Variable=B) :- bool(B).
generate_assignments(Variables, Assignments) :-
    maplist(generate_assignment, Variables, Assignments).

atoms_of_expr(A, A) :- atom(A).
atoms_of_expr(\+ E, A) :- atoms_of_expr(E, A).
atoms_of_expr(E1 /\ E2, A) :- atoms_of_expr(E1, A) ; atoms_of_expr(E2, A).
atoms_of_expr(E1 \/ E2, A) :- atoms_of_expr(E1, A) ; atoms_of_expr(E2, A).
atoms_of_expr(E1 -> E2, A) :- atoms_of_expr(E1, A) ; atoms_of_expr(E2, A).

table_for(E) :-
    setof(A, atoms_of_expr(E, A), Variables),
    write_header(Variables, E),
    write_separator(Variables, E),
    table_rest(Variables, E).

table_rest(Variables, E) :-    
    generate_assignments(Variables, Assignments),
    eval(Assignments, E, Value),
    write_assignments(Assignments, Value),
    fail.
table_rest(_, _) :- true.

write_header([Var|Rest], E) :- 
    write(' '), write(Var), write(' | '), write_header(Rest, E).
write_header([], E) :- writeln(E).

write_separator([_|R], E) :- write('---+-'), write_separator(R, E).
write_separator([], _) :- write('-+-'), nl.

write_assignments([_=Var|Rest], Value) :-
    write(' '), write(Var), write(' | '), write_assignments(Rest, Value).
write_assignments([], Value) :- writeln(Value).

This code produces the slightly worse than desired output, but I didn't want to bore you with a lot of formatting:

?- table_for(a/\b\/c).
 a |  b |  c | a/\b\/c
---+----+----+--+-
 0 |  0 |  0 | 0
 0 |  0 |  1 | 1
 0 |  1 |  0 | 0
 0 |  1 |  1 | 1
 1 |  0 |  0 | 0
 1 |  0 |  1 | 1
 1 |  1 |  0 | 1
 1 |  1 |  1 | 1
true.

I believe this solution is fairly simple and I like it, but I'm often surprised in Prolog by what the real wizards are able to do so I thought I'd ask if there are significant improvements to be made here. atoms_of_expr/2 feels a bit like boilerplate, since it duplicates the traversal in eval/3. I didn't see a way to use term_variables/2 instead because then I don't think I'd be able to actually supply the names the variables have or bind on them properly with memberchk/2. Am I mistaken?

标签： prologexpression-evaluation

解决方案

以下内容并不完全是该任务的字面要求。尽管如此，我还是想展示在推理此类任务时留在纯子集中是如何得到回报的，因此我将重点放在这一方面。

核心思想是以下谓词，定义布尔公式与其真值之间的关系：

eval(v(V), V) :- V in 0..1。
eval(\+ E0, V) :- eval(E0, V0), V #= 1 - V0。
eval(E1 /\ E2, V) :- eval(E1, V1), eval(E2, V2), V #<==> V1 #/\ V2.
eval(E1 \/ E2, V) :- eval(E1, V1), eval(E2, V2), V #<==> V1 #\/ V2。
eval((E1 -> E2), V) :- eval(E1, V1), eval(E2, V2), V #<==> (V1 #==> V2)。

这使用整数约束尽可能多地委托给 Prolog 引擎。有关详细信息，请参阅。如果您的 Prolog 系统支持它们，您也可以使用约束作为替代。请注意，我们正在处理实际的 Prolog 变量，而不是在 Prolog 中具体化变量及其绑定环境。

另请注意，我正在使用所谓的干净表示，通过唯一（任意）主要仿函数 v/1来区分变量。这使得谓词适合于参数索引，同时保留了它的一般性。它不是（但几乎！）预期的输入格式。然而，将预期的输入格式转换为如此清晰的表示是直截了当的，我将这部分作为一个挑战。

作为补充一点，请注意 中的括号(E1->E2)。他们的原因是：

6.3.3.1 参数

一个参数（在语法规则中由 arg 表示）
作为复合词项或元素的参数出现
一个列表。它可以是作为运算符的原子，也可以是术语
优先级不大于 999。...

因此，省略括号是不符合语法的，例如在 GNU Prolog 中不起作用。

现在我们几乎已经完成了，因为我们现在可以使用 Prolog 的内置机制来推理这些公式及其包含的变量。特别有帮助的是term_variables/2, 和variable_names/1read 和 write 选项。

以下是读取和打印的不纯部分：

跑 ：-
        read_term（公式，[variable_names（VNs）]），
        term_variables（公式，Vs），
        maplist(write_variable(VNs), Vs),
        write_term（公式，[variable_names（VNs）]），
        nl,
        eval（公式，值），
        标签（Vs），
        maplist(write_variable(VNs), Vs),
        格式（“~w\n”，[值]），
        错误的。

write_variable(VNs, V) :-
        write_term(V, [variable_names(VNs)]),
        格式（“|”，[]）。

示例用法：

？- 跑。
|: v(A)/\v(B)\/v(C)。
一个 | 乙| C | v(A)/\v(B)\/v(C)
0 | 0 | 0 | 0
0 | 0 | 1 | 1
0 | 1 | 0 | 0
0 | 1 | 1 | 1
1 | 0 | 0 | 0
1 | 0 | 1 | 1
1 | 1 | 0 | 1
1 | 1 | 1 | 1
错误的。

将代码中的纯部分和不纯部分分开是一种很好的做法，因为我们现在仍然可以在所有方向上使用纯部分。

例如：

?- eval（公式，0）。
公式 = v(0) ;
公式 = (\+v(1)) ;
公式 = (\+ \+v(0)) ;
公式 = (\+ \+ \+v(1)) ;
公式 = (\+ \+ \+ \+v(0)) ;
等等

它可能不是特别有用，但总比没有好。特别是，它说明“eval”不是这个关系的好名字，因为“eval”是一个命令式并且只建议一种可能的使用模式，而实际上这个关系也可以用于其他方向！我把寻找一个更好、更具说明性的名字作为一个挑战。

将这些干净的公式转换为其他表示是直截了当的，我强烈建议将它们用于所有“内部”推理。仅对于实际的输入和输出部分，在它们和其他表示之间进行转换可能很有用。

推荐阅读