Dusa @ POPL 2025

The POPL 2025 talk on finite-choice logic programming and Dusa links to this page. Here are some of the examples in the talk and how to run them.

Stop or continue

The “stop or continue” program shown in the talk can almost be cut-and-pasted into Dusa: the only changes are that free variables need to be uppercased, and that Dusa does not have an infix addition.

The simplest path is just to replace N+1 with s N, and use Dusa’s Prolog-style structured terms instead of built-in numbers:

run 0 is { "🛑", "🏃" }.
run (s N) is { "🛑", "🏃" } :- run N is "🏃".

You can explore this example on dusa.rocks, but beware: you really want to hit “pause” relatively quickly before you start generating very large examples.

Your other option is to use Dusa’s built-in addition.

#builtin INT_PLUS plus
run 0 is { "🛑", "🏃" }.
run (plus N 1) is { "🛑", "🏃" } :- run N is "🏃".

You can explore this example on dusa.rocks as well: it is a little less eager to crash your browser.

Command-line execution

If you have npx command line utility installed, you can run either of these examples by putting them in a file called run.dusa and, on the command line, running

npx dusa run.dusa -n10

The -n10 argument tells the dusa command-line utility to generate ten solutions.

Map generation

The central generation program example from the talk is this one:

reach "🏠".
reach R2 :-
  reach R1,
  next_to R1 R2,
  terrain R2 is "🌳".
terrain R is {"⛰️", "🌳", "🌊"} :-
  region R.
terrain R2 is {"🌳", "🌊"} :-
  terrain R1 is "🌊",
  next_to R1 R2.

This code doesn’t actually do much unless we populate the region and next_to relations. We could do that by adding a bunch of facts, but it’s nicer to write a program to generate all the regions. These rules create 26 regions, home and every space on a 5x5 grid:

dim 1. dim 2. dim 3. dim 4. dim 5.
region "🏠".
region (coord X Y) :- dim X, dim Y.

To populate the next-to relation, we place home adjacent to the upper-left corner of the map, use an auxillary delta relation along with the built-in addition operation to place every other region adjacent to the region to its right and to the region below it. Finally, we force the relation to be transitive.

#builtin INT_PLUS plus
delta 0 1.
delta 1 0.
next_to "🏠" (coord 1 1).
next_to (coord X Y) (coord (plus X DX) (plus Y DY)) :-
  delta DX DY,
  dim X,
  dim Y,
  dim (plus X DX),
  dim (plus Y DY).
next_to X Y :- next_to Y X.

The result is the example shown in the in-browser animation during the talk. Explore this example on dusa.rocks.

Additional constraints

We can add additional constraints, for example requiring that the lower-right region be reachable. This uses a new kind of rule, a #demand constraint, that is described in the paper’s appendix and documented here.

#demand reach (coord 5 5).

Another aesthetic preference might be to ensure that there’s exactly one contiguous ocean in every example. This is easily handled by a variant of the canonical-representative-selection algorithm from Section 3.2 in the paper.

representative X is? X :-
  terrain X is "🌊".
representative Y is Z :-
  next_to X Y,
  representative X is Z,
  terrain Y is "🌊".

#demand representative _ is _.
#forbid representative _ is X, representative _ is Y, X != Y.

Explore this example on dusa.rocks.