[HN Gopher] Dusa Programming Language (Finite-Choice Logic Progr...
___________________________________________________________________
Dusa Programming Language (Finite-Choice Logic Programming)
Author : febin
Score : 164 points
Date : 2025-01-18 15:45 UTC (1 days ago)
(HTM) web link (dusa.rocks)
(TXT) w3m dump (dusa.rocks)
| febin wrote:
| Research Paper https://arxiv.org/pdf/2405.19040
| robsimmons wrote:
| ...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)
| sitkack wrote:
| Oh, I'll be on the live streams!
|
| https://popl25.sigplan.org/attending/live-streams
|
| I want to say that the cultural changes inside of the ACM to
| make historical research open access and to have excellent
| live streams of the conferences is just so damn wholesome and
| wonderful. Thank you ACM and the people inside the ACM that
| made this happen.
|
| And in case someone from the ACM is reading this, the live
| streams are very useful for physical attendees. I was
| attending Splash! and there were a ton of talks where I would
| have needed to change rooms, wanted lots of desk space for
| notes and research. It was somewhat ironic attending half a
| day from a vacation rental. :)
| robsimmons wrote:
| 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
| robsimmons wrote:
| 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.
| ukd1 wrote:
| Yay RC. I was in a remote batch. Was great.
|
| Zig was also apparently partly developed whilst Andrew Kelley
| was there. Fun place.
| convolvatron wrote:
| not only do I think that choice is a really important tool for
| writing pragmatic logic programs, this is a key piece to a really
| interesting goal - unifying logical and procedural programming
| (see verse)
| vosper wrote:
| > Note that this if-then statement is written backwards from how
| it's written in English: the "then" part, the conclusion is
| written first, followed by the :- symbol. After the :- symbol
| come the premises
|
| Why not write it like it's written in English? It could be one
| less thing to learn for people trying to adopt the language.
|
| https://dusa.rocks/docs/introductions/graph/
| jonjojojon wrote:
| The :- is supposed to sort of look like a left facing arrow for
| an implication. I think this notation started with prolog, so
| that is my guess why they chose to make it like this.
| khaledh wrote:
| I think the reason is that the right hand side can be a long
| and complex set of premises. It is supposed to be read as: The
| lhs is true iff everything on the rhs is true.
|
| You can also think the same way about functions in typical
| languages: we don't write the body of the function first and
| then assign it to an identifier.
| Jtsummers wrote:
| Yes, but not `iff`. f(X) :- g(X), h(X).
| f(a).
|
| With those two statements, `f(a)` is true, but it does not
| mean that `g(a)` and `h(a)` are also true. Instead, it means
| that we happen to know some fact, `f(a)`, and some rule for
| cases beyond that fact. If it also happened that `g(a)` and
| `h(a)` are true then we'd have two ways of arriving at the
| fact of `f(a)` being true.
|
| It's a reverse of the implication arrow and is meant to be
| read that way: f(X) :- g(X), h(X).
|
| Is read as "f(X) if g(X) and h(X)", versus "if g(X) and h(X)
| then f(X)".
| khaledh wrote:
| Thanks for the correction :)
| robsimmons wrote:
| 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.)
| skybrian wrote:
| It's not really written backwards; it's just equivalent to a
| different if statement. Something like this:
|
| if (want: edge Y X) { search for: edge X Y }
|
| This is searching in reverse compared to a different if
| statement:
|
| if (have: edge X Y) { assert: edge Y X }
| treetalker wrote:
| I suppose you could read it (i.e., ":-") as "provided that
| ...", in which case it does follow standard English word order.
| robsimmons wrote:
| Good point! "Whenever" is probably even closer to the correct
| meaning.
| treetalker wrote:
| Agreed, "whenever" expresses a necessary implication, while
| "provided" expresses necessary but not necessarily
| sufficient prerequisites.
| gpm wrote:
| Is there an implicit algorithm for how this language is
| evaluated? It seems hard to use without having an understanding
| of the likely performance of your code.
| robsimmons wrote:
| 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.
| cryptonector wrote:
| Is it different from SQL though?
| cybice wrote:
| Any real life tasks examples?
| trenchgun wrote:
| What do you consider a real life task, if Graph reachability,
| Graph coloring nor finding Connected components count? They all
| have many straightforward applications.
| Zezima wrote:
| So happy to see Dusa on HN. Was a joy to see you work on it while
| in batch at RC. Congrats!
| robsimmons wrote:
| Thank you!
| summarity wrote:
| As someone whose day job involves a lot of graph analysis and
| logic programming[0], I'm always excited to see new applied
| research in this area. More energy is needed here.
|
| Logic systems will be a key part of solving problems of hybrid
| data analysis (e.g. involving both social graphs, embedding
| spaces, and traditional relational data) - Cozo[1] sticks out as
| a great example.
|
| [0] https://codeql.github.com/docs/ql-language-
| reference/about-t...
|
| [1] https://www.cozodb.org/
| Syzygies wrote:
| My mind is blown, a new language where I can see new reach. Back
| in the day, APL was good at multidimensional arrays, and from
| there could outstrip Fortran shops at anything. A surprising
| swath of discrete reality can be viewed as a graph, or graphs of
| graphs. For me, computational group theory, combinatorial
| enumeration, canonical forms... All topics Claude 3.5 Sonnet
| happens to be exceptional at.
|
| Even a month ago, I'd have asked "Where's the parallelism?"
| looking at any new language. AI has upended my world. My
| subscriptions are getting out of hand, they're starting to look
| like some peoples' sports channel cable bills. I'll be
| experimenting with the right specification prompt to get AI to
| write correct programs in three languages side by side, in either
| Cursor or Windsurf. Then ask it to write a better prompt, and go
| test that in the other editor. I'm not sleeping much, it's like
| buying my first Mac.
|
| One constant debate I have with Claude is how much the choice of
| language affects AI reasoning ability. There's training corpus,
| but AI is even more appreciative of high level reasoning
| constructs than we are. AI doesn't need our idioms; when it
| taught itself the game Go it came up with its own.
|
| So human documentation is nice, but who programs that way
| anymore? Where's the specification prompt that suffices for
| Claude to code whatever we want in Dusa?
| temporallobe wrote:
| Have to admit as a "regular" developer using general purpose
| languages such as Java, C, Ruby, Perl, etc., most of this goes
| over my head, but at the same time I find the mix of Prolog and
| VB syntax fascinating and confusing.
| wslh wrote:
| Genuinely asking: what are the advantages of this approach with
| other approaches like Prolog? How is the interplay between
| current state-of-the-art, and finite-choice logic programming
| over what was previously known about logic programming?
| spencerflem wrote:
| The linked paper tries to justify this
| robsimmons wrote:
| 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.
| Epa095 wrote:
| So it is not Turing complete? It's more a programming
| language in the 'answer set programing' sense than 'general
| purpose programming language' sense?
| maweki wrote:
| There are many useful things that are not turing complete
| and still considered programming.
|
| Regular Excel formulas are always terminating and therefore
| not computationally complete.
|
| SQL without recursive CTEs is always terminating and
| therefore not computationally complete.
|
| Simply typed lambda calculus is always terminating and
| therefore not computationally complete.
|
| It's not the same, but restriction to terminating subsets
| gives very nice guarantees for a lot of program properties
| that would otherwise be undecidable.
| Epa095 wrote:
| I don't have any problems with calling it programming
| even if it's not Turing complete. But I think it's nice
| to clarify, so I can understand where it is in the
| expressivity-landscape.
|
| Maybe it's obvious for the intended audience, given the
| mention of Datalog? But I suspect a lot of compsci people
| know of Prolog, and know about SAT(and similar) solvers,
| but don't really know how e.g Datalog places.
| robsimmons wrote:
| 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.
| Epa095 wrote:
| Cool, I did not know!
| Koshkin wrote:
| Dusa McDuff rocks!
| adastra22 wrote:
| > If you've X (as implemented in Y), you may want to start by
| reading about Z
|
| No, what I want is a code example, front and center.
| notarobot123 wrote:
| Go to the home page: https://dusa.rocks
| treetalker wrote:
| From https://dusa.rocks/docs/introductions/asp/ :
|
| > Answer set programming is a way of writing Datalog-like
| programs to compute acceptable models (answer sets) that meet
| certain constraints. Whereas traditional datalog aims to compute
| just one solution, answer set programming introduces choices that
| let multiple possible solutions diverge.
|
| Fascinating! I could see useful applications in litigation (e.g.,
| narrowing potential claims; developing the theory of the case;
| finding impeaching lines of questioning).
___________________________________________________________________
(page generated 2025-01-19 23:02 UTC)