Hacker News Reader

Comment by wkornewald | Hacker News Reader

67 pointswkornewald29 comments

If you're interested in declarative programming, you should also have a look at answer set programming. Here's an ASP version of the problem that additionally requires prime factors.

  domain(100..999).
  digit(0..9).
  
  % Variation w/ prime factors
  prime(P) :- domain(P), { domain(F) : F < P, P \ F == 0 } 0.
  prod(P1 * P2) :- prime(P1;P2).
  
  % Palindrome
  pd(X) :- prod(X), X = 100000*A + 10000*B + 1000*C + 100*C + 10*B + A, 
    digit(A;B;C).
  
  pdMax(M) :- M = #max { X : pd(X) }.
  #show pdMax/1.

Superficially it resembles Prolog, but brings "true" declarativity to the table, i.e., the order of rules and the order of atoms in the body is negligible. Various notions of safety and the prohibition of nested complex terms (e.g. `f(f(x))') guarantee termination. Most importantly though, solutions to an answer set program are not proofs (as in Prolog) but truth-assignments of atoms ("answer sets"). In this specific encoding there's no significant difference though, as we're only computing a single answer set containing an atom "pdMax(X)" with the maximum palindrome X.

Solving answer set programs usually involves heuristics and much work along the lines of SAT solving. Recent solvers such as clasp [1] are surprising efficient though and rival state of the art SAT solvers.

[1] http://potassco.sourceforge.net/

Another related language is Maude. It's a term-rewriting language, so for example we can implement arithmetic by defining symbols to represent numerals (eg. "zero" and "successor") and some rewrite rules which implement addition, subtraction, multiplication, etc. This is similar to languages like Pure, which lets us write code in a pure-functional style, but with the bonus that rewriting can avoid awkward recursion schemes (eg. "a + b" can recurse on both arguments at once). This makes it well-suited to implementing domain-specific languages.

However, Maude can go further than other rewrite languages since it is also a model checker: if A rewrites to B, we can supply A and get back B; or we can supply B and have Maude search for an A. If A and B are DSL terms, we can derive terms from their properties, as is being discussed here.

We can also have Maude show that some terms are unreachable, for example that there is no input which rewrites to an Error symbol.

Of course the advantage to Z3 is that it's hooked up to fast domain-specific solvers (SAT, SMT, arithmetic, etc.), whilst Maude's search is general-purpose and therefore slower.

Notice George Sakkis's comment to the post, the maximize function doesn't work well without the additional unexplained heuristic:

  Why did you need to change "(assert (and (>= a 1) (<= a 9)))" with "(assert (= a 9))"?
  Turns out that the former doesn’t find the correct solution, instead it yields 137*803=110011.
  Whatever the reason I think it’s worth mentioning in the article.

Related, Kaplan, a Scala based constraint language (uses Z3 for solving): http://lara.epfl.ch/~kuncak/papers/KoeksalETAL12ConstraintsC...

The Lara team at EPFL seems to be doing lots of research in this area: http://lara.epfl.ch/w/Start

If this interests you, please do check out prolog. Declarative languages let you do something quite similar. In particular, they let you specify what you want the computer to give you rather than what you want the computer to do.

Believe it or not, a very good example of such a language which you might be familiar with is SQL.

Worth noting though that Prolog will do similar things only with finite domain solvers, which are all extensions to the language. Otherwise it's just a search with backtracking (read: brute-force) with well-defined semantics.

I don't believe it, because I use SQL every day, and I need to tell it which rows to lock when reading, whether to read them in share mode or fully, sometimes I need to help it figure out which indexes to use (of course I also have to manually set up the indexes too), when doing transactions I need to tell it how exactly to isolate the transaction, and I need to be very careful how I order my queries in order to avoid deadlocks.

SQL is declarative only when you don't care about data integrity and performance.

Maybe a bit better example for this kind of behavior are compilers. They're pretty "declarative" these days. You write what code you want to compile, and the compiler will pass it through a thousand transformation stages, deciding which trick to apply at every instruction, which code isn't really needed and so on.

Of course, then you also need to deal with compilers getting it wrong too, so you start tweaking your code with special words like "volatile" and "restricted", mess with compiler options, and sometimes even disassemble code to see why turning the "fast" options makes your code slow. But in general, high quality compilers do this dance way better than SQL.

So what's the moral here? Two things.

First, calling something "declarative" doesn't really mean anything. It means the language is built on a very thick abstraction that lets the computer do more work than usual, so you can do less work.

Second, thick abstractions are leaky. Works for basic cases, past that you'll still end up doing a lot of work, but now you have to fight your computer while doing it, as well.

The Z3 Theorem Prover is an interesting toy, but I wouldn't trust it to do anything right in the real world. Much like most Microsoft Research projects, unfortunately.

Prolog is a very different beast, in that it doesn't rely on any "thick" abstraction. It's based on resolution [1], thus the way code is executed is straightforward and unsurprising (providing you understand resolution first).

If you have never tried it out you should, maybe you will like declarative languages a little bit more afterwards.

[1] http://en.wikipedia.org/wiki/Resolution_%28logic%29

So, when I say SQL, I meant ansi SQL, not PL/SQL, or any of the other various extensions of the language. Neither is purely declarative, but the prior is much closer.

Also I wasn't suggesting that declarative languages are broadly useful (in fact I'd suggest quite the opposite), just that they are very interesting.

Prolog is the kind of language that is sold on being declarative, but ultimately you have to study how the unification algorithm works. And probably also sprinkle cuts around your code in order to not let the runtime do too much work, or maybe so that it will work correctly.

Granted I've only used it in one university course (and only half of that course).

So, why someone don't write a stuff like this that takes your source code with tests and "builds" your app by creating the files in your dist without tests?

- I write the tests - I run the compiler which transforms the tests into implementation - Run the implementation

Is this even possible at all in meaningful time?

For some definitions of "meaningful," yes. Per my other comment, you're describing a declarative language (prolog). Prolog is known for being ridiculously cool, and just as ridiculously slow.

That said, I think the same was true for functional languages before the folks behind GHC came along. I'd be curious to see what could happen if some substantial resources (and a few heaps of modern optimisation knowledge) were poured into this sort of language.

There is an interesting area of computer science called [inductive programming](http://en.wikipedia.org/wiki/Inductive_programming) dedicated to this sort of thing, though in a slightly different way than shown in this blog post.

Yes, you're talking about Coq. The system in this post is a fairly simple one based on unification; Coq is a full-blown theorem prover.

http://jheusser.github.io/2013/02/03/satcoin.html is an article giving an example of using this approach (using a SAT solver) to bitcoin mining- how you would specify the problem etc.

Note that generating a grounding of boolean variables that satisfy a boolean expression is NP-complete (in general). That is just one of the many problem that lie a the bottom of conditional (if/else) logic (i.e. procedural programming).

Yes, it basically solves a SAT problem. But modern SAT solver are very very efficient. So although your worst case is exponential, in many cases heuristics will help find a solution very quickly. That's quite impressive; in fact, the motto "if you have a NP-hard problem just reduce it to SAT and throw a SAT solver on it" is becoming more and more common.

NP-complete is an unbreakable wall, strewn with the bloodied corpses of enthusiastic heuristic authors.

You can only break it if your problem domain was never NP-hard in the first place (e.g. sparse or some other exploitable structural features). Very very fast means nothing on a true NP-hard problem for quite modest n.

Note the author had to include a spurious constraint to get his system to converge, despite it being quite a small task in the first place. My point was that this approach has fundamental reasons why it won't scale to real programming tasks, of which the interesting ones that programmers get wrong all the time are likely to be the true NP-complete type.

I'm disappointed. I thought I was going to see the solver generates code that finds the largest palindrome. I recall how mini-Kanren was used to generate quines. Z3 should be capable of similar feats.

Yeah, that was my first thought, too, but the article is still inspirational. Could code generation ever be fast enough for practical problems? I'm wondering how far we could get if the generated code for each problem is cached between compiles (so we build up a huge database of solutions over time) and also reused, based on the satisfied constraints, when searching for solutions to more complex problems (much like developers reuse existing functions).

I good start might be getting RSpec and generating the correct scaffolds for it in Rails. It would only work for a tiny subset of problems but it would be a start, and also produce something many web developers could see the real world use for.

Well, as benjamincburns says in another comment, Z3 is basically equivalent to the finite domain solver of a Prolog. Since mini-Kanren is a Prolog, it is not surprising that it is more powerful. Otherwise Z3 would also be a Prolog :).

eval-quines are pretty mindblowing.

This is fantastic, if you want to solve only maths problems. But when there is real state and real side-effects and real hardware matters, this sort of approach breaks down.

recently i was tinkering with the idea vedil.wordpress.com/2014/07/09/test-driven-program-synthesis/

is this feasible?

Hmmm.. but how did the theorem prover find the solution? Probably by heuristics + brute force.

"Z3 integrates a modern DPLL-based SAT solver, a core theory solver that handles equalities and uninterpreted functions, satellite solvers (for arithmetic, arrays, etc.), and an E-matching abstract machine (for quantifiers)"

From http://research.microsoft.com/en-us/um/redmond/projects/z3/z...

I'm not well-versed on this topic, but I believe this [1] is presently the state of the art. I'd be curious to know whether or not Z3 performance beats GNU's prolog implementation for similar problem sets.

1: http://www.gprolog.org/#TOChead

I'm not sure which one exactly, but it's a SAT solver, so it uses a SAT solving algorithm [1].

1 - http://en.wikipedia.org/wiki/Boolean_satisfiability_problem#...

Reply on news.ycombinator.com