robsimmons's comments

The presentation (a PDF with the slides and the talk transcript) are now linked from https://typesafety.net/rob/blog/fclp-at-popl

If every program has a finite model, the language cannot be Turing complete.

If it is not possible to give every program a finite model, that doesn't imply that language IS Turing complete. However, in practice, a Datalog-family logic programming language where some programs have infinite models is likely, in my experience, to be Turing Complete.

(For what it's worth, I don't know what it means for ASP to be incomplete in the sense of soundness and completeness. Incomplete relative to what other thing?)

Indeed — answer set programming has been used for this purpose, see https://arxiv.org/pdf/2212.06719 (which was co-authored by Chris Martens, the co-designer of Dusa and the primary author of the Finite-Choice Logic Programming paper).

Good point! "Whenever" is probably even closer to the correct meaning.

All implementations of Answer Set Programming I am aware of are actually Turing complete, as are many practical implementations of the Datalog idea, and so is Dusa — this is a common misconception!

From the paper: "often people take “Datalog” to specifically refer to “function- free” logic programs where term constants have no arguments, a condition sufficient to ensure that every program has a finite model. We follow many theoretical developments and practical implementations of datalog in ignoring the function-free requirement." If every program has a finite model, the language cannot be Turing complete: the reverse is not necessarily true but in practice the reverse is usually true.

Unfortunately, starting from a perspective that logic programming is mostly Prolog is a pretty bad way of getting to understand what Dusa is about. There's nothing wrong with that starting point, it's just... kind of like trying to understand Kotlin because you learned Smalltalk and know that both are object-oriented.

The linked page suggests one intro if you have experience with Datalog, another intro if you have experience with Answer Set Programming (ASP), and a third for everyone else. That's because Datalog and ASP are the two logic programming things that are most like finite-choice logic programming. Finite-choice logic programming gives a completely new way of understanding what answer set programs mean. The Dusa implementation is able to solve some problems vastly more efficiently than state-of-the-art ASP solvers, and is able to easily solve other problems that mainstream ASP solvers are simply unable to handle because of something called the "grounding bottleneck." Right now it's not a strict win by any means: there are many problems that Dusa chokes on that state-of-the-art ASP solvers can easily handle, but we know how to solve at least some of those problems for implementations of finite-choice logic programming.

Thank you!

Additional shout out to the Recurse Center (https://www.recurse.com/) which was instrumental in giving me the space and environment to start working on Dusa. I did a partially-remote, partially-in-person batch at Recurse in late 2023.

There is an implicit algorithm, and I'm so happy about this question. The inability to reason about likely performance of one's code is, to me, one of the things that bothers me most about Answer Set Programming, the programming paradigm that's probably the most like Finite-Choice Logic Programming.

The Dusa implementation has a couple of ways to reason at a high level about the performance of programs. The academic paper that febin linked to elsethread spends a fair amount of time talking about this, and if you really want to dig in, I recommend searching the paper for the phrases "deduce, then choose" and "cost semantics".

There's work to do in helping non-academics who just want to use Dusa reason about program performance, so I appreciate your comment as encouragement to prioritize that work when I have the chance.

The two answers by jonjojojo and khaledh are great, because they are both the correct answers.

From a principled point of view, the rule "a :- b, c" helps define what "a" means, and it seems, in practice, most helpful to be able to quickly visually identify the rules that define a certain relation. The list of premises tends to be of secondary importance (in addition to often being longer and more complicated).

From a practical point of view, we wrote Dusa as people familiar with existing Datalog and Answer Set Programming languages, which use the backwards ordering and ":-" notation, and some of the core target audience we hope to get interested in this project is people familiar with those languages, so we made some syntax choices to make things familiar to a specific target audience. (Same reason Java uses C-like syntax.)

...and if you're in the vanishingly small overlap of folks reading this comment and people interesting in attending an academic talk in Denver next Wednesday, the official conference page for the paper is https://popl25.sigplan.org/details/POPL-2025-popl-research-p...

(The ArXiV preprint has the exact same content)

Oh, hello hacker news!

Also potentially interesting to this crowd are the underlying editor, which I split out from the online Dusa editor and called "sketchzone" (https://github.com/robsimmons/sketchzone). Some of my motivations and hopes for sketchzone are blogged here: https://typesafety.net/rob/blog/endless-sketchzone

Also, I more-or-less did Advent of Code 2024 in Dusa: journal entries and links to solutions are at https://typesafety.net/rob/blog/advent-of-dusa-2024