3 ms·

Thank you for sharing! A closely related puzzle was previously discussed at: https://news.ycombinator.com/item?id=14400017 https://news.ycombinator.com/item?id

by zmonx 9y ago

Thank you for sharing! A closely related puzzle was previously discussed at: https://news.ycombinator.com/item?id=14400017 https://news.ycombinator.com/item?id=14400017 The present puzzle can be seen as a natural continuation of this earlier thread, and the declarative programming language Prolog is again well-suited for this puzzle. For example, we can start with a short Prolog program that exhaustively generates all solutions: numbers_tree([N], leaf(N)). numbers_tree(Vs0, binary(Left, Right)) :- permutation(Vs0, Vs), append([L|Ls], [R|Rs], Vs), numbers_tree([L|Ls], Left), numbers_tree([R|Rs], Right). tree_op_expr_value(leaf(N), _, number(N), N). tree_op_expr_value(binary(Left0, Right0), Op, expr(Op,Left,Right), Value) :- tree_op_expr_value(Left0, _, Left, VL), tree_op_expr_value(Right0, _, Right, VR), op_values_value(Op, VL, VR, Value). op_values_value(+, A, B, V) :- V is A + B. op_values_value(-, A, B, V) :- V is A - B. op_values_value(×, A, B, V) :- V is A * B. op_values_value(÷, A, B, V) :- B =\= 0, V is A rdiv B. We can query it like this: ?- numbers_tree([4,6,6,6], T), tree_op_expr_value(T, _, Expr, 24). On backtracking, it generates all solutions, reported as abstract syntax trees Expr. This is of course not yet the full task. And I won't solve the full task here, because I would like to give others a chance to also have a look. However, I post a hint towards an efficient solution: In such cases where you want to detect whether something is "essentially the same", consider applying a notion from term rewriting: In term rewriting, we apply rewrite rules, and in strongly normalizing systems, each term has a so-called normal form, which is its canonical representation. Thus, in the language of term rewriting, when trying to decide if two terms are "essentially the same", you can reduce both of them to their respective normal forms, and then compare the normal forms! The two original terms are the same iff their normal forms are the same. Here is part of the term rewriting system I have come up with for this task, implemented in Prolog: commutative(+). commutative(×). expr_normal_form(number(N), number(N)). expr_normal_form(expr(Op,A0,B0), expr(Op,A,B)) :- commutative(Op), expr_comparison(A0, B0, Comp), smaller_first(Comp, A0, B0, A, B). expr_normal_form(expr(Op,A0,B0), expr(Op,A,B)) :- \+ commutative(Op), expr_normal_form(A0, A), expr_normal_form(B0, B). smaller_first(=, A0, B0, A, B) :- expr_normal_form(A0, A), expr_normal_form(B0, B). smaller_first(<, A0, B0, A, B) :- smaller_first(=, A0, B0, A, B). smaller_first(>, A0, B0, A, B) :- smaller_first(<, B0, A0, A, B). expr_comparison(number(A), number(B), C) :- compare(C, A, B). expr_comparison(number(_), expr(_,_,_), <). expr_comparison(expr(_,_,_), number(_), >). expr_comparison(Expr, Expr, =). expr_comparison(expr(Op1, _, _), expr(Op2, _, _), C) :- dif(Op1, Op2), compare(C, Op1, Op2). expr_comparison(expr(Op,A0,B), expr(Op,A,B), C) :- dif(A0, A), expr_comparison(A0, A, C). expr_comparison(expr(Op,A,B0), expr(Op,A,B), C) :- dif(B0, B), expr_comparison(B0, B, C). It works by imposing an order on terms, and recursively rewriting a single term to its normal form, which is smaller than or equal to the original term according to that (self-imposed) order. We can now use an additional predicate like the following to collect all solutions, remove duplicates, then rewrite each solution to its respective normal form, and then remove duplicates again: all_expressions(Ls, Value, Exprs) :- findall(Expr, (numbers_tree(Ls, T), tree_op_expr_value(T, _, Expr, Value)), Exprs0), sort(Exprs0, Exprs1), maplist(expr_normal_form, Exprs1, Exprs2), sort(Exprs2, Exprs). For example, in the [4,6,7,9] = 24 case, this algorithm reduces the expressions to 5 solutions: ?- all_expressions([4,6,7,9], 24, Exprs), maplist(portray_clause, Exprs), length(Exprs, L). expr(×, number(6), expr(÷, expr(+, number(7), number(9)), number(4))). expr(×, expr(+, number(7), number(9)), expr(÷, number(6), number(4))). expr(÷, number(6), expr(÷, number(4), expr(+, number(7), number(9)))). expr(÷, expr(+, number(7), number(9)), expr(÷, number(4), number(6))). expr(÷, expr(×, number(6), expr(+, number(7), number(9))), number(4)). Exprs = [...], L = 5 . I leave adding more rewrite rules as a challenge.

ZephyrP 9y ago
It's kindof funny zmonx, whenever there is a challenge that I think "oh I can do this with a SAT solver", you've already shown up and solved it with Prolog. I think you've gone for the more 'expressive' variant here. If I were writing SMTLIB directly or using an API, I'd prove the assertion that any possible parenthization is eqv by enumerating & checking them individually :)
- zmonx 9y ago
  This may get out of hand: The task asks not only for all parenthesizations, but also other equivalence classes. The rewrite rules and Prolog in general let you express the equivalence classes reasonably concisely and efficiently. I'm still always interested also in other approaches, and greatly enjoy your SAT solutions!
coolio222 9y ago
You defined rewrite rules that reduce an expression down to a 'normalized' form such that two expression are equivalent if they reduce to the same 'normalized' form. These rules are obvious for simple arithmetic expressions. Is it possible to deduce the normalized form and the rewrite rules from a set axioms automatically (e.g. for relational (like SQL) expression with operands like join, project, filter)?
- zmonx 9y ago
  In the terminology (may I say: terms) of term rewriting, you are looking for a so-called completion procedure. This takes a set of axioms and turns it into a convergent term rewriting system (or not, because it may not terminate!). If the completion procedure succeeds, you end up with rules that always terminate, and which reduce any given term to its normal form. In the literature, search for Knuth-Bendix and Huet completion procedure, if you are interested. For SQL, it may get quite complex, but still doable, potentially with some extensions of the primary method. There are all kinds of variations on the general scheme. If you are interested in term rewriting, a solid starting point is Term rewriting and all that by Baader and Nipkow.

by zmonx 9y ago

ZephyrP 9y ago

It's kindof funny zmonx, whenever there is a challenge that I think "oh I can do this with a SAT solver", you've already shown up and solved it with Prolog. I think you've gone for the more 'expressive' variant here. If I were writing SMTLIB directly or using an API, I'd prove the assertion that any possible parenthization is eqv by enumerating & checking them individually :)

zmonx 9y ago
This may get out of hand: The task asks not only for all parenthesizations, but also other equivalence classes. The rewrite rules and Prolog in general let you express the equivalence classes reasonably concisely and efficiently. I'm still always interested also in other approaches, and greatly enjoy your SAT solutions!

coolio222 9y ago

You defined rewrite rules that reduce an expression down to a 'normalized' form such that two expression are equivalent if they reduce to the same 'normalized' form. These rules are obvious for simple arithmetic expressions. Is it possible to deduce the normalized form and the rewrite rules from a set axioms automatically (e.g. for relational (like SQL) expression with operands like join, project, filter)?

zmonx 9y ago
In the terminology (may I say: terms) of term rewriting, you are looking for a so-called completion procedure. This takes a set of axioms and turns it into a convergent term rewriting system (or not, because it may not terminate!). If the completion procedure succeeds, you end up with rules that always terminate, and which reduce any given term to its normal form. In the literature, search for Knuth-Bendix and Huet completion procedure, if you are interested. For SQL, it may get quite complex, but still doable, potentially with some extensions of the primary method. There are all kinds of variations on the general scheme. If you are interested in term rewriting, a solid starting point is Term rewriting and all that by Baader and Nipkow.